From 12246d53ac1dd4bbd464dee9dea61b8ac05b4b49 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 9 Oct 2018 11:51:06 -0500 Subject: [PATCH] Allow multiple synthesis conjectures. (#2593) --- .../quantifiers/sygus/synth_conjecture.cpp | 17 +-- .../quantifiers/sygus/synth_conjecture.h | 21 ++- src/theory/quantifiers/sygus/synth_engine.cpp | 126 +++++++++--------- src/theory/quantifiers/sygus/synth_engine.h | 41 +++--- 4 files changed, 102 insertions(+), 103 deletions(-) diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 4dfe33b58..469775a46 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -843,7 +843,7 @@ void SynthConjecture::printAndContinueStream() // get the current output stream // this output stream should coincide with wherever --dump-synth is output on Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); - printSynthSolution(*nodeManagerOptions.getOut(), false); + printSynthSolution(*nodeManagerOptions.getOut()); // We will not refine the current candidate solution since it is a solution // thus, we clear information regarding the current refinement @@ -882,14 +882,13 @@ void SynthConjecture::printAndContinueStream() } } -void SynthConjecture::printSynthSolution(std::ostream& out, - bool singleInvocation) +void SynthConjecture::printSynthSolution(std::ostream& out) { Trace("cegqi-debug") << "Printing synth solution..." << std::endl; Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren()); std::vector sols; std::vector statuses; - if (!getSynthSolutionsInternal(sols, statuses, singleInvocation)) + if (!getSynthSolutionsInternal(sols, statuses)) { return; } @@ -963,13 +962,12 @@ void SynthConjecture::printSynthSolution(std::ostream& out, } } -void SynthConjecture::getSynthSolutions(std::map& sol_map, - bool singleInvocation) +void SynthConjecture::getSynthSolutions(std::map& sol_map) { NodeManager* nm = NodeManager::currentNM(); std::vector sols; std::vector statuses; - if (!getSynthSolutionsInternal(sols, statuses, singleInvocation)) + if (!getSynthSolutionsInternal(sols, statuses)) { return; } @@ -1000,8 +998,7 @@ void SynthConjecture::getSynthSolutions(std::map& sol_map, } bool SynthConjecture::getSynthSolutionsInternal(std::vector& sols, - std::vector& statuses, - bool singleInvocation) + std::vector& statuses) { for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) { @@ -1012,7 +1009,7 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector& sols, // get the solution Node sol; int status = -1; - if (singleInvocation) + if (isSingleInvocation()) { Assert(d_ceg_si != NULL); sol = d_ceg_si->getSolution(i, tn, status, true); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 4c18205af..d5ace4dfe 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -92,12 +92,11 @@ class SynthConjecture void doRefine(std::vector& lems); //-------------------------------end for counterexample-guided check/refine /** - * prints the synthesis solution to output stream out. - * - * singleInvocation : set to true if we should consult the single invocation - * module to get synthesis solutions. + * Prints the synthesis solution to output stream out. This invokes solution + * reconstruction if the conjecture is single invocation. Otherwise, it + * returns the enumer */ - void printSynthSolution(std::ostream& out, bool singleInvocation); + void printSynthSolution(std::ostream& out); /** get synth solutions * * This returns a map from function-to-synthesize variables to their @@ -105,11 +104,8 @@ class SynthConjecture * conjecture exists f. forall x. f( x )>x, this function may return the map * containing the entry: * f -> (lambda x. x+1) - * - * singleInvocation : set to true if we should consult the single invocation - * module to get synthesis solutions. */ - void getSynthSolutions(std::map& sol_map, bool singleInvocation); + void getSynthSolutions(std::map& sol_map); /** * The feasible guard whose semantics are "this conjecture is feasiable". * This is "G" in Figure 3 of Reynolds et al CAV 2015. @@ -309,16 +305,15 @@ class SynthConjecture * We store builtin versions under some conditions (such as when the sygus * grammar is being ignored). * - * singleInvocation : set to true if we should consult the single invocation - * module to get synthesis solutions. + * This consults the single invocation module to get synthesis solutions if + * isSingleInvocation() returns true. * * For example, for conjecture exists fg. forall x. f(x)>g(x), this function * may set ( sols, status ) to ( { x+1, d_x() }, { 1, 0 } ), where d_x() is * the sygus datatype constructor corresponding to variable x. */ bool getSynthSolutionsInternal(std::vector& sols, - std::vector& status, - bool singleInvocation); + std::vector& status); //-------------------------------- sygus stream /** current stream guard */ Node d_current_stream_guard; diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 296c10ff6..7ff16d82b 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -34,12 +34,12 @@ namespace quantifiers { SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c) : QuantifiersModule(qe) { - d_conj = new SynthConjecture(qe); - d_last_inst_si = false; + d_conjs.push_back( + std::unique_ptr(new SynthConjecture(d_quantEngine))); + d_conj = d_conjs.back().get(); } -SynthEngine::~SynthEngine() { delete d_conj; } - +SynthEngine::~SynthEngine() {} bool SynthEngine::needsCheck(Theory::Effort e) { return e >= Theory::EFFORT_LAST_CALL; @@ -47,65 +47,66 @@ bool SynthEngine::needsCheck(Theory::Effort e) QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e) { - return d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL; + return QEFFORT_MODEL; } void SynthEngine::check(Theory::Effort e, QEffort quant_e) { // are we at the proper effort level? - unsigned echeck = - d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL; - if (quant_e != echeck) + if (quant_e != QEFFORT_MODEL) { return; } // if we are waiting to assign the conjecture, do it now - if (!d_waiting_conj.isNull()) + bool assigned = !d_waiting_conj.empty(); + while (!d_waiting_conj.empty()) { - Node q = d_waiting_conj; + Node q = d_waiting_conj.back(); + d_waiting_conj.pop_back(); Trace("cegqi-engine") << "--- Conjecture waiting to assign: " << q << std::endl; - d_waiting_conj = Node::null(); - if (!d_conj->isAssigned()) - { - assignConjecture(q); - // assign conjecture always uses the output channel, we return and - // re-check here. - return; - } + assignConjecture(q); + } + if (assigned) + { + // assign conjecture always uses the output channel, either by reducing a + // quantified formula to another, or adding initial lemmas during + // SynthConjecture::assign. Thus, we return here and re-check. + return; } Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl; Trace("cegqi-engine-debug") << std::endl; - bool active = false; - bool value; - if (d_quantEngine->getValuation().hasSatValue(d_conj->getConjecture(), value)) - { - active = value; - } - else + Valuation& valuation = d_quantEngine->getValuation(); + for (unsigned i = 0, size = d_conjs.size(); i < size; i++) { + SynthConjecture* sc = d_conjs[i].get(); + bool active = false; + bool value; + if (valuation.hasSatValue(sc->getConjecture(), value)) + { + active = value; + } + else + { + Trace("cegqi-engine-debug") << "...no value for quantified formula." + << std::endl; + } Trace("cegqi-engine-debug") - << "...no value for quantified formula." << std::endl; - } - Trace("cegqi-engine-debug") - << "Current conjecture status : active : " << active << std::endl; - if (active && d_conj->needsCheck()) - { - checkConjecture(d_conj); + << "Current conjecture status : active : " << active << std::endl; + if (active && sc->needsCheck()) + { + checkConjecture(sc); + } } Trace("cegqi-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl; } -bool SynthEngine::assignConjecture(Node q) +void SynthEngine::assignConjecture(Node q) { - if (d_conj->isAssigned()) - { - return false; - } Trace("cegqi-engine") << "--- Assign conjecture " << q << std::endl; if (options::sygusQePreproc()) { @@ -224,33 +225,31 @@ bool SynthEngine::assignConjecture(Node q) << std::endl; d_quantEngine->getOutputChannel().lemma(lem); // we've reduced the original to a preprocessed version, return - return false; + return; } } - d_conj->assign(q); - return true; + // 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.back()->assign(q); } void SynthEngine::registerQuantifier(Node q) { if (d_quantEngine->getOwner(q) == this) - { // && d_eval_axioms.find( q )==d_eval_axioms.end() ){ - if (!d_conj->isAssigned()) + { + Trace("cegqi") << "Register conjecture : " << q << std::endl; + if (options::sygusQePreproc()) { - Trace("cegqi") << "Register conjecture : " << q << std::endl; - if (options::sygusQePreproc()) - { - d_waiting_conj = q; - } - else - { - // assign it now - assignConjecture(q); - } + d_waiting_conj.push_back(q); } else { - Assert(d_conj->getEmbeddedConjecture() == q); + // assign it now + assignConjecture(q); } } else @@ -278,7 +277,6 @@ void SynthEngine::checkConjecture(SynthConjecture* conj) conj->doSingleInvCheck(clems); if (!clems.empty()) { - d_last_inst_si = true; for (const Node& lem : clems) { Trace("cegqi-lemma") @@ -307,7 +305,6 @@ void SynthEngine::checkConjecture(SynthConjecture* conj) bool addedLemma = false; for (const Node& lem : cclems) { - d_last_inst_si = false; Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem << std::endl; if (d_quantEngine->addLemma(lem)) @@ -368,21 +365,24 @@ void SynthEngine::checkConjecture(SynthConjecture* conj) void SynthEngine::printSynthSolution(std::ostream& out) { - if (d_conj->isAssigned()) - { - d_conj->printSynthSolution(out, d_last_inst_si); - } - else + Assert(!d_conjs.empty()); + for (unsigned i = 0, size = d_conjs.size(); i < size; i++) { - Assert(false); + if (d_conjs[i]->isAssigned()) + { + d_conjs[i]->printSynthSolution(out); + } } } void SynthEngine::getSynthSolutions(std::map& sol_map) { - if (d_conj->isAssigned()) + for (unsigned i = 0, size = d_conjs.size(); i < size; i++) { - d_conj->getSynthSolutions(sol_map, d_last_inst_si); + if (d_conjs[i]->isAssigned()) + { + d_conjs[i]->getSynthSolutions(sol_map); + } } } diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index a7004c5c7..2a8994c25 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -31,24 +31,25 @@ class SynthEngine : public QuantifiersModule typedef context::CDHashMap NodeBoolMap; private: - /** the quantified formula stating the synthesis conjecture */ + /** the conjecture formula(s) we are waiting to assign */ + std::vector d_waiting_conj; + /** The synthesis conjectures that this class is managing. */ + std::vector > d_conjs; + /** + * The first conjecture in the above vector. We track this conjecture + * so that a synthesis conjecture can be preregistered during a call to + * preregisterAssertion. + */ SynthConjecture* d_conj; - /** last instantiation by single invocation module? */ - bool d_last_inst_si; - /** the conjecture we are waiting to assign */ - Node d_waiting_conj; - - private: - /** assign quantified formula q as the conjecture + /** assign quantified formula q as a conjecture * - * This method returns true if q was successfully assigned as the synthesis - * conjecture considered by this class. This method may return false, for - * instance, if this class determines that it would rather rewrite q to - * an equivalent form r (in which case this method returns the lemma - * q <=> r). An example of this is the quantifier elimination step - * option::sygusQePreproc(). + * This method either assigns q to a synthesis conjecture object in d_conjs, + * or otherwise reduces q to an equivalent form. This method does the latter + * if this class determines that it would rather rewrite q to an equivalent + * form r (in which case this method returns the lemma q <=> r). An example of + * this is the quantifier elimination step option::sygusQePreproc(). */ - bool assignConjecture(Node q); + void assignConjecture(Node q); /** check conjecture */ void checkConjecture(SynthConjecture* conj); @@ -56,7 +57,6 @@ class SynthEngine : public QuantifiersModule 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 */ @@ -78,7 +78,14 @@ class SynthEngine : public QuantifiersModule * SynthConjecture::getSynthSolutions. */ void getSynthSolutions(std::map& sol_map); - /** preregister assertion (before rewrite) */ + /** preregister assertion (before rewrite) + * + * 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. + */ void preregisterAssertion(Node n); public: -- 2.30.2