1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Aina Niemetz |
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 |
|
* Cegis core connective module. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H |
19 |
|
#define CVC5__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H |
20 |
|
|
21 |
|
#include <unordered_set> |
22 |
|
|
23 |
|
#include "expr/node.h" |
24 |
|
#include "expr/node_trie.h" |
25 |
|
#include "theory/evaluator.h" |
26 |
|
#include "theory/quantifiers/sygus/cegis.h" |
27 |
|
#include "util/result.h" |
28 |
|
|
29 |
|
namespace cvc5 { |
30 |
|
|
31 |
|
class SmtEngine; |
32 |
|
|
33 |
|
namespace theory { |
34 |
|
namespace quantifiers { |
35 |
|
|
36 |
|
/** |
37 |
|
* A trie that stores data at undetermined depth. Storing data at |
38 |
|
* undetermined depth is in contrast to the NodeTrie (expr/node_trie.h), which |
39 |
|
* assumes all data is stored at a fixed depth. |
40 |
|
* |
41 |
|
* Since data can be stored at any depth, we require both a d_children field |
42 |
|
* and a d_data field. |
43 |
|
*/ |
44 |
4640 |
class VariadicTrie |
45 |
|
{ |
46 |
|
public: |
47 |
|
/** the children of this node */ |
48 |
|
std::map<Node, VariadicTrie> d_children; |
49 |
|
/** the data at this node */ |
50 |
|
Node d_data; |
51 |
|
/** |
52 |
|
* Add data with identifier n indexed by i, return true if data is not already |
53 |
|
* stored at the node indexed by i. |
54 |
|
*/ |
55 |
|
bool add(Node n, const std::vector<Node>& i); |
56 |
|
/** Is there any data in this trie that is indexed by any subset of is? */ |
57 |
|
bool hasSubset(const std::vector<Node>& is) const; |
58 |
|
}; |
59 |
|
|
60 |
|
/** CegisCoreConnective |
61 |
|
* |
62 |
|
* A sygus module that is specialized in handling conjectures of the form: |
63 |
|
* exists P. forall x. (A[x] => C(x)) ^ (C(x) => B(x)) |
64 |
|
* That is, conjectures with a pre/post condition but no inductive relation |
65 |
|
* or other constraints. Additionally, we may have that the above conjecture |
66 |
|
* has a side condition SC, which requires that exists x. SC[x]^C(x) is |
67 |
|
* satisfiable. |
68 |
|
* |
69 |
|
* Two examples of this kind of sygus conjecture are abduction and |
70 |
|
* interpolation. |
71 |
|
* |
72 |
|
* This module implements a specific algorithm for constructing solutions |
73 |
|
* to this conjecture based on Boolean connectives and unsat cores, described |
74 |
|
* in following. We give two variants of the algorithm, both implemented as |
75 |
|
* special cases of this class. Below, let: |
76 |
|
* |
77 |
|
* pool(A) be a set of literals { c_1, ..., c_n } s.t. c_i => B for i=1,...,n, |
78 |
|
* pts(A) : a set of points { v | A[v] is true }, |
79 |
|
* pool(B) : a set of literals { d_1, ..., d_m } s.t. A => d_i for i=1,...,m, |
80 |
|
* pts(B) : a set of points { v | ~B[v] is true }, |
81 |
|
* cores(B) : a set of sets of literals { U_1, ..., U_p } s.t. for i=1,...,p: |
82 |
|
* - U_i is a subset of pool(B), |
83 |
|
* - A ^ U_i is unsat. |
84 |
|
* We construct pool(A)/pool(B) using enumerative SyGuS, discarding the literals |
85 |
|
* that do not match the criteria. |
86 |
|
* |
87 |
|
* Variant #1 (Interpolation) |
88 |
|
* |
89 |
|
* Let the synthesis conjecture be of the form |
90 |
|
* exists C. forall x. A[x] => C[x] ^ C[x] => B[x] |
91 |
|
* |
92 |
|
* The high level idea is we construct solutions for C of the form |
93 |
|
* c_1 OR ... OR c_n where c_i => B for each i=1,...,n, or |
94 |
|
* d_1 AND ... AND d_m where A => d_i for each i=1,...,m. |
95 |
|
* |
96 |
|
* while(true){ |
97 |
|
* Let e_i = next_sygus_enum(); |
98 |
|
* // check if e_i should be added to pool(B) |
99 |
|
* if e_i[v] is true for all v in pts(A) |
100 |
|
* if A => e_i |
101 |
|
* pool(B) += e_i; |
102 |
|
* else |
103 |
|
* pts(A) += { v } where { x -> v } is a model for A ^ ~e_i; |
104 |
|
* // try to construct a solution based on the pool |
105 |
|
* Let D = {}. |
106 |
|
* while |
107 |
|
* D[v] is true for some v in pts(B), and |
108 |
|
* d'[v] is false for some d' in pool(B) |
109 |
|
* { |
110 |
|
* D += { d' } |
111 |
|
* if D is false for all v in pts(B) |
112 |
|
* if D => B |
113 |
|
* return AND_{d in D}( d ) |
114 |
|
* else |
115 |
|
* pts(B) += { v } where { x -> v } is a model for D ^ ~B |
116 |
|
* } |
117 |
|
* |
118 |
|
* // analogous for the other direction |
119 |
|
* } |
120 |
|
* |
121 |
|
* |
122 |
|
* Variant #2 (Abduction) |
123 |
|
* |
124 |
|
* Let the synthesis conjecture be of the form exists C. forall x. C[x] => B[x] |
125 |
|
* such that S[x] ^ C[x] is satisfiable. We refer to S as the side condition |
126 |
|
* for this conjecture. Notice that A in this variant is false, hence the |
127 |
|
* algorithm below is modified accordingly. |
128 |
|
* |
129 |
|
* The high level idea is we construct solutions for C of the form |
130 |
|
* d_1 AND ... AND d_n |
131 |
|
* where the above conjunction is weakened based on only including conjuncts |
132 |
|
* that are in the unsat core of d_1 AND ... AND d_n => B. |
133 |
|
* |
134 |
|
* while(true){ |
135 |
|
* Let e_i = next_sygus_enum(); |
136 |
|
* // add e_i to the pool |
137 |
|
* pool(B) += e_i; |
138 |
|
* // try to construct a solution based on the pool |
139 |
|
* Let D = {}. |
140 |
|
* while |
141 |
|
* D[v] is true for some v in pts(B), and |
142 |
|
* d'[v] is false for some d' in pool(B) and |
143 |
|
* no element of cores(B) is a subset of D ++ { d' } |
144 |
|
* { |
145 |
|
* D += { d' } |
146 |
|
* if D is false for all v in pts(B) |
147 |
|
* if (S ^ D) => B |
148 |
|
* Let U be a subset of D such that S ^ U ^ ~B is unsat. |
149 |
|
* if S ^ U is unsat |
150 |
|
* Let W be a subset of D such that S ^ W is unsat. |
151 |
|
* cores(B) += W |
152 |
|
* remove some d'' in W from D |
153 |
|
* else |
154 |
|
* return u_1 AND ... AND u_m where U = { u_1, ..., u_m } |
155 |
|
* else |
156 |
|
* pts(B) += { v } where { x -> v } is a model for D ^ ~B |
157 |
|
* } |
158 |
|
* } |
159 |
|
*/ |
160 |
|
class CegisCoreConnective : public Cegis |
161 |
|
{ |
162 |
|
public: |
163 |
|
CegisCoreConnective(QuantifiersInferenceManager& qim, |
164 |
|
TermDbSygus* tds, |
165 |
|
SynthConjecture* p); |
166 |
2302 |
~CegisCoreConnective() {} |
167 |
|
/** |
168 |
|
* Return whether this module has the possibility to construct solutions. This |
169 |
|
* is true if this module has been initialized, and the shape of the |
170 |
|
* conjecture allows us to use the core connective algorithm. |
171 |
|
*/ |
172 |
|
bool isActive() const; |
173 |
|
|
174 |
|
protected: |
175 |
|
/** do cegis-implementation-specific initialization for this class */ |
176 |
|
bool processInitialize(Node conj, |
177 |
|
Node n, |
178 |
|
const std::vector<Node>& candidates) override; |
179 |
|
/** do cegis-implementation-specific post-processing for construct candidate |
180 |
|
* |
181 |
|
* satisfiedRl is whether all refinement lemmas are satisfied under the |
182 |
|
* substitution { enums -> enum_values }. |
183 |
|
*/ |
184 |
|
bool processConstructCandidates(const std::vector<Node>& enums, |
185 |
|
const std::vector<Node>& enum_values, |
186 |
|
const std::vector<Node>& candidates, |
187 |
|
std::vector<Node>& candidate_values, |
188 |
|
bool satisfiedRl) override; |
189 |
|
|
190 |
|
/** construct solution |
191 |
|
* |
192 |
|
* This function is called when candidates -> candidate_values is the current |
193 |
|
* candidate solution for the synthesis conjecture. |
194 |
|
* |
195 |
|
* If this function returns true, then this class adds to solv the |
196 |
|
* a candidate solution for candidates. |
197 |
|
*/ |
198 |
|
bool constructSolution(const std::vector<Node>& candidates, |
199 |
|
const std::vector<Node>& candidate_values, |
200 |
|
std::vector<Node>& solv); |
201 |
|
|
202 |
|
private: |
203 |
|
/** common constants */ |
204 |
|
Node d_true; |
205 |
|
Node d_false; |
206 |
|
/** The first-order datatype variable for the function-to-synthesize */ |
207 |
|
TNode d_candidate; |
208 |
|
/** |
209 |
|
* Information about the pre and post conditions of the synthesis conjecture. |
210 |
|
* This maintains all information needed for producing solutions relative to |
211 |
|
* one direction of the synthesis conjecture. In other words, this component |
212 |
|
* may be focused on finding a C1 ... Cn such that A => C1 V ... V Cn |
213 |
|
* or alteratively C1 ^ ... ^ Cn such that C1 ^ ... ^ Cn => B. |
214 |
|
*/ |
215 |
2302 |
class Component |
216 |
|
{ |
217 |
|
public: |
218 |
2302 |
Component() : d_numFalseCores(0), d_numRefPoints(0) {} |
219 |
|
/** initialize |
220 |
|
* |
221 |
|
* This initializes this component with pre/post condition given by n |
222 |
|
* and sygus constructor c. |
223 |
|
*/ |
224 |
|
void initialize(Node n, Node c); |
225 |
|
/** get the formula n that we initialized this with */ |
226 |
92 |
Node getFormula() const { return d_this; } |
227 |
|
/** Is this component active? */ |
228 |
284 |
bool isActive() const { return !d_scons.isNull(); } |
229 |
|
/** Add term n to pool whose sygus analog is s */ |
230 |
|
void addToPool(Node n, Node s); |
231 |
|
/** Add a refinement point to this component */ |
232 |
|
void addRefinementPt(Node id, const std::vector<Node>& pt); |
233 |
|
/** Add a false case to this component */ |
234 |
|
void addFalseCore(Node id, const std::vector<Node>& u); |
235 |
|
/** |
236 |
|
* Selects a node from passerts that evaluates to false on point mv if one |
237 |
|
* exists, or otherwise returns false. |
238 |
|
* The argument mvId is an identifier used for indexing the point mv. |
239 |
|
* The argument asserts stores the current candidate solution (set D in |
240 |
|
* Variant #2 described above). If the method returns true, it updates |
241 |
|
* an (the node version of asserts) to be the conjunction of the nodes |
242 |
|
* in asserts. |
243 |
|
* |
244 |
|
* If true is returned, it is removed from passerts. |
245 |
|
*/ |
246 |
|
bool addToAsserts(CegisCoreConnective* p, |
247 |
|
std::vector<Node>& passerts, |
248 |
|
const std::vector<Node>& mvs, |
249 |
|
Node mvId, |
250 |
|
std::vector<Node>& asserts, |
251 |
|
Node& an); |
252 |
|
|
253 |
|
/** |
254 |
|
* Get a refinement point that n evalutes to true on, taken from the |
255 |
|
* d_refinementPt trie, and store it in ss. The set visited is the set |
256 |
|
* of leaf nodes (reference by their data) that we have already processed |
257 |
|
* and should be ignored. |
258 |
|
*/ |
259 |
|
Node getRefinementPt(CegisCoreConnective* p, |
260 |
|
Node n, |
261 |
|
std::unordered_set<Node>& visited, |
262 |
|
std::vector<Node>& ss); |
263 |
|
/** Get term pool, i.e. pool(A)/pool(B) in the algorithms above */ |
264 |
|
void getTermPool(std::vector<Node>& passerts) const; |
265 |
|
/** |
266 |
|
* Get the sygus solution corresponding to the Boolean connective for |
267 |
|
* this component applied to conj. In particular, this returns a |
268 |
|
* right-associative chain of applications of sygus constructor d_scons |
269 |
|
* to the sygus analog of formulas in conj. |
270 |
|
*/ |
271 |
|
Node getSygusSolution(std::vector<Node>& conjs) const; |
272 |
|
/** debug print summary (for debugging) */ |
273 |
|
void debugPrintSummary(std::ostream& os) const; |
274 |
|
|
275 |
|
private: |
276 |
|
/** The original formula for the pre/post condition A/B. */ |
277 |
|
Node d_this; |
278 |
|
/** |
279 |
|
* The sygus constructor for constructing solutions based on the core |
280 |
|
* connective algorithm. This is a sygus datatype constructor that |
281 |
|
* encodes applications of AND or OR. |
282 |
|
*/ |
283 |
|
Node d_scons; |
284 |
|
/** This is pool(A)/pool(B) in the algorithms above */ |
285 |
|
std::vector<Node> d_cpool; |
286 |
|
/** |
287 |
|
* A map from the formulas in the above vector to their sygus analog. |
288 |
|
*/ |
289 |
|
std::map<Node, Node> d_cpoolToSol; |
290 |
|
/** |
291 |
|
* An index of list of predicates such that each list ( P1, ..., Pn ) |
292 |
|
* indexed by this trie is such that P1 ^ ... ^ Pn ^ S is unsatisfiable, |
293 |
|
* where S is the side condition of our synthesis conjecture. We call this |
294 |
|
* a "false core". This set is "cores(B)" in Variant #2 above. |
295 |
|
*/ |
296 |
|
VariadicTrie d_falseCores; |
297 |
|
/** |
298 |
|
* The number of points that have been added to the above trie, for |
299 |
|
* debugging. |
300 |
|
*/ |
301 |
|
unsigned d_numFalseCores; |
302 |
|
/** |
303 |
|
* An index of the points that satisfy d_this. |
304 |
|
*/ |
305 |
|
NodeTrie d_refinementPt; |
306 |
|
/** |
307 |
|
* The number of points that have been added to the above trie, for |
308 |
|
* debugging. |
309 |
|
*/ |
310 |
|
unsigned d_numRefPoints; |
311 |
|
}; |
312 |
|
/** Above information for the precondition of the synthesis conjecture */ |
313 |
|
Component d_pre; |
314 |
|
/** Above information for the postcondition of the synthesis conjecture */ |
315 |
|
Component d_post; |
316 |
|
/** |
317 |
|
* The free variables that may appear in the pre/post condition, and our |
318 |
|
* pools of predicates. |
319 |
|
*/ |
320 |
|
std::vector<Node> d_vars; |
321 |
|
/** |
322 |
|
* The evaluation term of the form: |
323 |
|
* (DT_SYGUS_EVAL d_candidate d_vars[0]...d_vars[n]) |
324 |
|
* This is used to convert enumerated sygus terms t to their builtin |
325 |
|
* equivalent via rewriting d_eterm * { d_candidate -> t }. |
326 |
|
*/ |
327 |
|
Node d_eterm; |
328 |
|
/** |
329 |
|
* The side condition of the conjecture. If this is non-null, then |
330 |
|
* this node is a formula such that (builtin) solutions t' are such that |
331 |
|
* t' ^ d_sc is satisfiable. Notice that the free variables of d_sc are |
332 |
|
* a subset of d_vars. |
333 |
|
*/ |
334 |
|
Node d_sc; |
335 |
|
//-----------------------------------for SMT engine calls |
336 |
|
/** |
337 |
|
* Assuming smt has just been called to check-sat and returned "SAT", this |
338 |
|
* method adds the model for d_vars to mvs. |
339 |
|
*/ |
340 |
|
void getModel(SmtEngine& smt, std::vector<Node>& mvs) const; |
341 |
|
/** |
342 |
|
* Assuming smt has just been called to check-sat and returned "UNSAT", this |
343 |
|
* method get the unsat core and adds it to uasserts. |
344 |
|
* |
345 |
|
* The assertions in the argument queryAsserts (which we are not interested |
346 |
|
* in tracking in the unsat core) are excluded from uasserts. |
347 |
|
* If one of the formulas in queryAsserts was in the unsat core, then this |
348 |
|
* method returns true. Otherwise, this method returns false. |
349 |
|
*/ |
350 |
|
bool getUnsatCore(SmtEngine& smt, |
351 |
|
const std::unordered_set<Node>& queryAsserts, |
352 |
|
std::vector<Node>& uasserts) const; |
353 |
|
/** |
354 |
|
* Return the result of checking satisfiability of formula n. |
355 |
|
* If n was satisfiable, then we store the model for d_vars in mvs. |
356 |
|
*/ |
357 |
|
Result checkSat(Node n, std::vector<Node>& mvs) const; |
358 |
|
//-----------------------------------end for SMT engine calls |
359 |
|
//-----------------------------------for evaluation |
360 |
|
/** |
361 |
|
* Return the evaluation of n under the substitution { d_vars -> mvs }. |
362 |
|
* If id is non-null, then id is a unique identifier for mvs, and we cache |
363 |
|
* the result of n for this point. |
364 |
|
*/ |
365 |
|
Node evaluate(Node n, Node id, const std::vector<Node>& mvs); |
366 |
|
/** A cache of the above function */ |
367 |
|
std::unordered_map<Node, std::unordered_map<Node, Node>> d_eval_cache; |
368 |
|
/** The evaluator utility used for the above function */ |
369 |
|
Evaluator d_eval; |
370 |
|
//-----------------------------------end for evaluation |
371 |
|
|
372 |
|
/** Construct solution from pool |
373 |
|
* |
374 |
|
* This is the main body of the core connective algorithm, which attempts |
375 |
|
* to build a solution based on one direction (pre/post) of the synthesis |
376 |
|
* conjecture. |
377 |
|
* |
378 |
|
* It takes as input: |
379 |
|
* - a component ccheck that maintains information regarding the direction |
380 |
|
* we are trying to build a solution for, |
381 |
|
* - the current set of assertions asserts that comprise the current solution |
382 |
|
* we are building, |
383 |
|
* - the current pool passerts of available assertions that we may add to |
384 |
|
* asserts. |
385 |
|
* |
386 |
|
* This implements the while loop in the algorithms above. If this method |
387 |
|
* returns a non-null node, then this is a solution for the given synthesis |
388 |
|
* conjecture. |
389 |
|
*/ |
390 |
|
Node constructSolutionFromPool(Component& ccheck, |
391 |
|
std::vector<Node>& asserts, |
392 |
|
std::vector<Node>& passerts); |
393 |
|
}; |
394 |
|
|
395 |
|
} // namespace quantifiers |
396 |
|
} // namespace theory |
397 |
|
} // namespace cvc5 |
398 |
|
|
399 |
|
#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */ |