1 /********************* */
2 /*! \file synth_conjecture.h
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Haniel Barbosa, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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_unif.h"
28 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
29 #include "theory/quantifiers/sygus/sygus_pbe.h"
30 #include "theory/quantifiers/sygus/sygus_process_conj.h"
31 #include "theory/quantifiers/sygus/sygus_repair_const.h"
35 namespace quantifiers
{
38 * A base class for generating values for actively-generated enumerators.
39 * At a high level, the job of this class is to accept a stream of "abstract
40 * values" a1, ..., an, ..., and generate a (possibly larger) stream of
41 * "concrete values" c11, ..., c1{m_1}, ..., cn1, ... cn{m_n}, ....
43 class EnumValGenerator
46 virtual ~EnumValGenerator() {}
47 /** initialize this class with enumerator e */
48 virtual void initialize(Node e
) = 0;
49 /** Inform this generator that abstract value v was enumerated. */
50 virtual void addValue(Node v
) = 0;
52 * Increment this value generator. If this returns false, then we are out of
53 * values. If this returns true, getCurrent(), if non-null, returns the
56 virtual bool increment() = 0;
57 /** Get the current concrete value generated by this class. */
58 virtual Node
getCurrent() = 0;
61 /** a synthesis conjecture
62 * This class implements approaches for a synthesis conecjture, given by data
64 * This includes both approaches for synthesis in Reynolds et al CAV 2015. It
65 * determines which approach and optimizations are applicable to the
66 * conjecture, and has interfaces for implementing them.
71 SynthConjecture(QuantifiersEngine
* qe
);
75 /** get original version of conjecture */
76 Node
getConjecture() { return d_quant
; }
77 /** get deep embedding version of conjecture */
78 Node
getEmbeddedConjecture() { return d_embed_quant
; }
79 //-------------------------------for counterexample-guided check/refine
80 /** increment the number of times we have successfully done candidate
82 void incrementRefineCount() { d_refine_count
++; }
83 /** whether the conjecture is waiting for a call to doCheck below */
85 /** whether the conjecture is waiting for a call to doRefine below */
86 bool needsRefinement() const;
87 /** do syntax-guided enumerative check
89 * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015.
91 * The method returns true if this conjecture is finished trying solutions
92 * for the given call to SynthEngine::check.
94 * Notice that we make multiple calls to doCheck on one call to
95 * SynthEngine::check. For example, if we are using an actively-generated
96 * enumerator, one enumerated (abstract) term may correspond to multiple
97 * concrete terms t1, ..., tn to check, where we make up to n calls to doCheck
98 * when each of t1, ..., tn fails to satisfy the current refinement lemmas.
100 bool doCheck(std::vector
<Node
>& lems
);
102 * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015.
104 void doRefine(std::vector
<Node
>& lems
);
105 //-------------------------------end for counterexample-guided check/refine
107 * Prints the synthesis solution to output stream out. This invokes solution
108 * reconstruction if the conjecture is single invocation. Otherwise, it
109 * returns the solution found by sygus enumeration.
111 void printSynthSolution(std::ostream
& out
);
112 /** get synth solutions
114 * This returns a map from function-to-synthesize variables to their
115 * builtin solution, which has the same type. For example, for synthesis
116 * conjecture exists f. forall x. f( x )>x, this function may return the map
117 * containing the entry:
118 * f -> (lambda x. x+1)
120 void getSynthSolutions(std::map
<Node
, Node
>& sol_map
);
122 * The feasible guard whose semantics are "this conjecture is feasiable".
123 * This is "G" in Figure 3 of Reynolds et al CAV 2015.
125 Node
getGuard() const;
127 bool isGround() { return d_inner_vars
.empty(); }
128 /** are we using single invocation techniques */
129 bool isSingleInvocation() const;
130 /** preregister conjecture
131 * This is used as a heuristic for solution reconstruction, so that we
132 * remember expressions in the conjecture before preprocessing, since they
133 * may be helpful during solution reconstruction (Figure 5 of Reynolds et al
136 void preregisterConjecture(Node q
);
137 /** assign conjecture q to this class */
139 /** has a conjecture been assigned to this class */
140 bool isAssigned() { return !d_embed_quant
.isNull(); }
142 * Get model value for term n.
144 Node
getModelValue(Node n
);
146 /** get utility for static preprocessing and analysis of conjectures */
147 SynthConjectureProcess
* getProcess() { return d_ceg_proc
.get(); }
148 /** get constant repair utility */
149 SygusRepairConst
* getRepairConst() { return d_sygus_rconst
.get(); }
150 /** get program by examples module */
151 SygusPbe
* getPbe() { return d_ceg_pbe
.get(); }
152 /** get the symmetry breaking predicate for type */
153 Node
getSymmetryBreakingPredicate(
154 Node x
, Node e
, TypeNode tn
, unsigned tindex
, unsigned depth
);
155 /** print out debug information about this conjecture */
156 void debugPrint(const char* c
);
159 /** reference to quantifier engine */
160 QuantifiersEngine
* d_qe
;
161 /** term database sygus of d_qe */
163 /** The feasible guard. */
164 Node d_feasible_guard
;
166 * Do we have a solution in this user context? This is user-context dependent
167 * to enable use cases of sygus in incremental mode.
169 context::CDO
<bool> d_hasSolution
;
170 /** the decision strategy for the feasible guard */
171 std::unique_ptr
<DecisionStrategy
> d_feasible_strategy
;
172 /** single invocation utility */
173 std::unique_ptr
<CegSingleInv
> d_ceg_si
;
174 /** utility for static preprocessing and analysis of conjectures */
175 std::unique_ptr
<SynthConjectureProcess
> d_ceg_proc
;
176 /** grammar utility */
177 std::unique_ptr
<CegGrammarConstructor
> d_ceg_gc
;
178 /** repair constant utility */
179 std::unique_ptr
<SygusRepairConst
> d_sygus_rconst
;
181 //------------------------modules
182 /** program by examples module */
183 std::unique_ptr
<SygusPbe
> d_ceg_pbe
;
185 std::unique_ptr
<Cegis
> d_ceg_cegis
;
186 /** CEGIS UNIF module */
187 std::unique_ptr
<CegisUnif
> d_ceg_cegisUnif
;
188 /** the set of active modules (subset of the above list) */
189 std::vector
<SygusModule
*> d_modules
;
192 * This is the module (one of those above) that takes sole responsibility
193 * for this conjecture, determined during assign(...).
195 SygusModule
* d_master
;
196 //------------------------end modules
198 //------------------------enumerators
200 * Get model values for terms n, store in vector v. This method returns true
201 * if and only if all values added to v are non-null.
203 * The argument activeIncomplete indicates whether n contains an active
204 * enumerator that is currently not finished enumerating values, but returned
205 * null on a call to getEnumeratedValue. This value is used for determining
206 * whether we should call getEnumeratedValues again within a call to
207 * SynthConjecture::check.
209 * It removes terms from n that correspond to "inactive" enumerators, that
210 * is, enumerators whose values have been exhausted.
212 bool getEnumeratedValues(std::vector
<Node
>& n
,
213 std::vector
<Node
>& v
,
214 bool& activeIncomplete
);
216 * Get model value for term n. If n has a value that was excluded by
217 * datatypes sygus symmetry breaking, this method returns null. It sets
218 * activeIncomplete to true if there is an actively-generated enumerator whose
219 * current value is null but it has not finished generating values.
221 Node
getEnumeratedValue(Node n
, bool& activeIncomplete
);
222 /** enumerator generators for each actively-generated enumerator */
223 std::map
<Node
, std::unique_ptr
<EnumValGenerator
> > d_evg
;
225 * Map from enumerators to whether they are currently being
226 * "actively-generated". That is, we are in a state where we have called
227 * d_evg[e].addValue(v) for some v, and d_evg[e].getNext() has not yet
228 * returned null. The range of this map stores the abstract value that
229 * we are currently generating values from.
231 std::map
<Node
, Node
> d_ev_curr_active_gen
;
232 /** the current waiting value of each actively-generated enumerator, if any
234 * This caches values that are actively generated and that we have not yet
235 * passed to a call to SygusModule::constructCandidates. An example of when
236 * this may occur is when there are two actively-generated enumerators e1 and
237 * e2. Say on some iteration we actively-generate v1 for e1, the value
238 * of e2 was excluded by symmetry breaking, and say the current master sygus
239 * module does not handle partial models. Hence, we abort the current check.
240 * We remember that the value of e1 was v1 by storing it here, so that on
241 * a future check when v2 has a proper value, it is returned.
243 std::map
<Node
, Node
> d_ev_active_gen_waiting
;
244 /** the first value enumerated for each actively-generated enumerator
246 * This is to implement an optimization that only guards the blocking lemma
247 * for the first value of an actively-generated enumerator.
249 std::map
<Node
, Node
> d_ev_active_gen_first_val
;
250 //------------------------end enumerators
252 /** list of constants for quantified formula
253 * The outer Skolems for the negation of d_embed_quant.
255 std::vector
<Node
> d_candidates
;
256 /** base instantiation
257 * If d_embed_quant is forall d. exists y. P( d, y ), then
258 * this is the formula exists y. P( d_candidates, y ). Notice that
259 * (exists y. F) is shorthand above for ~( forall y. ~F ).
262 /** list of variables on inner quantification */
263 std::vector
<Node
> d_inner_vars
;
265 * The set of skolems for the current "verification" lemma, if one exists.
266 * This may be added to during calls to doCheck(). The model values for these
267 * skolems are analyzed during doRefine().
269 std::vector
<Node
> d_ce_sk_vars
;
271 * If we have already tested the satisfiability of the current verification
272 * lemma, this stores the model values of d_ce_sk_vars in the current
273 * (satisfiable, failed) verification lemma.
275 std::vector
<Node
> d_ce_sk_var_mvs
;
277 * Whether the above vector has been set. We have this flag since the above
278 * vector may be set to empty (e.g. for ground synthesis conjectures).
280 bool d_set_ce_sk_vars
;
282 /** the asserted (negated) conjecture */
285 * The side condition for solving the conjecture, after conversion to deep
288 Node d_embedSideCondition
;
289 /** (negated) conjecture after simplification */
291 /** (negated) conjecture after simplification, conversion to deep embedding */
293 /** candidate information */
298 /** list of terms we have instantiated candidates with */
299 std::vector
<Node
> d_inst
;
301 std::map
<Node
, CandidateInfo
> d_cinfo
;
303 * The first index of an instantiation in CandidateInfo::d_inst that we have
304 * not yet tried to repair.
306 unsigned d_repair_index
;
307 /** number of times we have called doRefine */
308 unsigned d_refine_count
;
309 /** get candidadate */
310 Node
getCandidate(unsigned int i
) { return d_candidates
[i
]; }
311 /** record instantiation (this is used to construct solutions later) */
312 void recordInstantiation(std::vector
<Node
>& vs
)
314 Assert(vs
.size() == d_candidates
.size());
315 for (unsigned i
= 0; i
< vs
.size(); i
++)
317 d_cinfo
[d_candidates
[i
]].d_inst
.push_back(vs
[i
]);
320 /** get synth solutions internal
322 * This function constructs the body of solutions for all
323 * functions-to-synthesize in this conjecture and stores them in sols, in
324 * order. For each solution added to sols, we add an integer indicating what
325 * kind of solution n is, where if sols[i] = n, then
326 * if status[i] = 0: n is the (builtin term) corresponding to the solution,
327 * if status[i] = 1: n is the sygus representation of the solution.
328 * We store builtin versions under some conditions (such as when the sygus
329 * grammar is being ignored).
331 * This consults the single invocation module to get synthesis solutions if
332 * isSingleInvocation() returns true.
334 * For example, for conjecture exists fg. forall x. f(x)>g(x), this function
335 * may set ( sols, status ) to ( { x+1, d_x() }, { 1, 0 } ), where d_x() is
336 * the sygus datatype constructor corresponding to variable x.
338 bool getSynthSolutionsInternal(std::vector
<Node
>& sols
,
339 std::vector
<int>& status
);
340 //-------------------------------- sygus stream
341 /** current stream guard */
342 Node d_current_stream_guard
;
343 /** the decision strategy for streaming solutions */
344 class SygusStreamDecisionStrategy
: public DecisionStrategyFmf
347 SygusStreamDecisionStrategy(context::Context
* satContext
,
348 Valuation valuation
);
350 Node
mkLiteral(unsigned i
) override
;
352 std::string
identify() const override
354 return std::string("sygus_stream");
357 std::unique_ptr
<SygusStreamDecisionStrategy
> d_stream_strategy
;
358 /** get current stream guard */
359 Node
getCurrentStreamGuard() const;
360 /** get stream guarded lemma
362 * If sygusStream is enabled, this returns ( G V n ) where G is the guard
363 * returned by getCurrentStreamGuard, otherwise this returns n.
365 Node
getStreamGuardedLemma(Node n
) const;
367 * Prints the current synthesis solution to the output stream indicated by
368 * the Options object, send a lemma blocking the current solution to the
369 * output channel, which we refer to as a "stream exclusion lemma".
371 void printAndContinueStream();
372 /** exclude the current solution */
373 void excludeCurrentSolution();
375 * Whether we have guarded a stream exclusion lemma when using sygusStream.
376 * This is an optimization that allows us to guard only the first stream
379 bool d_guarded_stream_exc
;
380 //-------------------------------- end sygus stream
381 /** expression miner managers for each function-to-synthesize
383 * Notice that for each function-to-synthesize, we enumerate a stream of
384 * candidate solutions, where each of these streams is independent. Thus,
385 * we maintain separate expression miner managers for each of them.
387 * This is used for the sygusRewSynth() option to synthesize new candidate
390 std::map
<Node
, ExpressionMinerManager
> d_exprm
;
393 } // namespace quantifiers
394 } // namespace theory
395 } /* namespace CVC4 */