Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Haniel Barbosa, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #ifndef CVC5__THEORY__QUANTIFIERS__CEGIS_H
19 : : #define CVC5__THEORY__QUANTIFIERS__CEGIS_H
20 : :
21 : : #include <map>
22 : :
23 : : #include "expr/subs.h"
24 : : #include "smt/env_obj.h"
25 : : #include "theory/quantifiers/sygus/sygus_module.h"
26 : : #include "theory/quantifiers/sygus_sampler.h"
27 : :
28 : : namespace cvc5::internal {
29 : : namespace theory {
30 : : namespace quantifiers {
31 : :
32 : : class SygusEvalUnfold;
33 : :
34 : : /** Cegis
35 : : *
36 : : * The default sygus module for synthesis, counterexample-guided inductive
37 : : * synthesis (CEGIS).
38 : : *
39 : : * It initializes a list of sygus enumerators that are one-to-one with
40 : : * candidates, and returns a list of candidates that are the model values
41 : : * of these enumerators on calls to constructCandidates.
42 : : *
43 : : * It implements an optimization (getRefinementEvalLemmas) that evaluates all
44 : : * previous refinement lemmas for a term before returning it as a candidate
45 : : * in calls to constructCandidates.
46 : : */
47 : : class Cegis : public SygusModule
48 : : {
49 : : public:
50 : : Cegis(Env& env,
51 : : QuantifiersState& qs,
52 : : QuantifiersInferenceManager& qim,
53 : : TermDbSygus* tds,
54 : : SynthConjecture* p);
55 : 28632 : ~Cegis() override {}
56 : : /** initialize */
57 : : virtual bool initialize(Node conj,
58 : : Node n,
59 : : const std::vector<Node>& candidates) override;
60 : : /** get term list */
61 : : virtual void getTermList(const std::vector<Node>& candidates,
62 : : std::vector<Node>& enums) override;
63 : : /** construct candidate */
64 : : virtual bool constructCandidates(
65 : : const std::vector<Node>& enums,
66 : : const std::vector<Node>& enum_values,
67 : : const std::vector<Node>& candidates,
68 : : std::vector<Node>& candidate_values) override;
69 : : /** register refinement lemma
70 : : *
71 : : * This function stores lem as a refinement lemma, and adds it to lems.
72 : : */
73 : : virtual void registerRefinementLemma(const std::vector<Node>& vars,
74 : : Node lem) override;
75 : : /** using repair const */
76 : : virtual bool usingRepairConst() override;
77 : :
78 : : protected:
79 : : /** the evaluation unfold utility of d_tds */
80 : : SygusEvalUnfold* d_eval_unfold;
81 : : /** If SynthConjecture::d_base_inst is exists y. P( d, y ), then this is y. */
82 : : std::vector<Node> d_base_vars;
83 : : /**
84 : : * If SynthConjecture::d_base_inst is exists y. P( d, y ), then this is the
85 : : * formula P( SynthConjecture::d_candidates, y ).
86 : : */
87 : : Node d_base_body;
88 : : //----------------------------------cegis-implementation-specific
89 : : /**
90 : : * Do cegis-implementation-specific initialization for this class. The return
91 : : * value and behavior of this function is the same as initialize(...) above.
92 : : */
93 : : virtual bool processInitialize(Node conj,
94 : : Node n,
95 : : const std::vector<Node>& candidates);
96 : : /** do cegis-implementation-specific post-processing for construct candidate
97 : : *
98 : : * satisfiedRl is whether all refinement lemmas are satisfied under the
99 : : * substitution { enums -> enum_values }.
100 : : *
101 : : * The return value and behavior of this function is the same as
102 : : * constructCandidates(...) above.
103 : : */
104 : : virtual bool processConstructCandidates(const std::vector<Node>& enums,
105 : : const std::vector<Node>& enum_values,
106 : : const std::vector<Node>& candidates,
107 : : std::vector<Node>& candidate_values,
108 : : bool satisfiedRl);
109 : : //----------------------------------end cegis-implementation-specific
110 : :
111 : : //-----------------------------------refinement lemmas
112 : : /** refinement lemmas */
113 : : std::vector<Node> d_refinement_lemmas;
114 : : /** (processed) conjunctions of refinement lemmas that are not unit */
115 : : std::unordered_set<Node> d_refinement_lemma_conj;
116 : : /** (processed) conjunctions of refinement lemmas that are unit */
117 : : std::unordered_set<Node> d_refinement_lemma_unit;
118 : : /** substitution entailed by d_refinement_lemma_unit */
119 : : std::vector<Node> d_rl_eval_hds;
120 : : std::vector<Node> d_rl_vals;
121 : : /** all variables appearing in refinement lemmas */
122 : : std::unordered_set<Node> d_refinement_lemma_vars;
123 : : /**
124 : : * Are the counterexamples we are handling in this class of only closed
125 : : * enumerable types (see TypeNode::isClosedEnumerable). If this is false,
126 : : * then CEGIS refinement lemmas can contain terms that are unhandled by
127 : : * theory solvers, e.g. uninterpreted constants.
128 : : */
129 : : bool d_cexClosedEnum;
130 : :
131 : : /** adds lem as a refinement lemma */
132 : : void addRefinementLemma(Node lem);
133 : : /** add refinement lemma conjunct
134 : : *
135 : : * This is a helper function for addRefinementLemma.
136 : : *
137 : : * This adds waiting[wcounter] to the proper vector (d_refinement_lemma_conj
138 : : * or d_refinement_lemma_unit). In the case that waiting[wcounter] corresponds
139 : : * to a value propagation, e.g. it is of the form:
140 : : * (eval x c1...cn) = c
141 : : * then it is added to d_refinement_lemma_unit, (eval x c1...cn) -> c is added
142 : : * as a substitution in d_rl_eval_hds/d_rl_eval_vals, and applied to previous
143 : : * lemmas in d_refinement_lemma_conj and lemmas waiting[k] for k>wcounter.
144 : : * Each lemma in d_refinement_lemma_conj that is modifed in this process is
145 : : * moved to the vector waiting.
146 : : */
147 : : void addRefinementLemmaConjunct(unsigned wcounter,
148 : : std::vector<Node>& waiting);
149 : : /** sample add refinement lemma
150 : : *
151 : : * This function will check if there is a sample point in d_sampler that
152 : : * refutes the candidate solution (d_quant_vars->vals). If so, it adds a
153 : : * refinement lemma to the lists d_refinement_lemmas that corresponds to that
154 : : * sample point, and adds a lemma to d_qim pending lemmas if cegisSample mode
155 : : * is not trust.
156 : : */
157 : : bool sampleAddRefinementLemma(const std::vector<Node>& candidates,
158 : : const std::vector<Node>& vals);
159 : :
160 : : /** evaluates candidate values on current refinement lemmas
161 : : *
162 : : * This method performs techniques that ensure that
163 : : * { candidates -> candidate_values } is a candidate solution that should
164 : : * be checked by the solution verifier of the CEGIS loop. This method
165 : : * invokes two sub-methods which may reject the current solution.
166 : : * The first is "refinement evaluation", described above the method
167 : : * getRefinementEvalLemmas below. The second is "evaluation unfolding",
168 : : * which eagerly unfolds applications of evaluation functions (see
169 : : * sygus_eval_unfold.h for details).
170 : : *
171 : : * If this method returns true, then { candidates -> candidate_values }
172 : : * is not ready to be tried as a candidate solution. In this case, it may add
173 : : * lemmas to lems.
174 : : *
175 : : * Notice that this method may return true without adding any lemmas to
176 : : * lems, in the case that terms from candidates are "actively-generated
177 : : * enumerators", since the model values of such terms are managed
178 : : * explicitly within getEnumeratedValue. In this case, the owner of the
179 : : * actively-generated enumerators (e.g. SynthConjecture) is responsible for
180 : : * blocking the current value of candidates.
181 : : */
182 : : bool addEvalLemmas(const std::vector<Node>& candidates,
183 : : const std::vector<Node>& candidate_values);
184 : : /** Get the node corresponding to the conjunction of all refinement lemmas. */
185 : : Node getRefinementLemmaFormula();
186 : : //-----------------------------------end refinement lemmas
187 : :
188 : : /** Get refinement evaluation lemmas
189 : : *
190 : : * This method performs "refinement evaluation", that is, it tests
191 : : * whether the current solution, given by { vs -> ms },
192 : : * satisfies all current refinement lemmas. If it does not, it may add
193 : : * blocking lemmas L to lems which exclude (a generalization of) the current
194 : : * solution.
195 : : *
196 : : * Given a candidate solution ms for candidates vs, this function adds lemmas
197 : : * to lems based on evaluating the conjecture, instantiated for ms, on lemmas
198 : : * for previous refinements (d_refinement_lemmas).
199 : : *
200 : : * Returns true if any such lemma exists.
201 : : */
202 : : bool getRefinementEvalLemmas(const std::vector<Node>& vs,
203 : : const std::vector<Node>& ms,
204 : : std::vector<Node>& lems);
205 : : /** Check refinement evaluation lemmas
206 : : *
207 : : * This method is similar to above, but does not perform any generalization
208 : : * techniques. It is used when we are using only fast enumerators for
209 : : * all functions-to-synthesize.
210 : : *
211 : : * Returns true if a refinement lemma is false for the solution
212 : : * { vs -> ms }.
213 : : */
214 : : bool checkRefinementEvalLemmas(const std::vector<Node>& vs,
215 : : const std::vector<Node>& ms);
216 : : /** sampler object for the option cegisSample()
217 : : *
218 : : * This samples points of the type of the inner variables of the synthesis
219 : : * conjecture (d_base_vars).
220 : : */
221 : : SygusSampler d_cegis_sampler;
222 : : /** cegis sample refine points
223 : : *
224 : : * Stores the list of indices of sample points in d_cegis_sampler we have
225 : : * added as refinement lemmas.
226 : : */
227 : : std::unordered_set<unsigned> d_cegis_sample_refine;
228 : :
229 : : //---------------------------------for symbolic constructors
230 : : /** are we using symbolic constants?
231 : : *
232 : : * This flag is set ot true if at least one of the enumerators allocated
233 : : * by this class has been configured to allow model values with symbolic
234 : : * constructors, such as the "any constant" constructor.
235 : : */
236 : : bool d_usingSymCons;
237 : : //---------------------------------end for symbolic constructors
238 : : /**
239 : : * Subsitution for evaluation unfold, which maps functions-to-synthesize
240 : : * with lambdas in terms of their deep embeddings. For example, if d_f is the
241 : : * deep embedding of function to synthesize f with argument list
242 : : * ((x Int) (y Int)), then d_euSubs maps:
243 : : * f -> (lambda ((x Int) (y Int)) (DT_SYGUS_EVAL_UNFOLD d_f x y)).
244 : : */
245 : : Subs d_euSubs;
246 : : };
247 : :
248 : : } // namespace quantifiers
249 : : } // namespace theory
250 : : } // namespace cvc5::internal
251 : :
252 : : #endif /* CVC5__THEORY__QUANTIFIERS__CEGIS_H */
|
