Now, all inferences throughout cvc5 in our regression are properly marked with an InferenceId.
This PR includes minor simplifications to the interface for sygus modules. In particular it changes the behavior to send inferences via the inference manager instead of passing them around as a vector.
return "QUANTIFIERS_SYGUS_EXCLUDE_CURRENT";
case InferenceId::QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT:
return "QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT";
+ case InferenceId::QUANTIFIERS_SYGUS_SI_SOLVED:
+ return "QUANTIFIERS_SYGUS_SI_SOLVED";
+ case InferenceId::QUANTIFIERS_SYGUS_SAMPLE_TRUST_SOLVED:
+ return "QUANTIFIERS_SYGUS_SAMPLE_TRUST_SOLVED";
+ case InferenceId::QUANTIFIERS_SYGUS_VERIFY_SOLVED:
+ return "QUANTIFIERS_SYGUS_VERIFY_SOLVED";
case InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA:
return "QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA";
case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_INTER_ENUM_SB:
return "QUANTIFIERS_SYGUS_UNIF_PI_ENUM_SB";
case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_DOMAIN:
return "QUANTIFIERS_SYGUS_UNIF_PI_DOMAIN";
+ case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_COND_EXCLUDE:
+ return "QUANTIFIERS_SYGUS_UNIF_PI_COND_EXCLUDE";
+ case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_REFINEMENT:
+ return "QUANTIFIERS_SYGUS_UNIF_PI_REFINEMENT";
+ case InferenceId::QUANTIFIERS_SYGUS_CEGIS_UCL_SYM_BREAK:
+ return "QUANTIFIERS_SYGUS_CEGIS_UCL_SYM_BREAK";
+ case InferenceId::QUANTIFIERS_SYGUS_CEGIS_UCL_EXCLUDE:
+ return "QUANTIFIERS_SYGUS_CEGIS_UCL_EXCLUDE";
+ case InferenceId::QUANTIFIERS_SYGUS_REPAIR_CONST_EXCLUDE:
+ return "QUANTIFIERS_SYGUS_REPAIR_CONST_EXCLUDE";
+ case InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE:
+ return "QUANTIFIERS_SYGUS_CEGIS_REFINE";
+ case InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE_SAMPLE:
+ return "QUANTIFIERS_SYGUS_CEGIS_REFINE_SAMPLE";
+ case InferenceId::QUANTIFIERS_SYGUS_REFINE_EVAL:
+ return "QUANTIFIERS_SYGUS_REFINE_EVAL";
+ case InferenceId::QUANTIFIERS_SYGUS_EVAL_UNFOLD:
+ return "QUANTIFIERS_SYGUS_EVAL_UNFOLD";
+ case InferenceId::QUANTIFIERS_SYGUS_PBE_EXCLUDE:
+ return "QUANTIFIERS_SYGUS_PBE_EXCLUDE";
+ case InferenceId::QUANTIFIERS_SYGUS_PBE_CONSTRUCT_SOL:
+ return "QUANTIFIERS_SYGUS_PBE_CONSTRUCT_SOL";
case InferenceId::QUANTIFIERS_DSPLIT: return "QUANTIFIERS_DSPLIT";
case InferenceId::QUANTIFIERS_CONJ_GEN_SPLIT:
return "QUANTIFIERS_CONJ_GEN_SPLIT";
QUANTIFIERS_SYGUS_EXCLUDE_CURRENT,
// manual exclusion of a current solution for sygus-stream
QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT,
+ // Q where Q was solved by a subcall to the single invocation module
+ QUANTIFIERS_SYGUS_SI_SOLVED,
+ // Q where Q was (trusted) solved by sampling
+ QUANTIFIERS_SYGUS_SAMPLE_TRUST_SOLVED,
+ // Q where Q was solved by a verification subcall
+ QUANTIFIERS_SYGUS_VERIFY_SOLVED,
// ~Q where Q is a PBE conjecture with conflicting examples
QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA,
// unif+pi symmetry breaking between multiple enumerators
QUANTIFIERS_SYGUS_UNIF_PI_ENUM_SB,
// constraining terms to be in the domain of output
QUANTIFIERS_SYGUS_UNIF_PI_DOMAIN,
+ // condition exclusion from sygus unif
+ QUANTIFIERS_SYGUS_UNIF_PI_COND_EXCLUDE,
+ // refinement lemma from sygus unif
+ QUANTIFIERS_SYGUS_UNIF_PI_REFINEMENT,
+ // symmetry breaking lemma from unsat core learning algorithm initialization
+ QUANTIFIERS_SYGUS_CEGIS_UCL_SYM_BREAK,
+ // candidate exclusion lemma from unsat core learning algorithm
+ QUANTIFIERS_SYGUS_CEGIS_UCL_EXCLUDE,
+ // candidate exclusion lemma from repair constants algorithm
+ QUANTIFIERS_SYGUS_REPAIR_CONST_EXCLUDE,
+ // a counterexample-guided inductive synthesis refinement lemma
+ QUANTIFIERS_SYGUS_CEGIS_REFINE,
+ // a cegis refinement lemma found by sampling
+ QUANTIFIERS_SYGUS_CEGIS_REFINE_SAMPLE,
+ // a lemma based on refinement lemma evaluation
+ QUANTIFIERS_SYGUS_REFINE_EVAL,
+ // an evaluation unfolding lemma
+ QUANTIFIERS_SYGUS_EVAL_UNFOLD,
+ // candidate exclusion lemma from programming-by-examples
+ QUANTIFIERS_SYGUS_PBE_EXCLUDE,
+ // a lemma generated while constructing a candidate solution for PBE
+ QUANTIFIERS_SYGUS_PBE_CONSTRUCT_SOL,
//-------------------- dynamic splitting
// a dynamic split from quantifiers
QUANTIFIERS_DSPLIT,
{
}
-bool Cegis::initialize(Node conj,
- Node n,
- const std::vector<Node>& candidates,
- std::vector<Node>& lemmas)
+bool Cegis::initialize(Node conj, Node n, const std::vector<Node>& candidates)
{
d_base_body = n;
if (d_base_body.getKind() == NOT && d_base_body[0].getKind() == FORALL)
TypeNode bt = d_base_body.getType();
d_cegis_sampler.initialize(bt, d_base_vars, options::sygusSamples());
}
- return processInitialize(conj, n, candidates, lemmas);
+ return processInitialize(conj, n, candidates);
}
bool Cegis::processInitialize(Node conj,
Node n,
- const std::vector<Node>& candidates,
- std::vector<Node>& lemmas)
+ const std::vector<Node>& candidates)
{
Trace("cegis") << "Initialize cegis..." << std::endl;
unsigned csize = candidates.size();
}
bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
- const std::vector<Node>& candidate_values,
- std::vector<Node>& lems)
+ const std::vector<Node>& candidate_values)
{
// First, decide if this call will apply "conjecture-specific refinement".
// In other words, in some settings, the following method will identify and
getRefinementEvalLemmas(candidates, candidate_values, cre_lems);
if (!cre_lems.empty())
{
- lems.insert(lems.end(), cre_lems.begin(), cre_lems.end());
- addedEvalLemmas = true;
- if (Trace.isOn("cegqi-lemma"))
+ for (const Node& cl : cre_lems)
{
- for (const Node& lem : cre_lems)
- {
- Trace("cegqi-lemma")
- << "Cegqi::Lemma : ref evaluation : " << lem << std::endl;
- }
+ d_qim.addPendingLemma(cl, InferenceId::QUANTIFIERS_SYGUS_REFINE_EVAL);
}
+ addedEvalLemmas = true;
/* we could, but do not return here. experimentally, it is better to
add the lemmas below as well, in parallel. */
}
{
Node lem = nm->mkNode(
OR, eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i]));
- lems.push_back(lem);
+ d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_SYGUS_EVAL_UNFOLD);
addedEvalLemmas = true;
Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation unfold : " << lem
<< std::endl;
bool Cegis::constructCandidates(const std::vector<Node>& enums,
const std::vector<Node>& enum_values,
const std::vector<Node>& candidates,
- std::vector<Node>& candidate_values,
- std::vector<Node>& lems)
+ std::vector<Node>& candidate_values)
{
if (Trace.isOn("cegis"))
{
Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
// must guard it
expn = nm->mkNode(OR, d_parent->getGuard().negate(), expn.negate());
- lems.push_back(expn);
+ d_qim.addPendingLemma(
+ expn, InferenceId::QUANTIFIERS_SYGUS_REPAIR_CONST_EXCLUDE);
return ret;
}
}
// evaluate on refinement lemmas
- bool addedEvalLemmas = addEvalLemmas(enums, enum_values, lems);
+ bool addedEvalLemmas = addEvalLemmas(enums, enum_values);
// try to construct candidates
- if (!processConstructCandidates(enums,
- enum_values,
- candidates,
- candidate_values,
- !addedEvalLemmas,
- lems))
+ if (!processConstructCandidates(
+ enums, enum_values, candidates, candidate_values, !addedEvalLemmas))
{
return false;
}
- if (options::cegisSample() != options::CegisSampleMode::NONE && lems.empty())
+ if (options::cegisSample() != options::CegisSampleMode::NONE
+ && !addedEvalLemmas)
{
// if we didn't add a lemma, trying sampling to add a refinement lemma
// that immediately refutes the candidate we just constructed
- if (sampleAddRefinementLemma(candidates, candidate_values, lems))
+ if (sampleAddRefinementLemma(candidates, candidate_values))
{
candidate_values.clear();
// restart (should be guaranteed to add evaluation lemmas on this call)
return constructCandidates(
- enums, enum_values, candidates, candidate_values, lems);
+ enums, enum_values, candidates, candidate_values);
}
}
return true;
const std::vector<Node>& enum_values,
const std::vector<Node>& candidates,
std::vector<Node>& candidate_values,
- bool satisfiedRl,
- std::vector<Node>& lems)
+ bool satisfiedRl)
{
if (satisfiedRl)
{
}
}
-void Cegis::registerRefinementLemma(const std::vector<Node>& vars,
- Node lem,
- std::vector<Node>& lems)
+void Cegis::registerRefinementLemma(const std::vector<Node>& vars, Node lem)
{
addRefinementLemma(lem);
// Make the refinement lemma and add it to lems.
// for the given concrete point.
Node rlem =
NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem);
- lems.push_back(rlem);
+ d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE);
}
bool Cegis::usingRepairConst() { return true; }
}
bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
- const std::vector<Node>& vals,
- std::vector<Node>& lems)
+ const std::vector<Node>& vals)
{
Trace("sygus-engine") << " *** Do sample add refinement..." << std::endl;
if (Trace.isOn("cegis-sample"))
if (options::cegisSample() != options::CegisSampleMode::TRUST)
{
Node lem = nm->mkNode(OR, d_parent->getGuard().negate(), rlem);
- lems.push_back(lem);
+ d_qim.addPendingLemma(
+ lem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE_SAMPLE);
}
return true;
}
/** initialize */
virtual bool initialize(Node conj,
Node n,
- const std::vector<Node>& candidates,
- std::vector<Node>& lemmas) override;
+ const std::vector<Node>& candidates) override;
/** get term list */
virtual void getTermList(const std::vector<Node>& candidates,
std::vector<Node>& enums) override;
/** construct candidate */
- virtual bool constructCandidates(const std::vector<Node>& enums,
- const std::vector<Node>& enum_values,
- const std::vector<Node>& candidates,
- std::vector<Node>& candidate_values,
- std::vector<Node>& lems) override;
+ virtual bool constructCandidates(
+ const std::vector<Node>& enums,
+ const std::vector<Node>& enum_values,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& candidate_values) override;
/** register refinement lemma
*
* This function stores lem as a refinement lemma, and adds it to lems.
*/
virtual void registerRefinementLemma(const std::vector<Node>& vars,
- Node lem,
- std::vector<Node>& lems) override;
+ Node lem) override;
/** using repair const */
virtual bool usingRepairConst() override;
*/
virtual bool processInitialize(Node conj,
Node n,
- const std::vector<Node>& candidates,
- std::vector<Node>& lemmas);
+ const std::vector<Node>& candidates);
/** do cegis-implementation-specific post-processing for construct candidate
*
* satisfiedRl is whether all refinement lemmas are satisfied under the
const std::vector<Node>& enum_values,
const std::vector<Node>& candidates,
std::vector<Node>& candidate_values,
- bool satisfiedRl,
- std::vector<Node>& lems);
+ bool satisfiedRl);
//----------------------------------end cegis-implementation-specific
//-----------------------------------refinement lemmas
* This function will check if there is a sample point in d_sampler that
* refutes the candidate solution (d_quant_vars->vals). If so, it adds a
* refinement lemma to the lists d_refinement_lemmas that corresponds to that
- * sample point, and adds a lemma to lems if cegisSample mode is not trust.
+ * sample point, and adds a lemma to d_qim pending lemmas if cegisSample mode
+ * is not trust.
*/
bool sampleAddRefinementLemma(const std::vector<Node>& candidates,
- const std::vector<Node>& vals,
- std::vector<Node>& lems);
+ const std::vector<Node>& vals);
/** evaluates candidate values on current refinement lemmas
*
* blocking the current value of candidates.
*/
bool addEvalLemmas(const std::vector<Node>& candidates,
- const std::vector<Node>& candidate_values,
- std::vector<Node>& lems);
+ const std::vector<Node>& candidate_values);
/** Get the node corresponding to the conjunction of all refinement lemmas. */
Node getRefinementLemmaFormula();
//-----------------------------------end refinement lemmas
bool CegisCoreConnective::processInitialize(Node conj,
Node n,
- const std::vector<Node>& candidates,
- std::vector<Node>& lemmas)
+ const std::vector<Node>& candidates)
{
Trace("sygus-ccore-init") << "CegisCoreConnective::initialize" << std::endl;
Trace("sygus-ccore-init") << " conjecture : " << conj << std::endl;
// conjunctions).
Node tst = datatypes::utils::mkTester(d_candidate, i, gdt);
Trace("sygus-ccore-init") << "Sym break lemma " << tst << std::endl;
- lemmas.push_back(tst.negate());
+ d_qim.lemma(tst.negate(),
+ InferenceId::QUANTIFIERS_SYGUS_CEGIS_UCL_SYM_BREAK);
}
}
if (!isActive())
return false;
}
// initialize the enumerator
- return Cegis::processInitialize(conj, n, candidates, lemmas);
+ return Cegis::processInitialize(conj, n, candidates);
}
bool CegisCoreConnective::processConstructCandidates(
const std::vector<Node>& enum_values,
const std::vector<Node>& candidates,
std::vector<Node>& candidate_values,
- bool satisfiedRl,
- std::vector<Node>& lems)
+ bool satisfiedRl)
{
Assert(isActive());
bool ret = constructSolution(enums, enum_values, candidate_values);
{
lem = nm->mkNode(OR, g.negate(), lem);
}
- lems.push_back(lem);
+ d_qim.addPendingLemma(lem,
+ InferenceId::QUANTIFIERS_SYGUS_CEGIS_UCL_EXCLUDE);
}
return ret;
}
/** do cegis-implementation-specific initialization for this class */
bool processInitialize(Node conj,
Node n,
- const std::vector<Node>& candidates,
- std::vector<Node>& lemmas) override;
+ const std::vector<Node>& candidates) override;
/** do cegis-implementation-specific post-processing for construct candidate
*
* satisfiedRl is whether all refinement lemmas are satisfied under the
const std::vector<Node>& enum_values,
const std::vector<Node>& candidates,
std::vector<Node>& candidate_values,
- bool satisfiedRl,
- std::vector<Node>& lems) override;
+ bool satisfiedRl) override;
/** construct solution
*
CegisUnif::~CegisUnif() {}
bool CegisUnif::processInitialize(Node conj,
Node n,
- const std::vector<Node>& candidates,
- std::vector<Node>& lemmas)
+ const std::vector<Node>& candidates)
{
// list of strategy points for unification candidates
std::vector<Node> unif_candidate_pts;
bool CegisUnif::getEnumValues(const std::vector<Node>& enums,
const std::vector<Node>& enum_values,
std::map<Node, std::vector<Node>>& unif_cenums,
- std::map<Node, std::vector<Node>>& unif_cvalues,
- std::vector<Node>& lems)
+ std::map<Node, std::vector<Node>>& unif_cvalues)
{
NodeManager* nm = NodeManager::currentNM();
Node cost_lit = d_u_enum_manager.getAssertedLiteral();
void CegisUnif::setConditions(
const std::map<Node, std::vector<Node>>& unif_cenums,
- const std::map<Node, std::vector<Node>>& unif_cvalues,
- std::vector<Node>& lems)
+ const std::map<Node, std::vector<Node>>& unif_cvalues)
{
Node cost_lit = d_u_enum_manager.getAssertedLiteral();
NodeManager* nm = NodeManager::currentNM();
Node exp_exc = d_tds->getExplain()
->getExplanationForEquality(eu, itv->second[0])
.negate();
- lems.push_back(nm->mkNode(OR, g.negate(), exp_exc));
+ Node lem = nm->mkNode(OR, g.negate(), exp_exc);
+ d_qim.addPendingLemma(
+ lem, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_COND_EXCLUDE);
}
}
}
const std::vector<Node>& enum_values,
const std::vector<Node>& candidates,
std::vector<Node>& candidate_values,
- bool satisfiedRl,
- std::vector<Node>& lems)
+ bool satisfiedRl)
{
if (d_unif_candidates.empty())
{
Assert(d_non_unif_candidates.size() == candidates.size());
return Cegis::processConstructCandidates(
- enums, enum_values, candidates, candidate_values, satisfiedRl, lems);
+ enums, enum_values, candidates, candidate_values, satisfiedRl);
}
if (Trace.isOn("cegis-unif"))
{
// we only proceed to solution building if we are not introducing symmetry
// breaking lemmas between return values and if we have not previously
// introduced return values refinement lemmas
- if (!getEnumValues(enums, enum_values, unif_cenums, unif_cvalues, lems)
+ if (!getEnumValues(enums, enum_values, unif_cenums, unif_cvalues)
|| !satisfiedRl)
{
// if condition values are being indepedently enumerated, they should be
// proceeding to attempt solution building
if (usingConditionPool())
{
- setConditions(unif_cenums, unif_cvalues, lems);
+ setConditions(unif_cenums, unif_cvalues);
}
Trace("cegis-unif") << (!satisfiedRl
? "..added refinement lemmas"
// if we didn't satisfy the specification, there is no way to repair
return false;
}
- setConditions(unif_cenums, unif_cvalues, lems);
+ setConditions(unif_cenums, unif_cvalues);
// build solutions (for unif candidates a divide-and-conquer approach is used)
std::vector<Node> sols;
std::vector<Node> lemmas;
return false;
}
-void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
- Node lem,
- std::vector<Node>& lems)
+void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars, Node lem)
{
// Notify lemma to unification utility and get its purified form
std::map<Node, std::vector<Node>> eval_pts;
// parent's guard, which has the semantics "this conjecture has a solution",
// hence this lemma states: if the parent conjecture has a solution, it
// satisfies the specification for the given concrete point.
- lems.push_back(NodeManager::currentNM()->mkNode(
- OR, d_parent->getGuard().negate(), plem));
+ Node rlem =
+ NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), plem);
+ d_qim.addPendingLemma(rlem,
+ InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_REFINEMENT);
}
CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
* in which d is the deep embedding of the function-to-synthesize f
*/
void registerRefinementLemma(const std::vector<Node>& vars,
- Node lem,
- std::vector<Node>& lems) override;
+ Node lem) override;
private:
/** do cegis-implementation-specific initialization for this class */
bool processInitialize(Node conj,
Node n,
- const std::vector<Node>& candidates,
- std::vector<Node>& lemmas) override;
+ const std::vector<Node>& candidates) override;
/** Tries to build new candidate solutions with new enumerated expressions
*
* This function relies on a data-driven unification-based approach for
* for constructing candidate solutions when possible.
*
* This function also excludes models where (terms = terms_values) by adding
- * blocking clauses to lems. For example, for grammar:
+ * blocking clauses to d_qim pending lemmas. For example, for grammar:
* A -> A+A | x | 1 | 0
* and a call where terms = { d } and term_values = { +( x, 1 ) }, it adds:
* ~G V ~is_+( d ) V ~is_x( d.1 ) V ~is_1( d.2 )
- * to lems, where G is active guard of the enumerator d (see
+ * to d_qim pending lemmas, where G is active guard of the enumerator d (see
* TermDatabaseSygus::getActiveGuardForEnumerator). This blocking clause
* indicates that d should not be given the model value +( x, 1 ) anymore,
* since { d -> +( x, 1 ) } has now been added to the database of this class.
const std::vector<Node>& enum_values,
const std::vector<Node>& candidates,
std::vector<Node>& candidate_values,
- bool satisfiedRl,
- std::vector<Node>& lems) override;
+ bool satisfiedRl) override;
/** communicate condition values to solution building utility
*
* for each unification candidate and for each strategy point associated with
* condition enumerators (unif_cenums)
*/
void setConditions(const std::map<Node, std::vector<Node>>& unif_cenums,
- const std::map<Node, std::vector<Node>>& unif_cvalues,
- std::vector<Node>& lems);
+ const std::map<Node, std::vector<Node>>& unif_cvalues);
/** set values of condition enumerators based on current enumerator assignment
*
* enums and enum_values are the enumerators registered in getTermList and
bool getEnumValues(const std::vector<Node>& enums,
const std::vector<Node>& enum_values,
std::map<Node, std::vector<Node>>& unif_cenums,
- std::map<Node, std::vector<Node>>& unif_cvalues,
- std::vector<Node>& lems);
+ std::map<Node, std::vector<Node>>& unif_cvalues);
/**
* Whether we are using condition pool enumeration (Section 4 of Barbosa et al
* n is the "base instantiation" of the deep-embedding version of the
* synthesis conjecture under candidates (see SynthConjecture::d_base_inst).
*
- * This function may add lemmas to the argument lemmas, which should be
- * sent out on the output channel of quantifiers by the caller.
+ * This function may also sends lemmas during this call via the quantifiers
+ * inference manager. Note that lemmas should be sent immediately via
+ * d_qim.lemma in this call. This is in contrast to other methods which
+ * add pending lemmas to d_qim.
*/
virtual bool initialize(Node conj,
Node n,
- const std::vector<Node>& candidates,
- std::vector<Node>& lemmas) = 0;
+ const std::vector<Node>& candidates) = 0;
/** get term list
*
* This gets the list of terms that will appear as arguments to a subsequent
* tested by testing the (un)satisfiablity of P( v, cex ) for fresh cex by the
* caller.
*
- * This function may also add lemmas to lems, which are sent out as lemmas
- * on the output channel of quantifiers by the caller. For an example of
- * such lemmas, see SygusPbe::constructCandidates.
+ * This function may also add pending lemmas during this call via the
+ * quantifiers inference manager d_qim. For an example of such lemmas, see
+ * SygusPbe::constructCandidates..
*
* This function may return false if it does not have a candidate it wants
- * to test on this iteration. In this case, lems should be non-empty.
+ * to test on this iteration. In this case, the module should have sent
+ * lemmas.
*/
virtual bool constructCandidates(const std::vector<Node>& terms,
const std::vector<Node>& term_values,
const std::vector<Node>& candidates,
- std::vector<Node>& candidate_values,
- std::vector<Node>& lems) = 0;
+ std::vector<Node>& candidate_values) = 0;
/** register refinement lemma
*
* Assume this module, on a previous call to constructCandidates, added the
* is called when the refinement lemma P( v, cex ) has a model M. In calls to
* this function, the argument vars is cex and lem is P( k, cex^M ).
*
- * This function may also add lemmas to lems, which are sent out as lemmas
- * on the output channel of quantifiers by the caller. For an example of
- * such lemmas, see Cegis::registerRefinementLemma.
+ * This function may also add pending lemmas during this call via the
+ * quantifiers inference manager d_qim. For an example of such lemmas, see
+ * Cegis::registerRefinementLemma.
*/
- virtual void registerRefinementLemma(const std::vector<Node>& vars,
- Node lem,
- std::vector<Node>& lems)
+ virtual void registerRefinementLemma(const std::vector<Node>& vars, Node lem)
{
}
/**
bool SygusPbe::initialize(Node conj,
Node n,
- const std::vector<Node>& candidates,
- std::vector<Node>& lemmas)
+ const std::vector<Node>& candidates)
{
Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
NodeManager* nm = NodeManager::currentNM();
bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
const std::vector<Node>& enum_values,
const std::vector<Node>& candidates,
- std::vector<Node>& candidate_values,
- std::vector<Node>& lems)
+ std::vector<Node>& candidate_values)
{
Assert(enums.size() == enum_values.size());
if( !enums.empty() ){
Assert(!g.isNull());
for (unsigned k = 0, size = enum_lems.size(); k < size; k++)
{
- enum_lems[k] = nm->mkNode(OR, g.negate(), enum_lems[k]);
+ Node lem = nm->mkNode(OR, g.negate(), enum_lems[k]);
+ d_qim.addPendingLemma(lem,
+ InferenceId::QUANTIFIERS_SYGUS_PBE_EXCLUDE);
}
- lems.insert(lems.end(), enum_lems.begin(), enum_lems.end());
}
}
}
Node c = candidates[i];
//build decision tree for candidate
std::vector<Node> sol;
- if (d_sygus_unif[c]->constructSolution(sol, lems))
+ std::vector<Node> lems;
+ bool solSuccess = d_sygus_unif[c]->constructSolution(sol, lems);
+ for (const Node& lem : lems)
+ {
+ d_qim.addPendingLemma(lem,
+ InferenceId::QUANTIFIERS_SYGUS_PBE_CONSTRUCT_SOL);
+ }
+ if (solSuccess)
{
Assert(sol.size() == 1);
candidate_values.push_back(sol[0]);
~SygusPbe();
/** initialize this class
- *
- * This function may add lemmas to the vector lemmas corresponding
- * to initial lemmas regarding static analysis of enumerators it
- * introduced. For example, we may say that the top-level symbol
- * of an enumerator is not ITE if it is being used to construct
- * return values for decision trees.
- */
+ *
+ * This function may add lemmas via the inference manager corresponding
+ * to initial lemmas regarding static analysis of enumerators it
+ * introduced. For example, we may say that the top-level symbol
+ * of an enumerator is not ITE if it is being used to construct
+ * return values for decision trees.
+ */
bool initialize(Node conj,
Node n,
- const std::vector<Node>& candidates,
- std::vector<Node>& lemmas) override;
+ const std::vector<Node>& candidates) override;
/** get term list
*
* Adds all active enumerators associated with functions-to-synthesize in
* for constructing candidate solutions when possible.
*
* This function also excludes models where (terms = terms_values) by adding
- * blocking clauses to lems. For example, for grammar:
+ * blocking clauses to d_qim pending lemmas. For example, for grammar:
* A -> A+A | x | 1 | 0
* and a call where terms = { d } and term_values = { +( x, 1 ) }, it adds:
* ~G V ~is_+( d ) V ~is_x( d.1 ) V ~is_1( d.2 )
- * to lems, where G is active guard of the enumerator d (see
+ * to d_qim, where G is active guard of the enumerator d (see
* TermDatabaseSygus::getActiveGuardForEnumerator). This blocking clause
* indicates that d should not be given the model value +( x, 1 ) anymore,
* since { d -> +( x, 1 ) } has now been added to the database of this class.
bool constructCandidates(const std::vector<Node>& terms,
const std::vector<Node>& term_values,
const std::vector<Node>& candidates,
- std::vector<Node>& candidate_values,
- std::vector<Node>& lems) override;
+ std::vector<Node>& candidate_values) override;
/** is PBE enabled for any enumerator? */
bool isPbe() { return d_is_pbe; }
namespace quantifiers {
SygusStatistics::SygusStatistics()
- : d_cegqi_lemmas_ce(
- smtStatisticsRegistry().registerInt("SynthEngine::cegqi_lemmas_ce")),
- d_cegqi_lemmas_refine(smtStatisticsRegistry().registerInt(
- "SynthEngine::cegqi_lemmas_refine")),
- d_cegqi_si_lemmas(
- smtStatisticsRegistry().registerInt("SynthEngine::cegqi_lemmas_si")),
- d_solutions(
+ : d_solutions(
smtStatisticsRegistry().registerInt("SynthConjecture::solutions")),
d_filtered_solutions(smtStatisticsRegistry().registerInt(
"SynthConjecture::filtered_solutions")),
{
public:
SygusStatistics();
- /** Number of counterexample lemmas */
- IntStat d_cegqi_lemmas_ce;
- /** Number of refinement lemmas */
- IntStat d_cegqi_lemmas_refine;
- /** Number of single invocation lemmas */
- IntStat d_cegqi_si_lemmas;
/** Number of solutions printed (could be >1 for --sygus-stream) */
IntStat d_solutions;
/** Number of solutions filtered */
d_master(nullptr),
d_set_ce_sk_vars(false),
d_repair_index(0),
- d_refine_count(0),
d_guarded_stream_exc(false)
{
if (options::sygusSymBreakPbe() || options::sygusUnifPbe())
// register this term with sygus database and other utilities that impact
// the enumerative sygus search
- std::vector<Node> guarded_lemmas;
if (!isSingleInvocation())
{
d_ceg_proc->initialize(d_base_inst, d_candidates);
for (unsigned i = 0, size = d_modules.size(); i < size; i++)
{
- if (d_modules[i]->initialize(
- d_simp_quant, d_base_inst, d_candidates, guarded_lemmas))
+ if (d_modules[i]->initialize(d_simp_quant, d_base_inst, d_candidates))
{
d_master = d_modules[i];
break;
// has been used on this call to check.
d_qim.requirePhase(d_feasible_guard, true);
- Node gneg = d_feasible_guard.negate();
- for (unsigned i = 0; i < guarded_lemmas.size(); i++)
- {
- Node lem = nm->mkNode(OR, gneg, guarded_lemmas[i]);
- Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem
- << std::endl;
- d_qim.lemma(lem, InferenceId::UNKNOWN);
- }
-
Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation()
<< std::endl;
}
}
bool SynthConjecture::needsRefinement() const { return d_set_ce_sk_vars; }
-bool SynthConjecture::doCheck(std::vector<Node>& lems)
+bool SynthConjecture::doCheck()
{
if (isSingleInvocation())
{
{
d_hasSolution = true;
// the conjecture has a solution, so its negation holds
- lems.push_back(d_quant.negate());
+ Node qn = d_quant.negate();
+ d_qim.addPendingLemma(qn, InferenceId::QUANTIFIERS_SYGUS_SI_SOLVED);
}
return true;
}
}
Assert(candidate_values.empty());
constructed_cand = d_master->constructCandidates(
- terms, enum_values, d_candidates, candidate_values, lems);
+ terms, enum_values, d_candidates, candidate_values);
// now clear the evaluation caches
for (std::pair<const Node, std::unique_ptr<ExampleEvalCache> >& ecp :
d_exampleEvalCache)
// we have that the current candidate passed a sample test
// since we trust sampling in this mode, we assert there is no
// counterexample to the conjecture here.
- lems.push_back(d_quant.negate());
+ Node qn = d_quant.negate();
+ d_qim.addPendingLemma(qn,
+ InferenceId::QUANTIFIERS_SYGUS_SAMPLE_TRUST_SOLVED);
recordSolution(candidate_values);
return true;
}
}
// Use lemma to terminate with "unsat", this is justified by the verification
// check above, which confirms the synthesis conjecture is solved.
- lems.push_back(d_quant.negate());
+ Node qn = d_quant.negate();
+ d_qim.addPendingLemma(qn, InferenceId::QUANTIFIERS_SYGUS_VERIFY_SOLVED);
return true;
}
bool SynthConjecture::doRefine()
{
- std::vector<Node> lems;
Assert(d_set_ce_sk_vars);
// first, make skolem substitution
Assert(d_inner_vars.empty());
}
- std::vector<Node> lem_c;
Trace("cegqi-refine") << "doRefine : Construct refinement lemma..."
<< std::endl;
Trace("cegqi-refine-debug")
base_lem = d_tds->rewriteNode(base_lem);
Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem
<< "..." << std::endl;
- d_master->registerRefinementLemma(sk_vars, base_lem, lems);
+ size_t prevPending = d_qim.numPendingLemmas();
+ d_master->registerRefinementLemma(sk_vars, base_lem);
Trace("cegqi-refine") << "doRefine : finished" << std::endl;
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_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
- if (res)
- {
- ++(d_stats.d_cegqi_lemmas_refine);
- d_refine_count++;
- addedLemma = true;
- }
- else
- {
- Trace("cegqi-warn") << " ...FAILED to add refinement!" << std::endl;
- }
- }
+ // check if we added a lemma
+ bool addedLemma = d_qim.numPendingLemmas() > prevPending;
if (addedLemma)
{
Trace("sygus-engine-debug") << " ...refine candidate." << std::endl;
* concrete terms t1, ..., tn to check, where we make up to n calls to doCheck
* when each of t1, ..., tn fails to satisfy the current refinement lemmas.
*/
- bool doCheck(std::vector<Node>& lems);
+ bool doCheck();
/** do refinement
*
* This is step 2(b) of Figure 3 of Reynolds et al CAV 2015.
* not yet tried to repair.
*/
unsigned d_repair_index;
- /** number of times we have called doRefine */
- unsigned d_refine_count;
/** record solution (this is used to construct solutions later) */
void recordSolution(std::vector<Node>& vs);
/** get synth solutions internal
Trace("sygus-engine-debug") << "Do conjecture check..." << std::endl;
Trace("sygus-engine-debug")
<< " *** Check candidate phase..." << std::endl;
- std::vector<Node> cclems;
- bool ret = conj->doCheck(cclems);
- bool addedLemma = false;
- for (const Node& lem : cclems)
- {
- if (d_qim.addPendingLemma(lem, InferenceId::UNKNOWN))
- {
- ++(d_statistics.d_cegqi_lemmas_ce);
- addedLemma = true;
- }
- else
- {
- // this may happen if we eagerly unfold, simplify to true
- Trace("sygus-engine-debug")
- << " ...FAILED to add candidate!" << std::endl;
- }
- }
- if (addedLemma)
+ 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;
projects / cvc5.git / commitdiff