From: Andrew Reynolds Date: Thu, 12 Sep 2019 20:37:00 +0000 (-0500) Subject: Encapsulate synth engine (#3271) X-Git-Tag: cvc5-1.0.0~3963 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ad18e6d4bab518a29648823eca9ba5ee1ebc8400;p=cvc5.git Encapsulate synth engine (#3271) --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3d469f2b5..1cec8e123 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3213,15 +3213,6 @@ void SmtEnginePrivate::processAssertions() { d_passes["nl-ext-purify"]->apply(&d_assertions); } - 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() - ->getSynthEngine() - ->preregisterAssertion(d_assertions[i]); - } - } - if (options::solveRealAsInt()) { d_passes["real-to-int"]->apply(&d_assertions); } diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index fcfef1541..e2a8540d4 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -43,8 +43,9 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SynthConjecture::SynthConjecture(QuantifiersEngine* qe) +SynthConjecture::SynthConjecture(QuantifiersEngine* qe, SynthEngine* p) : d_qe(qe), + d_parent(p), d_tds(qe->getTermDatabaseSygus()), d_hasSolution(false, qe->getUserContext()), d_ceg_si(new CegSingleInv(qe, this)), @@ -1045,8 +1046,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out) ss << prog; std::string f(ss.str()); f.erase(f.begin()); - SynthEngine* cei = d_qe->getSynthEngine(); - ++(cei->d_statistics.d_solutions); + ++(d_parent->d_statistics.d_solutions); bool is_unique_term = true; @@ -1086,11 +1086,11 @@ void SynthConjecture::printSynthSolution(std::ostream& out) is_unique_term = d_exprm[prog].addTerm(sol, out, rew_print); if (rew_print) { - ++(cei->d_statistics.d_candidate_rewrites_print); + ++(d_parent->d_statistics.d_candidate_rewrites_print); } if (!is_unique_term) { - ++(cei->d_statistics.d_filtered_solutions); + ++(d_parent->d_statistics.d_filtered_solutions); } } if (is_unique_term) diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 33fff6844..8ae30f636 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -34,6 +34,8 @@ namespace CVC4 { namespace theory { namespace quantifiers { +class SynthEngine; + /** * A base class for generating values for actively-generated enumerators. * At a high level, the job of this class is to accept a stream of "abstract @@ -68,7 +70,7 @@ class EnumValGenerator class SynthConjecture { public: - SynthConjecture(QuantifiersEngine* qe); + SynthConjecture(QuantifiersEngine* qe, SynthEngine* p); ~SynthConjecture(); /** presolve */ void presolve(); @@ -165,6 +167,8 @@ class SynthConjecture private: /** reference to quantifier engine */ QuantifiersEngine* d_qe; + /** pointer to the synth engine that owns this */ + SynthEngine* d_parent; /** term database sygus of d_qe */ TermDbSygus* d_tds; /** The feasible guard. */ diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index f78886249..d13bd2dcf 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -35,8 +35,8 @@ namespace quantifiers { SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c) : QuantifiersModule(qe) { - d_conjs.push_back( - std::unique_ptr(new SynthConjecture(d_quantEngine))); + d_conjs.push_back(std::unique_ptr( + new SynthConjecture(d_quantEngine, this))); d_conj = d_conjs.back().get(); } @@ -255,8 +255,8 @@ void SynthEngine::assignConjecture(Node q) // allocate a new synthesis conjecture if not assigned if (d_conjs.back()->isAssigned()) { - d_conjs.push_back( - std::unique_ptr(new SynthConjecture(d_quantEngine))); + d_conjs.push_back(std::unique_ptr( + new SynthConjecture(d_quantEngine, this))); } d_conjs.back()->assign(q); } diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index c4c09e7e6..e099657ad 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -86,9 +86,9 @@ class SynthEngine : public QuantifiersModule * * The purpose of this method is to inform the solution reconstruction * techniques within the single invocation module that n is an original - * assertion, prior to rewriting. This is used as a heuristic to remember - * terms that are likely to help when trying to reconstruct a solution - * that fits a given input syntax. + * assertion. This is used as a heuristic to remember terms that are likely + * to help when trying to reconstruct a solution that fits a given input + * syntax. */ void preregisterAssertion(Node n); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a03596060..a6ec1c077 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -385,11 +385,6 @@ inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const return d_tr_trie.get(); } -quantifiers::SynthEngine* QuantifiersEngine::getSynthEngine() const -{ - return d_private->d_synth_e.get(); -} - QuantifiersModule * QuantifiersEngine::getOwner( Node q ) { std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q ); if( it==d_owner.end() ){ @@ -527,24 +522,32 @@ void QuantifiersEngine::ppNotifyAssertions( Trace("quant-engine-proc") << "ppNotifyAssertions in QE, #assertions = " << assertions.size() << " check epr = " << (d_qepr != NULL) << std::endl; - if ((options::instLevelInputOnly() && options::instMaxLevel() != -1) || - d_qepr != NULL) { - for (unsigned i = 0; i < assertions.size(); i++) { - if (options::instLevelInputOnly() && options::instMaxLevel() != -1) { - quantifiers::QuantAttributes::setInstantiationLevelAttr(assertions[i], - 0); - } - if (d_qepr != NULL) { - d_qepr->registerAssertion(assertions[i]); - } + if (options::instLevelInputOnly() && options::instMaxLevel() != -1) + { + for (const Node& a : assertions) + { + quantifiers::QuantAttributes::setInstantiationLevelAttr(a, 0); } - if (d_qepr != NULL) { - // must handle sources of other new constants e.g. separation logic - // FIXME: cleanup - sep::TheorySep* theory_sep = - static_cast(getTheoryEngine()->theoryOf(THEORY_SEP)); - theory_sep->initializeBounds(); - d_qepr->finishInit(); + } + if (d_qepr != NULL) + { + for (const Node& a : assertions) + { + d_qepr->registerAssertion(a); + } + // must handle sources of other new constants e.g. separation logic + // FIXME (as part of project 3) : cleanup + sep::TheorySep* theory_sep = + static_cast(getTheoryEngine()->theoryOf(THEORY_SEP)); + theory_sep->initializeBounds(); + d_qepr->finishInit(); + } + if (options::ceGuidedInst()) + { + quantifiers::SynthEngine* sye = d_private->d_synth_e.get(); + for (const Node& a : assertions) + { + sye->preregisterAssertion(a); } } } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 36b58fd60..0a534d090 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -35,7 +35,6 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/skolemize.h" -#include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" @@ -112,10 +111,6 @@ public: /** get relevant domain */ quantifiers::RelevantDomain* getRelevantDomain() const; //---------------------- end utilities - //---------------------- modules (TODO remove these #1163) - /** ceg instantiation */ - quantifiers::SynthEngine* getSynthEngine() const; - //---------------------- end modules private: /** * Maps quantified formulas to the module that owns them, if any module has