From: Andrew Reynolds Date: Fri, 25 Sep 2020 18:45:38 +0000 (-0500) Subject: Make sygus refinement step more robust to unevaluatable counterexamples (#5102) X-Git-Tag: cvc5-1.0.0~2807 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c59345b93b2ecf3552f5205b312c262a1ae5eab8;p=cvc5.git Make sygus refinement step more robust to unevaluatable counterexamples (#5102) Currently, the CEGIS refinement loop of the sygus solver may terminate with "unknown" when a duplicate counterexample is generated. This is caused by a candidate t for a conjecture exists f. forall x. G[f, x] such that: (1) G[t, c] evaluates to a non-constant expression, (2) ~G[t, k] is satisfiable with model k = c. Notice this exclusively limited to theories with incomplete functions, e.g. (non-linear) division. In this case, we know that t is an incorrect solution, but the counterexample we found was not new. Currently, we abort with "unknown" since the counterexample was not new. After this PR, we exclude t and continue, which is uncontroversially the correct behavior. This PR moves the resposibility for lemma from synth engine to synth conjecture, which simplifies the behavior of the main check conjecture method. --- 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& cvals) const return true; } -void SynthConjecture::doRefine(std::vector& lems) +bool SynthConjecture::doRefine() { - Assert(lems.empty()); + std::vector lems; Assert(d_set_ce_sk_vars); // first, make skolem substitution @@ -768,6 +768,42 @@ void SynthConjecture::doRefine(std::vector& 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& 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& 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 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)