GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_unif_strat.h Lines: 18 18 100.0 %
Date: 2021-03-23 Branches: 3 6 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_unif_strat.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief sygus_unif_strat
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
18
#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
19
20
#include <map>
21
#include "expr/node.h"
22
23
namespace CVC4 {
24
namespace theory {
25
26
class QuantifiersEngine;
27
28
namespace quantifiers {
29
30
/** roles for enumerators
31
 *
32
 * This indicates the role of an enumerator that is allocated by approaches
33
 * for synthesis-by-unification (see details below).
34
 *   io : the enumerator should enumerate values that are overall solutions
35
 *        for the function-to-synthesize,
36
 *   ite_condition : the enumerator should enumerate values that are useful
37
 *                   in ite conditions in the ITE strategy,
38
 *   concat_term : the enumerator should enumerate values that are used as
39
 *                 components of string concatenation solutions.
40
 */
41
enum EnumRole
42
{
43
  enum_invalid,
44
  enum_io,
45
  enum_ite_condition,
46
  enum_concat_term,
47
};
48
std::ostream& operator<<(std::ostream& os, EnumRole r);
49
50
/** roles for strategy nodes
51
 *
52
 * This indicates the role of a strategy node, which is a subprocedure of
53
 * SygusUnif::constructSolution (see details below).
54
 *   equal : the node constructed must be equal to the overall solution for
55
 *           the function-to-synthesize,
56
 *   string_prefix/suffix : the node constructed must be a prefix/suffix
57
 *                          of the function-to-synthesize,
58
 *   ite_condition : the node constructed must be a condition that makes some
59
 *                   active input examples true and some input examples false.
60
 */
61
enum NodeRole
62
{
63
  role_invalid,
64
  role_equal,
65
  role_string_prefix,
66
  role_string_suffix,
67
  role_ite_condition,
68
};
69
std::ostream& operator<<(std::ostream& os, NodeRole r);
70
71
/** enumerator role for node role */
72
EnumRole getEnumeratorRoleForNodeRole(NodeRole r);
73
74
/** strategy types
75
 *
76
 * This indicates a strategy for synthesis-by-unification (see details below).
77
 *   ITE : strategy for constructing if-then-else solutions via decision
78
 *         tree learning techniques,
79
 *   CONCAT_PREFIX/SUFFIX : strategy for constructing string concatenation
80
 *         solutions via a divide and conquer approach,
81
 *   ID : identity strategy used for calling strategies on child type through
82
 *        an identity function.
83
 */
84
enum StrategyType
85
{
86
  strat_INVALID,
87
  strat_ITE,
88
  strat_CONCAT_PREFIX,
89
  strat_CONCAT_SUFFIX,
90
  strat_ID,
91
};
92
std::ostream& operator<<(std::ostream& os, StrategyType st);
93
94
/** virtual base class for context in synthesis-by-unification approaches */
95
84
class UnifContext
96
{
97
 public:
98
84
  virtual ~UnifContext() {}
99
100
  /** Get the current role
101
   *
102
   * In a particular context when constructing solutions in synthesis by
103
   * unification, we may be solving based on a modified role. For example,
104
   * if we are currently synthesizing x in a solution ("a" ++ x), we are
105
   * synthesizing the string suffix of the overall solution. In this case, this
106
   * function returns role_string_suffix.
107
   */
108
  virtual NodeRole getCurrentRole() = 0;
109
  /** is return value modified?
110
   *
111
   * This returns true if we are currently in a state where the return value
112
   * of the solution has been modified, e.g. by a previous node that solved
113
   * for a string prefix.
114
   */
115
6654
  bool isReturnValueModified() { return getCurrentRole() != role_equal; }
116
};
117
118
/**
119
* This class stores information regarding an enumerator, including
120
* information regarding the role of this enumerator (see EnumRole), its
121
* parent, whether it is templated, its slave enumerators, and so on.
122
*
123
* We say an enumerator is a master enumerator if it is the variable that
124
* we use to enumerate values for its sort. Master enumerators may have
125
* (possibly multiple) slave enumerators, stored in d_enum_slave. When
126
* constructing a sygus unifciation strategy, we make the first enumerator for
127
* each type a master enumerator, and any additional ones slaves of it.
128
*/
129
257
class EnumInfo
130
{
131
 public:
132
257
  EnumInfo() : d_role(enum_io), d_is_conditional(false) {}
133
  /** initialize this class
134
  *
135
  * role is the "role" the enumerator plays in the high-level strategy,
136
  *   which is one of enum_* above.
137
  */
138
  void initialize(EnumRole role);
139
  /** is this enumerator associated with a template? */
140
4611
  bool isTemplated() { return !d_template.isNull(); }
141
  /** set conditional
142
    *
143
    * This flag is set to true if this enumerator may not apply to all
144
    * input/output examples. For example, if this enumerator is used
145
    * as an output value beneath a conditional in an instance of strat_ITE,
146
    * then this enumerator is conditional.
147
    */
148
121
  void setConditional() { d_is_conditional = true; }
149
  /** returns if this enumerator is conditional */
150
401
  bool isConditional() { return d_is_conditional; }
151
  /** get the role of this enumerator */
152
28818
  EnumRole getRole() { return d_role; }
153
  /** enumerator template
154
  *
155
  * If d_template non-null, enumerated values V are immediately transformed to
156
  * d_template { d_template_arg -> V }.
157
  */
158
  Node d_template;
159
  Node d_template_arg;
160
  /**
161
  * Slave enumerators of this enumerator. These are other enumerators that
162
  * have the same type, but a different role in the strategy tree. We
163
  * generally
164
  * only use one enumerator per type, and hence these slaves are notified when
165
  * values are enumerated for this enumerator.
166
  */
167
  std::vector<Node> d_enum_slave;
168
169
 private:
170
  /** the role of this enumerator (one of enum_* above). */
171
  EnumRole d_role;
172
  /** is this enumerator conditional */
173
  bool d_is_conditional;
174
};
175
176
class EnumTypeInfoStrat;
177
178
/** represents a node in the strategy graph
179
 *
180
 * It contains a list of possible strategies which are tried during calls
181
 * to constructSolution.
182
 */
183
class StrategyNode
184
{
185
 public:
186
244
  StrategyNode() {}
187
  ~StrategyNode();
188
  /** the set of strategies to try at this node in the strategy graph */
189
  std::vector<EnumTypeInfoStrat*> d_strats;
190
};
191
192
/**
193
 * Stores all enumerators and strategies for a SyGuS datatype type.
194
 */
195
153
class EnumTypeInfo
196
{
197
 public:
198
153
  EnumTypeInfo() {}
199
  /** the type that this information is for */
200
  TypeNode d_this_type;
201
  /** map from enum roles to enumerators for this type */
202
  std::map<EnumRole, Node> d_enum;
203
  /** map from node roles to strategy nodes */
204
  std::map<NodeRole, StrategyNode> d_snodes;
205
  /** get strategy node for node role */
206
  StrategyNode& getStrategyNode(NodeRole nrole);
207
};
208
209
/** represents a strategy for a SyGuS datatype type
210
  *
211
  * This represents a possible strategy to apply when processing a strategy
212
  * node in constructSolution. When applying the strategy represented by this
213
  * class, we may make recursive calls to the children of the strategy,
214
  * given in d_cenum. If all recursive calls to constructSolution for these
215
  * children are successful, say:
216
  *   constructSolution( d_cenum[1], ... ) = t1,
217
  *    ...,
218
  *   constructSolution( d_cenum[n], ... ) = tn,
219
  * Then, the solution returned by this strategy is
220
  *   d_sol_templ * { d_sol_templ_args -> (t1,...,tn) }
221
  * where * is application of substitution.
222
  */
223
338
class EnumTypeInfoStrat
224
{
225
 public:
226
  /** the type of strategy this represents */
227
  StrategyType d_this;
228
  /** the sygus datatype constructor that induced this strategy
229
    *
230
    * For example, this may be a sygus datatype whose sygus operator is ITE,
231
    * if the strategy type above is strat_ITE.
232
    */
233
  Node d_cons;
234
  /** children of this strategy */
235
  std::vector<std::pair<Node, NodeRole> > d_cenum;
236
  /** the arguments for the (templated) solution */
237
  std::vector<Node> d_sol_templ_args;
238
  /** the template for the solution */
239
  Node d_sol_templ;
240
  /** Returns true if argument is valid strategy in unification context x */
241
  bool isValid(UnifContext& x);
242
};
243
244
/**
245
 * flags for extra restrictions to be inferred during redundant operators
246
 * learning
247
 */
248
107
struct StrategyRestrictions
249
{
250
107
  StrategyRestrictions() : d_iteReturnBoolConst(false), d_iteCondOnlyAtoms(true)
251
  {
252
107
  }
253
  /**
254
   * if this flag is true then staticLearnRedundantOps will also try to make
255
   * the return value of boolean ITEs to be restricted to constants
256
   */
257
  bool d_iteReturnBoolConst;
258
  /**
259
   * if this flag is true then staticLearnRedundantOps will also try to make
260
   * the condition values of ITEs to be restricted to atoms
261
   */
262
  bool d_iteCondOnlyAtoms;
263
  /**
264
   * A list of unused strategies. This maps strategy points to the indices
265
   * in StrategyNode::d_strats that are not used by the caller of
266
   * staticLearnRedundantOps, and hence should not be taken into account
267
   * when doing redundant operator learning.
268
   */
269
  std::map<Node, std::unordered_set<unsigned>> d_unused_strategies;
270
};
271
272
/**
273
 * Stores strategy and enumeration information for a function-to-synthesize.
274
 *
275
 * When this class is initialized, we construct a "strategy tree" based on
276
 * the grammar of the function to synthesize f. This tree is represented by
277
 * the above classes.
278
 */
279
107
class SygusUnifStrategy
280
{
281
 public:
282
107
  SygusUnifStrategy() : d_qe(nullptr) {}
283
  /** initialize
284
   *
285
   * This initializes this class with function-to-synthesize f. We also call
286
   * f the candidate variable.
287
   *
288
   * This call constructs a set of enumerators for the relevant subfields of
289
   * the grammar of f and adds them to enums.
290
   */
291
  void initialize(QuantifiersEngine* qe, Node f, std::vector<Node>& enums);
292
  /** Get the root enumerator for this class */
293
  Node getRootEnumerator() const;
294
  /**
295
   * Get the enumerator info for enumerator e, where e must be an enumerator
296
   * initialized by this class (in enums after a call to initialize).
297
   */
298
  EnumInfo& getEnumInfo(Node e);
299
  /**
300
   * Get the enumerator type info for sygus type t, where t must be the type
301
   * of some enumerator initialized by this class
302
   */
303
  EnumTypeInfo& getEnumTypeInfo(TypeNode tn);
304
305
  /** static learn redundant operators
306
   *
307
   * This learns static lemmas for pruning enumerative space based on the
308
   * strategy for the function-to-synthesize of this class, and stores these
309
   * into strategy_lemmas.
310
   *
311
   * These may correspond to static symmetry breaking predicates (for example,
312
   * those that exclude ITE from enumerators whose role is enum_io when the
313
   * strategy is ITE_strat).
314
   *
315
   * then the module may also try to apply the given pruning restrictions (see
316
   * StrategyRestrictions for more details)
317
   */
318
  void staticLearnRedundantOps(
319
      std::map<Node, std::vector<Node>>& strategy_lemmas,
320
      StrategyRestrictions& restrictions);
321
  /**
322
   * creates the default restrictions when they are not given and calls the
323
   * above function
324
   */
325
  void staticLearnRedundantOps(
326
      std::map<Node, std::vector<Node>>& strategy_lemmas);
327
328
  /** debug print this strategy on Trace c */
329
  void debugPrint(const char* c);
330
331
 private:
332
  /** reference to quantifier engine */
333
  QuantifiersEngine* d_qe;
334
  /** The candidate variable this strategy is for */
335
  Node d_candidate;
336
  /** maps enumerators to relevant information */
337
  std::map<Node, EnumInfo> d_einfo;
338
  /** list of all enumerators for the function-to-synthesize */
339
  std::vector<Node> d_esym_list;
340
  /** Info for sygus datatype type occurring in a field of d_root */
341
  std::map<TypeNode, EnumTypeInfo> d_tinfo;
342
  /**
343
    * The root sygus datatype for the function-to-synthesize,
344
    * which encodes the overall syntactic restrictions on the space
345
    * of solutions.
346
    */
347
  TypeNode d_root;
348
  /**
349
    * Maps sygus datatypes to their master enumerator. This is the (single)
350
    * enumerator of that type that we enumerate values for.
351
    */
352
  std::map<TypeNode, Node> d_master_enum;
353
  /** Initialize necessary information for (sygus) type tn */
354
  void initializeType(TypeNode tn);
355
356
  //-----------------------debug printing
357
  /** print ind indentations on trace c */
358
  static void indent(const char* c, int ind);
359
  //-----------------------end debug printing
360
361
  //------------------------------ strategy registration
362
  /** build strategy graph
363
   *
364
   * This builds the strategy for enumerated values of type tn for the given
365
   * role of nrole, for solutions to function-to-synthesize of this class.
366
   */
367
  void buildStrategyGraph(TypeNode tn, NodeRole nrole);
368
  /** register enumerator
369
   *
370
   * This registers that et is an enumerator of type tn, having enumerator
371
   * role enum_role.
372
   *
373
   * inSearch is whether we will enumerate values based on this enumerator.
374
   * A strategy node is represented by a (enumerator, node role) pair. Hence,
375
   * we may use enumerators for which this flag is false to represent strategy
376
   * nodes that have child strategies.
377
   */
378
  void registerStrategyPoint(Node et,
379
                          TypeNode tn,
380
                          EnumRole enum_role,
381
                          bool inSearch);
382
  /** infer template */
383
  bool inferTemplate(unsigned k,
384
                     Node n,
385
                     std::map<Node, unsigned>& templ_var_index,
386
                     std::map<unsigned, unsigned>& templ_injection);
387
  /** helper for static learn redundant operators
388
   *
389
   * (e, nrole) specify the strategy node in the graph we are currently
390
   * analyzing, visited stores the nodes we have already visited.
391
   *
392
   * This method builds the mapping needs_cons, which maps (master) enumerators
393
   * to a map from the constructors that it needs.
394
   */
395
  void staticLearnRedundantOps(
396
      Node e,
397
      NodeRole nrole,
398
      std::map<Node, std::map<NodeRole, bool>>& visited,
399
      std::map<Node, std::map<unsigned, bool>>& needs_cons,
400
      StrategyRestrictions& restrictions);
401
  /** finish initialization of the strategy tree
402
   *
403
   * (e, nrole) specify the strategy node in the graph we are currently
404
   * analyzing, visited stores the nodes we have already visited.
405
   *
406
   * isCond is whether the current enumerator is conditional (beneath a
407
   * conditional of an strat_ITE strategy).
408
   */
409
  void finishInit(Node e,
410
                  NodeRole nrole,
411
                  std::map<Node, std::map<NodeRole, bool> >& visited,
412
                  bool isCond);
413
  /** helper for debug print
414
   *
415
   * Prints the node e with role nrole on Trace(c).
416
   *
417
   * (e, nrole) specify the strategy node in the graph we are currently
418
   * analyzing, visited stores the nodes we have already visited.
419
   *
420
   * ind is the current level of indentation (for debugging)
421
   */
422
  void debugPrint(const char* c,
423
                  Node e,
424
                  NodeRole nrole,
425
                  std::map<Node, std::map<NodeRole, bool> >& visited,
426
                  int ind);
427
  //------------------------------ end strategy registration
428
};
429
430
} /* CVC4::theory::quantifiers namespace */
431
} /* CVC4::theory namespace */
432
} /* CVC4 namespace */
433
434
#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */