From 5eafdb88526da64b60009e30bb45b7e0e47d360b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 1 Mar 2018 21:32:11 -0600 Subject: [PATCH] Create infrastructure for sygus modules (#1632) --- src/Makefile.am | 4 + .../sygus/ce_guided_conjecture.cpp | 203 +++------- .../quantifiers/sygus/ce_guided_conjecture.h | 71 +--- .../sygus/ce_guided_instantiation.cpp | 144 +------ .../sygus/ce_guided_instantiation.h | 3 - src/theory/quantifiers/sygus/cegis.cpp | 354 ++++++++++++++++++ src/theory/quantifiers/sygus/cegis.h | 121 ++++++ src/theory/quantifiers/sygus/sygus_module.cpp | 28 ++ src/theory/quantifiers/sygus/sygus_module.h | 120 ++++++ src/theory/quantifiers/sygus/sygus_pbe.cpp | 31 +- src/theory/quantifiers/sygus/sygus_pbe.h | 68 ++-- 11 files changed, 755 insertions(+), 392 deletions(-) create mode 100644 src/theory/quantifiers/sygus/cegis.cpp create mode 100644 src/theory/quantifiers/sygus/cegis.h create mode 100644 src/theory/quantifiers/sygus/sygus_module.cpp create mode 100644 src/theory/quantifiers/sygus/sygus_module.h diff --git a/src/Makefile.am b/src/Makefile.am index 8e516a00d..4f5730d63 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -448,6 +448,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/single_inv_partition.h \ theory/quantifiers/skolemize.cpp \ theory/quantifiers/skolemize.h \ + theory/quantifiers/sygus/cegis.cpp \ + theory/quantifiers/sygus/cegis.h \ theory/quantifiers/sygus/ce_guided_conjecture.cpp \ theory/quantifiers/sygus/ce_guided_conjecture.h \ theory/quantifiers/sygus/ce_guided_instantiation.cpp \ @@ -468,6 +470,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/sygus/sygus_grammar_norm.h \ theory/quantifiers/sygus/sygus_grammar_red.cpp \ theory/quantifiers/sygus/sygus_grammar_red.h \ + theory/quantifiers/sygus/sygus_module.cpp \ + theory/quantifiers/sygus/sygus_module.h \ theory/quantifiers/sygus/sygus_process_conj.cpp \ theory/quantifiers/sygus/sygus_process_conj.h \ theory/quantifiers/sygus/term_database_sygus.cpp \ diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index 7bcaa0cba..f2a1c334c 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -51,11 +51,20 @@ void collectDisjuncts( Node n, std::vector< Node >& d ) { CegConjecture::CegConjecture(QuantifiersEngine* qe) : d_qe(qe), d_ceg_si(new CegConjectureSingleInv(qe, this)), - d_ceg_pbe(new CegConjecturePbe(qe, this)), d_ceg_proc(new CegConjectureProcess(qe)), d_ceg_gc(new CegGrammarConstructor(qe, this)), + d_ceg_pbe(new CegConjecturePbe(qe, this)), + d_ceg_cegis(new Cegis(qe, this)), + d_master(nullptr), d_refine_count(0), - d_syntax_guided(false) {} + d_syntax_guided(false) +{ + if (options::sygusPbe()) + { + d_modules.push_back(d_ceg_pbe.get()); + } + d_modules.push_back(d_ceg_cegis.get()); +} CegConjecture::~CegConjecture() {} @@ -113,29 +122,21 @@ void CegConjecture::assign( Node q ) { d_base_inst = Rewriter::rewrite(d_qe->getInstantiate()->getInstantiation( d_embed_quant, vars, d_candidates)); Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; - d_base_body = d_base_inst; - if (d_base_body.getKind() == NOT && d_base_body[0].getKind() == FORALL) - { - for (const Node& v : d_base_body[0][0]) - { - d_base_vars.push_back(v); - } - d_base_body = d_base_body[0][1]; - } // register this term with sygus database and other utilities that impact // the enumerative sygus search std::vector< Node > guarded_lemmas; if( !isSingleInvocation() ){ d_ceg_proc->initialize(d_base_inst, d_candidates); - if( options::sygusPbe() ){ - d_ceg_pbe->initialize(d_base_inst, d_candidates, guarded_lemmas); - } else { - for (unsigned i = 0; i < d_candidates.size(); i++) { - Node e = d_candidates[i]; - d_qe->getTermDatabaseSygus()->registerEnumerator(e, e, this); + for (unsigned i = 0, size = d_modules.size(); i < size; i++) + { + if (d_modules[i]->initialize(d_base_inst, d_candidates, guarded_lemmas)) + { + d_master = d_modules[i]; + break; } } + Assert(d_master != nullptr); } if (d_qe->getQuantAttributes()->isSygus(q)) @@ -193,15 +194,6 @@ void CegConjecture::assign( Node q ) { d_qe->getOutputChannel().lemma( lem ); } - // assign the cegis sampler if applicable - if (options::cegisSample() != CEGIS_SAMPLE_NONE) - { - Trace("cegis-sample") << "Initialize sampler for " << d_base_body << "..." - << std::endl; - TypeNode bt = d_base_body.getType(); - d_cegis_sampler.initialize(bt, d_base_vars, options::sygusSamples()); - } - Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() << std::endl; } @@ -241,10 +233,8 @@ void CegConjecture::doSingleInvCheck(std::vector< Node >& lems) { void CegConjecture::doBasicCheck(std::vector< Node >& lems) { std::vector< Node > model_terms; - std::vector< Node > clist; - getCandidateList( clist, true ); - Assert( clist.size()==d_quant[0].getNumChildren() ); - getModelValues( clist, model_terms ); + Assert(d_candidates.size() == d_quant[0].getNumChildren()); + getModelValues(d_candidates, model_terms); if (d_qe->getInstantiate()->addInstantiation(d_quant, model_terms)) { //record the instantiation @@ -257,62 +247,57 @@ void CegConjecture::doBasicCheck(std::vector< Node >& lems) { bool CegConjecture::needsRefinement() { return !d_ce_sk.empty(); } +void CegConjecture::doCheck(std::vector& lems) +{ + Assert(d_master != nullptr); -void CegConjecture::getCandidateList( std::vector< Node >& clist, bool forceOrig ) { - if( d_ceg_pbe->isPbe() && !forceOrig ){ - d_ceg_pbe->getCandidateList( d_candidates, clist ); - }else{ - clist.insert( clist.end(), d_candidates.begin(), d_candidates.end() ); - } -} + // get the list of terms that the master strategy is interested in + std::vector terms; + d_master->getTermList(d_candidates, terms); -bool CegConjecture::constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, std::vector< Node >& candidate_values, - std::vector< Node >& lems ) { - Assert( clist.size()==model_values.size() ); - if( d_ceg_pbe->isPbe() ){ - return d_ceg_pbe->constructCandidates( clist, model_values, d_candidates, candidate_values, lems ); - }else{ - Assert( model_values.size()==d_candidates.size() ); - candidate_values.insert( candidate_values.end(), model_values.begin(), model_values.end() ); - } - return true; -} + // get their model value + std::vector enum_values; + getModelValues(terms, enum_values); -void CegConjecture::doCheck(std::vector< Node >& lems, std::vector< Node >& model_values) { - std::vector< Node > clist; - getCandidateList( clist ); - std::vector< Node > c_model_values; + std::vector candidate_values; Trace("cegqi-check") << "CegConjuncture : check, build candidates..." << std::endl; - bool constructed_cand = constructCandidates( clist, model_values, c_model_values, lems ); + bool constructed_cand = d_master->constructCandidates( + terms, enum_values, d_candidates, candidate_values, lems); + + NodeManager* nm = NodeManager::currentNM(); //must get a counterexample to the value of the current candidate Node inst; if( constructed_cand ){ if( Trace.isOn("cegqi-check") ){ Trace("cegqi-check") << "CegConjuncture : check candidate : " << std::endl; - for( unsigned i=0; i " << c_model_values[i] << std::endl; + for (unsigned i = 0, size = candidate_values.size(); i < size; i++) + { + Trace("cegqi-check") << " " << i << " : " << d_candidates[i] << " -> " + << candidate_values[i] << std::endl; } } - Assert( c_model_values.size()==d_candidates.size() ); - inst = d_base_inst.substitute( d_candidates.begin(), d_candidates.end(), c_model_values.begin(), c_model_values.end() ); + Assert(candidate_values.size() == d_candidates.size()); + inst = d_base_inst.substitute(d_candidates.begin(), + d_candidates.end(), + candidate_values.begin(), + candidate_values.end()); }else{ inst = d_base_inst; } //check whether we will run CEGIS on inner skolem variables - bool sk_refine = ( !isGround() || d_refine_count==0 ) && ( !d_ceg_pbe->isPbe() || constructed_cand ); + bool sk_refine = (!isGround() || d_refine_count == 0) && constructed_cand; if( sk_refine ){ if (options::cegisSample() == CEGIS_SAMPLE_TRUST) { // we have that the current candidate passed a sample test // since we trust sampling in this mode, we assert there is no // counterexample to the conjecture here. - NodeManager* nm = NodeManager::currentNM(); Node lem = nm->mkNode(OR, d_quant.negate(), nm->mkConst(false)); lem = getStreamGuardedLemma(lem); lems.push_back(lem); - recordInstantiation(c_model_values); + recordInstantiation(candidate_values); return; } Assert( d_ce_sk.empty() ); @@ -352,7 +337,7 @@ void CegConjecture::doCheck(std::vector< Node >& lems, std::vector< Node >& mode } } if( constructed_cand ){ - Node lem = NodeManager::currentNM()->mkNode( OR, ic ); + Node lem = nm->mkNode(OR, ic); lem = Rewriter::rewrite( lem ); //eagerly unfold applications of evaluation function if( options::sygusDirectEval() ){ @@ -362,7 +347,7 @@ void CegConjecture::doCheck(std::vector< Node >& lems, std::vector< Node >& mode } lem = getStreamGuardedLemma(lem); lems.push_back( lem ); - recordInstantiation( c_model_values ); + recordInstantiation(candidate_values); } } @@ -433,7 +418,7 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){ base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); base_lem = Rewriter::rewrite( base_lem ); - d_refinement_lemmas.push_back(base_lem); + d_master->registerRefinementLemma(base_lem); Node lem = NodeManager::currentNM()->mkNode(OR, getGuard().negate(), base_lem); @@ -533,6 +518,7 @@ Node CegConjecture::getNextDecisionRequest( unsigned& priority ) { return curr_stream_guard; }else{ if( !value ){ + Assert(d_master != nullptr); Trace("cegqi-debug") << "getNextDecision : we have a new solution since stream guard was propagated false: " << curr_stream_guard << std::endl; // we have generated a solution, print it // get the current output stream @@ -545,14 +531,15 @@ Node CegConjecture::getNextDecisionRequest( unsigned& priority ) { // We will not refine the current candidate solution since it is a solution // thus, we clear information regarding the current refinement d_ce_sk.clear(); - // However, we need to exclude the current solution using an explicit refinement - // so that we proceed to the next solution. - std::vector< Node > clist; - getCandidateList( clist ); + // However, we need to exclude the current solution using an + // explicit refinement + // so that we proceed to the next solution. + std::vector terms; + d_master->getTermList(d_candidates, terms); Trace("cegqi-debug") << "getNextDecision : solution was : " << std::endl; std::vector< Node > exp; - for( unsigned i=0; i& vals, - std::vector& lems) -{ - if (Trace.isOn("cegis-sample")) - { - Trace("cegis-sample") << "Check sampling for candidate solution" - << std::endl; - for (unsigned i = 0, size = vals.size(); i < size; i++) - { - Trace("cegis-sample") - << " " << d_candidates[i] << " -> " << vals[i] << std::endl; - } - } - Assert(vals.size() == d_candidates.size()); - Node sbody = d_base_body.substitute( - d_candidates.begin(), d_candidates.end(), vals.begin(), vals.end()); - Trace("cegis-sample-debug") << "Sample " << sbody << std::endl; - // do eager unfolding - std::map visited_n; - sbody = d_qe->getTermDatabaseSygus()->getEagerUnfold(sbody, visited_n); - Trace("cegis-sample") << "Sample (after unfolding): " << sbody << std::endl; - - NodeManager* nm = NodeManager::currentNM(); - for (unsigned i = 0, size = d_cegis_sampler.getNumSamplePoints(); i < size; - i++) - { - if (d_cegis_sample_refine.find(i) == d_cegis_sample_refine.end()) - { - Node ev = d_cegis_sampler.evaluate(sbody, i); - Trace("cegis-sample-debug") - << "...evaluate point #" << i << " to " << ev << std::endl; - Assert(ev.isConst()); - Assert(ev.getType().isBoolean()); - if (!ev.getConst()) - { - Trace("cegis-sample-debug") << "...false for point #" << i << std::endl; - // mark this as a CEGIS point (no longer sampled) - d_cegis_sample_refine.insert(i); - std::vector vars; - std::vector pt; - d_cegis_sampler.getSamplePoint(i, vars, pt); - Assert(d_base_vars.size() == pt.size()); - Node rlem = d_base_body.substitute( - d_base_vars.begin(), d_base_vars.end(), pt.begin(), pt.end()); - rlem = Rewriter::rewrite(rlem); - if (std::find( - d_refinement_lemmas.begin(), d_refinement_lemmas.end(), rlem) - == d_refinement_lemmas.end()) - { - if (Trace.isOn("cegis-sample")) - { - Trace("cegis-sample") << " false for point #" << i << " : "; - for (const Node& cn : pt) - { - Trace("cegis-sample") << cn << " "; - } - Trace("cegis-sample") << std::endl; - } - Trace("cegqi-engine") << " *** Refine by sampling" << std::endl; - d_refinement_lemmas.push_back(rlem); - // if trust, we are not interested in sending out refinement lemmas - if (options::cegisSample() != CEGIS_SAMPLE_TRUST) - { - Node lem = nm->mkNode(OR, getGuard().negate(), rlem); - lems.push_back(lem); - } - return true; - } - else - { - Trace("cegis-sample-debug") << "...duplicate." << std::endl; - } - } - } - } - return false; -} - }/* namespace CVC4::theory::quantifiers */ }/* namespace CVC4::theory */ }/* namespace CVC4 */ diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h index 1ef8fef10..9f3335ee2 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h @@ -20,9 +20,10 @@ #include -#include "theory/quantifiers/sygus/sygus_pbe.h" #include "theory/quantifiers/sygus/ce_guided_single_inv.h" +#include "theory/quantifiers/sygus/cegis.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" +#include "theory/quantifiers/sygus/sygus_pbe.h" #include "theory/quantifiers/sygus/sygus_process_conj.h" #include "theory/quantifiers/sygus_sampler.h" #include "theory/quantifiers_engine.h" @@ -57,8 +58,6 @@ public: bool needsCheck( std::vector< Node >& lem ); /** whether the conjecture is waiting for a call to doRefine below */ bool needsRefinement(); - /** get the list of candidates */ - void getCandidateList( std::vector< Node >& clist, bool forceOrig = false ); /** do single invocation check * This updates Gamma for an iteration of step 2 of Figure 1 of Reynolds et al CAV 2015. */ @@ -66,7 +65,7 @@ public: /** do syntax-guided enumerative check * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015. */ - void doCheck(std::vector< Node >& lems, std::vector< Node >& model_values); + void doCheck(std::vector& lems); /** do basic check * This is called for non-SyGuS synthesis conjectures */ @@ -118,26 +117,6 @@ public: /** get model value for term n */ Node getModelValue( Node n ); - //-----------------------------------refinement lemmas - /** get number of refinement lemmas we have added so far */ - unsigned getNumRefinementLemmas() { return d_refinement_lemmas.size(); } - /** 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]; } - /** 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& vals, - std::vector& lems); - //-----------------------------------end refinement lemmas - /** get program by examples utility */ CegConjecturePbe* getPbe() { return d_ceg_pbe.get(); } /** get utility for static preprocessing and analysis of conjectures */ @@ -152,12 +131,26 @@ private: QuantifiersEngine * d_qe; /** single invocation utility */ std::unique_ptr d_ceg_si; - /** program by examples utility */ - std::unique_ptr d_ceg_pbe; /** utility for static preprocessing and analysis of conjectures */ std::unique_ptr d_ceg_proc; /** grammar utility */ std::unique_ptr d_ceg_gc; + + //------------------------modules + /** program by examples module */ + std::unique_ptr d_ceg_pbe; + /** CEGIS module */ + std::unique_ptr d_ceg_cegis; + /** the set of active modules (subset of the above list) */ + std::vector d_modules; + /** master module + * + * This is the module (one of those above) that takes sole responsibility + * for this conjecture, determined during assign(...). + */ + SygusModule* d_master; + //------------------------end modules + /** list of constants for quantified formula * The outer Skolems for the negation of d_embed_quant. */ @@ -167,13 +160,6 @@ private: * 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 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 */ @@ -182,10 +168,6 @@ private: /** current extential quantifeirs whose couterexamples we must refine */ std::vector< std::vector< Node > > d_ce_sk; - //-----------------------------------refinement lemmas - /** refinement lemmas */ - std::vector< Node > d_refinement_lemmas; - //-----------------------------------end refinement lemmas /** the asserted (negated) conjecture */ Node d_quant; @@ -203,9 +185,6 @@ private: std::map< Node, CandidateInfo > d_cinfo; /** number of times we have called doRefine */ unsigned d_refine_count; - /** construct candidates */ - bool constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, - std::vector< Node >& candidate_values, std::vector< Node >& lems ); /** get candidadate */ Node getCandidate( unsigned int i ) { return d_candidates[i]; } /** record instantiation (this is used to construct solutions later) */ @@ -262,18 +241,6 @@ private: * rewrite rules. */ std::map 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 d_cegis_sample_refine; }; } /* namespace CVC4::theory::quantifiers */ diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp index 35098f5ea..125682e8c 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp @@ -21,8 +21,6 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" -//FIXME : remove this include (github issue #1156) -#include "theory/bv/theory_bv_rewriter.h" using namespace CVC4::kind; using namespace std; @@ -125,61 +123,10 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Trace("cegqi-engine") << " ...try single invocation." << std::endl; return; } - //ignore return value here - std::vector< Node > clist; - conj->getCandidateList( clist ); - std::vector< Node > model_values; - conj->getModelValues( clist, model_values ); - if( options::sygusDirectEval() ){ - bool addedEvalLemmas = false; - if( options::sygusCRefEval() ){ - Trace("cegqi-engine") << " *** Do conjecture refinement evaluation..." << std::endl; - // see if any refinement lemma is refuted by evaluation - std::vector< Node > cre_lems; - getCRefEvaluationLemmas( conj, clist, model_values, cre_lems ); - if( !cre_lems.empty() ){ - for( unsigned j=0; jaddLemma( lem ) ){ - Trace("cegqi-lemma") << "Cegqi::Lemma : cref evaluation : " << lem << std::endl; - addedEvalLemmas = true; - } - } - if( addedEvalLemmas ){ - //return; - } - } - } - Trace("cegqi-engine") << " *** Do direct evaluation..." << std::endl; - std::vector< Node > eager_terms; - std::vector< Node > eager_vals; - std::vector< Node > eager_exps; - for( unsigned j=0; j " << model_values[j] << std::endl; - d_quantEngine->getTermDatabaseSygus()->registerModelValue( clist[j], model_values[j], eager_terms, eager_vals, eager_exps ); - } - Trace("cegqi-debug") << "...produced " << eager_terms.size() << " eager evaluation lemmas." << std::endl; - if( !eager_terms.empty() ){ - for( unsigned j=0; jmkNode( kind::OR, eager_exps[j].negate(), eager_terms[j].eqNode( eager_vals[j] ) ); - if( d_quantEngine->getTheoryEngine()->isTheoryEnabled(THEORY_BV) ){ - //FIXME: hack to incorporate hacks from BV for division by zero (github issue #1156) - lem = bv::TheoryBVRewriter::eliminateBVSDiv( lem ); - } - if( d_quantEngine->addLemma( lem ) ){ - Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem << std::endl; - addedEvalLemmas = true; - } - } - } - if( addedEvalLemmas ){ - return; - } - } Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl; std::vector< Node > cclems; - conj->doCheck( cclems, model_values ); + conj->doCheck(cclems); bool addedLemma = false; for( unsigned i=0; i& vs, std::vector< Node >& ms, std::vector< Node >& lems ) { - Trace("sygus-cref-eval") << "Cref eval : conjecture has " << conj->getNumRefinementLemmas() << " refinement lemmas." << std::endl; - unsigned nlemmas = conj->getNumRefinementLemmas(); - if (nlemmas > 0 || options::cegisSample() != CEGIS_SAMPLE_NONE) - { - Assert( vs.size()==ms.size() ); - - TermDbSygus* tds = d_quantEngine->getTermDatabaseSygus(); - Node nfalse = d_quantEngine->getTermUtil()->d_false; - Node neg_guard = conj->getGuard().negate(); - for (unsigned i = 0; i <= nlemmas; i++) - { - if (i == nlemmas) - { - bool addedSample = false; - // find a new one by sampling, if applicable - if (options::cegisSample() != CEGIS_SAMPLE_NONE) - { - addedSample = conj->sampleAddRefinementLemma(ms, lems); - } - if (!addedSample) - { - return; - } - } - Node lem; - std::map< Node, Node > visited; - std::map< Node, std::vector< Node > > exp; - lem = conj->getRefinementLemma(i); - if( !lem.isNull() ){ - std::vector< Node > lem_conj; - //break into conjunctions - if( lem.getKind()==kind::AND ){ - for( unsigned i=0; igetTermUtil()->d_false ){ - std::vector< Node > msu; - std::vector< Node > mexp; - msu.insert( msu.end(), ms.begin(), ms.end() ); - for( unsigned k=0; kisAssigned() ) { diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.h b/src/theory/quantifiers/sygus/ce_guided_instantiation.h index 087836d5a..1b1d5e44b 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.h +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.h @@ -33,9 +33,6 @@ private: CegConjecture * d_conj; /** last instantiation by single invocation module? */ bool d_last_inst_si; -private: //for direct evaluation - /** get refinement evaluation */ - void getCRefEvaluationLemmas( CegConjecture * conj, std::vector< Node >& vs, std::vector< Node >& ms, std::vector< Node >& lems ); private: /** check conjecture */ void checkCegConjecture( CegConjecture * conj ); diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp new file mode 100644 index 000000000..a571c85fb --- /dev/null +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -0,0 +1,354 @@ +/********************* */ +/*! \file cegis.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of cegis + **/ + +#include "theory/quantifiers/sygus/cegis.h" +#include "options/quantifiers_options.h" +#include "theory/quantifiers/sygus/ce_guided_conjecture.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" +// FIXME : remove these includes (github issue #1156) +#include "theory/bv/theory_bv_rewriter.h" +#include "theory/theory_engine.h" + +using namespace std; +using namespace CVC4::kind; +using namespace CVC4::context; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p) : SygusModule(qe, p) {} +bool Cegis::initialize(Node n, + const std::vector& candidates, + std::vector& lemmas) +{ + d_base_body = n; + if (d_base_body.getKind() == NOT && d_base_body[0].getKind() == FORALL) + { + for (const Node& v : d_base_body[0][0]) + { + d_base_vars.push_back(v); + } + d_base_body = d_base_body[0][1]; + } + + // assign the cegis sampler if applicable + if (options::cegisSample() != CEGIS_SAMPLE_NONE) + { + Trace("cegis-sample") << "Initialize sampler for " << d_base_body << "..." + << std::endl; + TypeNode bt = d_base_body.getType(); + d_cegis_sampler.initialize(bt, d_base_vars, options::sygusSamples()); + } + + // initialize an enumerator for each candidate + TermDbSygus* tds = d_qe->getTermDatabaseSygus(); + for (unsigned i = 0; i < candidates.size(); i++) + { + tds->registerEnumerator(candidates[i], candidates[i], d_parent); + } + return true; +} + +void Cegis::getTermList(const std::vector& candidates, + std::vector& enums) +{ + enums.insert(enums.end(), candidates.begin(), candidates.end()); +} + +/** construct candidate */ +bool Cegis::constructCandidates(const std::vector& enums, + const std::vector& enum_values, + const std::vector& candidates, + std::vector& candidate_values, + std::vector& lems) +{ + candidate_values.insert( + candidate_values.end(), enum_values.begin(), enum_values.end()); + + if (options::sygusDirectEval()) + { + NodeManager* nm = NodeManager::currentNM(); + bool addedEvalLemmas = false; + if (options::sygusCRefEval()) + { + Trace("cegqi-engine") << " *** Do conjecture refinement evaluation..." + << std::endl; + // see if any refinement lemma is refuted by evaluation + std::vector cre_lems; + getRefinementEvalLemmas(candidates, candidate_values, cre_lems); + if (!cre_lems.empty()) + { + for (unsigned j = 0; j < cre_lems.size(); j++) + { + Node lem = cre_lems[j]; + if (d_qe->addLemma(lem)) + { + Trace("cegqi-lemma") << "Cegqi::Lemma : cref evaluation : " << lem + << std::endl; + addedEvalLemmas = true; + } + } + // we could, but do not return here. + // experimentally, it is better to add the lemmas below as well, + // in parallel. + } + } + Trace("cegqi-engine") << " *** Do direct evaluation..." << std::endl; + std::vector eager_terms; + std::vector eager_vals; + std::vector eager_exps; + TermDbSygus* tds = d_qe->getTermDatabaseSygus(); + for (unsigned j = 0, size = candidates.size(); j < size; j++) + { + Trace("cegqi-debug") << " register " << candidates[j] << " -> " + << candidate_values[j] << std::endl; + tds->registerModelValue(candidates[j], + candidate_values[j], + eager_terms, + eager_vals, + eager_exps); + } + Trace("cegqi-debug") << "...produced " << eager_terms.size() + << " eager evaluation lemmas." << std::endl; + + for (unsigned j = 0, size = eager_terms.size(); j < size; j++) + { + Node lem = nm->mkNode(kind::OR, + eager_exps[j].negate(), + eager_terms[j].eqNode(eager_vals[j])); + if (d_qe->getTheoryEngine()->isTheoryEnabled(THEORY_BV)) + { + // FIXME: hack to incorporate hacks from BV for division by zero + // (github issue #1156) + lem = bv::TheoryBVRewriter::eliminateBVSDiv(lem); + } + if (d_qe->addLemma(lem)) + { + Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem + << std::endl; + addedEvalLemmas = true; + } + } + if (addedEvalLemmas) + { + return false; + } + } + + return true; +} + +void Cegis::registerRefinementLemma(Node lem) +{ + d_refinement_lemmas.push_back(lem); +} + +void Cegis::getRefinementEvalLemmas(const std::vector& vs, + const std::vector& ms, + std::vector& lems) +{ + Trace("sygus-cref-eval") << "Cref eval : conjecture has " + << getNumRefinementLemmas() << " refinement lemmas." + << std::endl; + unsigned nlemmas = getNumRefinementLemmas(); + if (nlemmas > 0 || options::cegisSample() != CEGIS_SAMPLE_NONE) + { + Assert(vs.size() == ms.size()); + + TermDbSygus* tds = d_qe->getTermDatabaseSygus(); + NodeManager* nm = NodeManager::currentNM(); + + Node nfalse = nm->mkConst(false); + Node neg_guard = d_parent->getGuard().negate(); + for (unsigned i = 0; i <= nlemmas; i++) + { + if (i == nlemmas) + { + bool addedSample = false; + // find a new one by sampling, if applicable + if (options::cegisSample() != CEGIS_SAMPLE_NONE) + { + addedSample = sampleAddRefinementLemma(vs, ms, lems); + } + if (!addedSample) + { + return; + } + } + Node lem; + std::map visited; + std::map > exp; + lem = getRefinementLemma(i); + if (!lem.isNull()) + { + std::vector lem_conj; + // break into conjunctions + if (lem.getKind() == kind::AND) + { + for (unsigned i = 0; i < lem.getNumChildren(); i++) + { + lem_conj.push_back(lem[i]); + } + } + else + { + lem_conj.push_back(lem); + } + EvalSygusInvarianceTest vsit; + for (unsigned j = 0; j < lem_conj.size(); j++) + { + Node lemc = lem_conj[j]; + Trace("sygus-cref-eval") << "Check refinement lemma conjunct " << lemc + << " against current model." << std::endl; + Trace("sygus-cref-eval2") << "Check refinement lemma conjunct " + << lemc << " against current model." + << std::endl; + Node cre_lem; + Node lemcs = + lemc.substitute(vs.begin(), vs.end(), ms.begin(), ms.end()); + Trace("sygus-cref-eval2") << "...under substitution it is : " << lemcs + << std::endl; + Node lemcsu = vsit.doEvaluateWithUnfolding(tds, lemcs); + Trace("sygus-cref-eval2") << "...after unfolding is : " << lemcsu + << std::endl; + if (lemcsu.isConst() && !lemcsu.getConst()) + { + std::vector msu; + std::vector mexp; + msu.insert(msu.end(), ms.begin(), ms.end()); + for (unsigned k = 0; k < vs.size(); k++) + { + vsit.setUpdatedTerm(msu[k]); + msu[k] = vs[k]; + // substitute for everything except this + Node sconj = + lemc.substitute(vs.begin(), vs.end(), msu.begin(), msu.end()); + vsit.init(sconj, vs[k], nfalse); + // get minimal explanation for this + Node ut = vsit.getUpdatedTerm(); + Trace("sygus-cref-eval2-debug") + << " compute min explain of : " << vs[k] << " = " << ut + << std::endl; + tds->getExplain()->getExplanationFor(vs[k], ut, mexp, vsit); + msu[k] = ut; + } + if (!mexp.empty()) + { + Node en = + mexp.size() == 1 ? mexp[0] : nm->mkNode(kind::AND, mexp); + cre_lem = nm->mkNode(kind::OR, en.negate(), neg_guard); + } + else + { + cre_lem = neg_guard; + } + } + if (!cre_lem.isNull()) + { + if (std::find(lems.begin(), lems.end(), cre_lem) == lems.end()) + { + Trace("sygus-cref-eval") << "...produced lemma : " << cre_lem + << std::endl; + lems.push_back(cre_lem); + } + } + } + } + } + } +} + +bool Cegis::sampleAddRefinementLemma(const std::vector& candidates, + const std::vector& vals, + std::vector& lems) +{ + if (Trace.isOn("cegis-sample")) + { + Trace("cegis-sample") << "Check sampling for candidate solution" + << std::endl; + for (unsigned i = 0, size = vals.size(); i < size; i++) + { + Trace("cegis-sample") << " " << candidates[i] << " -> " << vals[i] + << std::endl; + } + } + Assert(vals.size() == candidates.size()); + Node sbody = d_base_body.substitute( + candidates.begin(), candidates.end(), vals.begin(), vals.end()); + Trace("cegis-sample-debug") << "Sample " << sbody << std::endl; + // do eager unfolding + std::map visited_n; + sbody = d_qe->getTermDatabaseSygus()->getEagerUnfold(sbody, visited_n); + Trace("cegis-sample") << "Sample (after unfolding): " << sbody << std::endl; + + NodeManager* nm = NodeManager::currentNM(); + for (unsigned i = 0, size = d_cegis_sampler.getNumSamplePoints(); i < size; + i++) + { + if (d_cegis_sample_refine.find(i) == d_cegis_sample_refine.end()) + { + Node ev = d_cegis_sampler.evaluate(sbody, i); + Trace("cegis-sample-debug") << "...evaluate point #" << i << " to " << ev + << std::endl; + Assert(ev.isConst()); + Assert(ev.getType().isBoolean()); + if (!ev.getConst()) + { + Trace("cegis-sample-debug") << "...false for point #" << i << std::endl; + // mark this as a CEGIS point (no longer sampled) + d_cegis_sample_refine.insert(i); + std::vector vars; + std::vector pt; + d_cegis_sampler.getSamplePoint(i, vars, pt); + Assert(d_base_vars.size() == pt.size()); + Node rlem = d_base_body.substitute( + d_base_vars.begin(), d_base_vars.end(), pt.begin(), pt.end()); + rlem = Rewriter::rewrite(rlem); + if (std::find( + d_refinement_lemmas.begin(), d_refinement_lemmas.end(), rlem) + == d_refinement_lemmas.end()) + { + if (Trace.isOn("cegis-sample")) + { + Trace("cegis-sample") << " false for point #" << i << " : "; + for (const Node& cn : pt) + { + Trace("cegis-sample") << cn << " "; + } + Trace("cegis-sample") << std::endl; + } + Trace("cegqi-engine") << " *** Refine by sampling" << std::endl; + d_refinement_lemmas.push_back(rlem); + // if trust, we are not interested in sending out refinement lemmas + if (options::cegisSample() != CEGIS_SAMPLE_TRUST) + { + Node lem = nm->mkNode(OR, d_parent->getGuard().negate(), rlem); + lems.push_back(lem); + } + return true; + } + else + { + Trace("cegis-sample-debug") << "...duplicate." << std::endl; + } + } + } + } + return false; +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h new file mode 100644 index 000000000..2cb668fa1 --- /dev/null +++ b/src/theory/quantifiers/sygus/cegis.h @@ -0,0 +1,121 @@ +/********************* */ +/*! \file cegis.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief cegis + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__CEGIS_H +#define __CVC4__THEORY__QUANTIFIERS__CEGIS_H + +#include +#include "theory/quantifiers/sygus/sygus_module.h" +#include "theory/quantifiers/sygus_sampler.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** Cegis + * + * The default sygus module for synthesis, counterexample-guided inductive + * synthesis (CEGIS). + * + * It initializes a list of sygus enumerators that are one-to-one with + * candidates, and returns a list of candidates that are the model values + * of these enumerators on calls to constructCandidates. + * + * It implements an optimization (getRefinementEvalLemmas) that evaluates all + * previous refinement lemmas for a term before returning it as a candidate + * in calls to constructCandidates. + */ +class Cegis : public SygusModule +{ + public: + Cegis(QuantifiersEngine* qe, CegConjecture* p); + ~Cegis() {} + /** initialize */ + virtual bool initialize(Node n, + const std::vector& candidates, + std::vector& lemmas) override; + /** get term list */ + virtual void getTermList(const std::vector& candidates, + std::vector& enums) override; + /** construct candidate */ + virtual bool constructCandidates(const std::vector& enums, + const std::vector& enum_values, + const std::vector& candidates, + std::vector& candidate_values, + std::vector& lems) override; + /** register refinement lemma */ + virtual void registerRefinementLemma(Node lem) override; + + private: + /** If CegConjecture::d_base_inst is exists y. P( d, y ), then this is y. */ + std::vector d_base_vars; + /** + * If CegConjecture::d_base_inst is exists y. P( d, y ), then this is the + * formula P( CegConjecture::d_candidates, y ). + */ + Node d_base_body; + + //-----------------------------------refinement lemmas + /** refinement lemmas */ + std::vector d_refinement_lemmas; + /** get number of refinement lemmas we have added so far */ + unsigned getNumRefinementLemmas() { return d_refinement_lemmas.size(); } + /** 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]; } + /** 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(const std::vector& candidates, + const std::vector& vals, + std::vector& lems); + //-----------------------------------end refinement lemmas + + /** Get refinement evaluation lemmas + * + * Given a candidate solution ms for candidates vs, this function adds lemmas + * to lems based on evaluating the conjecture, instantiated for ms, on lemmas + * for previous refinements (d_refinement_lemmas). + */ + void getRefinementEvalLemmas(const std::vector& vs, + const std::vector& ms, + std::vector& lems); + /** 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 d_cegis_sample_refine; +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__CEGIS_H */ diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp new file mode 100644 index 000000000..19e064350 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_module.cpp @@ -0,0 +1,28 @@ +/********************* */ +/*! \file sygus_module.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of sygus_module + **/ + +#include "theory/quantifiers/sygus/sygus_module.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +SygusModule::SygusModule(QuantifiersEngine* qe, CegConjecture* p) + : d_qe(qe), d_parent(p) +{ +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h new file mode 100644 index 000000000..230ea7a61 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -0,0 +1,120 @@ +/********************* */ +/*! \file sygus_module.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief sygus_module + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H +#define __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H + +#include +#include "expr/node.h" +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class CegConjecture; + +/** SygusModule + * + * This is the base class of sygus modules, owned by CegConjecture. The purpose + * of this class is to, when applicable, suggest candidate solutions for + * CegConjecture to test. + * + * In more detail, an instance of the conjecture class (CegConjecture) creates + * the negated deep embedding form of the synthesis conjecture. In the + * following, assume this is: + * forall d. exists x. P( d, x ) + * where d are of sygus datatype type. The "base instantiation" of this + * conjecture (see CegConjecture::d_base_inst) is the formula: + * exists y. P( k, y ) + * where k are the "candidate" variables for the conjecture. + * + * Modules implement an initialize function, which determines whether the module + * will take responsibility for the given conjecture. + */ +class SygusModule +{ + public: + SygusModule(QuantifiersEngine* qe, CegConjecture* p); + ~SygusModule() {} + /** initialize + * + * n is the "base instantiation" of the deep-embedding version of the + * synthesis conjecture under candidates (see CegConjecture::d_base_inst). + * + * This function may add lemmas to the argument lemmas, which should be + * sent out on the output channel of quantifiers by the caller. + * + * This function returns true if this module will take responsibility for + * constructing candidates for the given conjecture. + */ + virtual bool initialize(Node n, + const std::vector& candidates, + std::vector& lemmas) = 0; + /** get term list + * + * This gets the list of terms that will appear as arguments to a subsequent + * call to constructCandidates. + */ + virtual void getTermList(const std::vector& candidates, + std::vector& terms) = 0; + /** construct candidate + * + * This function takes as input: + * terms : the terms returned by a call to getTermList, + * term_values : the current model values of terms, + * candidates : the list of candidates. + * + * If this function returns true, it adds to candidate_values a list of terms + * of the same length and type as candidates that are candidate solutions + * to the synthesis conjecture in question. This candidate { v } will then be + * tested by testing the (un)satisfiablity of P( v, k' ) for fresh k' by the + * caller. + * + * This function may also add lemmas to lems, which are sent out as lemmas + * on the output channel of quantifiers by the caller. For an example of + * such lemmas, see SygusPbe::constructCandidates. + * + * This function may return false if it does not have a candidate it wants + * to test on this iteration. In this case, lems should be non-empty. + */ + virtual bool constructCandidates(const std::vector& terms, + const std::vector& term_values, + const std::vector& candidates, + std::vector& candidate_values, + std::vector& lems) = 0; + /** register refinement lemma + * + * Assume this module, on a previous call to constructCandidates, added the + * value { v } to candidate_values for candidates = { k }. This function is + * called if the base instantiation of the synthesis conjecture has a model + * under this substitution. In particular, in the above example, this function + * is called when the refinement lemma P( v, k' ) has a model. The argument + * lem in the call to this function is P( v, k' ). + */ + virtual void registerRefinementLemma(Node lem) {} + protected: + /** reference to quantifier engine */ + QuantifiersEngine* d_qe; + /** reference to the parent conjecture */ + CegConjecture* d_parent; +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */ diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 17c4c482d..36e883848 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -97,8 +97,8 @@ std::ostream& operator<<(std::ostream& os, StrategyType st) } CegConjecturePbe::CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p) - : d_qe(qe), - d_parent(p){ + : SygusModule(qe, p) +{ d_tds = d_qe->getTermDatabaseSygus(); d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -176,8 +176,8 @@ void CegConjecturePbe::collectExamples( Node n, std::map< Node, bool >& visited, } } -void CegConjecturePbe::initialize(Node n, - std::vector& candidates, +bool CegConjecturePbe::initialize(Node n, + const std::vector& candidates, std::vector& lemmas) { Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl; @@ -234,13 +234,7 @@ void CegConjecturePbe::initialize(Node n, } } } - if( !d_is_pbe ){ - Trace("sygus-unif") << "Do not do PBE optimizations, register..." << std::endl; - for( unsigned i=0; igetTermDatabaseSygus()->registerEnumerator( - candidates[i], candidates[i], d_parent); - } - } + return d_is_pbe; } Node CegConjecturePbe::PbeTrie::addPbeExample(TypeNode etn, Node e, Node b, @@ -1077,7 +1071,9 @@ void CegConjecturePbe::staticLearnRedundantOps( // ------------------------------------------- solution construction from enumeration -void CegConjecturePbe::getCandidateList( std::vector< Node >& candidates, std::vector< Node >& clist ) { +void CegConjecturePbe::getTermList(const std::vector& candidates, + std::vector& terms) +{ Valuation& valuation = d_qe->getValuation(); for( unsigned i=0; i& candidates, std::v Node gstatus = valuation.getSatValue(it->second.d_active_guard); if (!gstatus.isNull() && gstatus.getConst()) { - clist.push_back( e ); + terms.push_back(e); } } } } } -bool CegConjecturePbe::constructCandidates( std::vector< Node >& enums, std::vector< Node >& enum_values, - std::vector< Node >& candidates, std::vector< Node >& candidate_values, - std::vector< Node >& lems ) { +bool CegConjecturePbe::constructCandidates(const std::vector& enums, + const std::vector& enum_values, + const std::vector& candidates, + std::vector& candidate_values, + std::vector& lems) +{ Assert( enums.size()==enum_values.size() ); if( !enums.empty() ){ unsigned min_term_size = 0; diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index ce1f2bf5e..2b800db81 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -18,7 +18,7 @@ #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H #include "context/cdhashmap.h" -#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/sygus/sygus_module.h" namespace CVC4 { namespace theory { @@ -158,48 +158,58 @@ class CegConjecture; * This class is not designed to work in incremental mode, since there is no way * to specify incremental problems in SyguS. */ -class CegConjecturePbe { +class CegConjecturePbe : public SygusModule +{ public: CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p); ~CegConjecturePbe(); /** initialize this class * - * n is the "base instantiation" of the deep-embedding version of - * the synthesis conjecture under "candidates". - * (see CegConjecture::d_base_inst) - * * This function may add lemmas to the vector lemmas corresponding * to initial lemmas regarding static analysis of enumerators it * introduced. For example, we may say that the top-level symbol * of an enumerator is not ITE if it is being used to construct * return values for decision trees. */ - void initialize(Node n, - std::vector& candidates, - std::vector& lemmas); - /** get candidate list + bool initialize(Node n, + const std::vector& candidates, + std::vector& lemmas) override; + /** get term list + * * Adds all active enumerators associated with functions-to-synthesize in - * candidates to clist. + * candidates to terms. */ - void getCandidateList(std::vector& candidates, - std::vector& clist); + void getTermList(const std::vector& candidates, + std::vector& terms) override; /** construct candidates - * (1) Indicates that the list of enumerators in "enums" currently have model - * values "enum_values". - * (2) Asks whether based on these new enumerated values, we can construct a - * solution for - * the functions-to-synthesize in "candidates". If so, this function - * returns "true" and - * adds solutions for candidates into "candidate_values". - * During this class, this class may add auxiliary lemmas to "lems", which the - * caller should send on the output channel via lemma(...). - */ - bool constructCandidates(std::vector& enums, - std::vector& enum_values, - std::vector& candidates, + * + * This function attempts to use unification-based approaches for constructing + * solutions for all functions-to-synthesize (indicated by candidates). These + * approaches include decision tree learning and a divide-and-conquer + * algorithm based on string concatenation. + * + * Calls to this function are such that terms is the list of active + * enumerators (returned by getTermList), and term_values are their current + * model values. This function registers { terms -> terms_values } in + * the database of values that have been enumerated, which are in turn used + * for constructing candidate solutions when possible. + * + * This function also excludes models where (terms = terms_values) by adding + * blocking clauses to lems. For example, for grammar: + * A -> A+A | x | 1 | 0 + * and a call where terms = { d } and term_values = { +( x, 1 ) }, it adds: + * ~G V ~is_+( d ) V ~is_x( d.1 ) V ~is_1( d.2 ) + * to lems, where G is active guard of the enumerator d (see + * TermDatabaseSygus::getActiveGuardForEnumerator). This blocking clause + * indicates that d should not be given the model value +( x, 1 ) anymore, + * since { d -> +( x, 1 ) } has now been added to the database of this class. + */ + bool constructCandidates(const std::vector& terms, + const std::vector& term_values, + const std::vector& candidates, std::vector& candidate_values, - std::vector& lems); + std::vector& lems) override; /** is PBE enabled for any enumerator? */ bool isPbe() { return d_is_pbe; } /** is the enumerator e associated with I/O example pairs? */ @@ -243,15 +253,11 @@ class CegConjecturePbe { Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i); private: - /** quantifiers engine associated with this class */ - QuantifiersEngine* d_qe; /** sygus term database of d_qe */ quantifiers::TermDbSygus * d_tds; /** true and false nodes */ Node d_true; Node d_false; - /** A reference to the conjecture that owns this class. */ - CegConjecture* d_parent; /** is this a PBE conjecture for any function? */ bool d_is_pbe; /** for each candidate variable f (a function-to-synthesize), whether the -- 2.30.2