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