From fa557c39a89a2c8de198ea0400e6936c1790ad4e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 18 Sep 2018 10:26:36 -0500 Subject: [PATCH] Move and rename sygus solver classes (#2488) --- src/Makefile.am | 8 +- src/smt/smt_engine.cpp | 6 +- src/theory/datatypes/datatypes_sygus.cpp | 13 +- src/theory/datatypes/datatypes_sygus.h | 6 +- .../candidate_rewrite_database.cpp | 2 +- .../quantifiers/quantifiers_attributes.cpp | 7 +- .../sygus/ce_guided_single_inv.cpp | 72 ++--- .../quantifiers/sygus/ce_guided_single_inv.h | 32 +-- .../sygus/ce_guided_single_inv_sol.cpp | 132 ++++++---- .../sygus/ce_guided_single_inv_sol.h | 14 +- src/theory/quantifiers/sygus/cegis.cpp | 4 +- src/theory/quantifiers/sygus/cegis.h | 8 +- src/theory/quantifiers/sygus/cegis_unif.cpp | 8 +- src/theory/quantifiers/sygus/cegis_unif.h | 6 +- .../quantifiers/sygus/sygus_grammar_cons.cpp | 9 +- .../quantifiers/sygus/sygus_grammar_cons.h | 6 +- .../quantifiers/sygus/sygus_grammar_norm.cpp | 1 - .../quantifiers/sygus/sygus_invariance.cpp | 4 +- .../quantifiers/sygus/sygus_invariance.h | 6 +- src/theory/quantifiers/sygus/sygus_module.cpp | 2 +- src/theory/quantifiers/sygus/sygus_module.h | 18 +- src/theory/quantifiers/sygus/sygus_pbe.cpp | 74 +++--- src/theory/quantifiers/sygus/sygus_pbe.h | 148 +++++------ .../quantifiers/sygus/sygus_process_conj.cpp | 60 ++--- .../quantifiers/sygus/sygus_process_conj.h | 91 ++++--- .../quantifiers/sygus/sygus_unif_rl.cpp | 4 +- src/theory/quantifiers/sygus/sygus_unif_rl.h | 6 +- ...ed_conjecture.cpp => synth_conjecture.cpp} | 248 ++++++++++-------- ...guided_conjecture.h => synth_conjecture.h} | 121 +++++---- ...ded_instantiation.cpp => synth_engine.cpp} | 128 +++++---- ..._guided_instantiation.h => synth_engine.h} | 89 ++++--- .../quantifiers/sygus/term_database_sygus.cpp | 12 +- .../quantifiers/sygus/term_database_sygus.h | 8 +- src/theory/quantifiers_engine.cpp | 19 +- src/theory/quantifiers_engine.h | 6 +- 35 files changed, 761 insertions(+), 617 deletions(-) rename src/theory/quantifiers/sygus/{ce_guided_conjecture.cpp => synth_conjecture.cpp} (84%) rename src/theory/quantifiers/sygus/{ce_guided_conjecture.h => synth_conjecture.h} (79%) rename src/theory/quantifiers/sygus/{ce_guided_instantiation.cpp => synth_engine.cpp} (83%) rename src/theory/quantifiers/sygus/{ce_guided_instantiation.h => synth_engine.h} (50%) diff --git a/src/Makefile.am b/src/Makefile.am index bdba671ca..77cfccda5 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -532,10 +532,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/sygus/cegis.h \ theory/quantifiers/sygus/cegis_unif.cpp \ theory/quantifiers/sygus/cegis_unif.h \ - theory/quantifiers/sygus/ce_guided_conjecture.cpp \ - theory/quantifiers/sygus/ce_guided_conjecture.h \ - theory/quantifiers/sygus/ce_guided_instantiation.cpp \ - theory/quantifiers/sygus/ce_guided_instantiation.h \ theory/quantifiers/sygus/ce_guided_single_inv.cpp \ theory/quantifiers/sygus/ce_guided_single_inv.h \ theory/quantifiers/sygus/sygus_pbe.cpp \ @@ -568,6 +564,10 @@ libcvc4_la_SOURCES = \ theory/quantifiers/sygus/sygus_unif_rl.h \ theory/quantifiers/sygus/sygus_unif_strat.cpp \ theory/quantifiers/sygus/sygus_unif_strat.h \ + theory/quantifiers/sygus/synth_conjecture.cpp \ + theory/quantifiers/sygus/synth_conjecture.h \ + theory/quantifiers/sygus/synth_engine.cpp \ + theory/quantifiers/sygus/synth_engine.h \ theory/quantifiers/sygus/term_database_sygus.cpp \ theory/quantifiers/sygus/term_database_sygus.h \ theory/quantifiers/sygus_sampler.cpp \ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b4bc0b8dc..15f8280b5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -127,7 +127,7 @@ #include "theory/quantifiers/fun_def_process.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/single_inv_partition.h" -#include "theory/quantifiers/sygus/ce_guided_instantiation.h" +#include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" #include "theory/sort_inference.h" @@ -3182,7 +3182,9 @@ void SmtEnginePrivate::processAssertions() { if( options::ceGuidedInst() ){ //register sygus conjecture pre-rewrite (motivated by solution reconstruction) for (unsigned i = 0; i < d_assertions.size(); ++ i) { - d_smt.d_theoryEngine->getQuantifiersEngine()->getCegInstantiation()->preregisterAssertion( d_assertions[i] ); + d_smt.d_theoryEngine->getQuantifiersEngine() + ->getSynthEngine() + ->preregisterAssertion(d_assertions[i]); } } diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 82aa570c2..db1ce1c05 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -22,7 +22,6 @@ #include "printer/printer.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes.h" -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/sygus_explain.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -313,11 +312,11 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std: // static conjecture-dependent symmetry breaking Trace("sygus-sb-debug") << " conjecture-dependent symmetry breaking...\n"; - std::map::iterator itc = + std::map::iterator itc = d_anchor_to_conj.find(a); if (itc != d_anchor_to_conj.end()) { - quantifiers::CegConjecture* conj = itc->second; + quantifiers::SynthConjecture* conj = itc->second; Assert(conj != NULL); Node dpred = conj->getSymmetryBreakingPredicate(x, a, ntn, tindex, ds); if (!dpred.isNull()) @@ -803,7 +802,7 @@ Node SygusSymBreakNew::registerSearchValue( d_cache[a].d_search_val_proc.insert(cnv); // get the root (for PBE symmetry breaking) Assert(d_anchor_to_conj.find(a) != d_anchor_to_conj.end()); - quantifiers::CegConjecture* aconj = d_anchor_to_conj[a]; + quantifiers::SynthConjecture* aconj = d_anchor_to_conj[a]; Assert(aconj != NULL); Trace("sygus-sb-debug") << " ...register search value " << cnv << ", type=" << tn << std::endl; @@ -827,9 +826,9 @@ Node SygusSymBreakNew::registerSearchValue( bool by_examples = false; if( itsv==d_cache[a].d_search_val[tn].end() ){ // TODO (github #1210) conjecture-specific symmetry breaking - // this should be generalized and encapsulated within the CegConjecture - // class - // is it equivalent under examples? + // this should be generalized and encapsulated within the + // SynthConjecture class. + // Is it equivalent under examples? Node bvr_equiv; if (options::sygusSymBreakPbe()) { diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index e2ed4192a..99f9672e7 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -30,8 +30,8 @@ #include "expr/datatype.h" #include "expr/node.h" #include "theory/datatypes/sygus_simple_sym.h" -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/sygus_explain.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus_sampler.h" #include "theory/quantifiers/term_database.h" @@ -152,7 +152,7 @@ class SygusSymBreakNew /** * Map from anchors to the conjecture they are associated with. */ - std::map d_anchor_to_conj; + std::map d_anchor_to_conj; /** * Map from terms (selector chains) to their depth. The depth of a selector * chain S1( ... Sn( x ) ... ) is: @@ -229,7 +229,7 @@ private: * (2) static symmetry breaking clauses for subterms of n (those added to * lemmas on getSimpleSymBreakPred, see function below), * (3) conjecture-specific symmetry breaking lemmas, see - * CegConjecture::getSymmetryBreakingPredicate, + * SynthConjecture::getSymmetryBreakingPredicate, * (4) fairness conflicts if sygusFair() is SYGUS_FAIR_DIRECT, e.g.: * size( d ) <= 1 V ~is-C1( d ) V ~is-C2( d.1 ) * where C1 and C2 are non-nullary constructors. diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 3b7aab0b2..bba5b3c18 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -20,9 +20,9 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" -#include "theory/quantifiers/sygus/ce_guided_instantiation.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index dde6dc4a9..ff906a95b 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -17,7 +17,7 @@ #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/rewrite_engine.h" -#include "theory/quantifiers/sygus/ce_guided_instantiation.h" +#include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" @@ -229,10 +229,11 @@ void QuantAttributes::computeAttributes( Node q ) { d_fun_defs[f] = true; } if( d_qattr[q].d_sygus ){ - if( d_quantEngine->getCegInstantiation()==NULL ){ + if (d_quantEngine->getSynthEngine() == nullptr) + { Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; } - d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 ); + d_quantEngine->setOwner(q, d_quantEngine->getSynthEngine(), 2); } } diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 7d8db8c03..36690cfcc 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -42,12 +42,11 @@ bool CegqiOutputSingleInv::addLemma( Node n ) { return d_out->addLemma( n ); } -CegConjectureSingleInv::CegConjectureSingleInv(QuantifiersEngine* qe, - CegConjecture* p) +CegSingleInv::CegSingleInv(QuantifiersEngine* qe, SynthConjecture* p) : d_qe(qe), d_parent(p), d_sip(new SingleInvocationPartition), - d_sol(new CegConjectureSingleInvSol(qe)), + d_sol(new CegSingleInvSol(qe)), d_cosi(new CegqiOutputSingleInv(this)), d_cinst(new CegInstantiator(d_qe, d_cosi, false, false)), d_c_inst_match_trie(NULL), @@ -61,17 +60,17 @@ CegConjectureSingleInv::CegConjectureSingleInv(QuantifiersEngine* qe, } } -CegConjectureSingleInv::~CegConjectureSingleInv() { +CegSingleInv::~CegSingleInv() +{ if (d_c_inst_match_trie) { delete d_c_inst_match_trie; } delete d_cosi; - delete d_sol; // (new CegConjectureSingleInvSol(qe)), + delete d_sol; // (new CegSingleInvSol(qe)), delete d_sip; // d_sip(new SingleInvocationPartition), } -void CegConjectureSingleInv::getInitialSingleInvLemma(Node g, - std::vector& lems) +void CegSingleInv::getInitialSingleInvLemma(Node g, std::vector& lems) { Assert(!g.isNull()); Assert(!d_single_inv.isNull()); @@ -114,12 +113,13 @@ void CegConjectureSingleInv::getInitialSingleInvLemma(Node g, d_cinst->registerCounterexampleLemma(lems, d_single_inv_sk); } -void CegConjectureSingleInv::initialize( Node q ) { +void CegSingleInv::initialize(Node q) +{ // can only register one quantified formula with this Assert( d_quant.isNull() ); d_quant = q; d_simp_quant = q; - Trace("cegqi-si") << "CegConjectureSingleInv::initialize : " << q << std::endl; + Trace("cegqi-si") << "CegSingleInv::initialize : " << q << std::endl; // infer single invocation-ness // get the variables @@ -293,7 +293,7 @@ void CegConjectureSingleInv::initialize( Node q ) { } } -void CegConjectureSingleInv::finishInit(bool syntaxRestricted) +void CegSingleInv::finishInit(bool syntaxRestricted) { Trace("cegqi-si-debug") << "Single invocation: finish init" << std::endl; // do not do single invocation if grammar is restricted and CEGQI_SI_MODE_ALL is not enabled @@ -343,9 +343,10 @@ void CegConjectureSingleInv::finishInit(bool syntaxRestricted) } } -bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){ +bool CegSingleInv::doAddInstantiation(std::vector& subs) +{ Assert( d_single_inv_sk.size()==subs.size() ); - Trace("cegqi-si-inst-debug") << "CegConjectureSingleInv::doAddInstantiation, #vars = "; + Trace("cegqi-si-inst-debug") << "CegSingleInv::doAddInstantiation, #vars = "; Trace("cegqi-si-inst-debug") << d_single_inv_sk.size() << "..." << std::endl; std::stringstream siss; if( Trace.isOn("cegqi-si-inst-debug") || Trace.isOn("cegqi-engine") ){ @@ -400,19 +401,23 @@ bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){ return true; } -bool CegConjectureSingleInv::isEligibleForInstantiation( Node n ) { +bool CegSingleInv::isEligibleForInstantiation(Node n) +{ return n.getKind()!=SKOLEM || std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )!=d_single_inv_arg_sk.end(); } -bool CegConjectureSingleInv::addLemma( Node n ) { +bool CegSingleInv::addLemma(Node n) +{ d_curr_lemmas.push_back( n ); return true; } -bool CegConjectureSingleInv::check( std::vector< Node >& lems ) { +bool CegSingleInv::check(std::vector& lems) +{ if( !d_single_inv.isNull() ) { - Trace("cegqi-si-debug") << "CegConjectureSingleInv::check..." << std::endl; - Trace("cegqi-si-debug") << "CegConjectureSingleInv::check consulting ceg instantiation..." << std::endl; + Trace("cegqi-si-debug") << "CegSingleInv::check..." << std::endl; + Trace("cegqi-si-debug") + << "CegSingleInv::check consulting ceg instantiation..." << std::endl; d_curr_lemmas.clear(); Assert( d_cinst!=NULL ); //call check for instantiator @@ -427,7 +432,11 @@ bool CegConjectureSingleInv::check( std::vector< Node >& lems ) { } } -Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index, std::map< Node, Node >& weak_imp ) { +Node CegSingleInv::constructSolution(std::vector& indices, + unsigned i, + unsigned index, + std::map& weak_imp) +{ Assert( index& indices //TODO: use term size? struct sortSiInstanceIndices { - CegConjectureSingleInv* d_ccsi; + CegSingleInv* d_ccsi; int d_i; bool operator() (unsigned i, unsigned j) { if( d_ccsi->d_inst[i][d_i].isConst() && !d_ccsi->d_inst[j][d_i].isConst() ){ @@ -460,8 +469,8 @@ struct sortSiInstanceIndices { } }; - -Node CegConjectureSingleInv::postProcessSolution( Node n ){ +Node CegSingleInv::postProcessSolution(Node n) +{ bool childChanged = false; Kind k = n.getKind(); if( n.getKind()==INTS_DIVISION_TOTAL ){ @@ -487,8 +496,11 @@ Node CegConjectureSingleInv::postProcessSolution( Node n ){ } } - -Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed, bool rconsSygus ){ +Node CegSingleInv::getSolution(unsigned sol_index, + TypeNode stn, + int& reconstructed, + bool rconsSygus) +{ Assert( d_sol!=NULL ); Assert( !d_lemmas_produced.empty() ); const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); @@ -563,7 +575,11 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& return reconstructToSyntax( s, stn, reconstructed, rconsSygus ); } -Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& reconstructed, bool rconsSygus ) { +Node CegSingleInv::reconstructToSyntax(Node s, + TypeNode stn, + int& reconstructed, + bool rconsSygus) +{ d_solution = s; const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); @@ -645,13 +661,9 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec } } -bool CegConjectureSingleInv::needsCheck() { - return true; -} +bool CegSingleInv::needsCheck() { return true; } -void CegConjectureSingleInv::preregisterConjecture( Node q ) { - d_orig_conjecture = q; -} +void CegSingleInv::preregisterConjecture(Node q) { d_orig_conjecture = q; } bool DetTrace::DetTraceTrie::add( Node loc, std::vector< Node >& val, unsigned index ){ if( index==val.size() ){ diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index b27163549..c797bc3cb 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -28,18 +28,17 @@ namespace CVC4 { namespace theory { namespace quantifiers { -class CegConjecture; -class CegConjectureSingleInv; -class CegEntailmentInfer; +class SynthConjecture; +class CegSingleInv; class CegqiOutputSingleInv : public CegqiOutput { -public: - CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){} - virtual ~CegqiOutputSingleInv() {} - CegConjectureSingleInv * d_out; - bool doAddInstantiation(std::vector& subs) override; - bool isEligibleForInstantiation(Node n) override; - bool addLemma(Node lem) override; + public: + CegqiOutputSingleInv(CegSingleInv* out) : d_out(out) {} + virtual ~CegqiOutputSingleInv() {} + CegSingleInv* d_out; + bool doAddInstantiation(std::vector& subs) override; + bool isEligibleForInstantiation(Node n) override; + bool addLemma(Node lem) override; }; class DetTrace { @@ -123,7 +122,8 @@ private: // (2) inferring whether the conjecture corresponds to a deterministic transistion system (by utility d_ti). // For these techniques, we may generate a template (d_templ) which specifies a restricted // solution space. We may in turn embed this template as a SyGuS grammar. -class CegConjectureSingleInv { +class CegSingleInv +{ private: friend class CegqiOutputSingleInv; //presolve @@ -138,14 +138,16 @@ class CegConjectureSingleInv { unsigned index, std::map& weak_imp); Node postProcessSolution(Node n); private: + /** pointer to the quantifiers engine */ QuantifiersEngine* d_qe; - CegConjecture* d_parent; + /** the parent of this class */ + SynthConjecture* d_parent; // single invocation inference utility SingleInvocationPartition* d_sip; // transition inference module for each function to synthesize std::map< Node, TransitionInference > d_ti; // solution reconstruction - CegConjectureSingleInvSol* d_sol; + CegSingleInvSol* d_sol; // the instantiator's output channel CegqiOutputSingleInv* d_cosi; // the instantiator @@ -197,8 +199,8 @@ class CegConjectureSingleInv { std::map< Node, Node > d_templ_arg; public: - CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p ); - ~CegConjectureSingleInv(); + CegSingleInv(QuantifiersEngine* qe, SynthConjecture* p); + ~CegSingleInv(); // get simplified conjecture Node getSimplifiedConjecture() { return d_simp_quant; } diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index e575dff9b..7f7c56f84 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -20,8 +20,8 @@ #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/sygus/ce_guided_instantiation.h" #include "theory/quantifiers/sygus/ce_guided_single_inv.h" +#include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" @@ -42,10 +42,13 @@ bool doCompare(Node a, Node b, Kind k) return com.isConst() && com.getConst(); } -CegConjectureSingleInvSol::CegConjectureSingleInvSol(QuantifiersEngine* qe) - : d_qe(qe), d_id_count(0), d_root_id() {} +CegSingleInvSol::CegSingleInvSol(QuantifiersEngine* qe) + : d_qe(qe), d_id_count(0), d_root_id() +{ +} -bool CegConjectureSingleInvSol::debugSolution( Node sol ) { +bool CegSingleInvSol::debugSolution(Node sol) +{ if( sol.getKind()==SKOLEM ){ return false; }else{ @@ -59,7 +62,8 @@ bool CegConjectureSingleInvSol::debugSolution( Node sol ) { } -void CegConjectureSingleInvSol::debugTermSize( Node sol, int& t_size, int& num_ite ) { +void CegSingleInvSol::debugTermSize(Node sol, int& t_size, int& num_ite) +{ std::map< Node, int >::iterator it = d_dterm_size.find( sol ); if( it==d_dterm_size.end() ){ int prev = t_size; @@ -79,8 +83,8 @@ void CegConjectureSingleInvSol::debugTermSize( Node sol, int& t_size, int& num_i } } - -Node CegConjectureSingleInvSol::pullITEs( Node s ) { +Node CegSingleInvSol::pullITEs(Node s) +{ if( s.getKind()==ITE ){ bool success; do { @@ -107,7 +111,13 @@ Node CegConjectureSingleInvSol::pullITEs( Node s ) { } // pull condition common to all ITE conditions in path of size > 1 -bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::vector< Node >& conj, Node& t, Node& rem, int depth ) { +bool CegSingleInvSol::pullITECondition(Node root, + Node n_ite, + std::vector& conj, + Node& t, + Node& rem, + int depth) +{ Assert( n_ite.getKind()==ITE ); std::vector< Node > curr_conj; std::vector< Node > orig_conj; @@ -196,7 +206,8 @@ bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::ve } } -Node CegConjectureSingleInvSol::flattenITEs( Node n, bool rec ) { +Node CegSingleInvSol::flattenITEs(Node n, bool rec) +{ Assert( !n.isNull() ); if( n.getKind()==ITE ){ Trace("csi-sol-debug") << "Flatten ITE." << std::endl; @@ -260,8 +271,14 @@ Node CegConjectureSingleInvSol::flattenITEs( Node n, bool rec ) { // assign is from literals to booleans // union_find is from args to values -bool CegConjectureSingleInvSol::getAssign( bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign, std::vector< Node >& vars, - std::vector< Node >& new_vars, std::vector< Node >& new_subs ) { +bool CegSingleInvSol::getAssign(bool pol, + Node n, + std::map& assign, + std::vector& new_assign, + std::vector& vars, + std::vector& new_vars, + std::vector& new_subs) +{ std::map< Node, bool >::iterator ita = assign.find( n ); if( ita!=assign.end() ){ Trace("csi-simp-debug") << "---already assigned, lookup " << pol << " " << ita->second << std::endl; @@ -287,7 +304,11 @@ bool CegConjectureSingleInvSol::getAssign( bool pol, Node n, std::map< Node, boo return true; } -bool CegConjectureSingleInvSol::getAssignEquality( Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs ) { +bool CegSingleInvSol::getAssignEquality(Node eq, + std::vector& vars, + std::vector& new_vars, + std::vector& new_subs) +{ Assert( eq.getKind()==EQUAL ); //try to find valid argument for( unsigned r=0; r<2; r++ ){ @@ -309,7 +330,8 @@ bool CegConjectureSingleInvSol::getAssignEquality( Node eq, std::vector< Node >& return false; } -Node CegConjectureSingleInvSol::simplifySolution( Node sol, TypeNode stn ){ +Node CegSingleInvSol::simplifySolution(Node sol, TypeNode stn) +{ int tsize, itesize; if( Trace.isOn("csi-sol") ){ tsize = 0;itesize = 0; @@ -373,9 +395,13 @@ Node CegConjectureSingleInvSol::simplifySolution( Node sol, TypeNode stn ){ return curr_sol; } -Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, std::map< Node, bool >& assign, - std::vector< Node >& vars, std::vector< Node >& subs, int status ) { - +Node CegSingleInvSol::simplifySolutionNode(Node sol, + TypeNode stn, + std::map& assign, + std::vector& vars, + std::vector& subs, + int status) +{ Assert( vars.size()==subs.size() ); std::map< Node, bool >::iterator ita = assign.find( sol ); if( ita!=assign.end() ){ @@ -618,8 +644,8 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st } } - -void CegConjectureSingleInvSol::preregisterConjecture( Node q ) { +void CegSingleInvSol::preregisterConjecture(Node q) +{ Trace("csi-sol") << "Preregister conjecture : " << q << std::endl; Node n = q; if( n.getKind()==FORALL ){ @@ -641,10 +667,10 @@ void CegConjectureSingleInvSol::preregisterConjecture( Node q ) { registerEquivalentTerms( n ); } -Node CegConjectureSingleInvSol::reconstructSolution(Node sol, - TypeNode stn, - int& reconstructed, - int enumLimit) +Node CegSingleInvSol::reconstructSolution(Node sol, + TypeNode stn, + int& reconstructed, + int enumLimit) { Trace("csi-rcons") << "Solution (pre-reconstruction) is : " << sol << std::endl; int status; @@ -743,7 +769,8 @@ Node CegConjectureSingleInvSol::reconstructSolution(Node sol, return Node::null(); } -int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, int& status ) { +int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status) +{ std::map< Node, int >::iterator itri = d_rcons_to_status[stn].find( t ); if( itri!=d_rcons_to_status[stn].end() ){ status = itri->second; @@ -956,7 +983,12 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in } } -bool CegConjectureSingleInvSol::collectReconstructNodes( int pid, std::vector< Node >& ts, const DatatypeConstructor& dtc, std::vector< int >& ids, int& status ) { +bool CegSingleInvSol::collectReconstructNodes(int pid, + std::vector& ts, + const DatatypeConstructor& dtc, + std::vector& ids, + int& status) +{ Assert( dtc.getNumArgs()==ts.size() ); for( unsigned i=0; igetTermDatabaseSygus()->getArgType( dtc, i ); @@ -1001,8 +1033,9 @@ bool CegConjectureSingleInvSol::collectReconstructNodes( int pid, std::vector< N } */ - -Node CegConjectureSingleInvSol::CegConjectureSingleInvSol::getReconstructedSolution( int id, bool mod_eq ) { +Node CegSingleInvSol::CegSingleInvSol::getReconstructedSolution(int id, + bool mod_eq) +{ std::map< int, Node >::iterator it = d_reconstruct.find( id ); if( it!=d_reconstruct.end() ){ return it->second; @@ -1053,7 +1086,8 @@ Node CegConjectureSingleInvSol::CegConjectureSingleInvSol::getReconstructedSolut } } -int CegConjectureSingleInvSol::allocate( Node n, TypeNode stn ) { +int CegSingleInvSol::allocate(Node n, TypeNode stn) +{ std::map< Node, int >::iterator it = d_rcons_to_id[stn].find( n ); if( it==d_rcons_to_id[stn].end() ){ int ret = d_id_count; @@ -1073,7 +1107,8 @@ int CegConjectureSingleInvSol::allocate( Node n, TypeNode stn ) { } } -bool CegConjectureSingleInvSol::getPathToRoot( int id ) { +bool CegSingleInvSol::getPathToRoot(int id) +{ if( id==d_root_id ){ return true; }else{ @@ -1092,7 +1127,8 @@ bool CegConjectureSingleInvSol::getPathToRoot( int id ) { } } -void CegConjectureSingleInvSol::setReconstructed( int id, Node n ) { +void CegSingleInvSol::setReconstructed(int id, Node n) +{ //set all equivalent to this as reconstructed int rid = d_rep[id]; for( unsigned i=0; i& equiv ) { +void CegSingleInvSol::getEquivalentTerms(Kind k, + Node n, + std::vector& equiv) +{ if( k==AND || k==OR ){ equiv.push_back( NodeManager::currentNM()->mkNode( k, n, n ) ); equiv.push_back( NodeManager::currentNM()->mkNode( k, n, NodeManager::currentNM()->mkConst( k==AND ) ) ); @@ -1201,7 +1240,8 @@ void CegConjectureSingleInvSol::getEquivalentTerms( Kind k, Node n, std::vector< } } -void CegConjectureSingleInvSol::registerEquivalentTerms( Node n ) { +void CegSingleInvSol::registerEquivalentTerms(Node n) +{ for( unsigned i=0; i::iterator it = d_builtin_const_to_sygus[tn].find(c); if (it != d_builtin_const_to_sygus[tn].end()) @@ -1350,7 +1388,7 @@ struct sortConstants } }; -void CegConjectureSingleInvSol::registerType(TypeNode tn) +void CegSingleInvSol::registerType(TypeNode tn) { if (d_const_list_pos.find(tn) != d_const_list_pos.end()) { @@ -1407,10 +1445,10 @@ void CegConjectureSingleInvSol::registerType(TypeNode tn) } } -bool CegConjectureSingleInvSol::getMatch(Node p, - Node n, - std::map& s, - std::vector& new_s) +bool CegSingleInvSol::getMatch(Node p, + Node n, + std::map& s, + std::vector& new_s) { TermDbSygus* tds = d_qe->getTermDatabaseSygus(); if (tds->isFreeVar(p)) @@ -1461,12 +1499,12 @@ bool CegConjectureSingleInvSol::getMatch(Node p, return false; } -bool CegConjectureSingleInvSol::getMatch(Node t, - TypeNode st, - int& index_found, - std::vector& args, - int index_exc, - int index_start) +bool CegSingleInvSol::getMatch(Node t, + TypeNode st, + int& index_found, + std::vector& args, + int index_exc, + int index_start) { Assert(st.isDatatype()); const Datatype& dt = static_cast(st.toType()).getDatatype(); @@ -1517,9 +1555,7 @@ bool CegConjectureSingleInvSol::getMatch(Node t, return false; } -Node CegConjectureSingleInvSol::getGenericBase(TypeNode tn, - const Datatype& dt, - int c) +Node CegSingleInvSol::getGenericBase(TypeNode tn, const Datatype& dt, int c) { std::map::iterator it = d_generic_base[tn].find(c); if (it != d_generic_base[tn].end()) diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h index 8d18611cf..fb0862413 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h @@ -24,19 +24,19 @@ namespace CVC4 { namespace theory { namespace quantifiers { +class CegSingleInv; -class CegConjectureSingleInv; - -/** CegConjectureSingleInvSol +/** CegSingleInvSol * * This function implements Figure 5 of "Counterexample-Guided Quantifier * Instantiation for Synthesis in SMT", Reynolds et al CAV 2015. * */ -class CegConjectureSingleInvSol +class CegSingleInvSol { - friend class CegConjectureSingleInv; -private: + friend class CegSingleInv; + + private: QuantifiersEngine * d_qe; std::vector< Node > d_varList; std::map< Node, int > d_dterm_size; @@ -55,7 +55,7 @@ private: std::vector< Node >& vars, std::vector< Node >& subs, int status ); public: - CegConjectureSingleInvSol(QuantifiersEngine* qe); + CegSingleInvSol(QuantifiersEngine* qe); /** simplify solution * * Returns the simplified version of node sol whose syntax is restricted by diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 204daa49a..fbe0da7a8 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -16,7 +16,7 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/theory_engine.h" @@ -28,7 +28,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p) +Cegis::Cegis(QuantifiersEngine* qe, SynthConjecture* p) : SygusModule(qe, p), d_eval_unfold(nullptr), d_using_gr_repair(false) { if (options::sygusEvalUnfold()) diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index ce4186eb2..c7392b378 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -41,7 +41,7 @@ namespace quantifiers { class Cegis : public SygusModule { public: - Cegis(QuantifiersEngine* qe, CegConjecture* p); + Cegis(QuantifiersEngine* qe, SynthConjecture* p); ~Cegis() override {} /** initialize */ virtual bool initialize(Node n, @@ -69,11 +69,11 @@ class Cegis : public SygusModule protected: /** the evaluation unfold utility of d_tds */ SygusEvalUnfold* d_eval_unfold; - /** If CegConjecture::d_base_inst is exists y. P( d, y ), then this is y. */ + /** If SynthConjecture::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 ). + * If SynthConjecture::d_base_inst is exists y. P( d, y ), then this is the + * formula P( SynthConjecture::d_candidates, y ). */ Node d_base_body; //----------------------------------cegis-implementation-specific diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 56cc40244..456f44019 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -17,8 +17,8 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/sygus_unif_rl.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/theory_engine.h" @@ -28,7 +28,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -CegisUnif::CegisUnif(QuantifiersEngine* qe, CegConjecture* p) +CegisUnif::CegisUnif(QuantifiersEngine* qe, SynthConjecture* p) : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, p) { } @@ -299,8 +299,8 @@ void CegisUnif::registerRefinementLemma(const std::vector& vars, OR, d_parent->getGuard().negate(), plem)); } -CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, - CegConjecture* parent) +CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy( + QuantifiersEngine* qe, SynthConjecture* parent) : DecisionStrategyFmf(qe->getSatContext(), qe->getValuation()), d_qe(qe), d_parent(parent) diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index ae2d7964b..00cc5af72 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -47,7 +47,7 @@ namespace quantifiers { class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf { public: - CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, CegConjecture* parent); + CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, SynthConjecture* parent); /** Make the n^th literal of this strategy (G_uq_n). * * This call may add new lemmas of the form described above @@ -96,7 +96,7 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf /** sygus term database of d_qe */ TermDbSygus* d_tds; /** reference to the parent conjecture */ - CegConjecture* d_parent; + SynthConjecture* d_parent; /** whether this module has been initialized */ bool d_initialized; /** null node */ @@ -194,7 +194,7 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf class CegisUnif : public Cegis { public: - CegisUnif(QuantifiersEngine* qe, CegConjecture* p); + CegisUnif(QuantifiersEngine* qe, SynthConjecture* p); ~CegisUnif() override; /** Retrieves enumerators for constructing solutions * diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index e05df8581..eadbf766a 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -20,9 +20,9 @@ #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/datatypes_rewriter.h" -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/sygus_grammar_norm.h" #include "theory/quantifiers/sygus/sygus_process_conj.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -33,7 +33,7 @@ namespace theory { namespace quantifiers { CegGrammarConstructor::CegGrammarConstructor(QuantifiersEngine* qe, - CegConjecture* p) + SynthConjecture* p) : d_qe(qe), d_parent(p), d_is_syntax_restricted(false) { } @@ -95,10 +95,11 @@ Node CegGrammarConstructor::process(Node q, { // convert to deep embedding and finalize single invocation here // now, construct the grammar - Trace("cegqi") << "CegConjecture : convert to deep embedding..." << std::endl; + Trace("cegqi") << "SynthConjecture : convert to deep embedding..." + << std::endl; std::map< TypeNode, std::vector< Node > > extra_cons; if( options::sygusAddConstGrammar() ){ - Trace("cegqi") << "CegConjecture : collect constants..." << std::endl; + Trace("cegqi") << "SynthConjecture : collect constants..." << std::endl; collectTerms( q[1], extra_cons ); } std::map> exc_cons; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 33c0a836b..022031bef 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -24,7 +24,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -class CegConjecture; +class SynthConjecture; /** utility for constructing datatypes that correspond to syntactic restrictions, * and applying the deep embedding from Section 4 of Reynolds et al CAV 2015. @@ -32,7 +32,7 @@ class CegConjecture; class CegGrammarConstructor { public: - CegGrammarConstructor(QuantifiersEngine* qe, CegConjecture* p); + CegGrammarConstructor(QuantifiersEngine* qe, SynthConjecture* p); ~CegGrammarConstructor() {} /** process * @@ -114,7 +114,7 @@ public: /** parent conjecture * This contains global information about the synthesis conjecture. */ - CegConjecture* d_parent; + SynthConjecture* d_parent; /** is the syntax restricted? */ bool d_is_syntax_restricted; /** collect terms */ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 868e69b21..3d066e8dd 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -22,7 +22,6 @@ #include "smt/smt_engine_scope.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/sygus_grammar_red.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index 54a3cce50..24b47b216 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -14,8 +14,8 @@ #include "theory/quantifiers/sygus/sygus_invariance.h" -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/sygus_pbe.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" using namespace CVC4::kind; @@ -87,7 +87,7 @@ bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) } void EquivSygusInvarianceTest::init( - TermDbSygus* tds, TypeNode tn, CegConjecture* aconj, Node e, Node bvr) + TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr) { // compute the current examples d_bvr = bvr; diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index 20cd1fd03..59761da5c 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -27,7 +27,7 @@ namespace theory { namespace quantifiers { class TermDbSygus; -class CegConjecture; +class SynthConjecture; /* SygusInvarianceTest * @@ -181,7 +181,7 @@ class EquivSygusInvarianceTest : public SygusInvarianceTest * are checking for invariance */ void init( - TermDbSygus* tds, TypeNode tn, CegConjecture* aconj, Node e, Node bvr); + TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr); protected: /** checks whether the analog of nvn still rewrites to d_bvr */ @@ -189,7 +189,7 @@ class EquivSygusInvarianceTest : public SygusInvarianceTest private: /** the conjecture associated with the enumerator d_enum */ - CegConjecture* d_conj; + SynthConjecture* d_conj; /** the enumerator associated with the term for which this test is for */ Node d_enum; /** the RHS of the evaluation */ diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp index b36fe4281..3471472fa 100644 --- a/src/theory/quantifiers/sygus/sygus_module.cpp +++ b/src/theory/quantifiers/sygus/sygus_module.cpp @@ -18,7 +18,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SygusModule::SygusModule(QuantifiersEngine* qe, CegConjecture* p) +SygusModule::SygusModule(QuantifiersEngine* qe, SynthConjecture* p) : d_qe(qe), d_tds(qe->getTermDatabaseSygus()), d_parent(p) { } diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index e2a9fae80..c1b12dfd0 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -25,20 +25,20 @@ namespace CVC4 { namespace theory { namespace quantifiers { -class CegConjecture; +class SynthConjecture; /** 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. + * This is the base class of sygus modules, owned by SynthConjecture. The + * purpose of this class is to, when applicable, suggest candidate solutions for + * SynthConjecture to test. * - * In more detail, an instance of the conjecture class (CegConjecture) creates + * In more detail, an instance of the conjecture class (SynthConjecture) 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: + * conjecture (see SynthConjecture::d_base_inst) is the formula: * exists y. P( k, y ) * where k are the "candidate" variables for the conjecture. * @@ -48,12 +48,12 @@ class CegConjecture; class SygusModule { public: - SygusModule(QuantifiersEngine* qe, CegConjecture* p); + SygusModule(QuantifiersEngine* qe, SynthConjecture* p); virtual ~SygusModule() {} /** initialize * * n is the "base instantiation" of the deep-embedding version of the - * synthesis conjecture under candidates (see CegConjecture::d_base_inst). + * synthesis conjecture under candidates (see SynthConjecture::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. @@ -127,7 +127,7 @@ class SygusModule /** sygus term database of d_qe */ quantifiers::TermDbSygus* d_tds; /** reference to the parent conjecture */ - CegConjecture* d_parent; + SynthConjecture* d_parent; }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 6a82b9dad..9a6645560 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -28,7 +28,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -CegConjecturePbe::CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p) +SygusPbe::SygusPbe(QuantifiersEngine* qe, SynthConjecture* p) : SygusModule(qe, p) { d_true = NodeManager::currentNM()->mkConst(true); @@ -36,13 +36,15 @@ CegConjecturePbe::CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p) d_is_pbe = false; } -CegConjecturePbe::~CegConjecturePbe() { - -} +SygusPbe::~SygusPbe() {} //--------------------------------- collecting finite input/output domain information -void CegConjecturePbe::collectExamples( Node n, std::map< Node, bool >& visited, bool hasPol, bool pol ) { +void SygusPbe::collectExamples(Node n, + std::map& visited, + bool hasPol, + bool pol) +{ if( visited.find( n )==visited.end() ){ visited[n] = true; Node neval; @@ -116,9 +118,9 @@ void CegConjecturePbe::collectExamples( Node n, std::map< Node, bool >& visited, } } -bool CegConjecturePbe::initialize(Node n, - const std::vector& candidates, - std::vector& lemmas) +bool SygusPbe::initialize(Node n, + const std::vector& candidates, + std::vector& lemmas) { Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl; @@ -248,9 +250,13 @@ bool CegConjecturePbe::initialize(Node n, return true; } -Node CegConjecturePbe::PbeTrie::addPbeExample(TypeNode etn, Node e, Node b, - CegConjecturePbe* cpbe, - unsigned index, unsigned ntotal) { +Node SygusPbe::PbeTrie::addPbeExample(TypeNode etn, + Node e, + Node b, + SygusPbe* cpbe, + unsigned index, + unsigned ntotal) +{ if (index == ntotal) { // lazy child holds the leaf data if (d_lazy_child.isNull()) { @@ -281,16 +287,20 @@ Node CegConjecturePbe::PbeTrie::addPbeExample(TypeNode etn, Node e, Node b, } } -Node CegConjecturePbe::PbeTrie::addPbeExampleEval(TypeNode etn, Node e, Node b, - std::vector& ex, - CegConjecturePbe* cpbe, - unsigned index, - unsigned ntotal) { +Node SygusPbe::PbeTrie::addPbeExampleEval(TypeNode etn, + Node e, + Node b, + std::vector& ex, + SygusPbe* cpbe, + unsigned index, + unsigned ntotal) +{ Node eb = cpbe->d_tds->evaluateBuiltin(etn, b, ex); return d_children[eb].addPbeExample(etn, e, b, cpbe, index + 1, ntotal); } -bool CegConjecturePbe::hasExamples(Node e) { +bool SygusPbe::hasExamples(Node e) +{ if (isPbe()) { e = d_tds->getSynthFunForEnumerator(e); Assert(!e.isNull()); @@ -302,7 +312,8 @@ bool CegConjecturePbe::hasExamples(Node e) { return false; } -unsigned CegConjecturePbe::getNumExamples(Node e) { +unsigned SygusPbe::getNumExamples(Node e) +{ e = d_tds->getSynthFunForEnumerator(e); Assert(!e.isNull()); std::map > >::iterator it = @@ -314,7 +325,8 @@ unsigned CegConjecturePbe::getNumExamples(Node e) { } } -void CegConjecturePbe::getExample(Node e, unsigned i, std::vector& ex) { +void SygusPbe::getExample(Node e, unsigned i, std::vector& ex) +{ e = d_tds->getSynthFunForEnumerator(e); Assert(!e.isNull()); std::map > >::iterator it = @@ -327,7 +339,8 @@ void CegConjecturePbe::getExample(Node e, unsigned i, std::vector& ex) { } } -Node CegConjecturePbe::getExampleOut(Node e, unsigned i) { +Node SygusPbe::getExampleOut(Node e, unsigned i) +{ e = d_tds->getSynthFunForEnumerator(e); Assert(!e.isNull()); std::map >::iterator it = d_examples_out.find(e); @@ -340,7 +353,8 @@ Node CegConjecturePbe::getExampleOut(Node e, unsigned i) { } } -Node CegConjecturePbe::addSearchVal(TypeNode tn, Node e, Node bvr) { +Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr) +{ Assert(isPbe()); Assert(!e.isNull()); e = d_tds->getSynthFunForEnumerator(e); @@ -355,8 +369,8 @@ Node CegConjecturePbe::addSearchVal(TypeNode tn, Node e, Node bvr) { return Node::null(); } -Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, - unsigned i) { +Node SygusPbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i) +{ e = d_tds->getSynthFunForEnumerator(e); Assert(!e.isNull()); std::map::iterator itx = d_examples_invalid.find(e); @@ -373,8 +387,8 @@ Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, // ------------------------------------------- solution construction from enumeration -void CegConjecturePbe::getTermList(const std::vector& candidates, - std::vector& terms) +void SygusPbe::getTermList(const std::vector& candidates, + std::vector& terms) { Valuation& valuation = d_qe->getValuation(); for( unsigned i=0; i& candidates, } } -bool CegConjecturePbe::constructCandidates(const std::vector& enums, - const std::vector& enum_values, - const std::vector& candidates, - std::vector& candidate_values, - std::vector& lems) +bool SygusPbe::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() ){ diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 49d853248..66e19b6c9 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H -#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H +#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H +#define __CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H #include "context/cdhashmap.h" #include "theory/quantifiers/sygus/sygus_module.h" @@ -25,79 +25,79 @@ namespace CVC4 { namespace theory { namespace quantifiers { -class CegConjecture; +class SynthConjecture; -/** CegConjecturePbe -* -* This class implements optimizations that target synthesis conjectures -* that are in Programming-By-Examples (PBE) form. -* -* [EX#1] An example of a synthesis conjecture in PBE form is : -* exists f. forall x. -* ( x = 0 => f( x ) = 2 ) ^ ( x = 5 => f( x ) = 7 ) ^ ( x = 6 => f( x ) = 8 ) -* -* We say that the above conjecture has I/O examples (0)->2, (5)->7, (6)->8. -* -* Internally, this class does the following for SyGuS inputs: -* -* (1) Infers whether the input conjecture is in PBE form or not. -* (2) Based on this information and on the syntactic restrictions, it -* devises a strategy for enumerating terms and construction solutions, -* which is inspired by Alur et al. "Scaling Enumerative Program Synthesis -* via Divide and Conquer" TACAS 2017. In particular, it may consider -* strategies for constructing decision trees when the grammar permits ITEs -* and a strategy for divide-and-conquer string synthesis when the grammar -* permits string concatenation. This is managed through the SygusUnif -* utilities, d_sygus_unif. -* (3) It makes (possibly multiple) calls to -* TermDatabaseSygus::regstierEnumerator(...) based -* on the strategy, which inform the rest of the system to enumerate values -* of particular types in the grammar through use of fresh variables which -* we call "enumerators". -* -* Points (1)-(3) happen within a call to CegConjecturePbe::initialize(...). -* -* Notice that each enumerator is associated with a single -* function-to-synthesize, but a function-to-sythesize may be mapped to multiple -* enumerators. Some public functions of this class expect an enumerator as -* input, which we map to a function-to-synthesize via -* TermDatabaseSygus::getSynthFunFor(e). -* -* An enumerator is initially "active" but may become inactive if the enumeration -* exhausts all possible values in the datatype corresponding to syntactic -* restrictions for it. The search may continue unless all enumerators become -* inactive. -* -* (4) During search, the extension of quantifier-free datatypes procedure for -* SyGuS datatypes may ask this class whether current candidates can be -* discarded based on inferring when two candidate solutions are equivalent -* up to examples. For example, the candidate solutions: -* f = \x ite( x < 0, x+1, x ) and f = \x x -* are equivalent up to examples on the above conjecture, since they have the -* same value on the points x = 0,5,6. Hence, we need only consider one of -* them. The interface for querying this is -* CegConjecturePbe::addSearchVal(...). -* For details, see Reynolds et al. SYNT 2017. -* -* (5) When the extension of quantifier-free datatypes procedure for SyGuS -* datatypes terminates with a model, the parent of this class calls -* CegConjecturePbe::getCandidateList(...), where this class returns the list -* of active enumerators. -* (6) The parent class subsequently calls -* CegConjecturePbe::constructValues(...), which informs this class that new -* values have been enumerated for active enumerators, as indicated by the -* current model. This call also requests that based on these -* newly enumerated values, whether this class is now able to construct a -* solution based on the high-level strategy (stored in d_sygus_unif). -* -* This class is not designed to work in incremental mode, since there is no way -* to specify incremental problems in SyguS. -*/ -class CegConjecturePbe : public SygusModule +/** SygusPbe + * + * This class implements optimizations that target synthesis conjectures + * that are in Programming-By-Examples (PBE) form. + * + * [EX#1] An example of a synthesis conjecture in PBE form is : + * exists f. forall x. + * ( x = 0 => f( x ) = 2 ) ^ ( x = 5 => f( x ) = 7 ) ^ ( x = 6 => f( x ) = 8 ) + * + * We say that the above conjecture has I/O examples (0)->2, (5)->7, (6)->8. + * + * Internally, this class does the following for SyGuS inputs: + * + * (1) Infers whether the input conjecture is in PBE form or not. + * (2) Based on this information and on the syntactic restrictions, it + * devises a strategy for enumerating terms and construction solutions, + * which is inspired by Alur et al. "Scaling Enumerative Program Synthesis + * via Divide and Conquer" TACAS 2017. In particular, it may consider + * strategies for constructing decision trees when the grammar permits ITEs + * and a strategy for divide-and-conquer string synthesis when the grammar + * permits string concatenation. This is managed through the SygusUnif + * utilities, d_sygus_unif. + * (3) It makes (possibly multiple) calls to + * TermDatabaseSygus::regstierEnumerator(...) based + * on the strategy, which inform the rest of the system to enumerate values + * of particular types in the grammar through use of fresh variables which + * we call "enumerators". + * + * Points (1)-(3) happen within a call to SygusPbe::initialize(...). + * + * Notice that each enumerator is associated with a single + * function-to-synthesize, but a function-to-sythesize may be mapped to multiple + * enumerators. Some public functions of this class expect an enumerator as + * input, which we map to a function-to-synthesize via + * TermDatabaseSygus::getSynthFunFor(e). + * + * An enumerator is initially "active" but may become inactive if the + * enumeration exhausts all possible values in the datatype corresponding to + * syntactic restrictions for it. The search may continue unless all enumerators + * become inactive. + * + * (4) During search, the extension of quantifier-free datatypes procedure for + * SyGuS datatypes may ask this class whether current candidates can be + * discarded based on inferring when two candidate solutions are equivalent + * up to examples. For example, the candidate solutions: + * f = \x ite( x < 0, x+1, x ) and f = \x x + * are equivalent up to examples on the above conjecture, since they have + * the same value on the points x = 0,5,6. Hence, we need only consider one of + * them. The interface for querying this is + * SygusPbe::addSearchVal(...). + * For details, see Reynolds et al. SYNT 2017. + * + * (5) When the extension of quantifier-free datatypes procedure for SyGuS + * datatypes terminates with a model, the parent of this class calls + * SygusPbe::getCandidateList(...), where this class returns the list + * of active enumerators. + * (6) The parent class subsequently calls + * SygusPbe::constructValues(...), which informs this class that new + * values have been enumerated for active enumerators, as indicated by the + * current model. This call also requests that based on these + * newly enumerated values, whether this class is now able to construct a + * solution based on the high-level strategy (stored in d_sygus_unif). + * + * This class is not designed to work in incremental mode, since there is no way + * to specify incremental problems in SyguS. + */ +class SygusPbe : public SygusModule { public: - CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p); - ~CegConjecturePbe(); + SygusPbe(QuantifiersEngine* qe, SynthConjecture* p); + ~SygusPbe(); /** initialize this class * @@ -276,7 +276,7 @@ class CegConjecturePbe : public SygusModule Node addPbeExample(TypeNode etn, Node e, Node b, - CegConjecturePbe* cpbe, + SygusPbe* cpbe, unsigned index, unsigned ntotal); @@ -286,7 +286,7 @@ class CegConjecturePbe : public SygusModule Node e, Node b, std::vector& ex, - CegConjecturePbe* cpbe, + SygusPbe* cpbe, unsigned index, unsigned ntotal); }; diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index b0b6159be..a2454758a 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -29,7 +29,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -void CegConjectureProcessFun::init(Node f) +void SynthConjectureProcessFun::init(Node f) { d_synth_fun = f; Assert(f.getType().isFunction()); @@ -47,11 +47,11 @@ void CegConjectureProcessFun::init(Node f) Node k = NodeManager::currentNM()->mkBoundVar(ss.str(), atn); d_arg_vars.push_back(k); d_arg_var_num[k] = j; - d_arg_props.push_back(CegConjectureProcessArg()); + d_arg_props.push_back(SynthConjectureProcessArg()); } } -bool CegConjectureProcessFun::checkMatch( +bool SynthConjectureProcessFun::checkMatch( Node cn, Node n, std::unordered_map& n_arg_map) { std::vector vars; @@ -73,7 +73,7 @@ bool CegConjectureProcessFun::checkMatch( return cn_subs == n; } -bool CegConjectureProcessFun::isArgVar(Node n, unsigned& arg_index) +bool SynthConjectureProcessFun::isArgVar(Node n, unsigned& arg_index) { if (n.isVar()) { @@ -88,7 +88,7 @@ bool CegConjectureProcessFun::isArgVar(Node n, unsigned& arg_index) return false; } -Node CegConjectureProcessFun::inferDefinition( +Node SynthConjectureProcessFun::inferDefinition( Node n, std::unordered_map& term_to_arg_carry, std::unordered_map& args) +unsigned SynthConjectureProcessFun::assignRelevantDef( + Node def, std::vector& args) { unsigned id = 0; if (def.isNull()) @@ -250,7 +250,7 @@ unsigned CegConjectureProcessFun::assignRelevantDef(Node def, return rid; } -void CegConjectureProcessFun::processTerms( +void SynthConjectureProcessFun::processTerms( std::vector& ns, std::vector& ks, Node nf, @@ -504,12 +504,12 @@ void CegConjectureProcessFun::processTerms( } } -bool CegConjectureProcessFun::isArgRelevant(unsigned i) +bool SynthConjectureProcessFun::isArgRelevant(unsigned i) { return d_arg_props[i].d_relevant; } -void CegConjectureProcessFun::getIrrelevantArgs( +void SynthConjectureProcessFun::getIrrelevantArgs( std::unordered_set& args) { for (unsigned i = 0; i < d_arg_vars.size(); i++) @@ -521,15 +521,15 @@ void CegConjectureProcessFun::getIrrelevantArgs( } } -CegConjectureProcess::CegConjectureProcess(QuantifiersEngine* qe) {} -CegConjectureProcess::~CegConjectureProcess() {} -Node CegConjectureProcess::preSimplify(Node q) +SynthConjectureProcess::SynthConjectureProcess(QuantifiersEngine* qe) {} +SynthConjectureProcess::~SynthConjectureProcess() {} +Node SynthConjectureProcess::preSimplify(Node q) { Trace("sygus-process") << "Pre-simplify conjecture : " << q << std::endl; return q; } -Node CegConjectureProcess::postSimplify(Node q) +Node SynthConjectureProcess::postSimplify(Node q) { Trace("sygus-process") << "Post-simplify conjecture : " << q << std::endl; Assert(q.getKind() == FORALL); @@ -561,7 +561,7 @@ Node CegConjectureProcess::postSimplify(Node q) getComponentVector(AND, base, conjuncts); // process the conjunctions - for (std::map::iterator it = + for (std::map::iterator it = d_sf_info.begin(); it != d_sf_info.end(); ++it) @@ -577,7 +577,7 @@ Node CegConjectureProcess::postSimplify(Node q) return q; } -void CegConjectureProcess::initialize(Node n, std::vector& candidates) +void SynthConjectureProcess::initialize(Node n, std::vector& candidates) { if (Trace.isOn("sygus-process")) { @@ -590,13 +590,13 @@ void CegConjectureProcess::initialize(Node n, std::vector& candidates) } } -bool CegConjectureProcess::isArgRelevant(Node f, unsigned i) +bool SynthConjectureProcess::isArgRelevant(Node f, unsigned i) { if (!options::sygusArgRelevant()) { return true; } - std::map::iterator its = d_sf_info.find(f); + std::map::iterator its = d_sf_info.find(f); if (its != d_sf_info.end()) { return its->second.isArgRelevant(i); @@ -605,10 +605,10 @@ bool CegConjectureProcess::isArgRelevant(Node f, unsigned i) return true; } -bool CegConjectureProcess::getIrrelevantArgs(Node f, - std::unordered_set& args) +bool SynthConjectureProcess::getIrrelevantArgs( + Node f, std::unordered_set& args) { - std::map::iterator its = d_sf_info.find(f); + std::map::iterator its = d_sf_info.find(f); if (its != d_sf_info.end()) { its->second.getIrrelevantArgs(args); @@ -617,7 +617,7 @@ bool CegConjectureProcess::getIrrelevantArgs(Node f, return false; } -void CegConjectureProcess::processConjunct( +void SynthConjectureProcess::processConjunct( Node n, Node f, std::unordered_set& synth_fv) { Trace("sygus-process-arg-deps") << "Process conjunct: " << std::endl; @@ -655,7 +655,7 @@ void CegConjectureProcess::processConjunct( // process the applications of synthesis functions if (!ns.empty()) { - std::map::iterator its = d_sf_info.find(f); + std::map::iterator its = d_sf_info.find(f); if (its != d_sf_info.end()) { its->second.processTerms(ns, ks, nf, synth_fv_n, free_vars); @@ -663,7 +663,7 @@ void CegConjectureProcess::processConjunct( } } -Node CegConjectureProcess::CegConjectureProcess::flatten( +Node SynthConjectureProcess::SynthConjectureProcess::flatten( Node n, Node f, std::unordered_set& synth_fv, @@ -728,7 +728,7 @@ Node CegConjectureProcess::CegConjectureProcess::flatten( return visited[n]; } -void CegConjectureProcess::getFreeVariables( +void SynthConjectureProcess::getFreeVariables( Node n, std::unordered_set& synth_fv, std::unordered_map& args) +void SynthConjectureProcess::debugPrint(const char* c) {} +void SynthConjectureProcess::getComponentVector(Kind k, + Node n, + std::vector& args) { if (n.getKind() == k) { diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h index b16118b2e..199619699 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.h +++ b/src/theory/quantifiers/sygus/sygus_process_conj.h @@ -88,10 +88,10 @@ namespace quantifiers { * position in the function to synthesize is * relevant. */ -class CegConjectureProcessArg +class SynthConjectureProcessArg { public: - CegConjectureProcessArg() : d_var_single_occ(false), d_relevant(false) {} + SynthConjectureProcessArg() : d_var_single_occ(false), d_relevant(false) {} /** template definition * This is the term s[z] described * under "Argument Invariance" above. @@ -120,11 +120,11 @@ class CegConjectureProcessArg * It maintains information about each of the function to * synthesize's arguments. */ -struct CegConjectureProcessFun +struct SynthConjectureProcessFun { public: - CegConjectureProcessFun() {} - ~CegConjectureProcessFun() {} + SynthConjectureProcessFun() {} + ~SynthConjectureProcessFun() {} /** initialize this class for function f */ void init(Node f); /** process terms @@ -159,12 +159,12 @@ struct CegConjectureProcessFun /** the synth fun associated with this */ Node d_synth_fun; /** properties of each argument */ - std::vector d_arg_props; + std::vector d_arg_props; /** variables for each argument type of f * * These are used to express templates for argument * invariance, in the data member - * CegConjectureProcessArg::d_template. + * SynthConjectureProcessArg::d_template. */ std::vector d_arg_vars; /** map from d_arg_vars to the argument # @@ -254,51 +254,50 @@ struct CegConjectureProcessFun }; /** Ceg Conjecture Process -* -* This class implements static techniques for preprocessing and analysis of -* sygus conjectures. -* -* It is used as a back-end to CegConjecture, which calls it using the following -* interface: -* (1) When a sygus conjecture is asserted, we call -* CegConjectureProcess::simplify( q ), -* where q is the sygus conjecture in original form. -* -* (2) After a sygus conjecture is simplified and converted to deep -* embedding form, we call CegConjectureProcess::initialize( n, candidates ). -* -* (3) During enumerative SyGuS search, calls may be made by -* the extension of the quantifier-free datatypes decision procedure for -* sygus to CegConjectureProcess::getSymmetryBreakingPredicate(...), which are -* used for pruning search space based on conjecture-specific analysis. -*/ -class CegConjectureProcess + * + * This class implements static techniques for preprocessing and analysis of + * sygus conjectures. + * + * It is used as a back-end to SynthConjecture, which calls it using the + * following interface: (1) When a sygus conjecture is asserted, we call + * SynthConjectureProcess::simplify( q ), + * where q is the sygus conjecture in original form. + * + * (2) After a sygus conjecture is simplified and converted to deep + * embedding form, we call SynthConjectureProcess::initialize( n, candidates ). + * + * (3) During enumerative SyGuS search, calls may be made by + * the extension of the quantifier-free datatypes decision procedure for + * sygus to SynthConjectureProcess::getSymmetryBreakingPredicate(...), which are + * used for pruning search space based on conjecture-specific analysis. + */ +class SynthConjectureProcess { public: - CegConjectureProcess(QuantifiersEngine* qe); - ~CegConjectureProcess(); + SynthConjectureProcess(QuantifiersEngine* qe); + ~SynthConjectureProcess(); /** simplify the synthesis conjecture q - * Returns a formula that is equivalent to q. - * This simplification pass is called before all others - * in CegConjecture::assign. - * - * This function is intended for simplifications that - * impact whether or not the synthesis conjecture is - * single-invocation. - */ + * Returns a formula that is equivalent to q. + * This simplification pass is called before all others + * in SynthConjecture::assign. + * + * This function is intended for simplifications that + * impact whether or not the synthesis conjecture is + * single-invocation. + */ Node preSimplify(Node q); /** simplify the synthesis conjecture q - * Returns a formula that is equivalent to q. - * This simplification pass is called after all others - * in CegConjecture::assign. - */ + * Returns a formula that is equivalent to q. + * This simplification pass is called after all others + * in SynthConjecture::assign. + */ Node postSimplify(Node q); /** initialize - * - * n is the "base instantiation" of the deep-embedding version of - * the synthesis conjecture under "candidates". - * (see CegConjecture::d_base_inst) - */ + * + * n is the "base instantiation" of the deep-embedding version of + * the synthesis conjecture under "candidates". + * (see SynthConjecture::d_base_inst) + */ void initialize(Node n, std::vector& candidates); /** is the i^th argument of the function-to-synthesize f relevant? */ bool isArgRelevant(Node f, unsigned i); @@ -352,7 +351,7 @@ class CegConjectureProcess std::unordered_set, NodeHashFunction>& free_vars); /** for each synth-fun, information that is specific to this conjecture */ - std::map d_sf_info; + std::map d_sf_info; /** get component vector */ void getComponentVector(Kind k, Node n, std::vector& args); diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 66639b750..b8d98a6f7 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -18,7 +18,7 @@ #include "options/quantifiers_options.h" #include "printer/printer.h" #include "theory/datatypes/datatypes_rewriter.h" -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include @@ -29,7 +29,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SygusUnifRl::SygusUnifRl(CegConjecture* p) : d_parent(p) {} +SygusUnifRl::SygusUnifRl(SynthConjecture* p) : d_parent(p) {} SygusUnifRl::~SygusUnifRl() {} void SygusUnifRl::initializeCandidate( QuantifiersEngine* qe, diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index aad3c0b49..7b07de34e 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -35,7 +35,7 @@ using BoolNodePairMap = using NodePairMap = std::unordered_map; using NodePair = std::pair; -class CegConjecture; +class SynthConjecture; /** Sygus unification Refinement Lemmas utility * @@ -46,7 +46,7 @@ class CegConjecture; class SygusUnifRl : public SygusUnif { public: - SygusUnifRl(CegConjecture* p); + SygusUnifRl(SynthConjecture* p); ~SygusUnifRl(); /** initialize */ @@ -105,7 +105,7 @@ class SygusUnifRl : public SygusUnif protected: /** reference to the parent conjecture */ - CegConjecture* d_parent; + SynthConjecture* d_parent; /* Functions-to-synthesize (a.k.a. candidates) with unification strategies */ std::unordered_set d_unif_candidates; /** construct sol */ diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp similarity index 84% rename from src/theory/quantifiers/sygus/ce_guided_conjecture.cpp rename to src/theory/quantifiers/sygus/synth_conjecture.cpp index 30c0a3ae1..fde69d196 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file ce_guided_conjecture.cpp +/*! \file synth_conjecture.cpp ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Haniel Barbosa @@ -9,10 +9,10 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief implementation of class that encapsulates counterexample-guided instantiation - ** techniques for a single SyGuS synthesis conjecture + ** \brief Implementation of class that encapsulates techniques for a single + ** (SyGuS) synthesis conjecture. **/ -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" #include "expr/datatype.h" #include "options/base_options.h" @@ -26,7 +26,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/sygus/ce_guided_instantiation.h" +#include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" @@ -38,13 +38,13 @@ namespace CVC4 { namespace theory { namespace quantifiers { -CegConjecture::CegConjecture(QuantifiersEngine* qe) +SynthConjecture::SynthConjecture(QuantifiersEngine* qe) : d_qe(qe), - d_ceg_si(new CegConjectureSingleInv(qe, this)), - d_ceg_proc(new CegConjectureProcess(qe)), + d_ceg_si(new CegSingleInv(qe, this)), + d_ceg_proc(new SynthConjectureProcess(qe)), d_ceg_gc(new CegGrammarConstructor(qe, this)), d_sygus_rconst(new SygusRepairConst(qe)), - d_ceg_pbe(new CegConjecturePbe(qe, this)), + d_ceg_pbe(new SygusPbe(qe, this)), d_ceg_cegis(new Cegis(qe, this)), d_ceg_cegisUnif(new CegisUnif(qe, this)), d_master(nullptr), @@ -63,30 +63,33 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe) d_modules.push_back(d_ceg_cegis.get()); } -CegConjecture::~CegConjecture() {} +SynthConjecture::~SynthConjecture() {} -void CegConjecture::assign( Node q ) { - Assert( d_embed_quant.isNull() ); - Assert( q.getKind()==FORALL ); - Trace("cegqi") << "CegConjecture : assign : " << q << std::endl; +void SynthConjecture::assign(Node q) +{ + Assert(d_embed_quant.isNull()); + Assert(q.getKind() == FORALL); + Trace("cegqi") << "SynthConjecture : assign : " << q << std::endl; d_quant = q; NodeManager* nm = NodeManager::currentNM(); // pre-simplify the quantified formula based on the process utility d_simp_quant = d_ceg_proc->preSimplify(d_quant); - std::map< Node, Node > templates; - std::map< Node, Node > templates_arg; - //register with single invocation if applicable + std::map templates; + std::map templates_arg; + // register with single invocation if applicable if (d_qe->getQuantAttributes()->isSygus(q)) { d_ceg_si->initialize(d_simp_quant); d_simp_quant = d_ceg_si->getSimplifiedConjecture(); // carry the templates - for( unsigned i=0; igetTemplate(v); - if( !templ.isNull() ){ + if (!templ.isNull()) + { templates[v] = templ; templates_arg[v] = d_ceg_si->getTemplateArg(v); } @@ -100,23 +103,28 @@ void CegConjecture::assign( Node q ) { // convert to deep embedding and finalize single invocation here d_embed_quant = d_ceg_gc->process(d_simp_quant, templates, templates_arg); - Trace("cegqi") << "CegConjecture : converted to embedding : " << d_embed_quant << std::endl; + Trace("cegqi") << "SynthConjecture : converted to embedding : " + << d_embed_quant << std::endl; - // we now finalize the single invocation module, based on the syntax restrictions + // we now finalize the single invocation module, based on the syntax + // restrictions if (d_qe->getQuantAttributes()->isSygus(q)) { d_ceg_si->finishInit(d_ceg_gc->isSyntaxRestricted()); } - Assert( d_candidates.empty() ); - std::vector< Node > vars; - for( unsigned i=0; imkSkolem( "e", d_embed_quant[0][i].getType() ); - d_candidates.push_back( e ); + Assert(d_candidates.empty()); + std::vector vars; + for (unsigned i = 0; i < d_embed_quant[0].getNumChildren(); i++) + { + vars.push_back(d_embed_quant[0][i]); + Node e = + NodeManager::currentNM()->mkSkolem("e", d_embed_quant[0][i].getType()); + d_candidates.push_back(e); } - Trace("cegqi") << "Base quantified formula is : " << d_embed_quant << std::endl; - //construct base instantiation + Trace("cegqi") << "Base quantified formula is : " << d_embed_quant + << std::endl; + // construct base instantiation 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; @@ -139,8 +147,9 @@ void CegConjecture::assign( Node q ) { // register this term with sygus database and other utilities that impact // the enumerative sygus search - std::vector< Node > guarded_lemmas; - if( !isSingleInvocation() ){ + std::vector guarded_lemmas; + if (!isSingleInvocation()) + { d_ceg_proc->initialize(d_base_inst, d_candidates); for (unsigned i = 0, size = d_modules.size(); i < size; i++) { @@ -162,7 +171,7 @@ void CegConjecture::assign( Node q ) { d_inner_vars.push_back(v); } } - + // initialize the guard d_feasible_guard = nm->mkSkolem("G", nm->booleanType()); d_feasible_guard = Rewriter::rewrite(d_feasible_guard); @@ -183,22 +192,27 @@ void CegConjecture::assign( Node q ) { if (isSingleInvocation()) { - std::vector< Node > lems; + std::vector lems; d_ceg_si->getInitialSingleInvLemma(d_feasible_guard, lems); - for( unsigned i=0; igetOutputChannel().lemma( lems[i] ); - if( Trace.isOn("cegqi-debug") ){ - Node rlem = Rewriter::rewrite( lems[i] ); + for (unsigned i = 0; i < lems.size(); i++) + { + Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation " << i << " : " + << lems[i] << std::endl; + d_qe->getOutputChannel().lemma(lems[i]); + if (Trace.isOn("cegqi-debug")) + { + Node rlem = Rewriter::rewrite(lems[i]); Trace("cegqi-debug") << "...rewritten : " << rlem << std::endl; } } } Node gneg = d_feasible_guard.negate(); - for( unsigned i=0; imkNode(OR, gneg, guarded_lemmas[i]); - Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem << std::endl; - d_qe->getOutputChannel().lemma( lem ); + Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem + << std::endl; + d_qe->getOutputChannel().lemma(lem); } if (options::sygusStream()) @@ -210,18 +224,21 @@ void CegConjecture::assign( Node q ) { d_stream_strategy.get()); d_current_stream_guard = d_stream_strategy->getLiteral(0); } - Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() << std::endl; + Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() + << std::endl; } -Node CegConjecture::getGuard() const { return d_feasible_guard; } +Node SynthConjecture::getGuard() const { return d_feasible_guard; } -bool CegConjecture::isSingleInvocation() const { +bool SynthConjecture::isSingleInvocation() const +{ return d_ceg_si->isSingleInvocation(); } -bool CegConjecture::needsCheck() +bool SynthConjecture::needsCheck() { - if( isSingleInvocation() && !d_ceg_si->needsCheck() ){ + if (isSingleInvocation() && !d_ceg_si->needsCheck()) + { return false; } bool value; @@ -244,15 +261,16 @@ bool CegConjecture::needsCheck() return true; } - -void CegConjecture::doSingleInvCheck(std::vector< Node >& lems) { - if( d_ceg_si!=NULL ){ +void SynthConjecture::doSingleInvCheck(std::vector& lems) +{ + if (d_ceg_si != NULL) + { d_ceg_si->check(lems); } } -bool CegConjecture::needsRefinement() const { return d_set_ce_sk_vars; } -void CegConjecture::doCheck(std::vector& lems) +bool SynthConjecture::needsRefinement() const { return d_set_ce_sk_vars; } +void SynthConjecture::doCheck(std::vector& lems) { Assert(d_master != nullptr); @@ -331,11 +349,14 @@ void CegConjecture::doCheck(std::vector& lems) NodeManager* nm = NodeManager::currentNM(); - //must get a counterexample to the value of the current candidate + // 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; + if (constructed_cand) + { + if (Trace.isOn("cegqi-check")) + { + Trace("cegqi-check") << "CegConjuncture : check candidate : " + << std::endl; for (unsigned i = 0, size = candidate_values.size(); i < size; i++) { Trace("cegqi-check") << " " << i << " : " << d_candidates[i] << " -> " @@ -347,13 +368,16 @@ void CegConjecture::doCheck(std::vector& lems) d_candidates.end(), candidate_values.begin(), candidate_values.end()); - }else{ + } + else + { inst = d_base_inst; } - - //check whether we will run CEGIS on inner skolem variables + + // check whether we will run CEGIS on inner skolem variables bool sk_refine = (!isGround() || d_refine_count == 0) && constructed_cand; - if( sk_refine ){ + if (sk_refine) + { if (options::cegisSample() == CEGIS_SAMPLE_TRUST) { // we have that the current candidate passed a sample test @@ -366,13 +390,16 @@ void CegConjecture::doCheck(std::vector& lems) return; } Assert(!d_set_ce_sk_vars); - }else{ - if( !constructed_cand ){ + } + else + { + if (!constructed_cand) + { return; } } - - //immediately skolemize inner existentials + + // immediately skolemize inner existentials Node lem; // introduce the skolem variables std::vector sks; @@ -488,16 +515,18 @@ void CegConjecture::doCheck(std::vector& lems) lem = getStreamGuardedLemma(lem); lems.push_back(lem); } - -void CegConjecture::doRefine( std::vector< Node >& lems ){ - Assert( lems.empty() ); + +void SynthConjecture::doRefine(std::vector& lems) +{ + Assert(lems.empty()); Assert(d_set_ce_sk_vars); - //first, make skolem substitution - Trace("cegqi-refine") << "doRefine : construct skolem substitution..." << std::endl; - std::vector< Node > sk_vars; - std::vector< Node > sk_subs; - //collect the substitution over all disjuncts + // first, make skolem substitution + Trace("cegqi-refine") << "doRefine : construct skolem substitution..." + << std::endl; + std::vector sk_vars; + std::vector sk_subs; + // collect the substitution over all disjuncts if (!d_ce_sk_vars.empty()) { Trace("cegqi-refine") << "Get model values for skolems..." << std::endl; @@ -521,8 +550,9 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){ Assert(d_inner_vars.empty()); } - std::vector< Node > lem_c; - Trace("cegqi-refine") << "doRefine : Construct refinement lemma..." << std::endl; + std::vector lem_c; + Trace("cegqi-refine") << "doRefine : Construct refinement lemma..." + << std::endl; Trace("cegqi-refine-debug") << " For counterexample skolems : " << d_ce_sk_vars << std::endl; Node base_lem; @@ -535,12 +565,13 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){ base_lem = d_base_inst.negate(); } - Assert( sk_vars.size()==sk_subs.size() ); + Assert(sk_vars.size() == sk_subs.size()); Trace("cegqi-refine") << "doRefine : substitute..." << std::endl; - base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); + base_lem = base_lem.substitute( + sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end()); Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl; - base_lem = Rewriter::rewrite( base_lem ); + base_lem = Rewriter::rewrite(base_lem); Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem << "..." << std::endl; d_master->registerRefinementLemma(sk_vars, base_lem, lems); @@ -550,16 +581,20 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){ d_ce_sk_var_mvs.clear(); } -void CegConjecture::preregisterConjecture( Node q ) { - d_ceg_si->preregisterConjecture( q ); +void SynthConjecture::preregisterConjecture(Node q) +{ + d_ceg_si->preregisterConjecture(q); } -void CegConjecture::getModelValues( std::vector< Node >& n, std::vector< Node >& v ) { +void SynthConjecture::getModelValues(std::vector& n, std::vector& v) +{ Trace("cegqi-engine") << " * Value is : "; - for( unsigned i=0; i "; std::stringstream ss; @@ -572,23 +607,26 @@ void CegConjecture::getModelValues( std::vector< Node >& n, std::vector< Node >& Trace("cegqi-engine-rr") << " -> " << bv << std::endl; } } - Assert( !nv.isNull() ); + Assert(!nv.isNull()); } Trace("cegqi-engine") << std::endl; } -Node CegConjecture::getModelValue( Node n ) { +Node SynthConjecture::getModelValue(Node n) +{ Trace("cegqi-mv") << "getModelValue for : " << n << std::endl; - return d_qe->getModel()->getValue( n ); + return d_qe->getModel()->getValue(n); } -void CegConjecture::debugPrint( const char * c ) { +void SynthConjecture::debugPrint(const char* c) +{ Trace(c) << "Synthesis conjecture : " << d_embed_quant << std::endl; Trace(c) << " * Candidate programs : " << d_candidates << std::endl; Trace(c) << " * Counterexample skolems : " << d_ce_sk_vars << std::endl; } -Node CegConjecture::getCurrentStreamGuard() const { +Node SynthConjecture::getCurrentStreamGuard() const +{ if (d_stream_strategy != nullptr) { // the stream guard is the current asserted literal of the stream strategy @@ -603,7 +641,7 @@ Node CegConjecture::getCurrentStreamGuard() const { return Node::null(); } -Node CegConjecture::getStreamGuardedLemma(Node n) const +Node SynthConjecture::getStreamGuardedLemma(Node n) const { if (options::sygusStream()) { @@ -615,20 +653,20 @@ Node CegConjecture::getStreamGuardedLemma(Node n) const return n; } -CegConjecture::SygusStreamDecisionStrategy::SygusStreamDecisionStrategy( +SynthConjecture::SygusStreamDecisionStrategy::SygusStreamDecisionStrategy( context::Context* satContext, Valuation valuation) : DecisionStrategyFmf(satContext, valuation) { } -Node CegConjecture::SygusStreamDecisionStrategy::mkLiteral(unsigned i) +Node SynthConjecture::SygusStreamDecisionStrategy::mkLiteral(unsigned i) { NodeManager* nm = NodeManager::currentNM(); Node curr_stream_guard = nm->mkSkolem("G_Stream", nm->booleanType()); return curr_stream_guard; } -void CegConjecture::printAndContinueStream() +void SynthConjecture::printAndContinueStream() { Assert(d_master != nullptr); // we have generated a solution, print it @@ -668,9 +706,11 @@ void CegConjecture::printAndContinueStream() d_qe->getOutputChannel().lemma(exc_lem); } -void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation ) { +void SynthConjecture::printSynthSolution(std::ostream& out, + bool singleInvocation) +{ Trace("cegqi-debug") << "Printing synth solution..." << std::endl; - Assert( d_quant[0].getNumChildren()==d_embed_quant[0].getNumChildren() ); + Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren()); std::vector sols; std::vector statuses; if (!getSynthSolutionsInternal(sols, statuses, singleInvocation)) @@ -690,7 +730,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation ss << prog; std::string f(ss.str()); f.erase(f.begin()); - CegInstantiation* cei = d_qe->getCegInstantiation(); + SynthEngine* cei = d_qe->getSynthEngine(); ++(cei->d_statistics.d_solutions); bool is_unique_term = true; @@ -747,8 +787,8 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation } } -void CegConjecture::getSynthSolutions(std::map& sol_map, - bool singleInvocation) +void SynthConjecture::getSynthSolutions(std::map& sol_map, + bool singleInvocation) { NodeManager* nm = NodeManager::currentNM(); TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus(); @@ -784,9 +824,9 @@ void CegConjecture::getSynthSolutions(std::map& sol_map, } } -bool CegConjecture::getSynthSolutionsInternal(std::vector& sols, - std::vector& statuses, - bool singleInvocation) +bool SynthConjecture::getSynthSolutionsInternal(std::vector& sols, + std::vector& statuses, + bool singleInvocation) { for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) { @@ -868,7 +908,7 @@ bool CegConjecture::getSynthSolutionsInternal(std::vector& sols, return true; } -Node CegConjecture::getSymmetryBreakingPredicate( +Node SynthConjecture::getSymmetryBreakingPredicate( Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth) { std::vector sb_lemmas; @@ -895,6 +935,6 @@ Node CegConjecture::getSymmetryBreakingPredicate( } } -}/* namespace CVC4::theory::quantifiers */ -}/* namespace CVC4::theory */ -}/* namespace CVC4 */ +} // namespace quantifiers +} // namespace theory +} /* namespace CVC4 */ diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h similarity index 79% rename from src/theory/quantifiers/sygus/ce_guided_conjecture.h rename to src/theory/quantifiers/sygus/synth_conjecture.h index adc75056e..1cbd4e949 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file ce_guided_conjecture.h +/*! \file synth_conjecture.h ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Haniel Barbosa @@ -9,14 +9,14 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief class that encapsulates counterexample-guided instantiation - ** techniques for a single SyGuS synthesis conjecture + ** \brief Class that encapsulates techniques for a single (SyGuS) synthesis + ** conjecture. **/ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H -#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H +#ifndef __CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H +#define __CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H #include @@ -42,10 +42,11 @@ namespace quantifiers { * determines which approach and optimizations are applicable to the * conjecture, and has interfaces for implementing them. */ -class CegConjecture { -public: - CegConjecture( QuantifiersEngine * qe ); - ~CegConjecture(); +class SynthConjecture +{ + public: + SynthConjecture(QuantifiersEngine* qe); + ~SynthConjecture(); /** get original version of conjecture */ Node getConjecture() { return d_quant; } /** get deep embedding version of conjecture */ @@ -58,18 +59,19 @@ public: bool needsCheck(); /** whether the conjecture is waiting for a call to doRefine below */ bool needsRefinement() const; - /** do single invocation check - * This updates Gamma for an iteration of step 2 of Figure 1 of Reynolds et al CAV 2015. - */ - void doSingleInvCheck(std::vector< Node >& lems); - /** do syntax-guided enumerative check - * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015. - */ + /** do single invocation check + * This updates Gamma for an iteration of step 2 of Figure 1 of Reynolds et al + * CAV 2015. + */ + void doSingleInvCheck(std::vector& lems); + /** do syntax-guided enumerative check + * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015. + */ void doCheck(std::vector& lems); - /** do refinement - * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015. - */ - void doRefine(std::vector< Node >& lems); + /** do refinement + * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015. + */ + void doRefine(std::vector& lems); //-------------------------------end for counterexample-guided check/refine /** * prints the synthesis solution to output stream out. @@ -77,7 +79,7 @@ public: * singleInvocation : set to true if we should consult the single invocation * module to get synthesis solutions. */ - void printSynthSolution( std::ostream& out, bool singleInvocation ); + void printSynthSolution(std::ostream& out, bool singleInvocation); /** get synth solutions * * This returns a map from function-to-synthesize variables to their @@ -99,43 +101,45 @@ public: bool isGround() { return d_inner_vars.empty(); } /** are we using single invocation techniques */ bool isSingleInvocation() const; - /** preregister conjecture - * This is used as a heuristic for solution reconstruction, so that we - * remember expressions in the conjecture before preprocessing, since they - * may be helpful during solution reconstruction (Figure 5 of Reynolds et al CAV 2015) - */ - void preregisterConjecture( Node q ); + /** preregister conjecture + * This is used as a heuristic for solution reconstruction, so that we + * remember expressions in the conjecture before preprocessing, since they + * may be helpful during solution reconstruction (Figure 5 of Reynolds et al + * CAV 2015) + */ + void preregisterConjecture(Node q); /** assign conjecture q to this class */ - void assign( Node q ); + void assign(Node q); /** has a conjecture been assigned to this class */ bool isAssigned() { return !d_embed_quant.isNull(); } /** get model values for terms n, store in vector v */ - void getModelValues( std::vector< Node >& n, std::vector< Node >& v ); + void getModelValues(std::vector& n, std::vector& v); /** get model value for term n */ - Node getModelValue( Node n ); + Node getModelValue(Node n); /** get utility for static preprocessing and analysis of conjectures */ - CegConjectureProcess* getProcess() { return d_ceg_proc.get(); } + SynthConjectureProcess* getProcess() { return d_ceg_proc.get(); } /** get constant repair utility */ SygusRepairConst* getRepairConst() { return d_sygus_rconst.get(); } /** get program by examples module */ - CegConjecturePbe* getPbe() { return d_ceg_pbe.get(); } + SygusPbe* getPbe() { return d_ceg_pbe.get(); } /** get the symmetry breaking predicate for type */ Node getSymmetryBreakingPredicate( Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth); /** print out debug information about this conjecture */ - void debugPrint( const char * c ); -private: + void debugPrint(const char* c); + + private: /** reference to quantifier engine */ - QuantifiersEngine * d_qe; + QuantifiersEngine* d_qe; /** The feasible guard. */ Node d_feasible_guard; /** the decision strategy for the feasible guard */ std::unique_ptr d_feasible_strategy; /** single invocation utility */ - std::unique_ptr d_ceg_si; + std::unique_ptr d_ceg_si; /** utility for static preprocessing and analysis of conjectures */ - std::unique_ptr d_ceg_proc; + std::unique_ptr d_ceg_proc; /** grammar utility */ std::unique_ptr d_ceg_gc; /** repair constant utility */ @@ -143,7 +147,7 @@ private: //------------------------modules /** program by examples module */ - std::unique_ptr d_ceg_pbe; + std::unique_ptr d_ceg_pbe; /** CEGIS module */ std::unique_ptr d_ceg_cegis; /** CEGIS UNIF module */ @@ -159,17 +163,17 @@ private: //------------------------end modules /** list of constants for quantified formula - * The outer Skolems for the negation of d_embed_quant. - */ - std::vector< Node > d_candidates; + * The outer Skolems for the negation of d_embed_quant. + */ + std::vector d_candidates; /** base instantiation - * If d_embed_quant is forall d. exists y. P( d, y ), then - * this is the formula exists y. P( d_candidates, y ). Notice that - * (exists y. F) is shorthand above for ~( forall y. ~F ). - */ + * If d_embed_quant is forall d. exists y. P( d, y ), then + * this is the formula exists y. P( d_candidates, y ). Notice that + * (exists y. F) is shorthand above for ~( forall y. ~F ). + */ Node d_base_inst; /** list of variables on inner quantification */ - std::vector< Node > d_inner_vars; + std::vector d_inner_vars; /** * The set of skolems for the current "verification" lemma, if one exists. * This may be added to during calls to doCheck(). The model values for these @@ -195,11 +199,12 @@ private: /** (negated) conjecture after simplification, conversion to deep embedding */ Node d_embed_quant; /** candidate information */ - class CandidateInfo { - public: - CandidateInfo(){} + class CandidateInfo + { + public: + CandidateInfo() {} /** list of terms we have instantiated candidates with */ - std::vector< Node > d_inst; + std::vector d_inst; }; std::map d_cinfo; /** @@ -210,12 +215,14 @@ private: /** number of times we have called doRefine */ unsigned d_refine_count; /** get candidadate */ - Node getCandidate( unsigned int i ) { return d_candidates[i]; } + Node getCandidate(unsigned int i) { return d_candidates[i]; } /** record instantiation (this is used to construct solutions later) */ - void recordInstantiation( std::vector< Node >& vs ) { - Assert( vs.size()==d_candidates.size() ); - for( unsigned i=0; i& vs) + { + Assert(vs.size() == d_candidates.size()); + for (unsigned i = 0; i < vs.size(); i++) + { + d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]); } } /** get synth solutions internal @@ -284,8 +291,8 @@ private: std::map d_exprm; }; -} /* namespace CVC4::theory::quantifiers */ -} /* namespace CVC4::theory */ +} // namespace quantifiers +} // namespace theory } /* namespace CVC4 */ #endif diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp similarity index 83% rename from src/theory/quantifiers/sygus/ce_guided_instantiation.cpp rename to src/theory/quantifiers/sygus/synth_engine.cpp index d30cccd87..56844ec1f 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file ce_guided_instantiation.cpp +/*! \file synth_engine.cpp ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Morgan Deters @@ -9,11 +9,11 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief counterexample guided instantiation class - ** This class is the entry point for both synthesis algorithms in Reynolds et al CAV 2015 + ** \brief Implementation of the quantifiers module for managing all approaches + ** to synthesis, in particular, those described in Reynolds et al CAV 2015. ** **/ -#include "theory/quantifiers/sygus/ce_guided_instantiation.h" +#include "theory/quantifiers/sygus/synth_engine.h" #include "options/quantifiers_options.h" #include "smt/smt_engine.h" @@ -31,26 +31,27 @@ namespace CVC4 { namespace theory { namespace quantifiers { -CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){ - d_conj = new CegConjecture( qe ); +SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c) + : QuantifiersModule(qe) +{ + d_conj = new SynthConjecture(qe); d_last_inst_si = false; } -CegInstantiation::~CegInstantiation(){ - delete d_conj; -} +SynthEngine::~SynthEngine() { delete d_conj; } -bool CegInstantiation::needsCheck( Theory::Effort e ) { +bool SynthEngine::needsCheck(Theory::Effort e) +{ return !d_quantEngine->getTheoryEngine()->needCheck() && e >= Theory::EFFORT_LAST_CALL; } -QuantifiersModule::QEffort CegInstantiation::needsModel(Theory::Effort e) +QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e) { return d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL; } -void CegInstantiation::check(Theory::Effort e, QEffort quant_e) +void SynthEngine::check(Theory::Effort e, QEffort quant_e) { // are we at the proper effort level? unsigned echeck = @@ -100,7 +101,7 @@ void CegInstantiation::check(Theory::Effort e, QEffort quant_e) << "Finished Counterexample Guided Instantiation engine." << std::endl; } -bool CegInstantiation::assignConjecture(Node q) +bool SynthEngine::assignConjecture(Node q) { if (d_conj->isAssigned()) { @@ -231,7 +232,7 @@ bool CegInstantiation::assignConjecture(Node q) return true; } -void CegInstantiation::registerQuantifier(Node q) +void SynthEngine::registerQuantifier(Node q) { if (d_quantEngine->getOwner(q) == this) { // && d_eval_axioms.find( q )==d_eval_axioms.end() ){ @@ -247,24 +248,30 @@ void CegInstantiation::registerQuantifier(Node q) // assign it now assignConjecture(q); } - }else{ - Assert( d_conj->getEmbeddedConjecture()==q ); } - }else{ + else + { + Assert(d_conj->getEmbeddedConjecture() == q); + } + } + else + { Trace("cegqi-debug") << "Register quantifier : " << q << std::endl; } } -void CegInstantiation::checkConjecture(CegConjecture* conj) +void SynthEngine::checkConjecture(SynthConjecture* conj) { Node q = conj->getEmbeddedConjecture(); Node aq = conj->getConjecture(); - if( Trace.isOn("cegqi-engine-debug") ){ + if (Trace.isOn("cegqi-engine-debug")) + { conj->debugPrint("cegqi-engine-debug"); Trace("cegqi-engine-debug") << std::endl; } - if( !conj->needsRefinement() ){ + if (!conj->needsRefinement()) + { Trace("cegqi-engine-debug") << "Do conjecture check..." << std::endl; if (conj->isSingleInvocation()) { @@ -308,7 +315,9 @@ void CegInstantiation::checkConjecture(CegConjecture* conj) { ++(d_statistics.d_cegqi_lemmas_ce); addedLemma = true; - }else{ + } + else + { // this may happen if we eagerly unfold, simplify to true Trace("cegqi-engine-debug") << " ...FAILED to add candidate!" << std::endl; @@ -317,7 +326,9 @@ void CegInstantiation::checkConjecture(CegConjecture* conj) if (addedLemma) { Trace("cegqi-engine") << " ...check for counterexample." << std::endl; - }else{ + } + else + { if (conj->needsRefinement()) { // immediately go to refine candidate @@ -325,41 +336,50 @@ void CegInstantiation::checkConjecture(CegConjecture* conj) return; } } - }else{ + } + else + { Trace("cegqi-engine") << " *** Refine candidate phase..." << std::endl; - std::vector< Node > rlems; - conj->doRefine( rlems ); + std::vector rlems; + conj->doRefine(rlems); bool addedLemma = false; - for( unsigned i=0; iaddLemma( lem ); - if( res ){ + Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem + << std::endl; + bool res = d_quantEngine->addLemma(lem); + if (res) + { ++(d_statistics.d_cegqi_lemmas_refine); conj->incrementRefineCount(); addedLemma = true; - }else{ + } + else + { Trace("cegqi-warn") << " ...FAILED to add refinement!" << std::endl; } } - if( addedLemma ){ + if (addedLemma) + { Trace("cegqi-engine") << " ...refine candidate." << std::endl; } } } -void CegInstantiation::printSynthSolution( std::ostream& out ) { - if( d_conj->isAssigned() ) +void SynthEngine::printSynthSolution(std::ostream& out) +{ + if (d_conj->isAssigned()) { - d_conj->printSynthSolution( out, d_last_inst_si ); + d_conj->printSynthSolution(out, d_last_inst_si); } else { - Assert( false ); + Assert(false); } } -void CegInstantiation::getSynthSolutions(std::map& sol_map) +void SynthEngine::getSynthSolutions(std::map& sol_map) { if (d_conj->isAssigned()) { @@ -367,22 +387,25 @@ void CegInstantiation::getSynthSolutions(std::map& sol_map) } } -void CegInstantiation::preregisterAssertion( Node n ) { - //check if it sygus conjecture - if( QuantAttributes::checkSygusConjecture( n ) ){ - //this is a sygus conjecture +void SynthEngine::preregisterAssertion(Node n) +{ + // check if it sygus conjecture + if (QuantAttributes::checkSygusConjecture(n)) + { + // this is a sygus conjecture Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl; - d_conj->preregisterConjecture( n ); + d_conj->preregisterConjecture(n); } } -CegInstantiation::Statistics::Statistics() - : d_cegqi_lemmas_ce("CegInstantiation::cegqi_lemmas_ce", 0), - d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0), - d_cegqi_si_lemmas("CegInstantiation::cegqi_lemmas_si", 0), - d_solutions("CegConjecture::solutions", 0), - d_candidate_rewrites_print("CegConjecture::candidate_rewrites_print", 0), - d_candidate_rewrites("CegConjecture::candidate_rewrites", 0) +SynthEngine::Statistics::Statistics() + : d_cegqi_lemmas_ce("SynthEngine::cegqi_lemmas_ce", 0), + d_cegqi_lemmas_refine("SynthEngine::cegqi_lemmas_refine", 0), + d_cegqi_si_lemmas("SynthEngine::cegqi_lemmas_si", 0), + d_solutions("SynthConjecture::solutions", 0), + d_candidate_rewrites_print("SynthConjecture::candidate_rewrites_print", + 0), + d_candidate_rewrites("SynthConjecture::candidate_rewrites", 0) { smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce); @@ -393,7 +416,8 @@ CegInstantiation::Statistics::Statistics() smtStatisticsRegistry()->registerStat(&d_candidate_rewrites); } -CegInstantiation::Statistics::~Statistics(){ +SynthEngine::Statistics::~Statistics() +{ smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_ce); smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine); smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas); @@ -402,6 +426,6 @@ CegInstantiation::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites); } -}/* namespace CVC4::theory::quantifiers */ -}/* namespace CVC4::theory */ -}/* namespace CVC4 */ +} // namespace quantifiers +} // namespace theory +} /* namespace CVC4 */ diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.h b/src/theory/quantifiers/sygus/synth_engine.h similarity index 50% rename from src/theory/quantifiers/sygus/ce_guided_instantiation.h rename to src/theory/quantifiers/sygus/synth_engine.h index 6bf33effb..a7004c5c7 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file ce_guided_instantiation.h +/*! \file synth_engine.h ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds, Mathias Preiner, Tim King @@ -9,28 +9,30 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief counterexample guided instantiation class + ** \brief The quantifiers module for managing all approaches to synthesis, + ** in particular, those described in Reynolds et al CAV 2015. **/ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H -#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H +#ifndef __CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H +#define __CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H #include "context/cdhashmap.h" -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { namespace quantifiers { -class CegInstantiation : public QuantifiersModule +class SynthEngine : public QuantifiersModule { typedef context::CDHashMap NodeBoolMap; -private: + + private: /** the quantified formula stating the synthesis conjecture */ - CegConjecture * d_conj; + SynthConjecture* d_conj; /** last instantiation by single invocation module? */ bool d_last_inst_si; /** the conjecture we are waiting to assign */ @@ -48,38 +50,41 @@ private: */ bool assignConjecture(Node q); /** check conjecture */ - void checkConjecture(CegConjecture* conj); + void checkConjecture(SynthConjecture* conj); + + public: + SynthEngine(QuantifiersEngine* qe, context::Context* c); + ~SynthEngine(); + + public: + bool needsCheck(Theory::Effort e) override; + QEffort needsModel(Theory::Effort e) override; + /* Call during quantifier engine's check */ + void check(Theory::Effort e, QEffort quant_e) override; + /* Called for new quantifiers */ + void registerQuantifier(Node q) override; + /** Identify this module (for debugging, dynamic configuration, etc..) */ + std::string identify() const override { return "SynthEngine"; } + /** print solution for synthesis conjectures */ + void printSynthSolution(std::ostream& out); + /** get synth solutions + * + * This function adds entries to sol_map that map functions-to-synthesize + * with their solutions, for all active conjectures (currently just the one + * assigned to d_conj). This should be called immediately after the solver + * answers unsat for sygus input. + * + * For details on what is added to sol_map, see + * SynthConjecture::getSynthSolutions. + */ + void getSynthSolutions(std::map& sol_map); + /** preregister assertion (before rewrite) */ + void preregisterAssertion(Node n); public: - CegInstantiation( QuantifiersEngine * qe, context::Context* c ); - ~CegInstantiation(); -public: - bool needsCheck(Theory::Effort e) override; - QEffort needsModel(Theory::Effort e) override; - /* Call during quantifier engine's check */ - void check(Theory::Effort e, QEffort quant_e) override; - /* Called for new quantifiers */ - void registerQuantifier(Node q) override; - /** Identify this module (for debugging, dynamic configuration, etc..) */ - std::string identify() const override { return "CegInstantiation"; } - /** print solution for synthesis conjectures */ - void printSynthSolution(std::ostream& out); - /** get synth solutions - * - * This function adds entries to sol_map that map functions-to-synthesize - * with their solutions, for all active conjectures (currently just the one - * assigned to d_conj). This should be called immediately after the solver - * answers unsat for sygus input. - * - * For details on what is added to sol_map, see - * CegConjecture::getSynthSolutions. - */ - void getSynthSolutions(std::map& sol_map); - /** preregister assertion (before rewrite) */ - void preregisterAssertion(Node n); -public: - class Statistics { - public: + class Statistics + { + public: IntStat d_cegqi_lemmas_ce; IntStat d_cegqi_lemmas_refine; IntStat d_cegqi_si_lemmas; @@ -88,12 +93,12 @@ public: IntStat d_candidate_rewrites; Statistics(); ~Statistics(); - };/* class CegInstantiation::Statistics */ + }; /* class SynthEngine::Statistics */ Statistics d_statistics; -}; /* class CegInstantiation */ +}; /* class SynthEngine */ -} /* namespace CVC4::theory::quantifiers */ -} /* namespace CVC4::theory */ +} // namespace quantifiers +} // namespace theory } /* namespace CVC4 */ #endif diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 64adea6c5..1f4e34c1f 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -423,7 +423,7 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { void TermDbSygus::registerEnumerator(Node e, Node f, - CegConjecture* conj, + SynthConjecture* conj, bool mkActiveGuard, bool useSymbolicCons) { @@ -522,9 +522,9 @@ bool TermDbSygus::isEnumerator(Node e) const return d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end(); } -CegConjecture* TermDbSygus::getConjectureForEnumerator(Node e) const +SynthConjecture* TermDbSygus::getConjectureForEnumerator(Node e) const { - std::map::const_iterator itm = + std::map::const_iterator itm = d_enum_to_conjecture.find(e); if (itm != d_enum_to_conjecture.end()) { return itm->second; @@ -563,9 +563,11 @@ bool TermDbSygus::usingSymbolicConsForEnumerator(Node e) const void TermDbSygus::getEnumerators(std::vector& mts) { - for (std::map::iterator itm = + for (std::map::iterator itm = d_enum_to_conjecture.begin(); - itm != d_enum_to_conjecture.end(); ++itm) { + itm != d_enum_to_conjecture.end(); + ++itm) + { mts.push_back( itm->first ); } } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index fee556cf8..b7bdba3ab 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -29,7 +29,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -class CegConjecture; +class SynthConjecture; // TODO :issue #1235 split and document this class class TermDbSygus { @@ -76,13 +76,13 @@ class TermDbSygus { */ void registerEnumerator(Node e, Node f, - CegConjecture* conj, + SynthConjecture* conj, bool mkActiveGuard = false, bool useSymbolicCons = false); /** is e an enumerator registered with this class? */ bool isEnumerator(Node e) const; /** return the conjecture e is associated with */ - CegConjecture* getConjectureForEnumerator(Node e) const; + SynthConjecture* getConjectureForEnumerator(Node e) const; /** return the function-to-synthesize e is associated with */ Node getSynthFunForEnumerator(Node e) const; /** get active guard for e */ @@ -252,7 +252,7 @@ class TermDbSygus { //------------------------------enumerators /** mapping from enumerator terms to the conjecture they are associated with */ - std::map d_enum_to_conjecture; + std::map d_enum_to_conjecture; /** mapping from enumerator terms to the function-to-synthesize they are * associated with */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 7a5652e2f..320f50afb 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -47,8 +47,8 @@ #include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/skolemize.h" -#include "theory/quantifiers/sygus/ce_guided_instantiation.h" #include "theory/quantifiers/sygus/sygus_eval_unfold.h" +#include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_canonize.h" #include "theory/quantifiers/term_database.h" @@ -96,7 +96,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_qcf(nullptr), d_rr_engine(nullptr), d_sg_gen(nullptr), - d_ceg_inst(nullptr), + d_synth_e(nullptr), d_lte_part_inst(nullptr), d_fs(nullptr), d_i_cbqi(nullptr), @@ -192,8 +192,8 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, } } if( options::ceGuidedInst() ){ - d_ceg_inst.reset(new quantifiers::CegInstantiation(this, c)); - d_modules.push_back(d_ceg_inst.get()); + d_synth_e.reset(new quantifiers::SynthEngine(this, c)); + d_modules.push_back(d_synth_e.get()); //needsBuilder = true; } //finite model finding @@ -374,9 +374,9 @@ quantifiers::RewriteEngine* QuantifiersEngine::getRewriteEngine() const { return d_rr_engine.get(); } -quantifiers::CegInstantiation* QuantifiersEngine::getCegInstantiation() const +quantifiers::SynthEngine* QuantifiersEngine::getSynthEngine() const { - return d_ceg_inst.get(); + return d_synth_e.get(); } quantifiers::InstStrategyEnum* QuantifiersEngine::getInstStrategyEnum() const { @@ -1148,8 +1148,9 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) { } void QuantifiersEngine::printSynthSolution( std::ostream& out ) { - if( d_ceg_inst ){ - d_ceg_inst->printSynthSolution( out ); + if (d_synth_e) + { + d_synth_e->printSynthSolution(out); }else{ out << "Internal error : module for synth solution not found." << std::endl; } @@ -1260,7 +1261,7 @@ Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ void QuantifiersEngine::getSynthSolutions(std::map& sol_map) { - d_ceg_inst->getSynthSolutions(sol_map); + d_synth_e->getSynthSolutions(sol_map); } void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 77713744b..512f0c651 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -68,7 +68,7 @@ namespace quantifiers { class RewriteEngine; class QModelBuilder; class ConjectureGenerator; - class CegInstantiation; + class SynthEngine; class LtePartialInst; class AlphaEquivalence; class InstStrategyEnum; @@ -150,7 +150,7 @@ public: /** rewrite rules utility */ quantifiers::RewriteEngine* getRewriteEngine() const; /** ceg instantiation */ - quantifiers::CegInstantiation* getCegInstantiation() const; + quantifiers::SynthEngine* getSynthEngine() const; /** get full saturation */ quantifiers::InstStrategyEnum* getInstStrategyEnum() const; /** get inst strategy cbqi */ @@ -375,7 +375,7 @@ public: /** subgoal generator */ std::unique_ptr d_sg_gen; /** ceg instantiation */ - std::unique_ptr d_ceg_inst; + std::unique_ptr d_synth_e; /** lte partial instantiation */ std::unique_ptr d_lte_part_inst; /** full saturation */ -- 2.30.2