Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Abdalrhman Mohamed, Haniel Barbosa
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : : * Class that encapsulates techniques for a single (SyGuS) synthesis
14 : : * conjecture.
15 : : */
16 : :
17 : : #include "cvc5_private.h"
18 : :
19 : : #ifndef CVC5__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
20 : : #define CVC5__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
21 : :
22 : : #include <memory>
23 : :
24 : : #include "smt/env_obj.h"
25 : : #include "theory/quantifiers/expr_miner_manager.h"
26 : : #include "theory/quantifiers/sygus/ce_guided_single_inv.h"
27 : : #include "theory/quantifiers/sygus/cegis.h"
28 : : #include "theory/quantifiers/sygus/cegis_core_connective.h"
29 : : #include "theory/quantifiers/sygus/cegis_unif.h"
30 : : #include "theory/quantifiers/sygus/enum_val_generator.h"
31 : : #include "theory/quantifiers/sygus/example_eval_cache.h"
32 : : #include "theory/quantifiers/sygus/example_infer.h"
33 : : #include "theory/quantifiers/sygus/sygus_process_conj.h"
34 : : #include "theory/quantifiers/sygus/sygus_repair_const.h"
35 : : #include "theory/quantifiers/sygus/sygus_stats.h"
36 : : #include "theory/quantifiers/sygus/synth_verify.h"
37 : : #include "theory/quantifiers/sygus/template_infer.h"
38 : :
39 : : namespace cvc5::internal {
40 : : namespace theory {
41 : : namespace quantifiers {
42 : :
43 : : class EmbeddingConverter;
44 : : class SygusPbe;
45 : : class SygusStatistics;
46 : : class EnumValueManager;
47 : :
48 : : /** a synthesis conjecture
49 : : * This class implements approaches for a synthesis conjecture, given by data
50 : : * member d_quant.
51 : : * This includes both approaches for synthesis in Reynolds et al CAV 2015. It
52 : : * determines which approach and optimizations are applicable to the
53 : : * conjecture, and has interfaces for implementing them.
54 : : */
55 : : class SynthConjecture : protected EnvObj
56 : : {
57 : : public:
58 : : SynthConjecture(Env& env,
59 : : QuantifiersState& qs,
60 : : QuantifiersInferenceManager& qim,
61 : : QuantifiersRegistry& qr,
62 : : TermRegistry& tr,
63 : : SygusStatistics& s);
64 : : ~SynthConjecture();
65 : : /**
66 : : * Presolve, called once at the beginning of every check-sat.
67 : : */
68 : : void presolve();
69 : : /** get original version of conjecture */
70 : 26389 : Node getConjecture() const { return d_quant; }
71 : : /** get deep embedding version of conjecture */
72 : : Node getEmbeddedConjecture() const { return d_embed_quant; }
73 : : //-------------------------------for counterexample-guided check/refine
74 : : /** whether the conjecture is waiting for a call to doCheck below */
75 : : bool needsCheck();
76 : : /** do syntax-guided enumerative check
77 : : *
78 : : * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015.
79 : : *
80 : : * The method returns true if this conjecture is finished trying solutions
81 : : * for the given call to SynthEngine::check.
82 : : *
83 : : * Notice that we make multiple calls to doCheck on one call to
84 : : * SynthEngine::check. For example, if we are using an actively-generated
85 : : * enumerator, one enumerated (abstract) term may correspond to multiple
86 : : * concrete terms t1, ..., tn to check, where we make up to n calls to doCheck
87 : : * when each of t1, ..., tn fails to satisfy the current refinement lemmas.
88 : : */
89 : : bool doCheck();
90 : : //-------------------------------end for counterexample-guided check/refine
91 : : /** get synth solutions
92 : : *
93 : : * This method returns true if this class has a solution available to the
94 : : * conjecture that it was assigned.
95 : : *
96 : : * Let q be the synthesis conjecture assigned to this class.
97 : : * This method adds entries to sol_map[q] that map functions-to-synthesize to
98 : : * their builtin solution, which has the same type. For example, for synthesis
99 : : * conjecture exists f. forall x. f( x )>x, this function will update
100 : : * sol_map[q] to contain the entry:
101 : : * f -> (lambda x. x+1)
102 : : */
103 : : bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
104 : : /** is ground */
105 : : bool isGround() const { return d_innerVars.empty(); }
106 : : /** are we using single invocation techniques */
107 : : bool isSingleInvocation() const;
108 : : /** preprocess notify conjecture
109 : : * This is used as a heuristic for solution reconstruction, so that we
110 : : * remember expressions in the conjecture before preprocessing, since they
111 : : * may be helpful during solution reconstruction (Figure 5 of Reynolds et al
112 : : * CAV 2015)
113 : : */
114 : : void ppNotifyConjecture(Node q);
115 : : /** assign conjecture q to this class */
116 : : void assign(Node q);
117 : : /** has a conjecture been assigned to this class */
118 : 4766 : bool isAssigned() { return !d_embed_quant.isNull(); }
119 : : /**
120 : : * Get model value for term n.
121 : : */
122 : : Node getModelValue(Node n);
123 : :
124 : : /** get utility for static preprocessing and analysis of conjectures */
125 : 1109 : SynthConjectureProcess* getProcess() { return d_ceg_proc.get(); }
126 : : /** get constant repair utility */
127 : 753 : SygusRepairConst* getRepairConst() { return d_sygus_rconst.get(); }
128 : : /** get example inference utility */
129 : 36351 : ExampleInfer* getExampleInfer() { return d_exampleInfer.get(); }
130 : : /** get the example evaluation cache utility for enumerator e */
131 : : ExampleEvalCache* getExampleEvalCache(Node e);
132 : : /** get program by examples module */
133 : : SygusPbe* getPbe() { return d_ceg_pbe.get(); }
134 : : /** get the symmetry breaking predicate for type */
135 : : Node getSymmetryBreakingPredicate(
136 : : Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth);
137 : : /** print out debug information about this conjecture */
138 : : void debugPrint(const char* c);
139 : : /** check side condition
140 : : *
141 : : * This returns false if the solution { d_candidates -> cvals } does not
142 : : * satisfy the side condition of the conjecture maintained by this class,
143 : : * if it exists, and true otherwise.
144 : : */
145 : : bool checkSideCondition(const std::vector<Node>& cvals);
146 : :
147 : : /** get a reference to the statistics of parent */
148 : : SygusStatistics& getSygusStatistics() { return d_stats; };
149 : :
150 : : /** exclude the current solution { enums -> values } due to id */
151 : : void excludeCurrentSolution(const std::vector<Node>& values, InferenceId id);
152 : :
153 : : private:
154 : : /** do refinement
155 : : *
156 : : * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015.
157 : : *
158 : : * This method is run when skModel is corresponds to a counterexample to the
159 : : * last candidate in the doCheck method.
160 : : *
161 : : * This method adds a refinement lemma on the output channel of quantifiers
162 : : * engine. If the refinement lemma is a duplicate, then we manually
163 : : * exclude the current candidate via excludeCurrentSolution. This should
164 : : * only occur when the synthesis conjecture for the current candidate fails
165 : : * to evaluate to false for a given counterexample point, but regardless its
166 : : * negation is satisfiable for the current candidate and that point. This is
167 : : * exclusive to theories with partial functions, e.g. (non-linear) division.
168 : : *
169 : : * This method returns true if a lemma was added on the output channel, and
170 : : * false otherwise.
171 : : */
172 : : bool processCounterexample(const std::vector<Node>& skModel);
173 : : /** Reference to the quantifiers state */
174 : : QuantifiersState& d_qstate;
175 : : /** Reference to the quantifiers inference manager */
176 : : QuantifiersInferenceManager& d_qim;
177 : : /** The quantifiers registry */
178 : : QuantifiersRegistry& d_qreg;
179 : : /** Reference to the term registry */
180 : : TermRegistry& d_treg;
181 : : /** reference to the statistics of parent */
182 : : SygusStatistics& d_stats;
183 : : /** term database sygus of d_qe */
184 : : TermDbSygus* d_tds;
185 : : /** The synthesis verify utility */
186 : : SynthVerify d_verify;
187 : : /**
188 : : * Do we have a solution in this solve context? This flag is reset to false
189 : : * on every call to presolve.
190 : : */
191 : : bool d_hasSolution;
192 : : /** Whether we have computed a solution */
193 : : bool d_computedSolution;
194 : : /** whether we are running expression mining */
195 : : bool d_runExprMiner;
196 : : /**
197 : : * The final solution and status, caches getSynthSolutionsInternal, valid
198 : : * if d_computedSolution is true.
199 : : */
200 : : std::vector<Node> d_sol;
201 : : std::vector<int8_t> d_solStatus;
202 : : /**
203 : : * (SyGuS datatype) values for solutions, which is populated if we have a
204 : : * solution and only if we are not using the single invocation solver.
205 : : */
206 : : std::vector<std::vector<Node>> d_solutionValues;
207 : : /** the decision strategy for the feasible guard */
208 : : std::unique_ptr<DecisionStrategy> d_feasible_strategy;
209 : : /** single invocation utility */
210 : : std::unique_ptr<CegSingleInv> d_ceg_si;
211 : : /** template inference utility */
212 : : std::unique_ptr<SygusTemplateInfer> d_templInfer;
213 : : /** utility for static preprocessing and analysis of conjectures */
214 : : std::unique_ptr<SynthConjectureProcess> d_ceg_proc;
215 : : /** grammar utility */
216 : : std::unique_ptr<EmbeddingConverter> d_embConv;
217 : : /** repair constant utility */
218 : : std::unique_ptr<SygusRepairConst> d_sygus_rconst;
219 : : /** example inference utility */
220 : : std::unique_ptr<ExampleInfer> d_exampleInfer;
221 : : /** map from enumerators to their enumerator manager */
222 : : std::map<Node, std::unique_ptr<EnumValueManager>> d_enumManager;
223 : :
224 : : //------------------------modules
225 : : /** program by examples module */
226 : : std::unique_ptr<SygusPbe> d_ceg_pbe;
227 : : /** CEGIS module */
228 : : std::unique_ptr<Cegis> d_ceg_cegis;
229 : : /** CEGIS UNIF module */
230 : : std::unique_ptr<CegisUnif> d_ceg_cegisUnif;
231 : : /** connective core utility */
232 : : std::unique_ptr<CegisCoreConnective> d_sygus_ccore;
233 : : /** the set of active modules (subset of the above list) */
234 : : std::vector<SygusModule*> d_modules;
235 : : /** master module
236 : : *
237 : : * This is the module (one of those above) that takes sole responsibility
238 : : * for this conjecture, determined during assign(...).
239 : : */
240 : : SygusModule* d_master;
241 : : //------------------------end modules
242 : :
243 : : //------------------------enumerators
244 : : /**
245 : : * Get model values for terms n, store in vector v. This method returns true
246 : : * if and only if all values added to v are non-null.
247 : : *
248 : : * The argument activeIncomplete indicates whether n contains an active
249 : : * enumerator that is currently not finished enumerating values, but returned
250 : : * null on a call to getEnumeratedValue. This value is used for determining
251 : : * whether we should call getEnumeratedValues again within a call to
252 : : * SynthConjecture::check.
253 : : *
254 : : * It removes terms from n that correspond to "inactive" enumerators, that
255 : : * is, enumerators whose values have been exhausted.
256 : : */
257 : : bool getEnumeratedValues(std::vector<Node>& n,
258 : : std::vector<Node>& v,
259 : : bool& activeIncomplete);
260 : : /**
261 : : * Get or make enumerator manager for the enumerator e.
262 : : */
263 : : EnumValueManager* getEnumValueManagerFor(Node e);
264 : : /**
265 : : * Get or make the expression miner manager for enumerator e.
266 : : */
267 : : ExpressionMinerManager* getExprMinerManagerFor(Node e);
268 : : //------------------------end enumerators
269 : :
270 : : /** list of constants for quantified formula
271 : : * The outer Skolems for the negation of d_embed_quant.
272 : : */
273 : : std::vector<Node> d_candidates;
274 : : /** base instantiation
275 : : * If d_embed_quant is forall d. exists y. P( d, y ), then
276 : : * this is the formula exists y. P( d_candidates, y ). Notice that
277 : : * (exists y. F) is shorthand above for ~( forall y. ~F ).
278 : : */
279 : : Node d_base_inst;
280 : : /** The skolemized form of the above formula. */
281 : : Node d_checkBody;
282 : : /** list of variables on inner quantification */
283 : : std::vector<Node> d_innerVars;
284 : : /** list of skolems on inner quantification */
285 : : std::vector<Node> d_innerSks;
286 : : /** the asserted (negated) conjecture */
287 : : Node d_quant;
288 : : /**
289 : : * The side condition for solving the conjecture, after conversion to deep
290 : : * embedding.
291 : : */
292 : : Node d_embedSideCondition;
293 : : /** (negated) conjecture after simplification */
294 : : Node d_simp_quant;
295 : : /** (negated) conjecture after simplification, conversion to deep embedding */
296 : : Node d_embed_quant;
297 : : /**
298 : : * The first index of an instantiation in CandidateInfo::d_inst that we have
299 : : * not yet tried to repair.
300 : : */
301 : : unsigned d_repair_index;
302 : : /** record solution (this is used to construct solutions later) */
303 : : void recordSolution(const std::vector<Node>& vs);
304 : : /** get synth solutions internal
305 : : *
306 : : * This function constructs the body of solutions for all
307 : : * functions-to-synthesize in this conjecture and stores them in sols, in
308 : : * order. For each solution added to sols, we add an integer indicating what
309 : : * kind of solution n is, where if sols[i] = n, then
310 : : * if status[i] = 0: n is the (builtin term) corresponding to the solution,
311 : : * if status[i] = 1: n is the sygus representation of the solution.
312 : : * We store builtin versions under some conditions (such as when the sygus
313 : : * grammar is being ignored).
314 : : *
315 : : * This consults the single invocation module to get synthesis solutions if
316 : : * isSingleInvocation() returns true.
317 : : *
318 : : * For example, for conjecture exists fg. forall x. f(x)>g(x), this function
319 : : * may set ( sols, status ) to ( { x+1, d_x() }, { 1, 0 } ), where d_x() is
320 : : * the sygus datatype constructor corresponding to variable x.
321 : : */
322 : : bool getSynthSolutionsInternal(std::vector<Node>& sols,
323 : : std::vector<int8_t>& status);
324 : : /**
325 : : * Run expression mining on the last synthesis solution. Return true
326 : : * if we should skip it.
327 : : *
328 : : * This method also prints the current synthesis solution to output stream out
329 : : * when sygusStream is enabled, which does not enclose solutions in
330 : : * parentheses. If sygusStream is enabled, this always returns true, as the
331 : : * current solution should be printed and then immediately excluded.
332 : : */
333 : : bool runExprMiner();
334 : : /** expression miner managers for each function-to-synthesize
335 : : *
336 : : * Notice that for each function-to-synthesize, we enumerate a stream of
337 : : * candidate solutions, where each of these streams is independent. Thus,
338 : : * we maintain separate expression miner managers for each of them.
339 : : *
340 : : * This is used for the sygusRewSynth() option to synthesize new candidate
341 : : * rewrite rules.
342 : : */
343 : : std::map<Node, std::unique_ptr<ExpressionMinerManager>> d_exprm;
344 : : /** Have we given a warning for a candidate that failed verification? */
345 : : bool d_verifyWarned;
346 : : };
347 : :
348 : : } // namespace quantifiers
349 : : } // namespace theory
350 : : } // namespace cvc5::internal
351 : :
352 : : #endif
|
