GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/term_database_sygus.h Lines: 7 7 100.0 %
Date: 2021-03-23 Branches: 5 8 62.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_database_sygus.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, 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 term database sygus class
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
18
#define CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
19
20
#include <unordered_set>
21
22
#include "expr/dtype.h"
23
#include "theory/evaluator.h"
24
#include "theory/quantifiers/extended_rewrite.h"
25
#include "theory/quantifiers/fun_def_evaluator.h"
26
#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
27
#include "theory/quantifiers/sygus/sygus_explain.h"
28
#include "theory/quantifiers/sygus/type_info.h"
29
#include "theory/quantifiers/term_database.h"
30
31
namespace CVC4 {
32
namespace theory {
33
namespace quantifiers {
34
35
class SynthConjecture;
36
37
/** role for registering an enumerator */
38
enum EnumeratorRole
39
{
40
  /** The enumerator populates a pool of terms (e.g. for PBE). */
41
  ROLE_ENUM_POOL,
42
  /** The enumerator is the single solution of the problem. */
43
  ROLE_ENUM_SINGLE_SOLUTION,
44
  /**
45
   * The enumerator is part of the solution of the problem (e.g. multiple
46
   * functions to synthesize).
47
   */
48
  ROLE_ENUM_MULTI_SOLUTION,
49
  /** The enumerator must satisfy some set of constraints */
50
  ROLE_ENUM_CONSTRAINED,
51
};
52
std::ostream& operator<<(std::ostream& os, EnumeratorRole r);
53
54
// TODO :issue #1235 split and document this class
55
class TermDbSygus {
56
 public:
57
  TermDbSygus(QuantifiersState& qs);
58
2188
  ~TermDbSygus() {}
59
  /** Finish init, which sets the inference manager */
60
  void finishInit(QuantifiersInferenceManager* qim);
61
  /** Reset this utility */
62
  bool reset(Theory::Effort e);
63
  /** Identify this utility */
64
  std::string identify() const { return "TermDbSygus"; }
65
  /** register the sygus type
66
   *
67
   * This initializes this database for sygus datatype type tn. This may
68
   * throw an assertion failure if the sygus grammar has type errors. Otherwise,
69
   * after registering a sygus type, the query function getTypeInfo can be
70
   * called for tn.
71
   *
72
   * This method returns true if tn is a sygus datatype type and false
73
   * otherwise.
74
   */
75
  bool registerSygusType(TypeNode tn);
76
77
  //------------------------------utilities
78
  /** get the explanation utility */
79
42033
  SygusExplain* getExplain() { return d_syexp.get(); }
80
  /** get the extended rewrite utility */
81
395702
  ExtendedRewriter* getExtRewriter() { return d_ext_rw.get(); }
82
  /** get the evaluator */
83
14684
  Evaluator* getEvaluator() { return d_eval.get(); }
84
  /** (recursive) function evaluator utility */
85
39
  FunDefEvaluator* getFunDefEvaluator() { return d_funDefEval.get(); }
86
  /** evaluation unfolding utility */
87
305222
  SygusEvalUnfold* getEvalUnfold() { return d_eval_unfold.get(); }
88
  //------------------------------end utilities
89
90
  //------------------------------enumerators
91
  /**
92
   * Register a variable e that we will do enumerative search on.
93
   *
94
   * conj : the conjecture that the enumeration of e is for.
95
   *
96
   * f : the synth-fun that the enumeration of e is for.Notice that enumerator
97
   * e may not be one-to-one with f in synthesis-through-unification approaches
98
   * (e.g. decision tree construction for PBE synthesis).
99
   *
100
   * erole : the role of this enumerator (see definition of EnumeratorRole).
101
   * Depending on this and the policy for actively-generated enumerators
102
   * (--sygus-active-gen), the enumerator may be "actively-generated".
103
   * For example, if --sygus-active-gen=var-agnostic, then the enumerator will
104
   * only generate values whose variables are in canonical order (only x1-x2
105
   * and not x2-x1 will be generated, assuming x1 and x2 are in the same
106
   * "subclass", see getSubclassForVar).
107
   *
108
   * An "active guard" may be allocated by this method for e based on erole
109
   * and the policies for active generation.
110
   */
111
  void registerEnumerator(Node e,
112
                          Node f,
113
                          SynthConjecture* conj,
114
                          EnumeratorRole erole);
115
  /** is e an enumerator registered with this class? */
116
  bool isEnumerator(Node e) const;
117
  /** return the conjecture e is associated with */
118
  SynthConjecture* getConjectureForEnumerator(Node e) const;
119
  /** return the function-to-synthesize e is associated with */
120
  Node getSynthFunForEnumerator(Node e) const;
121
  /** get active guard for e */
122
  Node getActiveGuardForEnumerator(Node e) const;
123
  /** are we using symbolic constructors for enumerator e? */
124
  bool usingSymbolicConsForEnumerator(Node e) const;
125
  /** is this enumerator agnostic to variables? */
126
  bool isVariableAgnosticEnumerator(Node e) const;
127
  /** is this enumerator a "basic" enumerator.
128
   *
129
   * A basic enumerator is one that does not rely on the sygus extension of the
130
   * datatypes solver. Basic enumerators enumerate all concrete terms for their
131
   * type for a single abstract value.
132
   */
133
  bool isBasicEnumerator(Node e) const;
134
  /** is this a "passively-generated" enumerator?
135
   *
136
   * A "passively-generated" enumerator is one for which the terms it enumerates
137
   * are obtained by looking at its model value only. For passively-generated
138
   * enumerators, it is the responsibility of the user of that enumerator (say
139
   * a SygusModule) to block the current model value of it before asking for
140
   * another value. By default, the Cegis module uses passively-generated
141
   * enumerators and "conjecture-specific refinement" to rule out models
142
   * for passively-generated enumerators.
143
   *
144
   * On the other hand, an "actively-generated" enumerator is one for which the
145
   * terms it enumerates are not necessarily a subset of the model values the
146
   * enumerator takes. Actively-generated enumerators are centrally managed by
147
   * SynthConjecture. The user of actively-generated enumerators are prohibited
148
   * from influencing its model value. For example, conjecture-specific
149
   * refinement in Cegis is not applied to actively-generated enumerators.
150
   */
151
  bool isPassiveEnumerator(Node e) const;
152
  /** get all registered enumerators */
153
  void getEnumerators(std::vector<Node>& mts);
154
  /** Register symmetry breaking lemma
155
   *
156
   * This function registers lem as a symmetry breaking lemma template for
157
   * subterms of enumerator e. For more information on symmetry breaking
158
   * lemma templates, see datatypes/datatypes_sygus.h.
159
   *
160
   * tn : the (sygus datatype) type that lem applies to, i.e. the
161
   * type of terms that lem blocks models for,
162
   * sz : the minimum size of terms that the lem blocks,
163
   * isTempl : if this flag is false, then lem is a (concrete) lemma.
164
   * If this flag is true, then lem is a symmetry breaking lemma template
165
   * over x, where x is returned by the call to getFreeVar( tn, 0 ).
166
   */
167
  void registerSymBreakLemma(
168
      Node e, Node lem, TypeNode tn, unsigned sz, bool isTempl = true);
169
  /** Has symmetry breaking lemmas been added for any enumerator? */
170
  bool hasSymBreakLemmas(std::vector<Node>& enums) const;
171
  /** Get symmetry breaking lemmas
172
   *
173
   * Returns the set of symmetry breaking lemmas that have been registered
174
   * for enumerator e. It adds these to lemmas.
175
   */
176
  void getSymBreakLemmas(Node e, std::vector<Node>& lemmas) const;
177
  /** Get the type of term symmetry breaking lemma lem applies to */
178
  TypeNode getTypeForSymBreakLemma(Node lem) const;
179
  /** Get the minimum size of terms symmetry breaking lemma lem applies to */
180
  unsigned getSizeForSymBreakLemma(Node lem) const;
181
  /** Returns true if lem is a lemma template, false if lem is a lemma */
182
  bool isSymBreakLemmaTemplate(Node lem) const;
183
  /** Clear information about symmetry breaking lemmas for enumerator e */
184
  void clearSymBreakLemmas(Node e);
185
  //------------------------------end enumerators
186
187
  //-----------------------------conversion from sygus to builtin
188
  /** get free variable
189
   *
190
   * This class caches a list of free variables for each type, which are
191
   * used, for instance, for constructing canonical forms of terms with free
192
   * variables. This function returns the i^th free variable for type tn.
193
   * If useSygusType is true, then this function returns a variable of the
194
   * analog type for sygus type tn (see d_fv for details).
195
   */
196
  TNode getFreeVar(TypeNode tn, int i, bool useSygusType = false);
197
  /** get free variable and increment
198
   *
199
   * This function returns the next free variable for type tn, and increments
200
   * the counter in var_count for that type.
201
   */
202
  TNode getFreeVarInc(TypeNode tn,
203
                      std::map<TypeNode, int>& var_count,
204
                      bool useSygusType = false);
205
  /** returns true if n is a cached free variable (in d_fv). */
206
  bool isFreeVar(Node n) const;
207
  /** returns the identifier for a cached free variable. */
208
  size_t getFreeVarId(Node n) const;
209
  /** returns true if n has a cached free variable (in d_fv). */
210
  bool hasFreeVar(Node n);
211
  /** get sygus proxy variable
212
   *
213
   * Returns a fresh variable of type tn with the SygusPrintProxyAttribute set
214
   * to constant c. The type tn should be a sygus datatype type, and the type of
215
   * c should be the analog type of tn. The semantics of the returned node
216
   * is "the variable of sygus datatype tn that encodes constant c".
217
   */
218
  Node getProxyVariable(TypeNode tn, Node c);
219
  /** make generic
220
   *
221
   * This function returns a builtin term f( t1, ..., tn ) where f is the
222
   * builtin op of the sygus datatype constructor specified by arguments
223
   * dt and c. The mapping pre maps child indices to the term for that index
224
   * in the term we are constructing. That is, for each i = 1,...,n:
225
   *   If i is in the domain of pre, then ti = pre[i].
226
   *   If i is not in the domain of pre, then ti = d_fv[1][ var_count[Ti ] ],
227
   *     and var_count[Ti] is incremented.
228
   * If doBetaRed is true, then lambda operators are eagerly eliminated via
229
   * beta reduction.
230
   */
231
  Node mkGeneric(const DType& dt,
232
                 unsigned c,
233
                 std::map<TypeNode, int>& var_count,
234
                 std::map<int, Node>& pre,
235
                 bool doBetaRed = true);
236
  /** same as above, but with empty var_count */
237
  Node mkGeneric(const DType& dt,
238
                 int c,
239
                 std::map<int, Node>& pre,
240
                 bool doBetaRed = true);
241
  /** same as above, but with empty pre */
242
  Node mkGeneric(const DType& dt, int c, bool doBetaRed = true);
243
  /** makes a symbolic term concrete
244
   *
245
   * Given a sygus datatype term n of type tn with holes (symbolic constructor
246
   * applications), this function returns a term in which holes are replaced by
247
   * unique variables. To track counters for introducing unique variables, we
248
   * use the var_count map.
249
   */
250
  Node canonizeBuiltin(Node n);
251
  Node canonizeBuiltin(Node n, std::map<TypeNode, int>& var_count);
252
  /** sygus to builtin
253
   *
254
   * Given a sygus datatype term n of type tn, this function returns its analog,
255
   * that is, the term that n encodes.
256
   */
257
  Node sygusToBuiltin(Node n, TypeNode tn);
258
  /** same as above, but without tn */
259
197560
  Node sygusToBuiltin(Node n) { return sygusToBuiltin(n, n.getType()); }
260
  /** evaluate builtin
261
   *
262
   * bn is a term of some sygus datatype tn. This function returns the rewritten
263
   * form of bn [ args / vars(tn) ], where vars(tn) is the sygus variable
264
   * list for type tn (see Datatype::getSygusVarList).
265
   *
266
   * If the argument tryEval is true, we consult the evaluator before the
267
   * rewriter, for performance reasons.
268
   */
269
  Node evaluateBuiltin(TypeNode tn,
270
                       Node bn,
271
                       const std::vector<Node>& args,
272
                       bool tryEval = true);
273
  /** evaluate with unfolding
274
   *
275
   * n is any term that may involve sygus evaluation functions. This function
276
   * returns the result of unfolding the evaluation functions within n and
277
   * rewriting the result. For example, if eval_A is the evaluation function
278
   * for the datatype:
279
   *   A -> C_0 | C_1 | C_x | C_+( C_A, C_A )
280
   * corresponding to grammar:
281
   *   A -> 0 | 1 | x | A + A
282
   * then calling this function on eval( C_+( x, 1 ), 4 ) = y returns 5 = y.
283
   * The node returned by this function is in (extended) rewritten form.
284
   */
285
  Node evaluateWithUnfolding(Node n);
286
  /** same as above, but with a cache of visited nodes */
287
  Node evaluateWithUnfolding(
288
      Node n, std::unordered_map<Node, Node, NodeHashFunction>& visited);
289
  /** is evaluation point?
290
   *
291
   * Returns true if n is of the form eval( x, c1...cn ) for some variable x
292
   * and constants c1...cn.
293
   */
294
  bool isEvaluationPoint(Node n) const;
295
  /** return the builtin type of tn
296
   *
297
   * The type tn should be a sygus datatype type that has been registered to
298
   * this database.
299
   */
300
  TypeNode sygusToBuiltinType(TypeNode tn);
301
  //-----------------------------end conversion from sygus to builtin
302
  /**
303
   * Get type information about sygus datatype type tn. The type tn should be
304
   * (a subfield type of) a type that has been registered to this class.
305
   */
306
  SygusTypeInfo& getTypeInfo(TypeNode tn);
307
  /**
308
   * Rewrite the given node using the utilities in this class. This may
309
   * involve (recursive function) evaluation.
310
   */
311
  Node rewriteNode(Node n) const;
312
313
  /** print to sygus stream n on trace c */
314
  static void toStreamSygus(const char* c, Node n);
315
  /** print to sygus stream n on output out */
316
  static void toStreamSygus(std::ostream& out, Node n);
317
318
 private:
319
  /** Reference to the quantifiers state */
320
  QuantifiersState& d_qstate;
321
  /** Pointer to the quantifiers inference manager */
322
  QuantifiersInferenceManager* d_qim;
323
324
  //------------------------------utilities
325
  /** sygus explanation */
326
  std::unique_ptr<SygusExplain> d_syexp;
327
  /** extended rewriter */
328
  std::unique_ptr<ExtendedRewriter> d_ext_rw;
329
  /** evaluator */
330
  std::unique_ptr<Evaluator> d_eval;
331
  /** (recursive) function evaluator utility */
332
  std::unique_ptr<FunDefEvaluator> d_funDefEval;
333
  /** evaluation function unfolding utility */
334
  std::unique_ptr<SygusEvalUnfold> d_eval_unfold;
335
  //------------------------------end utilities
336
337
  //------------------------------enumerators
338
  /** mapping from enumerator terms to the conjecture they are associated with
339
   */
340
  std::map<Node, SynthConjecture*> d_enum_to_conjecture;
341
  /** mapping from enumerator terms to the function-to-synthesize they are
342
   * associated with
343
   */
344
  std::map<Node, Node> d_enum_to_synth_fun;
345
  /** mapping from enumerator terms to the guard they are associated with
346
   * The guard G for an enumerator e has the semantics
347
   *   if G is true, then there are more values of e to enumerate".
348
   */
349
  std::map<Node, Node> d_enum_to_active_guard;
350
  /**
351
   * Mapping from enumerators to whether we allow symbolic constructors to
352
   * appear as subterms of them.
353
   */
354
  std::map<Node, bool> d_enum_to_using_sym_cons;
355
  /** mapping from enumerators to symmetry breaking clauses for them */
356
  std::map<Node, std::vector<Node> > d_enum_to_sb_lemmas;
357
  /** mapping from symmetry breaking lemmas to type */
358
  std::map<Node, TypeNode> d_sb_lemma_to_type;
359
  /** mapping from symmetry breaking lemmas to size */
360
  std::map<Node, unsigned> d_sb_lemma_to_size;
361
  /** mapping from symmetry breaking lemmas to whether they are templates */
362
  std::map<Node, bool> d_sb_lemma_to_isTempl;
363
  /** enumerators to whether they are actively-generated */
364
  std::map<Node, bool> d_enum_active_gen;
365
  /** enumerators to whether they are variable agnostic */
366
  std::map<Node, bool> d_enum_var_agnostic;
367
  /** enumerators to whether they are basic */
368
  std::map<Node, bool> d_enum_basic;
369
  //------------------------------end enumerators
370
371
  //-----------------------------conversion from sygus to builtin
372
  /** a cache of fresh variables for each type
373
   *
374
   * We store two versions of this list:
375
   *   index 0: mapping from builtin types to fresh variables of that type,
376
   *   index 1: mapping from sygus types to fresh varaibles of the type they
377
   *            encode.
378
   */
379
  std::map<TypeNode, std::vector<Node> > d_fv[2];
380
  /** Maps free variables to the domain type they are associated with in d_fv */
381
  std::map<Node, TypeNode> d_fv_stype;
382
  /** Id count for free variables terms */
383
  std::map<TypeNode, size_t> d_fvTypeIdCounter;
384
  /**
385
   * Maps free variables to a unique identifier for their builtin type. Notice
386
   * that, e.g. free variables of type Int and those that are of a sygus
387
   * datatype type that encodes Int must have unique identifiers. This is
388
   * to ensure that sygusToBuiltin for non-ground terms maps variables to
389
   * unique variabales.
390
   */
391
  std::map<Node, size_t> d_fvId;
392
  /** recursive helper for hasFreeVar, visited stores nodes we have visited. */
393
  bool hasFreeVar(Node n, std::map<Node, bool>& visited);
394
  /** cache of getProxyVariable */
395
  std::map<TypeNode, std::map<Node, Node> > d_proxy_vars;
396
  //-----------------------------end conversion from sygus to builtin
397
  // TODO :issue #1235 : below here needs refactor
398
 public:
399
  Node d_true;
400
  Node d_false;
401
402
 private:
403
  /** computes the map d_min_type_depth */
404
  void computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth );
405
  bool involvesDivByZero( Node n, std::map< Node, bool >& visited );
406
407
 private:
408
  /**
409
   * Maps types that we have called registerSygusType to a flag indicating
410
   * whether that type is a sygus datatype type. Sygus datatype types that
411
   * are in this map have initialized type information stored in the map below.
412
   */
413
  std::map<TypeNode, bool> d_registerStatus;
414
  /**
415
   * The type information for each sygus datatype type that has been registered
416
   * to this class.
417
   */
418
  std::map<TypeNode, SygusTypeInfo> d_tinfo;
419
  /** a cache for getSelectorWeight */
420
  std::map<TypeNode, std::map<Node, unsigned> > d_sel_weight;
421
422
 public:  // general sygus utilities
423
  bool isRegistered(TypeNode tn) const;
424
  /** get the weight of the selector, where tn is the domain of sel */
425
  unsigned getSelectorWeight(TypeNode tn, Node sel);
426
  /** get arg type */
427
  TypeNode getArgType(const DTypeConstructor& c, unsigned i) const;
428
  /** Do constructors c1 and c2 have the same type? */
429
  bool isTypeMatch(const DTypeConstructor& c1, const DTypeConstructor& c2);
430
  /** return whether n is an application of a symbolic constructor */
431
  bool isSymbolicConsApp(Node n) const;
432
  /** can construct kind
433
   *
434
   * Given a sygus datatype type tn, if this method returns true, then there
435
   * exists values of tn whose builtin analog is equivalent to
436
   * <k>( t1, ..., tn ). The sygus types of t1...tn are added to arg_types.
437
   *
438
   * For example, if:
439
   *   A -> A+A | ite( B, A, A ) | x | 1 | 0
440
   *   B -> and( B, B ) | not( B ) | or( B, B ) | A = A
441
   * - canConstructKind( A, +, ... ) returns true and adds {A,A} to arg_types,
442
   * - canConstructKind( B, not, ... ) returns true and adds { B } to arg types.
443
   *
444
   * We also may infer that operator is constructable. For example,
445
   * - canConstructKind( B, ite, ... ) may return true, adding { B, B, B } to
446
   * arg_types, noting that the term
447
   *   (and (or (not b1) b2) (or b1 b3)) is equivalent to (ite b1 b2 b3)
448
   * The argument aggr is whether we use aggressive techniques like the one
449
   * above to infer a kind is constructable. If this flag is false, we only
450
   * check if the kind is literally a constructor of the grammar.
451
   */
452
  bool canConstructKind(TypeNode tn,
453
                        Kind k,
454
                        std::vector<TypeNode>& argts,
455
                        bool aggr = false);
456
457
  Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
458
  Node getNormalized(TypeNode t, Node prog);
459
  unsigned getSygusTermSize( Node n );
460
  /** involves div-by-zero */
461
  bool involvesDivByZero( Node n );
462
  /** get anchor */
463
  static Node getAnchor( Node n );
464
  static unsigned getAnchorDepth( Node n );
465
466
};
467
468
}/* CVC4::theory::quantifiers namespace */
469
}/* CVC4::theory namespace */
470
}/* CVC4 namespace */
471
472
#endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */