From 9c459e04f32f243a58d5afb6687bd8c5f423ac93 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 4 Aug 2021 15:25:37 -0500 Subject: [PATCH] Add inference ids for remainder of sygus solver (#6977) 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. --- src/theory/inference_id.cpp | 28 ++++++++ src/theory/inference_id.h | 28 ++++++++ src/theory/quantifiers/sygus/cegis.cpp | 64 +++++++------------ src/theory/quantifiers/sygus/cegis.h | 31 ++++----- .../sygus/cegis_core_connective.cpp | 14 ++-- .../quantifiers/sygus/cegis_core_connective.h | 6 +- src/theory/quantifiers/sygus/cegis_unif.cpp | 34 +++++----- src/theory/quantifiers/sygus/cegis_unif.h | 19 ++---- src/theory/quantifiers/sygus/sygus_module.h | 31 +++++---- src/theory/quantifiers/sygus/sygus_pbe.cpp | 20 ++++-- src/theory/quantifiers/sygus/sygus_pbe.h | 24 ++++--- src/theory/quantifiers/sygus/sygus_stats.cpp | 8 +-- src/theory/quantifiers/sygus/sygus_stats.h | 6 -- .../quantifiers/sygus/synth_conjecture.cpp | 53 ++++----------- .../quantifiers/sygus/synth_conjecture.h | 4 +- src/theory/quantifiers/sygus/synth_engine.cpp | 22 ++----- 16 files changed, 184 insertions(+), 208 deletions(-) diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index bf13b75b1..9d8cddb69 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -224,6 +224,12 @@ const char* toString(InferenceId i) 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: @@ -238,6 +244,28 @@ const char* toString(InferenceId i) 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"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index e93803170..3a317e0a4 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -338,6 +338,12 @@ enum class InferenceId 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 @@ -352,6 +358,28 @@ enum class InferenceId 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, diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index a0cebda8e..dff44eb1c 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -41,10 +41,7 @@ Cegis::Cegis(QuantifiersInferenceManager& qim, { } -bool Cegis::initialize(Node conj, - Node n, - const std::vector& candidates, - std::vector& lemmas) +bool Cegis::initialize(Node conj, Node n, const std::vector& candidates) { d_base_body = n; if (d_base_body.getKind() == NOT && d_base_body[0].getKind() == FORALL) @@ -64,13 +61,12 @@ bool Cegis::initialize(Node conj, 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& candidates, - std::vector& lemmas) + const std::vector& candidates) { Trace("cegis") << "Initialize cegis..." << std::endl; unsigned csize = candidates.size(); @@ -111,8 +107,7 @@ void Cegis::getTermList(const std::vector& candidates, } bool Cegis::addEvalLemmas(const std::vector& candidates, - const std::vector& candidate_values, - std::vector& lems) + const std::vector& candidate_values) { // First, decide if this call will apply "conjecture-specific refinement". // In other words, in some settings, the following method will identify and @@ -153,16 +148,11 @@ bool Cegis::addEvalLemmas(const std::vector& candidates, 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. */ } @@ -201,7 +191,7 @@ bool Cegis::addEvalLemmas(const std::vector& candidates, { 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; @@ -237,8 +227,7 @@ Node Cegis::getRefinementLemmaFormula() bool Cegis::constructCandidates(const std::vector& enums, const std::vector& enum_values, const std::vector& candidates, - std::vector& candidate_values, - std::vector& lems) + std::vector& candidate_values) { if (Trace.isOn("cegis")) { @@ -294,35 +283,33 @@ bool Cegis::constructCandidates(const std::vector& enums, 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; @@ -332,8 +319,7 @@ bool Cegis::processConstructCandidates(const std::vector& enums, const std::vector& enum_values, const std::vector& candidates, std::vector& candidate_values, - bool satisfiedRl, - std::vector& lems) + bool satisfiedRl) { if (satisfiedRl) { @@ -473,9 +459,7 @@ void Cegis::addRefinementLemmaConjunct(unsigned wcounter, } } -void Cegis::registerRefinementLemma(const std::vector& vars, - Node lem, - std::vector& lems) +void Cegis::registerRefinementLemma(const std::vector& vars, Node lem) { addRefinementLemma(lem); // Make the refinement lemma and add it to lems. @@ -485,7 +469,7 @@ void Cegis::registerRefinementLemma(const std::vector& vars, // 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; } @@ -628,8 +612,7 @@ bool Cegis::checkRefinementEvalLemmas(const std::vector& vs, } bool Cegis::sampleAddRefinementLemma(const std::vector& candidates, - const std::vector& vals, - std::vector& lems) + const std::vector& vals) { Trace("sygus-engine") << " *** Do sample add refinement..." << std::endl; if (Trace.isOn("cegis-sample")) @@ -691,7 +674,8 @@ bool Cegis::sampleAddRefinementLemma(const std::vector& candidates, 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; } diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index b9f593b69..f5114d7ca 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -47,24 +47,22 @@ class Cegis : public SygusModule /** initialize */ virtual bool initialize(Node conj, Node n, - const std::vector& candidates, - std::vector& lemmas) override; + const std::vector& candidates) override; /** get term list */ virtual void getTermList(const std::vector& candidates, std::vector& enums) override; /** construct candidate */ - virtual bool constructCandidates(const std::vector& enums, - const std::vector& enum_values, - const std::vector& candidates, - std::vector& candidate_values, - std::vector& lems) override; + virtual bool constructCandidates( + const std::vector& enums, + const std::vector& enum_values, + const std::vector& candidates, + std::vector& 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& vars, - Node lem, - std::vector& lems) override; + Node lem) override; /** using repair const */ virtual bool usingRepairConst() override; @@ -85,8 +83,7 @@ class Cegis : public SygusModule */ virtual bool processInitialize(Node conj, Node n, - const std::vector& candidates, - std::vector& lemmas); + const std::vector& candidates); /** do cegis-implementation-specific post-processing for construct candidate * * satisfiedRl is whether all refinement lemmas are satisfied under the @@ -99,8 +96,7 @@ class Cegis : public SygusModule const std::vector& enum_values, const std::vector& candidates, std::vector& candidate_values, - bool satisfiedRl, - std::vector& lems); + bool satisfiedRl); //----------------------------------end cegis-implementation-specific //-----------------------------------refinement lemmas @@ -139,11 +135,11 @@ class Cegis : public SygusModule * 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& candidates, - const std::vector& vals, - std::vector& lems); + const std::vector& vals); /** evaluates candidate values on current refinement lemmas * @@ -168,8 +164,7 @@ class Cegis : public SygusModule * blocking the current value of candidates. */ bool addEvalLemmas(const std::vector& candidates, - const std::vector& candidate_values, - std::vector& lems); + const std::vector& candidate_values); /** Get the node corresponding to the conjunction of all refinement lemmas. */ Node getRefinementLemmaFormula(); //-----------------------------------end refinement lemmas diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index 9953c5d05..4bcede905 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -81,8 +81,7 @@ CegisCoreConnective::CegisCoreConnective(QuantifiersInferenceManager& qim, bool CegisCoreConnective::processInitialize(Node conj, Node n, - const std::vector& candidates, - std::vector& lemmas) + const std::vector& candidates) { Trace("sygus-ccore-init") << "CegisCoreConnective::initialize" << std::endl; Trace("sygus-ccore-init") << " conjecture : " << conj << std::endl; @@ -234,7 +233,8 @@ bool CegisCoreConnective::processInitialize(Node conj, // 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()) @@ -242,7 +242,7 @@ bool CegisCoreConnective::processInitialize(Node conj, return false; } // initialize the enumerator - return Cegis::processInitialize(conj, n, candidates, lemmas); + return Cegis::processInitialize(conj, n, candidates); } bool CegisCoreConnective::processConstructCandidates( @@ -250,8 +250,7 @@ bool CegisCoreConnective::processConstructCandidates( const std::vector& enum_values, const std::vector& candidates, std::vector& candidate_values, - bool satisfiedRl, - std::vector& lems) + bool satisfiedRl) { Assert(isActive()); bool ret = constructSolution(enums, enum_values, candidate_values); @@ -273,7 +272,8 @@ bool CegisCoreConnective::processConstructCandidates( { lem = nm->mkNode(OR, g.negate(), lem); } - lems.push_back(lem); + d_qim.addPendingLemma(lem, + InferenceId::QUANTIFIERS_SYGUS_CEGIS_UCL_EXCLUDE); } return ret; } diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index baff98de3..005e85706 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -175,8 +175,7 @@ class CegisCoreConnective : public Cegis /** do cegis-implementation-specific initialization for this class */ bool processInitialize(Node conj, Node n, - const std::vector& candidates, - std::vector& lemmas) override; + const std::vector& candidates) override; /** do cegis-implementation-specific post-processing for construct candidate * * satisfiedRl is whether all refinement lemmas are satisfied under the @@ -186,8 +185,7 @@ class CegisCoreConnective : public Cegis const std::vector& enum_values, const std::vector& candidates, std::vector& candidate_values, - bool satisfiedRl, - std::vector& lems) override; + bool satisfiedRl) override; /** construct solution * diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 1e77087b7..0b7255e2d 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -41,8 +41,7 @@ CegisUnif::CegisUnif(QuantifiersState& qs, CegisUnif::~CegisUnif() {} bool CegisUnif::processInitialize(Node conj, Node n, - const std::vector& candidates, - std::vector& lemmas) + const std::vector& candidates) { // list of strategy points for unification candidates std::vector unif_candidate_pts; @@ -124,8 +123,7 @@ void CegisUnif::getTermList(const std::vector& candidates, bool CegisUnif::getEnumValues(const std::vector& enums, const std::vector& enum_values, std::map>& unif_cenums, - std::map>& unif_cvalues, - std::vector& lems) + std::map>& unif_cvalues) { NodeManager* nm = NodeManager::currentNM(); Node cost_lit = d_u_enum_manager.getAssertedLiteral(); @@ -240,8 +238,7 @@ bool CegisUnif::usingConditionPool() const void CegisUnif::setConditions( const std::map>& unif_cenums, - const std::map>& unif_cvalues, - std::vector& lems) + const std::map>& unif_cvalues) { Node cost_lit = d_u_enum_manager.getAssertedLiteral(); NodeManager* nm = NodeManager::currentNM(); @@ -271,7 +268,9 @@ void CegisUnif::setConditions( 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); } } } @@ -282,14 +281,13 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, const std::vector& enum_values, const std::vector& candidates, std::vector& candidate_values, - bool satisfiedRl, - std::vector& 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")) { @@ -325,7 +323,7 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, // 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 @@ -333,7 +331,7 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, // 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" @@ -342,7 +340,7 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, // 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 sols; std::vector lemmas; @@ -374,9 +372,7 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, return false; } -void CegisUnif::registerRefinementLemma(const std::vector& vars, - Node lem, - std::vector& lems) +void CegisUnif::registerRefinementLemma(const std::vector& vars, Node lem) { // Notify lemma to unification utility and get its purified form std::map> eval_pts; @@ -398,8 +394,10 @@ void CegisUnif::registerRefinementLemma(const std::vector& vars, // 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( diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index b2c3ba2be..0cddff9c1 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -241,15 +241,13 @@ class CegisUnif : public Cegis * in which d is the deep embedding of the function-to-synthesize f */ void registerRefinementLemma(const std::vector& vars, - Node lem, - std::vector& lems) override; + Node lem) override; private: /** do cegis-implementation-specific initialization for this class */ bool processInitialize(Node conj, Node n, - const std::vector& candidates, - std::vector& lemmas) override; + const std::vector& candidates) override; /** Tries to build new candidate solutions with new enumerated expressions * * This function relies on a data-driven unification-based approach for @@ -263,11 +261,11 @@ class CegisUnif : public Cegis * 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. @@ -276,8 +274,7 @@ class CegisUnif : public Cegis const std::vector& enum_values, const std::vector& candidates, std::vector& candidate_values, - bool satisfiedRl, - std::vector& lems) override; + bool satisfiedRl) override; /** communicate condition values to solution building utility * * for each unification candidate and for each strategy point associated with @@ -285,8 +282,7 @@ class CegisUnif : public Cegis * condition enumerators (unif_cenums) */ void setConditions(const std::map>& unif_cenums, - const std::map>& unif_cvalues, - std::vector& lems); + const std::map>& unif_cvalues); /** set values of condition enumerators based on current enumerator assignment * * enums and enum_values are the enumerators registered in getTermList and @@ -305,8 +301,7 @@ class CegisUnif : public Cegis bool getEnumValues(const std::vector& enums, const std::vector& enum_values, std::map>& unif_cenums, - std::map>& unif_cvalues, - std::vector& lems); + std::map>& unif_cvalues); /** * Whether we are using condition pool enumeration (Section 4 of Barbosa et al diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index f2c3f02de..d93957a15 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -69,13 +69,14 @@ class SygusModule * 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& candidates, - std::vector& lemmas) = 0; + const std::vector& candidates) = 0; /** get term list * * This gets the list of terms that will appear as arguments to a subsequent @@ -110,18 +111,18 @@ class SygusModule * 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& terms, const std::vector& term_values, const std::vector& candidates, - std::vector& candidate_values, - std::vector& lems) = 0; + std::vector& candidate_values) = 0; /** register refinement lemma * * Assume this module, on a previous call to constructCandidates, added the @@ -131,13 +132,11 @@ class SygusModule * 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& vars, - Node lem, - std::vector& lems) + virtual void registerRefinementLemma(const std::vector& vars, Node lem) { } /** diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 892ee6dd4..27a1e3f3b 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -44,8 +44,7 @@ SygusPbe::~SygusPbe() {} bool SygusPbe::initialize(Node conj, Node n, - const std::vector& candidates, - std::vector& lemmas) + const std::vector& candidates) { Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl; NodeManager* nm = NodeManager::currentNM(); @@ -166,8 +165,7 @@ bool SygusPbe::allowPartialModel() { return !options::sygusPbeMultiFair(); } bool SygusPbe::constructCandidates(const std::vector& enums, const std::vector& enum_values, const std::vector& candidates, - std::vector& candidate_values, - std::vector& lems) + std::vector& candidate_values) { Assert(enums.size() == enum_values.size()); if( !enums.empty() ){ @@ -234,9 +232,10 @@ bool SygusPbe::constructCandidates(const std::vector& enums, 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()); } } } @@ -244,7 +243,14 @@ bool SygusPbe::constructCandidates(const std::vector& enums, Node c = candidates[i]; //build decision tree for candidate std::vector sol; - if (d_sygus_unif[c]->constructSolution(sol, lems)) + std::vector 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]); diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 1be4e2b91..e27f4ce35 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -92,17 +92,16 @@ class SygusPbe : public SygusModule ~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& candidates, - std::vector& lemmas) override; + const std::vector& candidates) override; /** get term list * * Adds all active enumerators associated with functions-to-synthesize in @@ -129,11 +128,11 @@ class SygusPbe : public SygusModule * 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. @@ -141,8 +140,7 @@ class SygusPbe : public SygusModule bool constructCandidates(const std::vector& terms, const std::vector& term_values, const std::vector& candidates, - std::vector& candidate_values, - std::vector& lems) override; + std::vector& candidate_values) override; /** is PBE enabled for any enumerator? */ bool isPbe() { return d_is_pbe; } diff --git a/src/theory/quantifiers/sygus/sygus_stats.cpp b/src/theory/quantifiers/sygus/sygus_stats.cpp index 19d799eb3..a1ae3d811 100644 --- a/src/theory/quantifiers/sygus/sygus_stats.cpp +++ b/src/theory/quantifiers/sygus/sygus_stats.cpp @@ -22,13 +22,7 @@ namespace theory { 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")), diff --git a/src/theory/quantifiers/sygus/sygus_stats.h b/src/theory/quantifiers/sygus/sygus_stats.h index 6236547f9..d5166d4da 100644 --- a/src/theory/quantifiers/sygus/sygus_stats.h +++ b/src/theory/quantifiers/sygus/sygus_stats.h @@ -31,12 +31,6 @@ class SygusStatistics { 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 */ diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 73bd6b8a4..ad9aceb8f 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -74,7 +74,6 @@ SynthConjecture::SynthConjecture(QuantifiersState& qs, 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()) @@ -218,14 +217,12 @@ void SynthConjecture::assign(Node q) // register this term with sygus database and other utilities that impact // the enumerative sygus search - std::vector 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; @@ -257,15 +254,6 @@ void SynthConjecture::assign(Node q) // 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; } @@ -307,7 +295,7 @@ bool SynthConjecture::needsCheck() } bool SynthConjecture::needsRefinement() const { return d_set_ce_sk_vars; } -bool SynthConjecture::doCheck(std::vector& lems) +bool SynthConjecture::doCheck() { if (isSingleInvocation()) { @@ -318,7 +306,8 @@ bool SynthConjecture::doCheck(std::vector& lems) { 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; } @@ -449,7 +438,7 @@ bool SynthConjecture::doCheck(std::vector& lems) } 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 >& ecp : d_exampleEvalCache) @@ -512,7 +501,9 @@ bool SynthConjecture::doCheck(std::vector& lems) // 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; } @@ -606,7 +597,8 @@ bool SynthConjecture::doCheck(std::vector& lems) } // 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; } @@ -635,7 +627,6 @@ bool SynthConjecture::checkSideCondition(const std::vector& cvals) const bool SynthConjecture::doRefine() { - std::vector lems; Assert(d_set_ce_sk_vars); // first, make skolem substitution @@ -672,7 +663,6 @@ bool SynthConjecture::doRefine() Assert(d_inner_vars.empty()); } - std::vector lem_c; Trace("cegqi-refine") << "doRefine : Construct refinement lemma..." << std::endl; Trace("cegqi-refine-debug") @@ -696,30 +686,15 @@ bool SynthConjecture::doRefine() 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; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 04999da0d..748ab8b3b 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -83,7 +83,7 @@ class SynthConjecture * 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& lems); + bool doCheck(); /** do refinement * * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015. @@ -341,8 +341,6 @@ class SynthConjecture * 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& vs); /** get synth solutions internal diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 1792f9386..65907cb31 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -213,24 +213,10 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj) Trace("sygus-engine-debug") << "Do conjecture check..." << std::endl; Trace("sygus-engine-debug") << " *** Check candidate phase..." << std::endl; - std::vector 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; -- 2.30.2