diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 40 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.h | 24 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 44 |
3 files changed, 61 insertions, 47 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 8a79be867..0531d859d 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -700,9 +700,9 @@ bool SynthConjecture::checkSideCondition(const std::vector<Node>& cvals) const return true; } -void SynthConjecture::doRefine(std::vector<Node>& lems) +bool SynthConjecture::doRefine() { - Assert(lems.empty()); + std::vector<Node> lems; Assert(d_set_ce_sk_vars); // first, make skolem substitution @@ -768,6 +768,42 @@ void SynthConjecture::doRefine(std::vector<Node>& lems) d_set_ce_sk_vars = false; d_ce_sk_vars.clear(); d_ce_sk_var_mvs.clear(); + + // now send the lemmas + bool addedLemma = false; + for (const Node& lem : lems) + { + Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem + << std::endl; + bool res = d_qe->addLemma(lem); + if (res) + { + ++(d_stats.d_cegqi_lemmas_refine); + d_refine_count++; + addedLemma = true; + } + else + { + Trace("cegqi-warn") << " ...FAILED to add refinement!" << std::endl; + } + } + if (addedLemma) + { + Trace("sygus-engine-debug") << " ...refine candidate." << std::endl; + } + else + { + Trace("sygus-engine-debug") << " ...(warning) failed to refine candidate, " + "manually exclude candidate." + << std::endl; + // something went wrong, exclude the current candidate + excludeCurrentSolution(sk_vars, sk_subs); + // Note this happens when evaluation is incapable of disproving a candidate + // for counterexample point c, but satisfiability checking happened to find + // the the same point c is indeed a true counterexample. It is sound + // to exclude the candidate in this case. + } + return addedLemma; } void SynthConjecture::preregisterConjecture(Node q) diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index cd9a275ad..5572032b6 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -87,13 +87,10 @@ class SynthConjecture /** presolve */ void presolve(); /** get original version of conjecture */ - Node getConjecture() { return d_quant; } + Node getConjecture() const { return d_quant; } /** get deep embedding version of conjecture */ - Node getEmbeddedConjecture() { return d_embed_quant; } + Node getEmbeddedConjecture() const { return d_embed_quant; } //-------------------------------for counterexample-guided check/refine - /** increment the number of times we have successfully done candidate - * refinement */ - void incrementRefineCount() { d_refine_count++; } /** whether the conjecture is waiting for a call to doCheck below */ bool needsCheck(); /** whether the conjecture is waiting for a call to doRefine below */ @@ -113,9 +110,24 @@ class SynthConjecture */ bool doCheck(std::vector<Node>& lems); /** do refinement + * * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015. + * + * This method is run when needsRefinement() returns true, indicating that + * the last call to doCheck found a counterexample to the last candidate. + * + * This method adds a refinement lemma on the output channel of quantifiers + * engine. If the refinement lemma is a duplicate, then we manually + * exclude the current candidate via excludeCurrentSolution. This should + * only occur when the synthesis conjecture for the current candidate fails + * to evaluate to false for a given counterexample point, but regardless its + * negation is satisfiable for the current candidate and that point. This is + * exclusive to theories with partial functions, e.g. (non-linear) division. + * + * This method returns true if a lemma was added on the output channel, and + * false otherwise. */ - void doRefine(std::vector<Node>& lems); + bool doRefine(); //-------------------------------end for counterexample-guided check/refine /** * Prints the synthesis solution to output stream out. This invokes solution diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index a64dd9c25..95f1acb25 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -304,8 +304,6 @@ void SynthEngine::registerQuantifier(Node q) bool SynthEngine::checkConjecture(SynthConjecture* conj) { - Node q = conj->getEmbeddedConjecture(); - Node aq = conj->getConjecture(); if (Trace.isOn("sygus-engine-debug")) { conj->debugPrint("sygus-engine-debug"); @@ -340,46 +338,14 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj) << " ...check for counterexample." << std::endl; return true; } - else - { - if (conj->needsRefinement()) - { - // immediately go to refine candidate - return checkConjecture(conj); - } - } - return ret; - } - else - { - Trace("sygus-engine-debug") - << " *** Refine candidate phase..." << std::endl; - std::vector<Node> rlems; - conj->doRefine(rlems); - bool addedLemma = false; - for (unsigned i = 0; i < rlems.size(); i++) - { - Node lem = rlems[i]; - 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 - { - Trace("cegqi-warn") << " ...FAILED to add refinement!" << std::endl; - } - } - if (addedLemma) + if (!conj->needsRefinement()) { - Trace("sygus-engine-debug") << " ...refine candidate." << std::endl; + return ret; } + // otherwise, immediately go to refine candidate } - return true; + Trace("sygus-engine-debug") << " *** Refine candidate phase..." << std::endl; + return conj->doRefine(); } void SynthEngine::printSynthSolution(std::ostream& out) |