1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner, Gereon Kremer |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* The sygus extension of the theory of datatypes. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__THEORY__DATATYPES__SYGUS_EXTENSION_H |
19 |
|
#define CVC5__THEORY__DATATYPES__SYGUS_EXTENSION_H |
20 |
|
|
21 |
|
#include <iostream> |
22 |
|
#include <map> |
23 |
|
|
24 |
|
#include "context/cdhashmap.h" |
25 |
|
#include "context/cdhashset.h" |
26 |
|
#include "context/context.h" |
27 |
|
#include "expr/node.h" |
28 |
|
#include "theory/datatypes/sygus_simple_sym.h" |
29 |
|
#include "theory/decision_manager.h" |
30 |
|
#include "theory/quantifiers/sygus_sampler.h" |
31 |
|
#include "theory/quantifiers/term_database.h" |
32 |
|
|
33 |
|
namespace cvc5 { |
34 |
|
namespace theory { |
35 |
|
namespace quantifiers { |
36 |
|
class SynthConjecture; |
37 |
|
} |
38 |
|
namespace datatypes { |
39 |
|
|
40 |
|
class InferenceManager; |
41 |
|
|
42 |
|
/** |
43 |
|
* This is the sygus extension of the decision procedure for quantifier-free |
44 |
|
* inductive datatypes. At a high level, this class takes as input a |
45 |
|
* set of asserted testers is-C1( x ), is-C2( x.1 ), is-C3( x.2 ), and |
46 |
|
* generates lemmas that restrict the models of x, if x is a "sygus enumerator" |
47 |
|
* (see TermDbSygus::registerEnumerator). |
48 |
|
* |
49 |
|
* Some of these techniques are described in these papers: |
50 |
|
* "Refutation-Based Synthesis in SMT", Reynolds et al 2017. |
51 |
|
* "Sygus Techniques in the Core of an SMT Solver", Reynolds et al 2017. |
52 |
|
* |
53 |
|
* This class enforces two decisions stragies via calls to registerStrategy |
54 |
|
* of the owning theory's DecisionManager: |
55 |
|
* (1) Positive decisions on the active guards G of enumerators e registered |
56 |
|
* to this class. These assert "there are more values to enumerate for e". |
57 |
|
* (2) Positive bounds (DT_SYGUS_BOUND m n) for "measure terms" m (see below), |
58 |
|
* where n is a non-negative integer. This asserts "the measure of terms |
59 |
|
* we are enumerating for enumerators whose measure term m is at most n", |
60 |
|
* where measure is commonly term size, but can also be height. |
61 |
|
* |
62 |
|
* We prioritize decisions of form (1) before (2). Both kinds of decision are |
63 |
|
* critical for solution completeness, which is enforced by DecisionManager. |
64 |
|
*/ |
65 |
|
class SygusExtension |
66 |
|
{ |
67 |
|
typedef context::CDHashMap<Node, int> IntMap; |
68 |
|
typedef context::CDHashMap<Node, Node> NodeMap; |
69 |
|
typedef context::CDHashMap<Node, bool> BoolMap; |
70 |
|
typedef context::CDHashSet<Node> NodeSet; |
71 |
|
|
72 |
|
public: |
73 |
|
SygusExtension(TheoryState& s, |
74 |
|
InferenceManager& im, |
75 |
|
quantifiers::TermDbSygus* tds); |
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 |
|
/** pre-register term n |
93 |
|
* |
94 |
|
* This is called when n is pre-registered 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 quantifier-free 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 |
|
/** the simple symmetry breaking utility */ |
117 |
|
SygusSimpleSymBreak d_ssb; |
118 |
|
/** |
119 |
|
* Map from terms to the index of the tester that is asserted for them in |
120 |
|
* the current SAT context. In other words, if d_testers[n] = 2, then the |
121 |
|
* tester is-C_2(n) is asserted in this SAT context. |
122 |
|
*/ |
123 |
|
IntMap d_testers; |
124 |
|
/** |
125 |
|
* Map from terms to the tester asserted for them. In the example above, |
126 |
|
* d_testers[n] = is-C_2(n). |
127 |
|
*/ |
128 |
|
NodeMap d_testers_exp; |
129 |
|
/** |
130 |
|
* The set of (selector chain) terms that are active in the current SAT |
131 |
|
* context. A selector chain term S_n( ... S_1( x )... ) is active if either: |
132 |
|
* (1) n=0 and x is a sygus enumerator, |
133 |
|
* or: |
134 |
|
* (2.1) S_{n-1}( ... S_1( x )) is active, |
135 |
|
* (2.2) is-C( S_{n-1}( ... S_1( x )) ) is asserted in this SAT context, and |
136 |
|
* (2.3) S_n is a selector for constructor C. |
137 |
|
*/ |
138 |
|
NodeSet d_active_terms; |
139 |
|
/** |
140 |
|
* Map from enumerators to a lower bound on their size in the current SAT |
141 |
|
* context. |
142 |
|
*/ |
143 |
|
IntMap d_currTermSize; |
144 |
|
/** zero */ |
145 |
|
Node d_zero; |
146 |
|
/** true */ |
147 |
|
Node d_true; |
148 |
|
/** |
149 |
|
* Map from terms (selector chains) to their anchors. The anchor of a |
150 |
|
* selector chain S1( ... Sn( x ) ... ) is x. |
151 |
|
*/ |
152 |
|
std::unordered_map<Node, Node> d_term_to_anchor; |
153 |
|
/** |
154 |
|
* Map from anchors to the conjecture they are associated with. |
155 |
|
*/ |
156 |
|
std::map<Node, quantifiers::SynthConjecture*> d_anchor_to_conj; |
157 |
|
/** |
158 |
|
* Map from terms (selector chains) to their depth. The depth of a selector |
159 |
|
* chain S1( ... Sn( x ) ... ) is: |
160 |
|
* weight( S1 ) + ... + weight( Sn ), |
161 |
|
* where weight is the selector weight of Si |
162 |
|
* (see SygusTermDatabase::getSelectorWeight). |
163 |
|
*/ |
164 |
|
std::unordered_map<Node, unsigned> d_term_to_depth; |
165 |
|
/** |
166 |
|
* Map from terms (selector chains) to whether they are the topmost term |
167 |
|
* of their type. For example, if: |
168 |
|
* S1 : T1 -> T2 |
169 |
|
* S2 : T2 -> T2 |
170 |
|
* S3 : T2 -> T1 |
171 |
|
* S4 : T1 -> T3 |
172 |
|
* Then, x, S1( x ), and S4( S3( S2( S1( x ) ) ) ) are top-level terms, |
173 |
|
* whereas S2( S1( x ) ) and S3( S2( S1( x ) ) ) are not. |
174 |
|
*/ |
175 |
|
std::unordered_map<Node, bool> d_is_top_level; |
176 |
|
/** |
177 |
|
* Returns true if the selector chain n is top-level based on the above |
178 |
|
* definition, when tn is the type of n. |
179 |
|
*/ |
180 |
|
bool computeTopLevel( TypeNode tn, Node n ); |
181 |
|
private: |
182 |
|
/** This caches all information regarding symmetry breaking for an anchor. */ |
183 |
426 |
class SearchCache |
184 |
|
{ |
185 |
|
public: |
186 |
426 |
SearchCache(){} |
187 |
|
/** |
188 |
|
* A cache of all search terms for (types, sizes). See registerSearchTerm |
189 |
|
* for definition of search terms. |
190 |
|
*/ |
191 |
|
std::map< TypeNode, std::map< unsigned, std::vector< Node > > > d_search_terms; |
192 |
|
/** A cache of all symmetry breaking lemma templates for (types, sizes). */ |
193 |
|
std::map<TypeNode, std::map<uint64_t, std::vector<Node>>> d_sbLemmas; |
194 |
|
/** search value |
195 |
|
* |
196 |
|
* For each sygus type, a map from a builtin term to a sygus term for that |
197 |
|
* type that we encountered during the search whose analog rewrites to that |
198 |
|
* term. The range of this map can be updated if we later encounter a sygus |
199 |
|
* term that also rewrites to the builtin value but has a smaller term size. |
200 |
|
*/ |
201 |
|
std::map<TypeNode, std::unordered_map<Node, Node>> d_search_val; |
202 |
|
/** the size of terms in the range of d_search val. */ |
203 |
|
std::map<TypeNode, std::unordered_map<Node, unsigned>> d_search_val_sz; |
204 |
|
/** For each term, whether this cache has processed that term */ |
205 |
|
std::unordered_set<Node> d_search_val_proc; |
206 |
|
}; |
207 |
|
/** An instance of the above cache, for each anchor */ |
208 |
|
std::map< Node, SearchCache > d_cache; |
209 |
|
//-----------------------------------traversal predicates |
210 |
|
/** pre/post traversal predicates for each type, variable |
211 |
|
* |
212 |
|
* This stores predicates (pre, post) whose semantics correspond to whether |
213 |
|
* a variable has occurred by a (pre, post) traversal of a symbolic term, |
214 |
|
* where index = 0 corresponds to pre, index = 1 corresponds to post. For |
215 |
|
* details, see getTraversalPredicate below. |
216 |
|
*/ |
217 |
|
std::map<TypeNode, std::map<Node, Node>> d_traversal_pred[2]; |
218 |
|
/** traversal applications to Boolean variables |
219 |
|
* |
220 |
|
* This maps each application of a traversal predicate pre_x( t ) or |
221 |
|
* post_x( t ) to a fresh Boolean variable. |
222 |
|
*/ |
223 |
|
std::map<Node, Node> d_traversal_bool; |
224 |
|
/** get traversal predicate |
225 |
|
* |
226 |
|
* Get the predicates (pre, post) whose semantics correspond to whether |
227 |
|
* a variable has occurred by this point in a (pre, post) traversal of a term. |
228 |
|
* The type of getTraversalPredicate(tn, n, _) is tn -> Bool. |
229 |
|
* |
230 |
|
* For example, consider the term: |
231 |
|
* f( x_1, g( x_2, x_3 ) ) |
232 |
|
* and a left-to-right, depth-first traversal of this term. Let e be |
233 |
|
* a variable of the same type as this term. We say that for the above term: |
234 |
|
* pre_{x_1} is false for e, e.1 and true for e.2, e.2.1, e.2.2 |
235 |
|
* pre_{x_2} is false for e, e.1, e.2, e.2.1, and true for e.2.2 |
236 |
|
* pre_{x_3} is false for e, e.1, e.2, e.2.1, e.2.2 |
237 |
|
* post_{x_1} is true for e.1, e.2.1, e.2.2, e.2, e |
238 |
|
* post_{x_2} is false for e.1 and true for e.2.1, e.2.2, e.2, e |
239 |
|
* post_{x_3} is false for e.1, e.2.1 and true for e.2.2, e.2, e |
240 |
|
* |
241 |
|
* We enforce a symmetry breaking scheme for each enumerator e that is |
242 |
|
* "variable-agnostic" (see argument isVarAgnostic in registerEnumerator) |
243 |
|
* that ensures the variables are ordered. This scheme makes use of these |
244 |
|
* predicates, described in the following: |
245 |
|
* |
246 |
|
* Let x_1, ..., x_m be variables that occur in the same subclass in the type |
247 |
|
* of e (see TermDbSygus::getSubclassForVar). |
248 |
|
* For i = 1, ..., m: |
249 |
|
* // each variable does not occur initially in a traversal of e |
250 |
|
* ~pre_{x_i}( e ) AND |
251 |
|
* // for each subterm of e |
252 |
|
* template z. |
253 |
|
* // if this is variable x_i, then x_{i-1} must have already occurred |
254 |
|
* is-x_i( z ) => pre_{x_{i-1}}( z ) AND |
255 |
|
* for args a = 1...n |
256 |
|
* // pre-definition for each argument of this term |
257 |
|
* pre_{x_i}( z.a ) = a=0 ? pre_{x_i}( z ) : post_{x_i}( z.{a-1} ) AND |
258 |
|
* // post-definition for this term |
259 |
|
* post_{x_i}( z ) = post_{x_i}( z.n ) OR is-x_i( z ) |
260 |
|
* |
261 |
|
* For clarity, above we have written pre and post as first-order predicates. |
262 |
|
* However, applications of pre/post should be seen as indexed Boolean |
263 |
|
* variables. The reason for this is pre and post cannot be given a consistent |
264 |
|
* semantics. For example, consider term f( x_1, x_1 ) and enumerator variable |
265 |
|
* e of the same type over which we are encoding a traversal. We have that |
266 |
|
* pre_{x_1}( e.1 ) is false and pre_{x_1}( e.2 ) is true, although the model |
267 |
|
* values for e.1 and e.2 are equal. Instead, pre_{x_1}( e.1 ) should be seen |
268 |
|
* as a Boolean variable V_pre_{x_1,e.1} indexed by x_1 and e.1. and likewise |
269 |
|
* for e.2. We convert all applications of pre/post to Boolean variables in |
270 |
|
* the method eliminateTraversalPredicates below. Nevertheless, it is |
271 |
|
* important that applications pre and post are encoded as APPLY_UF |
272 |
|
* applications so that they behave as expected under substitutions. For |
273 |
|
* example, pre_{x_1}( z.1 ) { z -> e.2 } results in pre_{x_1}( e.2.1 ), which |
274 |
|
* after eliminateTraversalPredicates is V_pre_{x_1, e.2.1}. |
275 |
|
*/ |
276 |
|
Node getTraversalPredicate(TypeNode tn, Node n, bool isPre); |
277 |
|
/** eliminate traversal predicates |
278 |
|
* |
279 |
|
* This replaces all applications of traversal predicates P( x ) in n with |
280 |
|
* unique Boolean variables, given by d_traversal_bool[ P( x ) ], and |
281 |
|
* returns the result. |
282 |
|
*/ |
283 |
|
Node eliminateTraversalPredicates(Node n); |
284 |
|
//-----------------------------------end traversal predicates |
285 |
|
/** a sygus sampler object for each (anchor, sygus type) pair |
286 |
|
* |
287 |
|
* This is used for the sygusRewVerify() option to verify the correctness of |
288 |
|
* the rewriter. |
289 |
|
*/ |
290 |
|
std::map<Node, std::map<TypeNode, quantifiers::SygusSampler>> d_sampler; |
291 |
|
/** Assert tester internal |
292 |
|
* |
293 |
|
* This function is called when the tester with index tindex is asserted for |
294 |
|
* n, exp is the tester predicate. For example, for grammar: |
295 |
|
* A -> A+A | x | 1 | 0 |
296 |
|
* when is_+( d ) is asserted, |
297 |
|
* assertTesterInternal(0, s( d ), is_+( s( d ) ),...) is called. This |
298 |
|
* function may send lemmas via inference manager. |
299 |
|
* |
300 |
|
* These lemmas are of various forms, including: |
301 |
|
* (1) dynamic symmetry breaking clauses for subterms of n (those added to |
302 |
|
* lemmas on calls to addSymBreakLemmasFor, see function below), |
303 |
|
* (2) static symmetry breaking clauses for subterms of n (those added to |
304 |
|
* lemmas on getSimpleSymBreakPred, see function below), |
305 |
|
* (3) conjecture-specific symmetry breaking lemmas, see |
306 |
|
* SynthConjecture::getSymmetryBreakingPredicate, |
307 |
|
* (4) fairness conflicts if sygusFair() is SygusFairMode::DIRECT, e.g.: |
308 |
|
* size( d ) <= 1 V ~is-C1( d ) V ~is-C2( d.1 ) |
309 |
|
* where C1 and C2 are non-nullary constructors. |
310 |
|
*/ |
311 |
|
void assertTesterInternal(int tindex, TNode n, Node exp); |
312 |
|
/** |
313 |
|
* This function is called when term n is registered to the theory of |
314 |
|
* datatypes. It makes the appropriate call to registerSearchTerm below, |
315 |
|
* if applicable. |
316 |
|
*/ |
317 |
|
void registerTerm(Node n); |
318 |
|
|
319 |
|
//------------------------dynamic symmetry breaking |
320 |
|
/** Register search term |
321 |
|
* |
322 |
|
* This function is called when selector chain n of the form |
323 |
|
* S_1( ... S_m( x ) ... ) is registered to the theory of datatypes, where |
324 |
|
* tn is the type of n, d indicates the depth of n (the sum of weights of the |
325 |
|
* selectors S_1...S_m), and topLevel is whether n is a top-level term |
326 |
|
* (see d_is_top_level). We refer to n as a "search term". |
327 |
|
* |
328 |
|
* The purpose of this function is to notify this class that symmetry breaking |
329 |
|
* lemmas should be instantiated for n. Any symmetry breaking lemmas that |
330 |
|
* are active for n (see description of addSymBreakLemmasFor) are added to |
331 |
|
* lemmas in this call. |
332 |
|
*/ |
333 |
|
void registerSearchTerm(TypeNode tn, unsigned d, Node n, bool topLevel); |
334 |
|
/** Register search value |
335 |
|
* |
336 |
|
* This function is called when a selector chain n has been assigned a model |
337 |
|
* value nv. This function calls itself recursively so that extensions of the |
338 |
|
* selector chain n are registered with all the subterms of nv. For example, |
339 |
|
* if we call this function with: |
340 |
|
* n = x, nv = +( 1(), x() ) |
341 |
|
* we make recursive calls with: |
342 |
|
* n = x.1, nv = 1() and n = x.2, nv = x() |
343 |
|
* |
344 |
|
* a : the anchor of n, |
345 |
|
* d : the depth of n. |
346 |
|
* |
347 |
|
* This function determines if the value nv is equivalent via rewriting to |
348 |
|
* any previously registered search values for anchor a. If so, we construct |
349 |
|
* a symmetry breaking lemma template and register it in d_cache[a]. For |
350 |
|
* example, for grammar: |
351 |
|
* A -> A+A | x | 1 | 0 |
352 |
|
* Registering search value d -> x followed by d -> +( x, 0 ) results in the |
353 |
|
* construction of the symmetry breaking lemma template: |
354 |
|
* ~is_+( z ) V ~is_x( z.1 ) V ~is_0( z.2 ) |
355 |
|
* which is stored in d_cache[a].d_sbLemmas. This lemma is instantiated with |
356 |
|
* z -> t for all terms t of appropriate depth, including d. |
357 |
|
* This function strengthens blocking clauses using generalization techniques |
358 |
|
* described in Reynolds et al SYNT 2017. |
359 |
|
* |
360 |
|
* The return value of this function is an abstraction of model assignment |
361 |
|
* of nv to n, or null if we wish to exclude the model assignment nv to n. |
362 |
|
* The return value of this method is different from nv itself, e.g. if it |
363 |
|
* contains occurrences of the "any constant" constructor. For example, if |
364 |
|
* nv is C_+( C_x(), C_{any_constant}( 5 ) ), then the return value of this |
365 |
|
* function will either be null, or C_+( C_x(), C_{any_constant}( n.1.0 ) ), |
366 |
|
* where n.1.0 is the appropriate selector chain applied to n. We build this |
367 |
|
* abstraction since the semantics of C_{any_constant} is "any constant" and |
368 |
|
* not "some constant". Thus, we should consider the subterm |
369 |
|
* C_{any_constant}( 5 ) above to be an unconstrained variable (as represented |
370 |
|
* by a selector chain), instead of the concrete value 5. |
371 |
|
* |
372 |
|
* The flag isVarAgnostic is whether "a" is a variable agnostic enumerator. If |
373 |
|
* this is the case, we restrict symmetry breaking to subterms of n on its |
374 |
|
* leftmost subchain. For example, consider the grammar: |
375 |
|
* A -> B=B |
376 |
|
* B -> B+B | x | y | 0 |
377 |
|
* Say we are registering the search value x = y+x. Notice that this value is |
378 |
|
* ordered. If a were a variable-agnostic enumerator of type A in this |
379 |
|
* case, we would only register x = y+x and x, and not y+x or y, since the |
380 |
|
* latter two terms are not leftmost subterms in this value. If we did on the |
381 |
|
* other hand register y+x, we would be prevented from solutions like x+y = 0 |
382 |
|
* later, since x+y is equivalent to (the already registered value) y+x. |
383 |
|
* |
384 |
|
* If doSym is false, we are not performing symmetry breaking on n. This flag |
385 |
|
* is set to false on branches of n that are not leftmost. |
386 |
|
*/ |
387 |
|
Node registerSearchValue(Node a, |
388 |
|
Node n, |
389 |
|
Node nv, |
390 |
|
unsigned d, |
391 |
|
bool isVarAgnostic, |
392 |
|
bool doSym); |
393 |
|
/** Register symmetry breaking lemma |
394 |
|
* |
395 |
|
* This function adds the symmetry breaking lemma template lem for terms of |
396 |
|
* type tn with anchor a. This is added to d_cache[a].d_sbLemmas. Notice that |
397 |
|
* we use lem as a template with free variable x, e.g. our template is: |
398 |
|
* (lambda ((x tn)) lem) |
399 |
|
* where x = getFreeVar( tn ). For all search terms t of the appropriate |
400 |
|
* depth, we send the lemma lem{ x -> t } via the inference manager. |
401 |
|
* |
402 |
|
* The argument sz indicates the size of terms that the lemma applies to, e.g. |
403 |
|
* ~is_+( z ) has size 1 |
404 |
|
* ~is_+( z ) V ~is_x( z.1 ) V ~is_0( z.2 ) has size 1 |
405 |
|
* ~is_+( z ) V ~is_+( z.1 ) has size 2 |
406 |
|
* This is equivalent to sum of weights of constructors corresponding to each |
407 |
|
* tester, e.g. above + has weight 1, and x and 0 have weight 0. |
408 |
|
*/ |
409 |
|
void registerSymBreakLemma(TypeNode tn, Node lem, unsigned sz, Node a); |
410 |
|
/** Register symmetry breaking lemma for value |
411 |
|
* |
412 |
|
* This function adds a symmetry breaking lemma template for selector chains |
413 |
|
* with anchor a, that effectively states that val should never be a subterm |
414 |
|
* of any value for a. |
415 |
|
* |
416 |
|
* et : an "invariance test" (see sygus/sygus_invariance.h) which states a |
417 |
|
* criterion that val meets, which is the reason for its exclusion. This is |
418 |
|
* used for generalizing the symmetry breaking lemma template. |
419 |
|
* valr : if non-null, this states a value that should *not* be excluded by |
420 |
|
* the symmetry breaking lemma template, which is a restriction to the above |
421 |
|
* generalization. |
422 |
|
* |
423 |
|
* This function may add instances of the symmetry breaking template for |
424 |
|
* existing search terms, which are sent via the inference manager. |
425 |
|
*/ |
426 |
|
void registerSymBreakLemmaForValue(Node a, |
427 |
|
Node val, |
428 |
|
quantifiers::SygusInvarianceTest& et, |
429 |
|
Node valr, |
430 |
|
std::map<TypeNode, int>& var_count); |
431 |
|
/** Add symmetry breaking lemmas for term |
432 |
|
* |
433 |
|
* Sends all active symmetry breaking lemmas for selector chain t via the |
434 |
|
* inference manager. A symmetry breaking lemma L is active for t based on |
435 |
|
* three factors: |
436 |
|
* (1) the current search size sz(a) for its anchor a, |
437 |
|
* (2) the depth d of term t (see d_term_to_depth), |
438 |
|
* (3) the size sz(L) of the symmetry breaking lemma L. |
439 |
|
* In particular, L is active if sz(L) <= sz(a) - d. In other words, a |
440 |
|
* symmetry breaking lemma is active if it is intended to block terms of |
441 |
|
* size sz(L), and the maximum size that t can take in the current search, |
442 |
|
* sz(a)-d, is greater than or equal to this value. |
443 |
|
* |
444 |
|
* tn : the type of term t, |
445 |
|
* a : the anchor of term t, |
446 |
|
* d : the depth of term t. |
447 |
|
*/ |
448 |
|
void addSymBreakLemmasFor(TypeNode tn, TNode t, unsigned d, Node a); |
449 |
|
/** calls the above function where a is the anchor t */ |
450 |
|
void addSymBreakLemmasFor(TypeNode tn, TNode t, unsigned d); |
451 |
|
//------------------------end dynamic symmetry breaking |
452 |
|
|
453 |
|
/** Get relevancy condition |
454 |
|
* |
455 |
|
* This returns (the negation of) a predicate that holds in the contexts in |
456 |
|
* which the selector chain n is specified. For example, the negation of the |
457 |
|
* relevancy condition for sel_{C2,1}( sel_{C1,1}( d ) ) is |
458 |
|
* ~( is-C1( d ) ^ is-C2( sel_{C1,1}( d ) ) ) |
459 |
|
* If shared selectors are enabled, this is a conjunction of disjunctions, |
460 |
|
* since shared selectors may apply to multiple constructors. |
461 |
|
*/ |
462 |
|
Node getRelevancyCondition( Node n ); |
463 |
|
/** Cache of the above function */ |
464 |
|
std::map<Node, Node> d_rlv_cond; |
465 |
|
|
466 |
|
//------------------------static symmetry breaking |
467 |
|
/** Get simple symmetry breakind predicate |
468 |
|
* |
469 |
|
* This function returns the "static" symmetry breaking lemma template for |
470 |
|
* terms with type tn and constructor index tindex, for the given depth. This |
471 |
|
* includes inferences about size with depth=0. Given grammar: |
472 |
|
* A -> ite( B, A, A ) | A+A | x | 1 | 0 |
473 |
|
* B -> A = A |
474 |
|
* Examples of static symmetry breaking lemma templates are: |
475 |
|
* for +, depth 0: size(z)=size(z.1)+size(z.2)+1 |
476 |
|
* for +, depth 1: ~is-0( z.1 ) ^ ~is-0( z.2 ) ^ F |
477 |
|
* where F ensures the constructor of z.1 is less than that of z.2 based |
478 |
|
* on some ordering. |
479 |
|
* for ite, depth 1: z.2 != z.3 |
480 |
|
* These templates can be thought of as "hard-coded" cases of dynamic symmetry |
481 |
|
* breaking lemma templates. Notice that the above lemma templates are in |
482 |
|
* terms of getFreeVar( tn ), hence only one is created per |
483 |
|
* (constructor, depth). A static symmetry break lemma template F[z] for |
484 |
|
* constructor C are included in lemmas of the form: |
485 |
|
* is-C( t ) => F[t] |
486 |
|
* where t is a search term, see registerSearchTerm for definition of search |
487 |
|
* term. |
488 |
|
* |
489 |
|
* usingSymCons: whether we are using symbolic constructors for subterms in |
490 |
|
* the type tn, |
491 |
|
* isVarAgnostic: whether the terms we are enumerating are agnostic to |
492 |
|
* variables. |
493 |
|
* |
494 |
|
* The latter two options may affect the form of the predicate we construct. |
495 |
|
*/ |
496 |
|
Node getSimpleSymBreakPred(Node e, |
497 |
|
TypeNode tn, |
498 |
|
int tindex, |
499 |
|
unsigned depth, |
500 |
|
bool usingSymCons, |
501 |
|
bool isVarAgnostic); |
502 |
|
/** Cache of the above function */ |
503 |
|
std::map<Node, |
504 |
|
std::map<TypeNode, |
505 |
|
std::map<int, std::map<bool, std::map<unsigned, Node>>>>> |
506 |
|
d_simple_sb_pred; |
507 |
|
/** |
508 |
|
* For each search term, this stores the maximum depth for which we have added |
509 |
|
* a static symmetry breaking lemma. |
510 |
|
* |
511 |
|
* This should be user context-dependent if sygus is updated to work in |
512 |
|
* incremental mode. |
513 |
|
*/ |
514 |
|
std::unordered_map<Node, unsigned> d_simple_proc; |
515 |
|
//------------------------end static symmetry breaking |
516 |
|
|
517 |
|
/** Get the canonical free variable for type tn */ |
518 |
|
TNode getFreeVar( TypeNode tn ); |
519 |
|
/** get term order predicate |
520 |
|
* |
521 |
|
* Assuming that n1 and n2 are children of a commutative operator, this |
522 |
|
* returns a symmetry breaking predicate that can be instantiated for n1 and |
523 |
|
* n2 while preserving satisfiability. By default, this is the predicate |
524 |
|
* ( DT_SIZE n1 ) >= ( DT_SIZE n2 ) |
525 |
|
*/ |
526 |
|
Node getTermOrderPredicate( Node n1, Node n2 ); |
527 |
|
|
528 |
|
private: |
529 |
|
/** |
530 |
|
* Map from registered variables to whether they are a sygus enumerator. |
531 |
|
* |
532 |
|
* This should be user context-dependent if sygus is updated to work in |
533 |
|
* incremental mode. |
534 |
|
*/ |
535 |
|
std::map<Node, bool> d_register_st; |
536 |
|
//----------------------search size information |
537 |
|
/** |
538 |
|
* Checks whether e is a sygus enumerator, that is, a term for which this |
539 |
|
* class will track size for. |
540 |
|
* |
541 |
|
* We associate each sygus enumerator e with a "measure term", which is used |
542 |
|
* for bounding the size of terms for the models of e. The measure term for a |
543 |
|
* sygus enumerator may be e itself (if e has an active guard), or an |
544 |
|
* arbitrary sygus variable otherwise. A measure term m is one for which our |
545 |
|
* decision strategy decides on literals of the form (DT_SYGUS_BOUND m n). |
546 |
|
* |
547 |
|
* After determining the measure term m for e, if applicable, we initialize |
548 |
|
* SygusSizeDecisionStrategy for m below. This may result in lemmas sent via |
549 |
|
* the inference manager. |
550 |
|
*/ |
551 |
|
void registerSizeTerm(Node e); |
552 |
|
/** A decision strategy for each measure term allocated by this class */ |
553 |
510 |
class SygusSizeDecisionStrategy : public DecisionStrategyFmf |
554 |
|
{ |
555 |
|
public: |
556 |
|
SygusSizeDecisionStrategy(InferenceManager& im, Node t, TheoryState& s); |
557 |
|
/** the measure term */ |
558 |
|
Node d_this; |
559 |
|
/** |
560 |
|
* For each size n, an explanation for why this measure term has size at |
561 |
|
* most n. This is typically the literal (DT_SYGUS_BOUND m n), which |
562 |
|
* we call the (n^th) "fairness literal" for m. |
563 |
|
*/ |
564 |
|
std::map< unsigned, Node > d_search_size_exp; |
565 |
|
/** |
566 |
|
* For each size, whether we have called SygusExtension::notifySearchSize. |
567 |
|
*/ |
568 |
|
std::map< unsigned, bool > d_search_size; |
569 |
|
/** |
570 |
|
* The current search size. This corresponds to the number of times |
571 |
|
* incrementCurrentSearchSize has been called for this measure term. |
572 |
|
*/ |
573 |
|
unsigned d_curr_search_size; |
574 |
|
/** the list of all enumerators whose measure term is this */ |
575 |
|
std::vector< Node > d_anchors; |
576 |
|
/** get or make the measure value |
577 |
|
* |
578 |
|
* The measure value is an integer variable v that is a (symbolic) integer |
579 |
|
* value that is constrained to be less than or equal to the current search |
580 |
|
* size. For example, if we are using the fairness strategy |
581 |
|
* SygusFairMode::DT_SIZE (see options/datatype_options.h), then we |
582 |
|
* constrain: (DT_SYGUS_BOUND m n) <=> (v <= n) for all asserted fairness |
583 |
|
* literals. Then, if we are enforcing fairness based on the maximum size, |
584 |
|
* we assert: (DT_SIZE e) <= v for all enumerators e. |
585 |
|
*/ |
586 |
|
Node getOrMkMeasureValue(); |
587 |
|
/** get or make the active measure value |
588 |
|
* |
589 |
|
* The active measure value av is an integer variable that corresponds to |
590 |
|
* the (symbolic) value of the sum of enumerators that are yet to be |
591 |
|
* registered. This is to enforce the "sum of measures" strategy. For |
592 |
|
* example, if we are using the fairness strategy SygusFairMode::DT_SIZE, |
593 |
|
* then initially av is equal to the measure value v, and the constraints |
594 |
|
* (DT_SYGUS_BOUND m n) <=> (v <= n) |
595 |
|
* are added as before. When an enumerator e is registered, we add the |
596 |
|
* lemma: |
597 |
|
* av = (DT_SIZE e) + av' |
598 |
|
* and update the active measure value to av'. This ensures that the sum |
599 |
|
* of sizes of active enumerators is at most n. |
600 |
|
* |
601 |
|
* If the flag mkNew is set to true, then we return a fresh variable and |
602 |
|
* update the active measure value. |
603 |
|
*/ |
604 |
|
Node getOrMkActiveMeasureValue(bool mkNew = false); |
605 |
|
/** Returns the s^th fairness literal for this measure term. */ |
606 |
|
Node mkLiteral(unsigned s) override; |
607 |
|
/** identify */ |
608 |
858085 |
std::string identify() const override |
609 |
|
{ |
610 |
858085 |
return std::string("sygus_enum_size"); |
611 |
|
} |
612 |
|
|
613 |
|
private: |
614 |
|
/** The inference manager we are using */ |
615 |
|
InferenceManager& d_im; |
616 |
|
/** the measure value */ |
617 |
|
Node d_measure_value; |
618 |
|
/** the sygus measure value */ |
619 |
|
Node d_measure_value_active; |
620 |
|
}; |
621 |
|
/** the above information for each registered measure term */ |
622 |
|
std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>> d_szinfo; |
623 |
|
/** map from enumerators (anchors) to their associated measure term */ |
624 |
|
std::map< Node, Node > d_anchor_to_measure_term; |
625 |
|
/** map from enumerators (anchors) to their active guard*/ |
626 |
|
std::map< Node, Node > d_anchor_to_active_guard; |
627 |
|
/** map from enumerators (anchors) to a decision stratregy for that guard */ |
628 |
|
std::map<Node, std::unique_ptr<DecisionStrategy>> d_anchor_to_ag_strategy; |
629 |
|
/** generic measure term |
630 |
|
* |
631 |
|
* This is a global term that is used as the measure term for all sygus |
632 |
|
* enumerators that do not have active guards. This class enforces that |
633 |
|
* all enumerators have size at most n, where n is the minimal integer |
634 |
|
* such that (DT_SYGUS_BOUND d_generic_measure_term n) is asserted. |
635 |
|
*/ |
636 |
|
Node d_generic_measure_term; |
637 |
|
/** |
638 |
|
* This increments the current search size for measure term m. This may |
639 |
|
* cause lemmas to be added to lemmas based on the fact that symmetry |
640 |
|
* breaking lemmas are now relevant for new search terms, see discussion |
641 |
|
* of how search size affects which lemmas are relevant above |
642 |
|
* addSymBreakLemmasFor. |
643 |
|
*/ |
644 |
|
void incrementCurrentSearchSize(TNode m); |
645 |
|
/** |
646 |
|
* Notify this class that we are currently searching for terms of size at |
647 |
|
* most s as model values for measure term m. Literal exp corresponds to the |
648 |
|
* explanation of why the measure term has size at most n. This calls |
649 |
|
* incrementSearchSize above, until the total number of times we have called |
650 |
|
* incrementSearchSize so far is at least s. |
651 |
|
*/ |
652 |
|
void notifySearchSize(TNode m, uint64_t s, Node exp); |
653 |
|
/** Allocates a SygusSizeDecisionStrategy object in d_szinfo. */ |
654 |
|
void registerMeasureTerm( Node m ); |
655 |
|
/** |
656 |
|
* Return the current search size for arbitrary term n. This is the current |
657 |
|
* search size of the anchor of n. |
658 |
|
*/ |
659 |
|
unsigned getSearchSizeFor( Node n ); |
660 |
|
/** return the current search size for enumerator (anchor) e */ |
661 |
|
unsigned getSearchSizeForAnchor(Node e); |
662 |
|
/** Get the current search size for measure term m in this SAT context. */ |
663 |
|
unsigned getSearchSizeForMeasureTerm(Node m); |
664 |
|
/** get current template |
665 |
|
* |
666 |
|
* For debugging. This returns a term that corresponds to the current |
667 |
|
* inferred shape of n. For example, if the testers |
668 |
|
* is-C1( n ) and is-C2( n.1 ) |
669 |
|
* have been asserted where C1 and C2 are binary constructors, then this |
670 |
|
* method may return a term of the form: |
671 |
|
* C1( C2( x1, x2 ), x3 ) |
672 |
|
* for fresh variables x1, x2, x3. The map var_count maintains the variable |
673 |
|
* count for generating these fresh variables. |
674 |
|
*/ |
675 |
|
Node getCurrentTemplate( Node n, std::map< TypeNode, int >& var_count ); |
676 |
|
//----------------------end search size information |
677 |
|
/** check value |
678 |
|
* |
679 |
|
* This is called when we have a model assignment vn for n, where n is |
680 |
|
* a selector chain applied to an enumerator (a search term). This function |
681 |
|
* ensures that testers have been asserted for each subterm of vn. This is |
682 |
|
* critical for ensuring that the proper steps have been taken by this class |
683 |
|
* regarding whether or not vn is a legal value for n (not greater than the |
684 |
|
* current search size and not a value that can be blocked by symmetry |
685 |
|
* breaking). |
686 |
|
* |
687 |
|
* For example, if vn = +( x(), x() ), then we ensure that the testers |
688 |
|
* is-+( n ), is-x( n.1 ), is-x( n.2 ) |
689 |
|
* have been asserted to this class. If a tester is not asserted for some |
690 |
|
* relevant selector chain S( n ) of n, then we add a lemma L for that |
691 |
|
* selector chain to lemmas, where L is the "splitting lemma" for S( n ), that |
692 |
|
* states that the top symbol of S( n ) must be one of the constructors of |
693 |
|
* its type. |
694 |
|
* |
695 |
|
* Notice that this function is a sanity check. Typically, it should be the |
696 |
|
* case that testers are asserted for all subterms of vn, and hence this |
697 |
|
* method should not ever add anything to lemmas. However, due to its |
698 |
|
* importance, we check this regardless. |
699 |
|
*/ |
700 |
|
bool checkValue(Node n, TNode vn, int ind); |
701 |
|
/** |
702 |
|
* Get the current SAT status of the guard g. |
703 |
|
* In particular, this returns 1 if g is asserted true, -1 if it is asserted |
704 |
|
* false, and 0 if it is not asserted. |
705 |
|
*/ |
706 |
|
int getGuardStatus( Node g ); |
707 |
|
}; |
708 |
|
|
709 |
|
} |
710 |
|
} |
711 |
|
} // namespace cvc5 |
712 |
|
|
713 |
|
#endif |
714 |
|
|