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