This tightens the interface of the sygus solver, which was a product of not using subsolver calls in the original design.
d_ceg_cegisUnif(new CegisUnif(env, qs, qim, d_tds, this)),
d_sygus_ccore(new CegisCoreConnective(env, qs, qim, d_tds, this)),
d_master(nullptr),
- d_setInnerSksModel(false),
d_repair_index(0),
d_guarded_stream_exc(false)
{
return true;
}
-bool SynthConjecture::needsRefinement() const { return d_setInnerSksModel; }
bool SynthConjecture::doCheck()
{
if (isSingleInvocation())
recordSolution(candidate_values);
return true;
}
- Assert(!d_setInnerSksModel);
// print the candidate solution for debugging
if (constructed_cand && printDebug)
out << ")" << std::endl;
}
- d_setInnerSksModel = true;
-
if (query.isNull())
{
// no lemma to check
// here since the result of the satisfiability test may be unknown.
recordSolution(candidate_values);
- Result r = d_verify.verify(query, d_innerSks, d_innerSksModel);
+ std::vector<Node> skModel;
+ Result r = d_verify.verify(query, d_innerSks, skModel);
if (r.asSatisfiabilityResult().isSat() == Result::SAT)
{
// we have a counterexample
- return false;
+ return processCounterexample(skModel);
}
else if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
{
return true;
}
-bool SynthConjecture::doRefine()
+bool SynthConjecture::processCounterexample(const std::vector<Node>& skModel)
{
- Assert(d_setInnerSksModel);
Trace("cegqi-refine") << "doRefine : Construct refinement lemma..."
<< std::endl;
Trace("cegqi-refine-debug")
<< " For counterexample skolems : " << d_innerSks << std::endl;
Node base_lem = d_checkBody.negate();
- Assert(d_innerSks.size() == d_innerSksModel.size());
+ Assert(d_innerSks.size() == skModel.size());
Trace("cegqi-refine") << "doRefine : substitute..." << std::endl;
- base_lem = base_lem.substitute(d_innerSks.begin(),
- d_innerSks.end(),
- d_innerSksModel.begin(),
- d_innerSksModel.end());
+ base_lem = base_lem.substitute(
+ d_innerSks.begin(), d_innerSks.end(), skModel.begin(), skModel.end());
Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl;
base_lem = d_tds->rewriteNode(base_lem);
Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem
size_t prevPending = d_qim.numPendingLemmas();
d_master->registerRefinementLemma(d_innerSks, base_lem);
Trace("cegqi-refine") << "doRefine : finished" << std::endl;
- d_setInnerSksModel = false;
- d_innerSksModel.clear();
// check if we added a lemma
bool addedLemma = d_qim.numPendingLemmas() > prevPending;
{
Trace("cegqi-debug") << "Exclude current solution: " << enums << " / "
<< values << std::endl;
- // We will not refine the current candidate solution since it is a solution
- // thus, we clear information regarding the current refinement
- d_setInnerSksModel = false;
- d_innerSksModel.clear();
// However, we need to exclude the current solution using an explicit
// blocking clause, so that we proceed to the next solution. We do this only
// for passively-generated enumerators (TermDbSygus::isPassiveEnumerator).
//-------------------------------for counterexample-guided check/refine
/** 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 needsRefinement() const;
/** do syntax-guided enumerative check
*
* This is step 2(a) of Figure 3 of Reynolds et al CAV 2015.
* when each of t1, ..., tn fails to satisfy the current refinement lemmas.
*/
bool doCheck();
- /** 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.
- */
- bool doRefine();
//-------------------------------end for counterexample-guided check/refine
/**
* Prints the current synthesis solution to output stream out. This is
SygusStatistics& getSygusStatistics() { return d_stats; };
private:
+ /** do refinement
+ *
+ * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015.
+ *
+ * This method is run when skModel is corresponds to a counterexample to the
+ * last candidate in the doCheck method.
+ *
+ * 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.
+ */
+ bool processCounterexample(const std::vector<Node>& skModel);
/** Reference to the quantifiers state */
QuantifiersState& d_qstate;
/** Reference to the quantifiers inference manager */
std::vector<Node> d_innerVars;
/** list of skolems on inner quantification */
std::vector<Node> d_innerSks;
- /**
- * If we have already tested the satisfiability of the current verification
- * lemma, this stores the model values of d_innerSks in the current
- * (satisfiable, failed) verification lemma.
- */
- std::vector<Node> d_innerSksModel;
- /**
- * Whether the above vector has been set. We have this flag since the above
- * vector may be set to empty (e.g. for ground synthesis conjectures).
- */
- bool d_setInnerSksModel;
-
/** the asserted (negated) conjecture */
Node d_quant;
/**
SynthConjecture* sc = activeCheckConj[i];
if (!checkConjecture(sc))
{
- if (!sc->needsRefinement())
- {
- acnext.push_back(sc);
- }
+ acnext.push_back(sc);
}
}
activeCheckConj.clear();
conj->debugPrint("sygus-engine-debug");
Trace("sygus-engine-debug") << std::endl;
}
-
- if (!conj->needsRefinement())
+ Trace("sygus-engine-debug") << "Do conjecture check..." << std::endl;
+ Trace("sygus-engine-debug") << " *** Check candidate phase..." << std::endl;
+ size_t prevPending = d_qim.numPendingLemmas();
+ bool ret = conj->doCheck();
+ // if we added a lemma, return true
+ if (d_qim.numPendingLemmas() > prevPending)
{
- Trace("sygus-engine-debug") << "Do conjecture check..." << std::endl;
Trace("sygus-engine-debug")
- << " *** Check candidate phase..." << std::endl;
- size_t prevPending = d_qim.numPendingLemmas();
- bool ret = conj->doCheck();
- // if we added a lemma, return true
- if (d_qim.numPendingLemmas() > prevPending)
- {
- Trace("sygus-engine-debug")
- << " ...check for counterexample." << std::endl;
- return true;
- }
- if (!conj->needsRefinement())
- {
- return ret;
- }
- // otherwise, immediately go to refine candidate
+ << " ...check for counterexample." << std::endl;
+ return true;
}
- Trace("sygus-engine-debug") << " *** Refine candidate phase..." << std::endl;
- return conj->doRefine();
+ return ret;
}
bool SynthEngine::getSynthSolutions(
projects / cvc5.git / commitdiff