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.
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
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)
/** 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 */
*/
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
bool SynthEngine::checkConjecture(SynthConjecture* conj)
{
- Node q = conj->getEmbeddedConjecture();
- Node aq = conj->getConjecture();
if (Trace.isOn("sygus-engine-debug"))
{
conj->debugPrint("sygus-engine-debug");
<< " ...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)
projects / cvc5.git / commitdiff