diff options
Diffstat (limited to 'src/theory/quantifiers/ce_guided_conjecture.h')
| -rw-r--r-- | src/theory/quantifiers/ce_guided_conjecture.h | 103 |
1 files changed, 90 insertions, 13 deletions
diff --git a/src/theory/quantifiers/ce_guided_conjecture.h b/src/theory/quantifiers/ce_guided_conjecture.h index 0f000bba5..dae261111 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.h +++ b/src/theory/quantifiers/ce_guided_conjecture.h @@ -24,6 +24,7 @@ #include "theory/quantifiers/ce_guided_single_inv.h" #include "theory/quantifiers/sygus_grammar_cons.h" #include "theory/quantifiers/sygus_process_conj.h" +#include "theory/quantifiers/sygus_sampler.h" #include "theory/quantifiers_engine.h" namespace CVC4 { @@ -74,12 +75,26 @@ public: * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015. */ void doRefine(std::vector< Node >& lems); - /** Print the synthesis solution - * singleInvocation is whether the solution was found by single invocation techniques. - */ //-------------------------------end for counterexample-guided check/refine - + /** + * prints the synthesis solution to output stream out. + * + * singleInvocation : set to true if we should consult the single invocation + * module to get synthesis solutions. + */ void printSynthSolution( std::ostream& out, bool singleInvocation ); + /** get synth solutions + * + * This returns a map from function-to-synthesize variables to their + * builtin solution, which has the same type. For example, for synthesis + * conjecture exists f. forall x. f( x )>x, this function may return the map + * containing the entry: + * f -> (lambda x. x+1) + * + * singleInvocation : set to true if we should consult the single invocation + * module to get synthesis solutions. + */ + void getSynthSolutions(std::map<Node, Node>& sol_map, bool singleInvocation); /** get guard, this is "G" in Figure 3 of Reynolds et al CAV 2015 */ Node getGuard(); /** is ground */ @@ -106,10 +121,21 @@ public: //-----------------------------------refinement lemmas /** get number of refinement lemmas we have added so far */ unsigned getNumRefinementLemmas() { return d_refinement_lemmas.size(); } - /** get refinement lemma */ + /** get refinement lemma + * + * If d_embed_quant is forall d. exists y. P( d, y ), then a refinement + * lemma is one of the form ~P( d_candidates, c ) for some c. + */ Node getRefinementLemma( unsigned i ) { return d_refinement_lemmas[i]; } - /** get refinement lemma */ - Node getRefinementBaseLemma( unsigned i ) { return d_refinement_lemmas_base[i]; } + /** sample add refinement lemma + * + * This function will check if there is a sample point in d_sampler that + * refutes the candidate solution (d_quant_vars->vals). If so, it adds a + * refinement lemma to the lists d_refinement_lemmas that corresponds to that + * sample point, and adds a lemma to lems if cegisSample mode is not trust. + */ + bool sampleAddRefinementLemma(std::vector<Node>& vals, + std::vector<Node>& lems); //-----------------------------------end refinement lemmas /** get program by examples utility */ @@ -133,14 +159,21 @@ private: /** grammar utility */ std::unique_ptr<CegGrammarConstructor> d_ceg_gc; /** list of constants for quantified formula - * The Skolems for the negation of d_embed_quant. + * The outer Skolems for the negation of d_embed_quant. */ std::vector< Node > d_candidates; /** base instantiation * If d_embed_quant is forall d. exists y. P( d, y ), then - * this is the formula P( candidates, y ). + * this is the formula exists y. P( d_candidates, y ). */ Node d_base_inst; + /** If d_base_inst is exists y. P( d, y ), then this is y. */ + std::vector<Node> d_base_vars; + /** + * If d_base_inst is exists y. P( d, y ), then this is the formula + * P( d_candidates, y ). + */ + Node d_base_body; /** expand base inst to disjuncts */ std::vector< Node > d_base_disj; /** list of variables on inner quantification */ @@ -152,14 +185,13 @@ private: //-----------------------------------refinement lemmas /** refinement lemmas */ std::vector< Node > d_refinement_lemmas; - std::vector< Node > d_refinement_lemmas_base; //-----------------------------------end refinement lemmas - /** quantified formula asserted */ + /** the asserted (negated) conjecture */ Node d_quant; - /** quantified formula (after simplification) */ + /** (negated) conjecture after simplification */ Node d_simp_quant; - /** quantified formula (after simplification, conversion to deep embedding) */ + /** (negated) conjecture after simplification, conversion to deep embedding */ Node d_embed_quant; /** candidate information */ class CandidateInfo { @@ -183,11 +215,38 @@ private: d_cinfo[d_candidates[i]].d_inst.push_back( vs[i] ); } } + /** get synth solutions internal + * + * This function constructs the body of solutions for all + * functions-to-synthesize in this conjecture and stores them in sols, in + * order. For each solution added to sols, we add an integer indicating what + * kind of solution n is, where if sols[i] = n, then + * if status[i] = 0: n is the (builtin term) corresponding to the solution, + * if status[i] = 1: n is the sygus representation of the solution. + * We store builtin versions under some conditions (such as when the sygus + * grammar is being ignored). + * + * singleInvocation : set to true if we should consult the single invocation + * module to get synthesis solutions. + * + * For example, for conjecture exists fg. forall x. f(x)>g(x), this function + * may set ( sols, status ) to ( { x+1, d_x() }, { 1, 0 } ), where d_x() is + * the sygus datatype constructor corresponding to variable x. + */ + void getSynthSolutionsInternal(std::vector<Node>& sols, + std::vector<int>& status, + bool singleInvocation); //-------------------------------- sygus stream /** the streaming guards for sygus streaming mode */ std::vector< Node > d_stream_guards; /** get current stream guard */ Node getCurrentStreamGuard() const; + /** get stream guarded lemma + * + * If sygusStream is enabled, this returns ( G V n ) where G is the guard + * returned by getCurrentStreamGuard, otherwise this returns n. + */ + Node getStreamGuardedLemma(Node n) const; //-------------------------------- end sygus stream //-------------------------------- non-syntax guided (deprecated) /** Whether we are syntax-guided (e.g. was the input in SyGuS format). @@ -197,6 +256,24 @@ private: /** the guard for non-syntax-guided synthesis */ Node d_nsg_guard; //-------------------------------- end non-syntax guided (deprecated) + /** sygus sampler objects for each program variable + * + * This is used for the sygusRewSynth() option to synthesize new candidate + * rewrite rules. + */ + std::map<Node, SygusSampler> d_sampler; + /** sampler object for the option cegisSample() + * + * This samples points of the type of the inner variables of the synthesis + * conjecture (d_base_vars). + */ + SygusSampler d_cegis_sampler; + /** cegis sample refine points + * + * Stores the list of indices of sample points in d_cegis_sampler we have + * added as refinement lemmas. + */ + std::unordered_set<unsigned> d_cegis_sample_refine; }; } /* namespace CVC4::theory::quantifiers */ |