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