1 /********************* */
2 /*! \file synth_conjecture.h
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Mathias Preiner, Haniel Barbosa
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Class that encapsulates techniques for a single (SyGuS) synthesis
16 #include "cvc4_private.h"
18 #ifndef CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
19 #define CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
23 #include "theory/decision_manager.h"
24 #include "theory/quantifiers/expr_miner_manager.h"
25 #include "theory/quantifiers/sygus/ce_guided_single_inv.h"
26 #include "theory/quantifiers/sygus/cegis.h"
27 #include "theory/quantifiers/sygus/cegis_core_connective.h"
28 #include "theory/quantifiers/sygus/cegis_unif.h"
29 #include "theory/quantifiers/sygus/example_eval_cache.h"
30 #include "theory/quantifiers/sygus/example_infer.h"
31 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
32 #include "theory/quantifiers/sygus/sygus_pbe.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/template_infer.h"
40 namespace quantifiers
{
42 class SygusStatistics
;
45 * A base class for generating values for actively-generated enumerators.
46 * At a high level, the job of this class is to accept a stream of "abstract
47 * values" a1, ..., an, ..., and generate a (possibly larger) stream of
48 * "concrete values" c11, ..., c1{m_1}, ..., cn1, ... cn{m_n}, ....
50 class EnumValGenerator
53 virtual ~EnumValGenerator() {}
54 /** initialize this class with enumerator e */
55 virtual void initialize(Node e
) = 0;
56 /** Inform this generator that abstract value v was enumerated. */
57 virtual void addValue(Node v
) = 0;
59 * Increment this value generator. If this returns false, then we are out of
60 * values. If this returns true, getCurrent(), if non-null, returns the
63 * Notice that increment() may return true and afterwards it may be the case
64 * getCurrent() is null. We do this so that increment() does not take too
65 * much time per call, which can be the case for grammars where it is
66 * difficult to find the next (non-redundant) term. Returning true with
67 * a null current term gives the caller the chance to interleave other
70 virtual bool increment() = 0;
71 /** Get the current concrete value generated by this class. */
72 virtual Node
getCurrent() = 0;
75 /** a synthesis conjecture
76 * This class implements approaches for a synthesis conjecture, given by data
78 * This includes both approaches for synthesis in Reynolds et al CAV 2015. It
79 * determines which approach and optimizations are applicable to the
80 * conjecture, and has interfaces for implementing them.
85 SynthConjecture(QuantifiersEngine
* qe
,
91 /** get original version of conjecture */
92 Node
getConjecture() const { return d_quant
; }
93 /** get deep embedding version of conjecture */
94 Node
getEmbeddedConjecture() const { return d_embed_quant
; }
95 //-------------------------------for counterexample-guided check/refine
96 /** whether the conjecture is waiting for a call to doCheck below */
98 /** whether the conjecture is waiting for a call to doRefine below */
99 bool needsRefinement() const;
100 /** do syntax-guided enumerative check
102 * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015.
104 * The method returns true if this conjecture is finished trying solutions
105 * for the given call to SynthEngine::check.
107 * Notice that we make multiple calls to doCheck on one call to
108 * SynthEngine::check. For example, if we are using an actively-generated
109 * enumerator, one enumerated (abstract) term may correspond to multiple
110 * concrete terms t1, ..., tn to check, where we make up to n calls to doCheck
111 * when each of t1, ..., tn fails to satisfy the current refinement lemmas.
113 bool doCheck(std::vector
<Node
>& lems
);
116 * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015.
118 * This method is run when needsRefinement() returns true, indicating that
119 * the last call to doCheck found a counterexample to the last candidate.
121 * This method adds a refinement lemma on the output channel of quantifiers
122 * engine. If the refinement lemma is a duplicate, then we manually
123 * exclude the current candidate via excludeCurrentSolution. This should
124 * only occur when the synthesis conjecture for the current candidate fails
125 * to evaluate to false for a given counterexample point, but regardless its
126 * negation is satisfiable for the current candidate and that point. This is
127 * exclusive to theories with partial functions, e.g. (non-linear) division.
129 * This method returns true if a lemma was added on the output channel, and
133 //-------------------------------end for counterexample-guided check/refine
135 * Prints the synthesis solution to output stream out. This invokes solution
136 * reconstruction if the conjecture is single invocation. Otherwise, it
137 * returns the solution found by sygus enumeration.
139 void printSynthSolution(std::ostream
& out
);
140 /** get synth solutions
142 * This method returns true if this class has a solution available to the
143 * conjecture that it was assigned.
145 * Let q be the synthesis conjecture assigned to this class.
146 * This method adds entries to sol_map[q] that map functions-to-synthesize to
147 * their builtin solution, which has the same type. For example, for synthesis
148 * conjecture exists f. forall x. f( x )>x, this function will update
149 * sol_map[q] to contain the entry:
150 * f -> (lambda x. x+1)
152 bool getSynthSolutions(std::map
<Node
, std::map
<Node
, Node
> >& sol_map
);
154 * The feasible guard whose semantics are "this conjecture is feasiable".
155 * This is "G" in Figure 3 of Reynolds et al CAV 2015.
157 Node
getGuard() const;
159 bool isGround() { return d_inner_vars
.empty(); }
160 /** are we using single invocation techniques */
161 bool isSingleInvocation() const;
162 /** preregister conjecture
163 * This is used as a heuristic for solution reconstruction, so that we
164 * remember expressions in the conjecture before preprocessing, since they
165 * may be helpful during solution reconstruction (Figure 5 of Reynolds et al
168 void preregisterConjecture(Node q
);
169 /** assign conjecture q to this class */
171 /** has a conjecture been assigned to this class */
172 bool isAssigned() { return !d_embed_quant
.isNull(); }
174 * Get model value for term n.
176 Node
getModelValue(Node n
);
178 /** get utility for static preprocessing and analysis of conjectures */
179 SynthConjectureProcess
* getProcess() { return d_ceg_proc
.get(); }
180 /** get constant repair utility */
181 SygusRepairConst
* getRepairConst() { return d_sygus_rconst
.get(); }
182 /** get example inference utility */
183 ExampleInfer
* getExampleInfer() { return d_exampleInfer
.get(); }
184 /** get the example evaluation cache utility for enumerator e */
185 ExampleEvalCache
* getExampleEvalCache(Node e
);
186 /** get program by examples module */
187 SygusPbe
* getPbe() { return d_ceg_pbe
.get(); }
188 /** get the symmetry breaking predicate for type */
189 Node
getSymmetryBreakingPredicate(
190 Node x
, Node e
, TypeNode tn
, unsigned tindex
, unsigned depth
);
191 /** print out debug information about this conjecture */
192 void debugPrint(const char* c
);
193 /** check side condition
195 * This returns false if the solution { d_candidates -> cvals } does not
196 * satisfy the side condition of the conjecture maintained by this class,
197 * if it exists, and true otherwise.
199 bool checkSideCondition(const std::vector
<Node
>& cvals
) const;
202 /** reference to quantifier engine */
203 QuantifiersEngine
* d_qe
;
204 /** Reference to the quantifiers state */
205 QuantifiersState
& d_qstate
;
206 /** reference to the statistics of parent */
207 SygusStatistics
& d_stats
;
208 /** term database sygus of d_qe */
210 /** The feasible guard. */
211 Node d_feasible_guard
;
213 * Do we have a solution in this solve context? This flag is reset to false
214 * on every call to presolve.
217 /** the decision strategy for the feasible guard */
218 std::unique_ptr
<DecisionStrategy
> d_feasible_strategy
;
219 /** single invocation utility */
220 std::unique_ptr
<CegSingleInv
> d_ceg_si
;
221 /** template inference utility */
222 std::unique_ptr
<SygusTemplateInfer
> d_templInfer
;
223 /** utility for static preprocessing and analysis of conjectures */
224 std::unique_ptr
<SynthConjectureProcess
> d_ceg_proc
;
225 /** grammar utility */
226 std::unique_ptr
<CegGrammarConstructor
> d_ceg_gc
;
227 /** repair constant utility */
228 std::unique_ptr
<SygusRepairConst
> d_sygus_rconst
;
229 /** example inference utility */
230 std::unique_ptr
<ExampleInfer
> d_exampleInfer
;
231 /** example evaluation cache utility for each enumerator */
232 std::map
<Node
, std::unique_ptr
<ExampleEvalCache
> > d_exampleEvalCache
;
234 //------------------------modules
235 /** program by examples module */
236 std::unique_ptr
<SygusPbe
> d_ceg_pbe
;
238 std::unique_ptr
<Cegis
> d_ceg_cegis
;
239 /** CEGIS UNIF module */
240 std::unique_ptr
<CegisUnif
> d_ceg_cegisUnif
;
241 /** connective core utility */
242 std::unique_ptr
<CegisCoreConnective
> d_sygus_ccore
;
243 /** the set of active modules (subset of the above list) */
244 std::vector
<SygusModule
*> d_modules
;
247 * This is the module (one of those above) that takes sole responsibility
248 * for this conjecture, determined during assign(...).
250 SygusModule
* d_master
;
251 //------------------------end modules
253 //------------------------enumerators
255 * Get model values for terms n, store in vector v. This method returns true
256 * if and only if all values added to v are non-null.
258 * The argument activeIncomplete indicates whether n contains an active
259 * enumerator that is currently not finished enumerating values, but returned
260 * null on a call to getEnumeratedValue. This value is used for determining
261 * whether we should call getEnumeratedValues again within a call to
262 * SynthConjecture::check.
264 * It removes terms from n that correspond to "inactive" enumerators, that
265 * is, enumerators whose values have been exhausted.
267 bool getEnumeratedValues(std::vector
<Node
>& n
,
268 std::vector
<Node
>& v
,
269 bool& activeIncomplete
);
271 * Get model value for term n. If n has a value that was excluded by
272 * datatypes sygus symmetry breaking, this method returns null. It sets
273 * activeIncomplete to true if there is an actively-generated enumerator whose
274 * current value is null but it has not finished generating values.
276 Node
getEnumeratedValue(Node n
, bool& activeIncomplete
);
277 /** enumerator generators for each actively-generated enumerator */
278 std::map
<Node
, std::unique_ptr
<EnumValGenerator
> > d_evg
;
280 * Map from enumerators to whether they are currently being
281 * "actively-generated". That is, we are in a state where we have called
282 * d_evg[e].addValue(v) for some v, and d_evg[e].getNext() has not yet
283 * returned null. The range of this map stores the abstract value that
284 * we are currently generating values from.
286 std::map
<Node
, Node
> d_ev_curr_active_gen
;
287 /** the current waiting value of each actively-generated enumerator, if any
289 * This caches values that are actively generated and that we have not yet
290 * passed to a call to SygusModule::constructCandidates. An example of when
291 * this may occur is when there are two actively-generated enumerators e1 and
292 * e2. Say on some iteration we actively-generate v1 for e1, the value
293 * of e2 was excluded by symmetry breaking, and say the current master sygus
294 * module does not handle partial models. Hence, we abort the current check.
295 * We remember that the value of e1 was v1 by storing it here, so that on
296 * a future check when v2 has a proper value, it is returned.
298 std::map
<Node
, Node
> d_ev_active_gen_waiting
;
299 /** the first value enumerated for each actively-generated enumerator
301 * This is to implement an optimization that only guards the blocking lemma
302 * for the first value of an actively-generated enumerator.
304 std::map
<Node
, Node
> d_ev_active_gen_first_val
;
305 //------------------------end enumerators
307 /** list of constants for quantified formula
308 * The outer Skolems for the negation of d_embed_quant.
310 std::vector
<Node
> d_candidates
;
311 /** base instantiation
312 * If d_embed_quant is forall d. exists y. P( d, y ), then
313 * this is the formula exists y. P( d_candidates, y ). Notice that
314 * (exists y. F) is shorthand above for ~( forall y. ~F ).
317 /** list of variables on inner quantification */
318 std::vector
<Node
> d_inner_vars
;
320 * The set of skolems for the current "verification" lemma, if one exists.
321 * This may be added to during calls to doCheck(). The model values for these
322 * skolems are analyzed during doRefine().
324 std::vector
<Node
> d_ce_sk_vars
;
326 * If we have already tested the satisfiability of the current verification
327 * lemma, this stores the model values of d_ce_sk_vars in the current
328 * (satisfiable, failed) verification lemma.
330 std::vector
<Node
> d_ce_sk_var_mvs
;
332 * Whether the above vector has been set. We have this flag since the above
333 * vector may be set to empty (e.g. for ground synthesis conjectures).
335 bool d_set_ce_sk_vars
;
337 /** the asserted (negated) conjecture */
340 * The side condition for solving the conjecture, after conversion to deep
343 Node d_embedSideCondition
;
344 /** (negated) conjecture after simplification */
346 /** (negated) conjecture after simplification, conversion to deep embedding */
348 /** candidate information */
353 /** list of terms we have instantiated candidates with */
354 std::vector
<Node
> d_inst
;
356 std::map
<Node
, CandidateInfo
> d_cinfo
;
358 * The first index of an instantiation in CandidateInfo::d_inst that we have
359 * not yet tried to repair.
361 unsigned d_repair_index
;
362 /** number of times we have called doRefine */
363 unsigned d_refine_count
;
364 /** record solution (this is used to construct solutions later) */
365 void recordSolution(std::vector
<Node
>& vs
);
366 /** get synth solutions internal
368 * This function constructs the body of solutions for all
369 * functions-to-synthesize in this conjecture and stores them in sols, in
370 * order. For each solution added to sols, we add an integer indicating what
371 * kind of solution n is, where if sols[i] = n, then
372 * if status[i] = 0: n is the (builtin term) corresponding to the solution,
373 * if status[i] = 1: n is the sygus representation of the solution.
374 * We store builtin versions under some conditions (such as when the sygus
375 * grammar is being ignored).
377 * This consults the single invocation module to get synthesis solutions if
378 * isSingleInvocation() returns true.
380 * For example, for conjecture exists fg. forall x. f(x)>g(x), this function
381 * may set ( sols, status ) to ( { x+1, d_x() }, { 1, 0 } ), where d_x() is
382 * the sygus datatype constructor corresponding to variable x.
384 bool getSynthSolutionsInternal(std::vector
<Node
>& sols
,
385 std::vector
<int>& status
);
386 //-------------------------------- sygus stream
388 * Prints the current synthesis solution to the output stream indicated by
389 * the Options object, send a lemma blocking the current solution to the
390 * output channel, which we refer to as a "stream exclusion lemma".
392 * The argument enums is the set of enumerators that comprise the current
393 * solution, and values is their current values.
395 void printAndContinueStream(const std::vector
<Node
>& enums
,
396 const std::vector
<Node
>& values
);
397 /** exclude the current solution { enums -> values } */
398 void excludeCurrentSolution(const std::vector
<Node
>& enums
,
399 const std::vector
<Node
>& values
);
401 * Whether we have guarded a stream exclusion lemma when using sygusStream.
402 * This is an optimization that allows us to guard only the first stream
405 bool d_guarded_stream_exc
;
406 //-------------------------------- end sygus stream
407 /** expression miner managers for each function-to-synthesize
409 * Notice that for each function-to-synthesize, we enumerate a stream of
410 * candidate solutions, where each of these streams is independent. Thus,
411 * we maintain separate expression miner managers for each of them.
413 * This is used for the sygusRewSynth() option to synthesize new candidate
416 std::map
<Node
, ExpressionMinerManager
> d_exprm
;
419 } // namespace quantifiers
420 } // namespace theory
421 } /* namespace CVC4 */