From 19ab3936ef46e93a98a142e0c454659ecc1d1e27 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 17 May 2018 09:23:14 -0500 Subject: [PATCH] Internal propagation for refinement lemmas (#1932) --- .../sygus/ce_guided_conjecture.cpp | 8 +- src/theory/quantifiers/sygus/cegis.cpp | 322 ++++++++++++------ src/theory/quantifiers/sygus/cegis.h | 29 +- src/theory/quantifiers/sygus/cegis_unif.cpp | 3 +- src/theory/quantifiers/sygus/cegis_unif.h | 2 - src/theory/quantifiers/sygus/sygus_module.cpp | 2 +- src/theory/quantifiers/sygus/sygus_module.h | 2 + src/theory/quantifiers/sygus/sygus_pbe.cpp | 1 - src/theory/quantifiers/sygus/sygus_pbe.h | 2 - .../quantifiers/sygus/term_database_sygus.cpp | 27 ++ .../quantifiers/sygus/term_database_sygus.h | 6 + 11 files changed, 273 insertions(+), 131 deletions(-) diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index cc12fdf17..6f5709fc2 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -367,11 +367,9 @@ void CegConjecture::doCheck(std::vector& lems) { lem = Rewriter::rewrite( lem ); //eagerly unfold applications of evaluation function - if( options::sygusDirectEval() ){ - Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl; - std::map< Node, Node > visited_n; - lem = d_qe->getTermDatabaseSygus()->getEagerUnfold( lem, visited_n ); - } + Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl; + std::map visited_n; + lem = d_qe->getTermDatabaseSygus()->getEagerUnfold(lem, visited_n); // record the instantiation // this is used for remembering the solution recordInstantiation(candidate_values); diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index e8d29835a..47053080a 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -51,10 +51,9 @@ bool Cegis::initialize(Node n, } // initialize an enumerator for each candidate - TermDbSygus* tds = d_qe->getTermDatabaseSygus(); for (unsigned i = 0; i < candidates.size(); i++) { - tds->registerEnumerator(candidates[i], candidates[i], d_parent); + d_tds->registerEnumerator(candidates[i], candidates[i], d_parent); } return true; } @@ -68,10 +67,6 @@ void Cegis::getTermList(const std::vector& candidates, bool Cegis::addEvalLemmas(const std::vector& candidates, const std::vector& candidate_values) { - if (!options::sygusDirectEval()) - { - return false; - } NodeManager* nm = NodeManager::currentNM(); bool addedEvalLemmas = false; if (options::sygusCRefEval()) @@ -96,18 +91,21 @@ bool Cegis::addEvalLemmas(const std::vector& candidates, add the lemmas below as well, in parallel. */ } } + if (!options::sygusDirectEval()) + { + return addedEvalLemmas; + } Trace("cegqi-engine") << " *** Do direct evaluation..." << std::endl; std::vector eager_terms, eager_vals, eager_exps; - TermDbSygus* tds = d_qe->getTermDatabaseSygus(); for (unsigned i = 0, size = candidates.size(); i < size; ++i) { Trace("cegqi-debug") << " register " << candidates[i] << " -> " << candidate_values[i] << std::endl; - tds->registerModelValue(candidates[i], - candidate_values[i], - eager_terms, - eager_vals, - eager_exps); + d_tds->registerModelValue(candidates[i], + candidate_values[i], + eager_terms, + eager_vals, + eager_exps); } Trace("cegqi-debug") << "...produced " << eager_terms.size() << " eager evaluation lemmas.\n"; @@ -148,11 +146,136 @@ bool Cegis::constructCandidates(const std::vector& enums, return true; } +void Cegis::addRefinementLemma(Node lem) +{ + d_refinement_lemmas.push_back(lem); + // apply existing substitution + Node slem = lem; + if (!d_rl_eval_hds.empty()) + { + slem = lem.substitute(d_rl_eval_hds.begin(), + d_rl_eval_hds.end(), + d_rl_vals.begin(), + d_rl_vals.end()); + } + // rewrite with extended rewriter + slem = d_tds->getExtRewriter()->extendedRewrite(slem); + std::vector waiting; + waiting.push_back(lem); + unsigned wcounter = 0; + // while we are not done adding lemmas + while (wcounter < waiting.size()) + { + // add the conjunct, possibly propagating + addRefinementLemmaConjunct(wcounter, waiting); + wcounter++; + } +} + +void Cegis::addRefinementLemmaConjunct(unsigned wcounter, + std::vector& waiting) +{ + Node lem = waiting[wcounter]; + lem = Rewriter::rewrite(lem); + // apply substitution and rewrite if applicable + if (lem.isConst()) + { + if (!lem.getConst()) + { + // conjecture is infeasible + } + else + { + return; + } + } + // break into conjunctions + if (lem.getKind() == AND) + { + for (const Node& lc : lem) + { + waiting.push_back(lc); + } + return; + } + // does this correspond to a substitution? + NodeManager* nm = NodeManager::currentNM(); + TNode term; + TNode val; + if (lem.getKind() == EQUAL) + { + for (unsigned i = 0; i < 2; i++) + { + if (lem[i].isConst() && d_tds->isEvaluationPoint(lem[1 - i])) + { + term = lem[1 - i]; + val = lem[i]; + break; + } + } + } + else + { + term = lem.getKind() == NOT ? lem[0] : lem; + // predicate case: the conjunct is a (negated) evaluation point + if (d_tds->isEvaluationPoint(term)) + { + val = nm->mkConst(lem.getKind() != NOT); + } + } + if (!val.isNull()) + { + if (d_refinement_lemma_unit.find(lem) != d_refinement_lemma_unit.end()) + { + // already added + return; + } + Trace("cegis-rl") << "* cegis-rl: propagate: " << term << " -> " << val + << std::endl; + d_rl_eval_hds.push_back(term); + d_rl_vals.push_back(val); + d_refinement_lemma_unit.insert(lem); + // apply to waiting lemmas beyond this one + for (unsigned i = wcounter + 1, size = waiting.size(); i < size; i++) + { + waiting[i] = waiting[i].substitute(term, val); + } + // apply to all existing refinement lemmas + std::vector to_rem; + for (const Node& rl : d_refinement_lemma_conj) + { + Node srl = rl.substitute(term, val); + if (srl != rl) + { + Trace("cegis-rl") << "* cegis-rl: replace: " << rl << " -> " << srl + << std::endl; + waiting.push_back(srl); + to_rem.push_back(rl); + } + } + for (const Node& tr : to_rem) + { + d_refinement_lemma_conj.erase(tr); + } + } + else + { + if (Trace.isOn("cegis-rl")) + { + if (d_refinement_lemma_conj.find(lem) == d_refinement_lemma_conj.end()) + { + Trace("cegis-rl") << "cegis-rl: add: " << lem << std::endl; + } + } + d_refinement_lemma_conj.insert(lem); + } +} + void Cegis::registerRefinementLemma(const std::vector& vars, Node lem, std::vector& lems) { - d_refinement_lemmas.push_back(lem); + addRefinementLemma(lem); // Make the refinement lemma and add it to lems. // This lemma is guarded by the parent's guard, which has the semantics // "this conjecture has a solution", hence this lemma states: @@ -168,118 +291,93 @@ void Cegis::getRefinementEvalLemmas(const std::vector& vs, std::vector& lems) { Trace("sygus-cref-eval") << "Cref eval : conjecture has " - << getNumRefinementLemmas() << " refinement lemmas." + << d_refinement_lemma_unit.size() << " unit and " + << d_refinement_lemma_conj.size() + << " non-unit refinement lemma conjunctions." << std::endl; - unsigned nlemmas = getNumRefinementLemmas(); - if (nlemmas > 0 || options::cegisSample() != CEGIS_SAMPLE_NONE) - { - Assert(vs.size() == ms.size()); + Assert(vs.size() == ms.size()); - TermDbSygus* tds = d_qe->getTermDatabaseSygus(); - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = NodeManager::currentNM(); - Node nfalse = nm->mkConst(false); - Node neg_guard = d_parent->getGuard().negate(); - for (unsigned i = 0; i <= nlemmas; i++) + Node nfalse = nm->mkConst(false); + Node neg_guard = d_parent->getGuard().negate(); + for (unsigned r = 0; r < 2; r++) + { + std::unordered_set& rlemmas = + r == 0 ? d_refinement_lemma_unit : d_refinement_lemma_conj; + for (const Node& lem : rlemmas) { - if (i == nlemmas) - { - bool addedSample = false; - // find a new one by sampling, if applicable - if (options::cegisSample() != CEGIS_SAMPLE_NONE) - { - addedSample = sampleAddRefinementLemma(vs, ms, lems); - } - if (!addedSample) - { - return; - } - } - Node lem; + Assert(!lem.isNull()); std::map visited; std::map > exp; - lem = getRefinementLemma(i); - if (!lem.isNull()) + EvalSygusInvarianceTest vsit; + Trace("sygus-cref-eval") << "Check refinement lemma conjunct " << lem + << " against current model." << std::endl; + Trace("sygus-cref-eval2") << "Check refinement lemma conjunct " << lem + << " against current model." << std::endl; + Node cre_lem; + Node lemcs = lem.substitute(vs.begin(), vs.end(), ms.begin(), ms.end()); + Trace("sygus-cref-eval2") + << "...under substitution it is : " << lemcs << std::endl; + Node lemcsu = vsit.doEvaluateWithUnfolding(d_tds, lemcs); + Trace("sygus-cref-eval2") + << "...after unfolding is : " << lemcsu << std::endl; + if (lemcsu.isConst() && !lemcsu.getConst()) { - std::vector lem_conj; - // break into conjunctions - if (lem.getKind() == kind::AND) + std::vector msu; + std::vector mexp; + msu.insert(msu.end(), ms.begin(), ms.end()); + std::map var_count; + for (unsigned k = 0; k < vs.size(); k++) { - for (unsigned i = 0; i < lem.getNumChildren(); i++) - { - lem_conj.push_back(lem[i]); - } + vsit.setUpdatedTerm(msu[k]); + msu[k] = vs[k]; + // substitute for everything except this + Node sconj = + lem.substitute(vs.begin(), vs.end(), msu.begin(), msu.end()); + vsit.init(sconj, vs[k], nfalse); + // get minimal explanation for this + Node ut = vsit.getUpdatedTerm(); + Trace("sygus-cref-eval2-debug") + << " compute min explain of : " << vs[k] << " = " << ut + << std::endl; + d_tds->getExplain()->getExplanationFor( + vs[k], ut, mexp, vsit, var_count, false); + Trace("sygus-cref-eval2-debug") << "exp now: " << mexp << std::endl; + msu[k] = vsit.getUpdatedTerm(); + Trace("sygus-cref-eval2-debug") + << "updated term : " << msu[k] << std::endl; } - else + if (!mexp.empty()) { - lem_conj.push_back(lem); + Node en = mexp.size() == 1 ? mexp[0] : nm->mkNode(kind::AND, mexp); + cre_lem = nm->mkNode(kind::OR, en.negate(), neg_guard); } - EvalSygusInvarianceTest vsit; - for (unsigned j = 0; j < lem_conj.size(); j++) + else { - Node lemc = lem_conj[j]; - Trace("sygus-cref-eval") << "Check refinement lemma conjunct " << lemc - << " against current model." << std::endl; - Trace("sygus-cref-eval2") << "Check refinement lemma conjunct " - << lemc << " against current model." - << std::endl; - Node cre_lem; - Node lemcs = - lemc.substitute(vs.begin(), vs.end(), ms.begin(), ms.end()); - Trace("sygus-cref-eval2") << "...under substitution it is : " << lemcs - << std::endl; - Node lemcsu = vsit.doEvaluateWithUnfolding(tds, lemcs); - Trace("sygus-cref-eval2") << "...after unfolding is : " << lemcsu - << std::endl; - if (lemcsu.isConst() && !lemcsu.getConst()) - { - std::vector msu; - std::vector mexp; - msu.insert(msu.end(), ms.begin(), ms.end()); - std::map var_count; - for (unsigned k = 0; k < vs.size(); k++) - { - vsit.setUpdatedTerm(msu[k]); - msu[k] = vs[k]; - // substitute for everything except this - Node sconj = - lemc.substitute(vs.begin(), vs.end(), msu.begin(), msu.end()); - vsit.init(sconj, vs[k], nfalse); - // get minimal explanation for this - Node ut = vsit.getUpdatedTerm(); - Trace("sygus-cref-eval2-debug") - << " compute min explain of : " << vs[k] << " = " << ut - << std::endl; - tds->getExplain()->getExplanationFor( - vs[k], ut, mexp, vsit, var_count, false); - Trace("sygus-cref-eval2-debug") - << "exp now: " << mexp << std::endl; - msu[k] = vsit.getUpdatedTerm(); - Trace("sygus-cref-eval2-debug") - << "updated term : " << msu[k] << std::endl; - } - if (!mexp.empty()) - { - Node en = - mexp.size() == 1 ? mexp[0] : nm->mkNode(kind::AND, mexp); - cre_lem = nm->mkNode(kind::OR, en.negate(), neg_guard); - } - else - { - cre_lem = neg_guard; - } - } - if (!cre_lem.isNull()) - { - if (std::find(lems.begin(), lems.end(), cre_lem) == lems.end()) - { - Trace("sygus-cref-eval") << "...produced lemma : " << cre_lem - << std::endl; - lems.push_back(cre_lem); - } - } + cre_lem = neg_guard; } } + if (!cre_lem.isNull() + && std::find(lems.begin(), lems.end(), cre_lem) == lems.end()) + { + Trace("sygus-cref-eval") + << "...produced lemma : " << cre_lem << std::endl; + lems.push_back(cre_lem); + } + } + if (!lems.empty()) + { + break; + } + } + // if we didn't add a lemma, trying sampling to add one + if (options::cegisSample() != CEGIS_SAMPLE_NONE && lems.empty()) + { + if (sampleAddRefinementLemma(vs, ms, lems)) + { + // restart (should be guaranteed to add evaluation lemmas + getRefinementEvalLemmas(vs, ms, lems); } } } @@ -344,7 +442,7 @@ bool Cegis::sampleAddRefinementLemma(const std::vector& candidates, Trace("cegis-sample") << std::endl; } Trace("cegqi-engine") << " *** Refine by sampling" << std::endl; - d_refinement_lemmas.push_back(rlem); + addRefinementLemma(rlem); // if trust, we are not interested in sending out refinement lemmas if (options::cegisSample() != CEGIS_SAMPLE_TRUST) { diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 7500abb78..cbd563e07 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -76,14 +76,31 @@ class Cegis : public SygusModule //-----------------------------------refinement lemmas /** refinement lemmas */ std::vector d_refinement_lemmas; - /** get number of refinement lemmas we have added so far */ - unsigned getNumRefinementLemmas() { return d_refinement_lemmas.size(); } - /** get refinement lemma + /** (processed) conjunctions of refinement lemmas that are not unit */ + std::unordered_set d_refinement_lemma_conj; + /** (processed) conjunctions of refinement lemmas that are unit */ + std::unordered_set d_refinement_lemma_unit; + /** substitution entailed by d_refinement_lemma_unit */ + std::vector d_rl_eval_hds; + std::vector d_rl_vals; + /** adds lem as a refinement lemma */ + void addRefinementLemma(Node lem); + /** add refinement lemma conjunct * - * If d_embed_quant is forall d. exists y. P( d, y ), then a refinement - * lemma is one of the form ~P( d_candidates, c ) for some c. + * This is a helper function for addRefinementLemma. + * + * This adds waiting[wcounter] to the proper vector (d_refinement_lemma_conj + * or d_refinement_lemma_unit). In the case that waiting[wcounter] corresponds + * to a value propagation, e.g. it is of the form: + * (eval x c1...cn) = c + * then it is added to d_refinement_lemma_unit, (eval x c1...cn) -> c is added + * as a substitution in d_rl_eval_hds/d_rl_eval_vals, and applied to previous + * lemmas in d_refinement_lemma_conj and lemmas waiting[k] for k>wcounter. + * Each lemma in d_refinement_lemma_conj that is modifed in this process is + * moved to the vector waiting. */ - Node getRefinementLemma(unsigned i) { return d_refinement_lemmas[i]; } + void addRefinementLemmaConjunct(unsigned wcounter, + std::vector& waiting); /** sample add refinement lemma * * This function will check if there is a sample point in d_sampler that diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index ab9834254..20f062722 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -30,7 +30,6 @@ namespace quantifiers { CegisUnif::CegisUnif(QuantifiersEngine* qe, CegConjecture* p) : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, p) { - d_tds = d_qe->getTermDatabaseSygus(); } CegisUnif::~CegisUnif() {} @@ -254,7 +253,7 @@ void CegisUnif::registerRefinementLemma(const std::vector& vars, // Notify lemma to unification utility and get its purified form std::map> eval_pts; Node plem = d_sygus_unif.addRefLemma(lem, eval_pts); - d_refinement_lemmas.push_back(plem); + addRefinementLemma(plem); Trace("cegis-unif-lemma") << "* Refinement lemma:\n" << plem << "\n"; // Notify the enumeration manager if there are new evaluation points for (const std::pair>& ep : eval_pts) diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 735477821..ecaec4129 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -249,8 +249,6 @@ class CegisUnif : public Cegis Node getNextDecisionRequest(unsigned& priority) override; private: - /** sygus term database of d_qe */ - TermDbSygus* d_tds; /** * Sygus unif utility. This class implements the core algorithm (e.g. decision * tree learning) that this module relies upon. diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp index 19e064350..11747830d 100644 --- a/src/theory/quantifiers/sygus/sygus_module.cpp +++ b/src/theory/quantifiers/sygus/sygus_module.cpp @@ -19,7 +19,7 @@ namespace theory { namespace quantifiers { SygusModule::SygusModule(QuantifiersEngine* qe, CegConjecture* p) - : d_qe(qe), d_parent(p) + : d_qe(qe), d_tds(qe->getTermDatabaseSygus()), d_parent(p) { } diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index 07f5aec9d..75be570e6 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -126,6 +126,8 @@ class SygusModule protected: /** reference to quantifier engine */ QuantifiersEngine* d_qe; + /** sygus term database of d_qe */ + quantifiers::TermDbSygus* d_tds; /** reference to the parent conjecture */ CegConjecture* d_parent; }; diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index cd011ef44..9919dff49 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -31,7 +31,6 @@ namespace quantifiers { CegConjecturePbe::CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p) : SygusModule(qe, p) { - d_tds = d_qe->getTermDatabaseSygus(); d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); d_is_pbe = false; diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index fbf89fee9..dc61f459b 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -188,8 +188,6 @@ class CegConjecturePbe : public SygusModule Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i); private: - /** sygus term database of d_qe */ - quantifiers::TermDbSygus* d_tds; /** true and false nodes */ Node d_true; Node d_false; diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 3d88cbe5d..0b7841170 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -1597,6 +1597,33 @@ Node TermDbSygus::evaluateWithUnfolding( Node n ) { return evaluateWithUnfolding( n, visited ); } +bool TermDbSygus::isEvaluationPoint(Node n) const +{ + if (n.getKind() != APPLY_UF || n.getNumChildren() == 0 || !n[0].isVar()) + { + return false; + } + for (unsigned i = 1, nchild = n.getNumChildren(); i < nchild; i++) + { + if (!n[i].isConst()) + { + return false; + } + } + TypeNode tn = n[0].getType(); + if (!tn.isDatatype()) + { + return false; + } + const Datatype& dt = static_cast(tn.toType()).getDatatype(); + if (!dt.isSygus()) + { + return false; + } + Node eval_op = Node::fromExpr(dt.getSygusEvaluationFunc()); + return eval_op == n.getOperator(); +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 4a3dcb8d6..9466a6a10 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -183,6 +183,12 @@ class TermDbSygus { /** same as above, but with a cache of visited nodes */ Node evaluateWithUnfolding( Node n, std::unordered_map& visited); + /** is evaluation point? + * + * Returns true if n is of the form eval( x, c1...cn ) for some variable x + * and constants c1...cn. + */ + bool isEvaluationPoint(Node n) const; //-----------------------------end conversion from sygus to builtin private: -- 2.30.2