1 

/********************* */ 
2 

/*! \file sygus_extension.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Andrew Reynolds, Mathias Preiner, Dejan Jovanovic 
6 

** This file is part of the CVC4 project. 
7 

** Copyright (c) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel source 
10 

** directory for licensing information.\endverbatim 
11 

** 
12 

** \brief The sygus extension of the theory of datatypes. 
13 

**/ 
14 


15 

#include "cvc4_private.h" 
16 


17 

#ifndef CVC4__THEORY__DATATYPES__SYGUS_EXTENSION_H 
18 

#define CVC4__THEORY__DATATYPES__SYGUS_EXTENSION_H 
19 


20 

#include <iostream> 
21 

#include <map> 
22 


23 

#include "context/cdhashmap.h" 
24 

#include "context/cdhashset.h" 
25 

#include "context/context.h" 
26 

#include "expr/node.h" 
27 

#include "theory/datatypes/sygus_simple_sym.h" 
28 

#include "theory/decision_manager.h" 
29 

#include "theory/quantifiers/sygus_sampler.h" 
30 

#include "theory/quantifiers/term_database.h" 
31 


32 

namespace CVC4 { 
33 

namespace theory { 
34 

namespace quantifiers { 
35 

class SynthConjecture; 
36 

} 
37 

namespace datatypes { 
38 


39 

class InferenceManager; 
40 


41 

/** 
42 

* This is the sygus extension of the decision procedure for quantifierfree 
43 

* inductive datatypes. At a high level, this class takes as input a 
44 

* set of asserted testers isC1( x ), isC2( x.1 ), isC3( x.2 ), and 
45 

* generates lemmas that restrict the models of x, if x is a "sygus enumerator" 
46 

* (see TermDbSygus::registerEnumerator). 
47 

* 
48 

* Some of these techniques are described in these papers: 
49 

* "RefutationBased Synthesis in SMT", Reynolds et al 2017. 
50 

* "Sygus Techniques in the Core of an SMT Solver", Reynolds et al 2017. 
51 

* 
52 

* This class enforces two decisions stragies via calls to registerStrategy 
53 

* of the owning theory's DecisionManager: 
54 

* (1) Positive decisions on the active guards G of enumerators e registered 
55 

* to this class. These assert "there are more values to enumerate for e". 
56 

* (2) Positive bounds (DT_SYGUS_BOUND m n) for "measure terms" m (see below), 
57 

* where n is a nonnegative integer. This asserts "the measure of terms 
58 

* we are enumerating for enumerators whose measure term m is at most n", 
59 

* where measure is commonly term size, but can also be height. 
60 

* 
61 

* We prioritize decisions of form (1) before (2). Both kinds of decision are 
62 

* critical for solution completeness, which is enforced by DecisionManager. 
63 

*/ 
64 

class SygusExtension 
65 

{ 
66 

typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap; 
67 

typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; 
68 

typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; 
69 

typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; 
70 


71 

public: 
72 

SygusExtension(TheoryState& s, 
73 

InferenceManager& im, 
74 

quantifiers::TermDbSygus* tds, 
75 

DecisionManager* dm); 
76 

~SygusExtension(); 
77 

/** 
78 

* Notify this class that tester for constructor tindex has been asserted for 
79 

* n. Exp is the literal corresponding to this tester. This method may send 
80 

* lemmas via inference manager, for details see assertTesterInternal below. 
81 

* These lemmas are sent out on the output channel of datatypes by the caller. 
82 

*/ 
83 

void assertTester(int tindex, TNode n, Node exp); 
84 

/** 
85 

* Notify this class that literal n has been asserted with the given 
86 

* polarity. This method may send lemmas via inference manager, for instance 
87 

* based on inferring consequences of (not) n. One example is if n is 
88 

* (DT_SIZE_BOUND x n), we add the lemma: 
89 

* (DT_SIZE_BOUND x n) <=> ((DT_SIZE x) <= n ) 
90 

*/ 
91 

void assertFact(Node n, bool polarity); 
92 

/** preregister term n 
93 

* 
94 

* This is called when n is preregistered with the theory of datatypes. 
95 

* If n is a sygus enumerator, then we may send lemmas via inference manager 
96 

* that are used to enforce fairness regarding the size of n. 
97 

*/ 
98 

void preRegisterTerm(TNode n); 
99 

/** check 
100 

* 
101 

* This is called at last call effort, when the current model assignment is 
102 

* satisfiable according to the quantifierfree decision procedures and a 
103 

* model is built. This method may send lemmas via inference manager based 
104 

* on dynamic symmetry breaking techniques, based on the model values of 
105 

* all preregistered enumerators. 
106 

*/ 
107 

void check(); 
108 


109 

private: 
110 

/** The theory state of the datatype theory */ 
111 

TheoryState& d_state; 
112 

/** The inference manager of the datatype theory */ 
113 

InferenceManager& d_im; 
114 

/** Pointer to the sygus term database */ 
115 

quantifiers::TermDbSygus* d_tds; 
116 

/** Pointer to the decision manager */ 
117 

DecisionManager* d_dm; 
118 

/** the simple symmetry breaking utility */ 
119 

SygusSimpleSymBreak d_ssb; 
120 

/** 
121 

* Map from terms to the index of the tester that is asserted for them in 
122 

* the current SAT context. In other words, if d_testers[n] = 2, then the 
123 

* tester isC_2(n) is asserted in this SAT context. 
124 

*/ 
125 

IntMap d_testers; 
126 

/** 
127 

* Map from terms to the tester asserted for them. In the example above, 
128 

* d_testers[n] = isC_2(n). 
129 

*/ 
130 

NodeMap d_testers_exp; 
131 

/** 
132 

* The set of (selector chain) terms that are active in the current SAT 
133 

* context. A selector chain term S_n( ... S_1( x )... ) is active if either: 
134 

* (1) n=0 and x is a sygus enumerator, 
135 

* or: 
136 

* (2.1) S_{n1}( ... S_1( x )) is active, 
137 

* (2.2) isC( S_{n1}( ... S_1( x )) ) is asserted in this SAT context, and 
138 

* (2.3) S_n is a selector for constructor C. 
139 

*/ 
140 

NodeSet d_active_terms; 
141 

/** 
142 

* Map from enumerators to a lower bound on their size in the current SAT 
143 

* context. 
144 

*/ 
145 

IntMap d_currTermSize; 
146 

/** zero */ 
147 

Node d_zero; 
148 

/** true */ 
149 

Node d_true; 
150 

/** 
151 

* Map from terms (selector chains) to their anchors. The anchor of a 
152 

* selector chain S1( ... Sn( x ) ... ) is x. 
153 

*/ 
154 

std::unordered_map<Node, Node, NodeHashFunction> d_term_to_anchor; 
155 

/** 
156 

* Map from anchors to the conjecture they are associated with. 
157 

*/ 
158 

std::map<Node, quantifiers::SynthConjecture*> d_anchor_to_conj; 
159 

/** 
160 

* Map from terms (selector chains) to their depth. The depth of a selector 
161 

* chain S1( ... Sn( x ) ... ) is: 
162 

* weight( S1 ) + ... + weight( Sn ), 
163 

* where weight is the selector weight of Si 
164 

* (see SygusTermDatabase::getSelectorWeight). 
165 

*/ 
166 

std::unordered_map<Node, unsigned, NodeHashFunction> d_term_to_depth; 
167 

/** 
168 

* Map from terms (selector chains) to whether they are the topmost term 
169 

* of their type. For example, if: 
170 

* S1 : T1 > T2 
171 

* S2 : T2 > T2 
172 

* S3 : T2 > T1 
173 

* S4 : T1 > T3 
174 

* Then, x, S1( x ), and S4( S3( S2( S1( x ) ) ) ) are toplevel terms, 
175 

* whereas S2( S1( x ) ) and S3( S2( S1( x ) ) ) are not. 
176 

*/ 
177 

std::unordered_map<Node, bool, NodeHashFunction> d_is_top_level; 
178 

/** 
179 

* Returns true if the selector chain n is toplevel based on the above 
180 

* definition, when tn is the type of n. 
181 

*/ 
182 

bool computeTopLevel( TypeNode tn, Node n ); 
183 

private: 
184 

/** This caches all information regarding symmetry breaking for an anchor. */ 
185 
629 
class SearchCache 
186 

{ 
187 

public: 
188 
629 
SearchCache(){} 
189 

/** 
190 

* A cache of all search terms for (types, sizes). See registerSearchTerm 
191 

* for definition of search terms. 
192 

*/ 
193 

std::map< TypeNode, std::map< unsigned, std::vector< Node > > > d_search_terms; 
194 

/** A cache of all symmetry breaking lemma templates for (types, sizes). */ 
195 

std::map<TypeNode, std::map<uint64_t, std::vector<Node>>> d_sbLemmas; 
196 

/** search value 
197 

* 
198 

* For each sygus type, a map from a builtin term to a sygus term for that 
199 

* type that we encountered during the search whose analog rewrites to that 
200 

* term. The range of this map can be updated if we later encounter a sygus 
201 

* term that also rewrites to the builtin value but has a smaller term size. 
202 

*/ 
203 

std::map<TypeNode, std::unordered_map<Node, Node, NodeHashFunction>> 
204 

d_search_val; 
205 

/** the size of terms in the range of d_search val. */ 
206 

std::map<TypeNode, std::unordered_map<Node, unsigned, NodeHashFunction>> 
207 

d_search_val_sz; 
208 

/** For each term, whether this cache has processed that term */ 
209 

std::unordered_set<Node, NodeHashFunction> d_search_val_proc; 
210 

}; 
211 

/** An instance of the above cache, for each anchor */ 
212 

std::map< Node, SearchCache > d_cache; 
213 

//traversal predicates 
214 

/** pre/post traversal predicates for each type, variable 
215 

* 
216 

* This stores predicates (pre, post) whose semantics correspond to whether 
217 

* a variable has occurred by a (pre, post) traversal of a symbolic term, 
218 

* where index = 0 corresponds to pre, index = 1 corresponds to post. For 
219 

* details, see getTraversalPredicate below. 
220 

*/ 
221 

std::map<TypeNode, std::map<Node, Node>> d_traversal_pred[2]; 
222 

/** traversal applications to Boolean variables 
223 

* 
224 

* This maps each application of a traversal predicate pre_x( t ) or 
225 

* post_x( t ) to a fresh Boolean variable. 
226 

*/ 
227 

std::map<Node, Node> d_traversal_bool; 
228 

/** get traversal predicate 
229 

* 
230 

* Get the predicates (pre, post) whose semantics correspond to whether 
231 

* a variable has occurred by this point in a (pre, post) traversal of a term. 
232 

* The type of getTraversalPredicate(tn, n, _) is tn > Bool. 
233 

* 
234 

* For example, consider the term: 
235 

* f( x_1, g( x_2, x_3 ) ) 
236 

* and a lefttoright, depthfirst traversal of this term. Let e be 
237 

* a variable of the same type as this term. We say that for the above term: 
238 

* pre_{x_1} is false for e, e.1 and true for e.2, e.2.1, e.2.2 
239 

* pre_{x_2} is false for e, e.1, e.2, e.2.1, and true for e.2.2 
240 

* pre_{x_3} is false for e, e.1, e.2, e.2.1, e.2.2 
241 

* post_{x_1} is true for e.1, e.2.1, e.2.2, e.2, e 
242 

* post_{x_2} is false for e.1 and true for e.2.1, e.2.2, e.2, e 
243 

* post_{x_3} is false for e.1, e.2.1 and true for e.2.2, e.2, e 
244 

* 
245 

* We enforce a symmetry breaking scheme for each enumerator e that is 
246 

* "variableagnostic" (see argument isVarAgnostic in registerEnumerator) 
247 

* that ensures the variables are ordered. This scheme makes use of these 
248 

* predicates, described in the following: 
249 

* 
250 

* Let x_1, ..., x_m be variables that occur in the same subclass in the type 
251 

* of e (see TermDbSygus::getSubclassForVar). 
252 

* For i = 1, ..., m: 
253 

* // each variable does not occur initially in a traversal of e 
254 

* ~pre_{x_i}( e ) AND 
255 

* // for each subterm of e 
256 

* template z. 
257 

* // if this is variable x_i, then x_{i1} must have already occurred 
258 

* isx_i( z ) => pre_{x_{i1}}( z ) AND 
259 

* for args a = 1...n 
260 

* // predefinition for each argument of this term 
261 

* pre_{x_i}( z.a ) = a=0 ? pre_{x_i}( z ) : post_{x_i}( z.{a1} ) AND 
262 

* // postdefinition for this term 
263 

* post_{x_i}( z ) = post_{x_i}( z.n ) OR isx_i( z ) 
264 

* 
265 

* For clarity, above we have written pre and post as firstorder predicates. 
266 

* However, applications of pre/post should be seen as indexed Boolean 
267 

* variables. The reason for this is pre and post cannot be given a consistent 
268 

* semantics. For example, consider term f( x_1, x_1 ) and enumerator variable 
269 

* e of the same type over which we are encoding a traversal. We have that 
270 

* pre_{x_1}( e.1 ) is false and pre_{x_1}( e.2 ) is true, although the model 
271 

* values for e.1 and e.2 are equal. Instead, pre_{x_1}( e.1 ) should be seen 
272 

* as a Boolean variable V_pre_{x_1,e.1} indexed by x_1 and e.1. and likewise 
273 

* for e.2. We convert all applications of pre/post to Boolean variables in 
274 

* the method eliminateTraversalPredicates below. Nevertheless, it is 
275 

* important that applications pre and post are encoded as APPLY_UF 
276 

* applications so that they behave as expected under substitutions. For 
277 

* example, pre_{x_1}( z.1 ) { z > e.2 } results in pre_{x_1}( e.2.1 ), which 
278 

* after eliminateTraversalPredicates is V_pre_{x_1, e.2.1}. 
279 

*/ 
280 

Node getTraversalPredicate(TypeNode tn, Node n, bool isPre); 
281 

/** eliminate traversal predicates 
282 

* 
283 

* This replaces all applications of traversal predicates P( x ) in n with 
284 

* unique Boolean variables, given by d_traversal_bool[ P( x ) ], and 
285 

* returns the result. 
286 

*/ 
287 

Node eliminateTraversalPredicates(Node n); 
288 

//end traversal predicates 
289 

/** a sygus sampler object for each (anchor, sygus type) pair 
290 

* 
291 

* This is used for the sygusRewVerify() option to verify the correctness of 
292 

* the rewriter. 
293 

*/ 
294 

std::map<Node, std::map<TypeNode, quantifiers::SygusSampler>> d_sampler; 
295 

/** Assert tester internal 
296 

* 
297 

* This function is called when the tester with index tindex is asserted for 
298 

* n, exp is the tester predicate. For example, for grammar: 
299 

* A > A+A  x  1  0 
300 

* when is_+( d ) is asserted, 
301 

* assertTesterInternal(0, s( d ), is_+( s( d ) ),...) is called. This 
302 

* function may send lemmas via inference manager. 
303 

* 
304 

* These lemmas are of various forms, including: 
305 

* (1) dynamic symmetry breaking clauses for subterms of n (those added to 
306 

* lemmas on calls to addSymBreakLemmasFor, see function below), 
307 

* (2) static symmetry breaking clauses for subterms of n (those added to 
308 

* lemmas on getSimpleSymBreakPred, see function below), 
309 

* (3) conjecturespecific symmetry breaking lemmas, see 
310 

* SynthConjecture::getSymmetryBreakingPredicate, 
311 

* (4) fairness conflicts if sygusFair() is SygusFairMode::DIRECT, e.g.: 
312 

* size( d ) <= 1 V ~isC1( d ) V ~isC2( d.1 ) 
313 

* where C1 and C2 are nonnullary constructors. 
314 

*/ 
315 

void assertTesterInternal(int tindex, TNode n, Node exp); 
316 

/** 
317 

* This function is called when term n is registered to the theory of 
318 

* datatypes. It makes the appropriate call to registerSearchTerm below, 
319 

* if applicable. 
320 

*/ 
321 

void registerTerm(Node n); 
322 


323 

//dynamic symmetry breaking 
324 

/** Register search term 
325 

* 
326 

* This function is called when selector chain n of the form 
327 

* S_1( ... S_m( x ) ... ) is registered to the theory of datatypes, where 
328 

* tn is the type of n, d indicates the depth of n (the sum of weights of the 
329 

* selectors S_1...S_m), and topLevel is whether n is a toplevel term 
330 

* (see d_is_top_level). We refer to n as a "search term". 
331 

* 
332 

* The purpose of this function is to notify this class that symmetry breaking 
333 

* lemmas should be instantiated for n. Any symmetry breaking lemmas that 
334 

* are active for n (see description of addSymBreakLemmasFor) are added to 
335 

* lemmas in this call. 
336 

*/ 
337 

void registerSearchTerm(TypeNode tn, unsigned d, Node n, bool topLevel); 
338 

/** Register search value 
339 

* 
340 

* This function is called when a selector chain n has been assigned a model 
341 

* value nv. This function calls itself recursively so that extensions of the 
342 

* selector chain n are registered with all the subterms of nv. For example, 
343 

* if we call this function with: 
344 

* n = x, nv = +( 1(), x() ) 
345 

* we make recursive calls with: 
346 

* n = x.1, nv = 1() and n = x.2, nv = x() 
347 

* 
348 

* a : the anchor of n, 
349 

* d : the depth of n. 
350 

* 
351 

* This function determines if the value nv is equivalent via rewriting to 
352 

* any previously registered search values for anchor a. If so, we construct 
353 

* a symmetry breaking lemma template and register it in d_cache[a]. For 
354 

* example, for grammar: 
355 

* A > A+A  x  1  0 
356 

* Registering search value d > x followed by d > +( x, 0 ) results in the 
357 

* construction of the symmetry breaking lemma template: 
358 

* ~is_+( z ) V ~is_x( z.1 ) V ~is_0( z.2 ) 
359 

* which is stored in d_cache[a].d_sbLemmas. This lemma is instantiated with 
360 

* z > t for all terms t of appropriate depth, including d. 
361 

* This function strengthens blocking clauses using generalization techniques 
362 

* described in Reynolds et al SYNT 2017. 
363 

* 
364 

* The return value of this function is an abstraction of model assignment 
365 

* of nv to n, or null if we wish to exclude the model assignment nv to n. 
366 

* The return value of this method is different from nv itself, e.g. if it 
367 

* contains occurrences of the "any constant" constructor. For example, if 
368 

* nv is C_+( C_x(), C_{any_constant}( 5 ) ), then the return value of this 
369 

* function will either be null, or C_+( C_x(), C_{any_constant}( n.1.0 ) ), 
370 

* where n.1.0 is the appropriate selector chain applied to n. We build this 
371 

* abstraction since the semantics of C_{any_constant} is "any constant" and 
372 

* not "some constant". Thus, we should consider the subterm 
373 

* C_{any_constant}( 5 ) above to be an unconstrained variable (as represented 
374 

* by a selector chain), instead of the concrete value 5. 
375 

* 
376 

* The flag isVarAgnostic is whether "a" is a variable agnostic enumerator. If 
377 

* this is the case, we restrict symmetry breaking to subterms of n on its 
378 

* leftmost subchain. For example, consider the grammar: 
379 

* A > B=B 
380 

* B > B+B  x  y  0 
381 

* Say we are registering the search value x = y+x. Notice that this value is 
382 

* ordered. If a were a variableagnostic enumerator of type A in this 
383 

* case, we would only register x = y+x and x, and not y+x or y, since the 
384 

* latter two terms are not leftmost subterms in this value. If we did on the 
385 

* other hand register y+x, we would be prevented from solutions like x+y = 0 
386 

* later, since x+y is equivalent to (the already registered value) y+x. 
387 

* 
388 

* If doSym is false, we are not performing symmetry breaking on n. This flag 
389 

* is set to false on branches of n that are not leftmost. 
390 

*/ 
391 

Node registerSearchValue(Node a, 
392 

Node n, 
393 

Node nv, 
394 

unsigned d, 
395 

bool isVarAgnostic, 
396 

bool doSym); 
397 

/** Register symmetry breaking lemma 
398 

* 
399 

* This function adds the symmetry breaking lemma template lem for terms of 
400 

* type tn with anchor a. This is added to d_cache[a].d_sbLemmas. Notice that 
401 

* we use lem as a template with free variable x, e.g. our template is: 
402 

* (lambda ((x tn)) lem) 
403 

* where x = getFreeVar( tn ). For all search terms t of the appropriate 
404 

* depth, we send the lemma lem{ x > t } via the inference manager. 
405 

* 
406 

* The argument sz indicates the size of terms that the lemma applies to, e.g. 
407 

* ~is_+( z ) has size 1 
408 

* ~is_+( z ) V ~is_x( z.1 ) V ~is_0( z.2 ) has size 1 
409 

* ~is_+( z ) V ~is_+( z.1 ) has size 2 
410 

* This is equivalent to sum of weights of constructors corresponding to each 
411 

* tester, e.g. above + has weight 1, and x and 0 have weight 0. 
412 

*/ 
413 

void registerSymBreakLemma(TypeNode tn, Node lem, unsigned sz, Node a); 
414 

/** Register symmetry breaking lemma for value 
415 

* 
416 

* This function adds a symmetry breaking lemma template for selector chains 
417 

* with anchor a, that effectively states that val should never be a subterm 
418 

* of any value for a. 
419 

* 
420 

* et : an "invariance test" (see sygus/sygus_invariance.h) which states a 
421 

* criterion that val meets, which is the reason for its exclusion. This is 
422 

* used for generalizing the symmetry breaking lemma template. 
423 

* valr : if nonnull, this states a value that should *not* be excluded by 
424 

* the symmetry breaking lemma template, which is a restriction to the above 
425 

* generalization. 
426 

* 
427 

* This function may add instances of the symmetry breaking template for 
428 

* existing search terms, which are sent via the inference manager. 
429 

*/ 
430 

void registerSymBreakLemmaForValue(Node a, 
431 

Node val, 
432 

quantifiers::SygusInvarianceTest& et, 
433 

Node valr, 
434 

std::map<TypeNode, int>& var_count); 
435 

/** Add symmetry breaking lemmas for term 
436 

* 
437 

* Sends all active symmetry breaking lemmas for selector chain t via the 
438 

* inference manager. A symmetry breaking lemma L is active for t based on 
439 

* three factors: 
440 

* (1) the current search size sz(a) for its anchor a, 
441 

* (2) the depth d of term t (see d_term_to_depth), 
442 

* (3) the size sz(L) of the symmetry breaking lemma L. 
443 

* In particular, L is active if sz(L) <= sz(a)  d. In other words, a 
444 

* symmetry breaking lemma is active if it is intended to block terms of 
445 

* size sz(L), and the maximum size that t can take in the current search, 
446 

* sz(a)d, is greater than or equal to this value. 
447 

* 
448 

* tn : the type of term t, 
449 

* a : the anchor of term t, 
450 

* d : the depth of term t. 
451 

*/ 
452 

void addSymBreakLemmasFor(TypeNode tn, TNode t, unsigned d, Node a); 
453 

/** calls the above function where a is the anchor t */ 
454 

void addSymBreakLemmasFor(TypeNode tn, TNode t, unsigned d); 
455 

//end dynamic symmetry breaking 
456 


457 

/** Get relevancy condition 
458 

* 
459 

* This returns (the negation of) a predicate that holds in the contexts in 
460 

* which the selector chain n is specified. For example, the negation of the 
461 

* relevancy condition for sel_{C2,1}( sel_{C1,1}( d ) ) is 
462 

* ~( isC1( d ) ^ isC2( sel_{C1,1}( d ) ) ) 
463 

* If shared selectors are enabled, this is a conjunction of disjunctions, 
464 

* since shared selectors may apply to multiple constructors. 
465 

*/ 
466 

Node getRelevancyCondition( Node n ); 
467 

/** Cache of the above function */ 
468 

std::map<Node, Node> d_rlv_cond; 
469 


470 

//static symmetry breaking 
471 

/** Get simple symmetry breakind predicate 
472 

* 
473 

* This function returns the "static" symmetry breaking lemma template for 
474 

* terms with type tn and constructor index tindex, for the given depth. This 
475 

* includes inferences about size with depth=0. Given grammar: 
476 

* A > ite( B, A, A )  A+A  x  1  0 
477 

* B > A = A 
478 

* Examples of static symmetry breaking lemma templates are: 
479 

* for +, depth 0: size(z)=size(z.1)+size(z.2)+1 
480 

* for +, depth 1: ~is0( z.1 ) ^ ~is0( z.2 ) ^ F 
481 

* where F ensures the constructor of z.1 is less than that of z.2 based 
482 

* on some ordering. 
483 

* for ite, depth 1: z.2 != z.3 
484 

* These templates can be thought of as "hardcoded" cases of dynamic symmetry 
485 

* breaking lemma templates. Notice that the above lemma templates are in 
486 

* terms of getFreeVar( tn ), hence only one is created per 
487 

* (constructor, depth). A static symmetry break lemma template F[z] for 
488 

* constructor C are included in lemmas of the form: 
489 

* isC( t ) => F[t] 
490 

* where t is a search term, see registerSearchTerm for definition of search 
491 

* term. 
492 

* 
493 

* usingSymCons: whether we are using symbolic constructors for subterms in 
494 

* the type tn, 
495 

* isVarAgnostic: whether the terms we are enumerating are agnostic to 
496 

* variables. 
497 

* 
498 

* The latter two options may affect the form of the predicate we construct. 
499 

*/ 
500 

Node getSimpleSymBreakPred(Node e, 
501 

TypeNode tn, 
502 

int tindex, 
503 

unsigned depth, 
504 

bool usingSymCons, 
505 

bool isVarAgnostic); 
506 

/** Cache of the above function */ 
507 

std::map<Node, 
508 

std::map<TypeNode, 
509 

std::map<int, std::map<bool, std::map<unsigned, Node>>>>> 
510 

d_simple_sb_pred; 
511 

/** 
512 

* For each search term, this stores the maximum depth for which we have added 
513 

* a static symmetry breaking lemma. 
514 

* 
515 

* This should be user contextdependent if sygus is updated to work in 
516 

* incremental mode. 
517 

*/ 
518 

std::unordered_map<Node, unsigned, NodeHashFunction> d_simple_proc; 
519 

//end static symmetry breaking 
520 


521 

/** Get the canonical free variable for type tn */ 
522 

TNode getFreeVar( TypeNode tn ); 
523 

/** get term order predicate 
524 

* 
525 

* Assuming that n1 and n2 are children of a commutative operator, this 
526 

* returns a symmetry breaking predicate that can be instantiated for n1 and 
527 

* n2 while preserving satisfiability. By default, this is the predicate 
528 

* ( DT_SIZE n1 ) >= ( DT_SIZE n2 ) 
529 

*/ 
530 

Node getTermOrderPredicate( Node n1, Node n2 ); 
531 


532 

private: 
533 

/** 
534 

* Map from registered variables to whether they are a sygus enumerator. 
535 

* 
536 

* This should be user contextdependent if sygus is updated to work in 
537 

* incremental mode. 
538 

*/ 
539 

std::map<Node, bool> d_register_st; 
540 

//search size information 
541 

/** 
542 

* Checks whether e is a sygus enumerator, that is, a term for which this 
543 

* class will track size for. 
544 

* 
545 

* We associate each sygus enumerator e with a "measure term", which is used 
546 

* for bounding the size of terms for the models of e. The measure term for a 
547 

* sygus enumerator may be e itself (if e has an active guard), or an 
548 

* arbitrary sygus variable otherwise. A measure term m is one for which our 
549 

* decision strategy decides on literals of the form (DT_SYGUS_BOUND m n). 
550 

* 
551 

* After determining the measure term m for e, if applicable, we initialize 
552 

* SygusSizeDecisionStrategy for m below. This may result in lemmas sent via 
553 

* the inference manager. 
554 

*/ 
555 

void registerSizeTerm(Node e); 
556 

/** A decision strategy for each measure term allocated by this class */ 
557 
826 
class SygusSizeDecisionStrategy : public DecisionStrategyFmf 
558 

{ 
559 

public: 
560 

SygusSizeDecisionStrategy(InferenceManager& im, Node t, TheoryState& s); 
561 

/** the measure term */ 
562 

Node d_this; 
563 

/** 
564 

* For each size n, an explanation for why this measure term has size at 
565 

* most n. This is typically the literal (DT_SYGUS_BOUND m n), which 
566 

* we call the (n^th) "fairness literal" for m. 
567 

*/ 
568 

std::map< unsigned, Node > d_search_size_exp; 
569 

/** 
570 

* For each size, whether we have called SygusExtension::notifySearchSize. 
571 

*/ 
572 

std::map< unsigned, bool > d_search_size; 
573 

/** 
574 

* The current search size. This corresponds to the number of times 
575 

* incrementCurrentSearchSize has been called for this measure term. 
576 

*/ 
577 

unsigned d_curr_search_size; 
578 

/** the list of all enumerators whose measure term is this */ 
579 

std::vector< Node > d_anchors; 
580 

/** get or make the measure value 
581 

* 
582 

* The measure value is an integer variable v that is a (symbolic) integer 
583 

* value that is constrained to be less than or equal to the current search 
584 

* size. For example, if we are using the fairness strategy 
585 

* SygusFairMode::DT_SIZE (see options/datatype_options.h), then we 
586 

* constrain: (DT_SYGUS_BOUND m n) <=> (v <= n) for all asserted fairness 
587 

* literals. Then, if we are enforcing fairness based on the maximum size, 
588 

* we assert: (DT_SIZE e) <= v for all enumerators e. 
589 

*/ 
590 

Node getOrMkMeasureValue(); 
591 

/** get or make the active measure value 
592 

* 
593 

* The active measure value av is an integer variable that corresponds to 
594 

* the (symbolic) value of the sum of enumerators that are yet to be 
595 

* registered. This is to enforce the "sum of measures" strategy. For 
596 

* example, if we are using the fairness strategy SygusFairMode::DT_SIZE, 
597 

* then initially av is equal to the measure value v, and the constraints 
598 

* (DT_SYGUS_BOUND m n) <=> (v <= n) 
599 

* are added as before. When an enumerator e is registered, we add the 
600 

* lemma: 
601 

* av = (DT_SIZE e) + av' 
602 

* and update the active measure value to av'. This ensures that the sum 
603 

* of sizes of active enumerators is at most n. 
604 

* 
605 

* If the flag mkNew is set to true, then we return a fresh variable and 
606 

* update the active measure value. 
607 

*/ 
608 

Node getOrMkActiveMeasureValue(bool mkNew = false); 
609 

/** Returns the s^th fairness literal for this measure term. */ 
610 

Node mkLiteral(unsigned s) override; 
611 

/** identify */ 
612 
1300595 
std::string identify() const override 
613 

{ 
614 
1300595 
return std::string("sygus_enum_size"); 
615 

} 
616 


617 

private: 
618 

/** The inference manager we are using */ 
619 

InferenceManager& d_im; 
620 

/** the measure value */ 
621 

Node d_measure_value; 
622 

/** the sygus measure value */ 
623 

Node d_measure_value_active; 
624 

}; 
625 

/** the above information for each registered measure term */ 
626 

std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>> d_szinfo; 
627 

/** map from enumerators (anchors) to their associated measure term */ 
628 

std::map< Node, Node > d_anchor_to_measure_term; 
629 

/** map from enumerators (anchors) to their active guard*/ 
630 

std::map< Node, Node > d_anchor_to_active_guard; 
631 

/** map from enumerators (anchors) to a decision stratregy for that guard */ 
632 

std::map<Node, std::unique_ptr<DecisionStrategy>> d_anchor_to_ag_strategy; 
633 

/** generic measure term 
634 

* 
635 

* This is a global term that is used as the measure term for all sygus 
636 

* enumerators that do not have active guards. This class enforces that 
637 

* all enumerators have size at most n, where n is the minimal integer 
638 

* such that (DT_SYGUS_BOUND d_generic_measure_term n) is asserted. 
639 

*/ 
640 

Node d_generic_measure_term; 
641 

/** 
642 

* This increments the current search size for measure term m. This may 
643 

* cause lemmas to be added to lemmas based on the fact that symmetry 
644 

* breaking lemmas are now relevant for new search terms, see discussion 
645 

* of how search size affects which lemmas are relevant above 
646 

* addSymBreakLemmasFor. 
647 

*/ 
648 

void incrementCurrentSearchSize(TNode m); 
649 

/** 
650 

* Notify this class that we are currently searching for terms of size at 
651 

* most s as model values for measure term m. Literal exp corresponds to the 
652 

* explanation of why the measure term has size at most n. This calls 
653 

* incrementSearchSize above, until the total number of times we have called 
654 

* incrementSearchSize so far is at least s. 
655 

*/ 
656 

void notifySearchSize(TNode m, uint64_t s, Node exp); 
657 

/** Allocates a SygusSizeDecisionStrategy object in d_szinfo. */ 
658 

void registerMeasureTerm( Node m ); 
659 

/** 
660 

* Return the current search size for arbitrary term n. This is the current 
661 

* search size of the anchor of n. 
662 

*/ 
663 

unsigned getSearchSizeFor( Node n ); 
664 

/** return the current search size for enumerator (anchor) e */ 
665 

unsigned getSearchSizeForAnchor(Node e); 
666 

/** Get the current search size for measure term m in this SAT context. */ 
667 

unsigned getSearchSizeForMeasureTerm(Node m); 
668 

/** get current template 
669 

* 
670 

* For debugging. This returns a term that corresponds to the current 
671 

* inferred shape of n. For example, if the testers 
672 

* isC1( n ) and isC2( n.1 ) 
673 

* have been asserted where C1 and C2 are binary constructors, then this 
674 

* method may return a term of the form: 
675 

* C1( C2( x1, x2 ), x3 ) 
676 

* for fresh variables x1, x2, x3. The map var_count maintains the variable 
677 

* count for generating these fresh variables. 
678 

*/ 
679 

Node getCurrentTemplate( Node n, std::map< TypeNode, int >& var_count ); 
680 

//end search size information 
681 

/** check value 
682 

* 
683 

* This is called when we have a model assignment vn for n, where n is 
684 

* a selector chain applied to an enumerator (a search term). This function 
685 

* ensures that testers have been asserted for each subterm of vn. This is 
686 

* critical for ensuring that the proper steps have been taken by this class 
687 

* regarding whether or not vn is a legal value for n (not greater than the 
688 

* current search size and not a value that can be blocked by symmetry 
689 

* breaking). 
690 

* 
691 

* For example, if vn = +( x(), x() ), then we ensure that the testers 
692 

* is+( n ), isx( n.1 ), isx( n.2 ) 
693 

* have been asserted to this class. If a tester is not asserted for some 
694 

* relevant selector chain S( n ) of n, then we add a lemma L for that 
695 

* selector chain to lemmas, where L is the "splitting lemma" for S( n ), that 
696 

* states that the top symbol of S( n ) must be one of the constructors of 
697 

* its type. 
698 

* 
699 

* Notice that this function is a sanity check. Typically, it should be the 
700 

* case that testers are asserted for all subterms of vn, and hence this 
701 

* method should not ever add anything to lemmas. However, due to its 
702 

* importance, we check this regardless. 
703 

*/ 
704 

bool checkValue(Node n, TNode vn, int ind); 
705 

/** 
706 

* Get the current SAT status of the guard g. 
707 

* In particular, this returns 1 if g is asserted true, 1 if it is asserted 
708 

* false, and 0 if it is not asserted. 
709 

*/ 
710 

int getGuardStatus( Node g ); 
711 

}; 
712 


713 

} 
714 

} 
715 

} 
716 


717 

#endif 
718 

