From 0e5655c7d1fddde55bfeba9f59bf9af79e8b5f0a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 21 Nov 2019 09:54:12 -0600 Subject: [PATCH] Evaluation unfolding for symbolic SyGuS constructors (#3483) --- src/theory/quantifiers/sygus/cegis.cpp | 29 ++-- src/theory/quantifiers/sygus/cegis.h | 8 +- .../quantifiers/sygus/sygus_eval_unfold.cpp | 139 +++++++++++++++++- .../quantifiers/sygus/sygus_eval_unfold.h | 43 ++++++ .../quantifiers/sygus/sygus_unif_rl.cpp | 3 +- .../quantifiers/sygus/sygus_unif_strat.cpp | 3 +- src/theory/quantifiers/sygus/synth_engine.cpp | 2 - .../quantifiers/sygus/term_database_sygus.cpp | 112 +------------- .../quantifiers/sygus/term_database_sygus.h | 25 ---- 9 files changed, 210 insertions(+), 154 deletions(-) diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index aa0af6f1d..c806bb1e7 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -31,12 +31,9 @@ namespace theory { namespace quantifiers { Cegis::Cegis(QuantifiersEngine* qe, SynthConjecture* p) - : SygusModule(qe, p), d_eval_unfold(nullptr), d_using_gr_repair(false) + : SygusModule(qe, p), d_eval_unfold(nullptr), d_usingSymCons(false) { - if (options::sygusEvalUnfold()) - { - d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold(); - } + d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold(); } bool Cegis::initialize(Node conj, @@ -80,7 +77,7 @@ bool Cegis::processInitialize(Node conj, for (unsigned i = 0; i < csize; i++) { Trace("cegis") << "...register enumerator " << candidates[i]; - bool do_repair_const = false; + bool useSymCons = false; if (options::sygusRepairConst()) { TypeNode ctn = candidates[i].getType(); @@ -88,15 +85,15 @@ bool Cegis::processInitialize(Node conj, SygusTypeInfo& cti = d_tds->getTypeInfo(ctn); if (cti.hasSubtermSymbolicCons()) { - do_repair_const = true; - // remember that we are doing grammar-based repair - d_using_gr_repair = true; - Trace("cegis") << " (using repair)"; + useSymCons = true; + // remember that we are using symbolic constructors + d_usingSymCons = true; + Trace("cegis") << " (using symbolic constructors)"; } } Trace("cegis") << std::endl; d_tds->registerEnumerator( - candidates[i], candidates[i], d_parent, erole, do_repair_const); + candidates[i], candidates[i], d_parent, erole, useSymCons); } return true; } @@ -135,7 +132,10 @@ bool Cegis::addEvalLemmas(const std::vector& candidates, } NodeManager* nm = NodeManager::currentNM(); bool addedEvalLemmas = false; - if (options::sygusRefEval()) + // Refinement evaluation should not be done for grammars with symbolic + // constructors. + bool doRefEval = options::sygusRefEval() && !d_usingSymCons; + if (doRefEval) { Trace("cegqi-engine") << " *** Do refinement lemma evaluation" << (doGen ? " with conjecture-specific refinement" @@ -169,7 +169,8 @@ bool Cegis::addEvalLemmas(const std::vector& candidates, } } // we only do evaluation unfolding for passive enumerators - if (doGen && d_eval_unfold != nullptr) + bool doEvalUnfold = (doGen && options::sygusEvalUnfold()) || d_usingSymCons; + if (doEvalUnfold) { Trace("cegqi-engine") << " *** Do evaluation unfolding..." << std::endl; std::vector eager_terms, eager_vals, eager_exps; @@ -239,7 +240,7 @@ bool Cegis::constructCandidates(const std::vector& enums, } } // if we are using grammar-based repair - if (d_using_gr_repair) + if (d_usingSymCons && options::sygusRepairConst()) { SygusRepairConst* src = d_parent->getRepairConst(); Assert(src != nullptr); diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 08cf98c99..adaecc7f6 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -204,15 +204,15 @@ class Cegis : public SygusModule */ std::unordered_set d_cegis_sample_refine; - //---------------------------------for sygus repair - /** are we using grammar-based repair? + //---------------------------------for symbolic constructors + /** are we using symbolic constants? * * This flag is set ot true if at least one of the enumerators allocated * by this class has been configured to allow model values with symbolic * constructors, such as the "any constant" constructor. */ - bool d_using_gr_repair; - //---------------------------------end for sygus repair + bool d_usingSymCons; + //---------------------------------end for symbolic constructors }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 5286ab6f7..42ddbbb7d 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -14,7 +14,9 @@ #include "theory/quantifiers/sygus/sygus_eval_unfold.h" +#include "expr/sygus_datatype.h" #include "options/quantifiers_options.h" +#include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" using namespace std; @@ -101,6 +103,10 @@ void SygusEvalUnfold::registerModelValue(Node a, antec_exp.size() == 1 ? antec_exp[0] : nm->mkNode(AND, antec_exp); // Node antec = n.eqNode( vn ); TypeNode tn = n.getType(); + // Check if the sygus type has any symbolic constructors. This will + // impact how the unfolding is computed below. + SygusTypeInfo& sti = d_tds->getTypeInfo(tn); + bool hasSymCons = sti.hasSubtermSymbolicCons(); // n occurs as an evaluation head, thus it has sygus datatype type Assert(tn.isDatatype()); const Datatype& dt = static_cast(tn.toType()).getDatatype(); @@ -148,7 +154,7 @@ void SygusEvalUnfold::registerModelValue(Node a, do_unfold = true; } } - if (do_unfold) + if (do_unfold || hasSymCons) { // note that this is replicated for different values std::map vtm; @@ -158,7 +164,10 @@ void SygusEvalUnfold::registerModelValue(Node a, eval_children.end(), it->second[i].begin(), it->second[i].end()); Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children); eval_children.resize(1); - res = d_tds->unfold(eval_fun, vtm, exp); + // If we explicitly asked to unfold, we use single step, otherwise + // we use multi step. + res = unfold(eval_fun, vtm, exp, true, !do_unfold); + Trace("sygus-eval-unfold") << "Unfold returns " << res << std::endl; expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp); } else @@ -170,6 +179,8 @@ void SygusEvalUnfold::registerModelValue(Node a, eval_children[0] = vn; Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children); res = d_tds->evaluateWithUnfolding(eval_fun); + Trace("sygus-eval-unfold") + << "Evaluate with unfolding returns " << res << std::endl; esit.init(conj, n, res); eval_children.resize(1); eval_children[0] = n; @@ -193,6 +204,130 @@ void SygusEvalUnfold::registerModelValue(Node a, } } +Node SygusEvalUnfold::unfold(Node en, + std::map& vtm, + std::vector& exp, + bool track_exp, + bool doRec) +{ + if (en.getKind() != DT_SYGUS_EVAL) + { + Assert(en.isConst()); + return en; + } + Trace("sygus-eval-unfold-debug") + << "Unfold : " << en << ", track exp is " << track_exp << ", doRec is " + << doRec << std::endl; + Node ev = en[0]; + if (track_exp) + { + std::map::iterator itv = vtm.find(en[0]); + Assert(itv != vtm.end()); + if (itv != vtm.end()) + { + ev = itv->second; + } + Assert(en[0].getType() == ev.getType()); + Assert(ev.isConst()); + } + Trace("sygus-eval-unfold-debug") + << "Unfold model value is : " << ev << std::endl; + AlwaysAssert(ev.getKind() == APPLY_CONSTRUCTOR); + std::vector args; + for (unsigned i = 1, nchild = en.getNumChildren(); i < nchild; i++) + { + args.push_back(en[i]); + } + + TypeNode headType = en[0].getType(); + Type headTypeT = headType.toType(); + NodeManager* nm = NodeManager::currentNM(); + const Datatype& dt = headType.getDatatype(); + unsigned i = datatypes::utils::indexOf(ev.getOperator()); + if (track_exp) + { + // explanation + Node ee = + nm->mkNode(APPLY_TESTER, Node::fromExpr(dt[i].getTester()), en[0]); + if (std::find(exp.begin(), exp.end(), ee) == exp.end()) + { + exp.push_back(ee); + } + } + // if we are a symbolic constructor, unfolding returns the subterm itself + Node sop = Node::fromExpr(dt[i].getSygusOp()); + if (sop.getAttribute(SygusAnyConstAttribute())) + { + Trace("sygus-eval-unfold-debug") + << "...it is an any-constant constructor" << std::endl; + Assert(dt[i].getNumArgs() == 1); + // If the argument to evaluate is itself concrete, then we use its + // argument; otherwise we return its selector. + if (en[0].getKind() == APPLY_CONSTRUCTOR) + { + Trace("sygus-eval-unfold-debug") + << "...return (from constructor) " << en[0][0] << std::endl; + return en[0][0]; + } + else + { + Node ret = nm->mkNode( + APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headTypeT, 0), en[0]); + Trace("sygus-eval-unfold-debug") + << "...return (from constructor) " << ret << std::endl; + return ret; + } + } + + Assert(!dt.isParametric()); + std::map pre; + for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) + { + std::vector cc; + Node s; + // get the j^th subfield of en + if (en[0].getKind() == APPLY_CONSTRUCTOR) + { + // if it is a concrete constructor application, as an optimization, + // just return the argument + s = en[0][j]; + } + else + { + s = nm->mkNode( + APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headTypeT, j), en[0]); + } + cc.push_back(s); + if (track_exp) + { + // update vtm map + vtm[s] = ev[j]; + } + cc.insert(cc.end(), args.begin(), args.end()); + Node argj = nm->mkNode(DT_SYGUS_EVAL, cc); + if (doRec) + { + Trace("sygus-eval-unfold-debug") << "Recurse on " << s << std::endl; + // evaluate recursively + argj = unfold(argj, vtm, exp, track_exp, doRec); + } + pre[j] = argj; + } + Node ret = d_tds->mkGeneric(dt, i, pre); + // apply the appropriate substitution to ret + ret = datatypes::utils::applySygusArgs(dt, sop, ret, args); + // rewrite + ret = Rewriter::rewrite(ret); + return ret; +} + +Node SygusEvalUnfold::unfold(Node en) +{ + std::map vtm; + std::vector exp; + return unfold(en, vtm, exp, false, false); +} + } // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h index adc54c6a7..50b361fc4 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h @@ -83,6 +83,49 @@ class SygusEvalUnfold std::vector& exps, std::vector& terms, std::vector& vals); + /** unfold + * + * This method is called when a sygus term d (typically a variable for a SyGuS + * enumerator) has a model value specified by the map vtm. The argument en + * is an application of kind DT_SYGUS_EVAL, i.e. eval( d, c1, ..., cm ). + * Typically, d is a shared selector chain, although it may also be a + * non-constant application of a constructor. + * + * If doRec is false, this method returns the one-step unfolding of this + * evaluation function application. An example of a one step unfolding is: + * eval( C_+( d1, d2 ), t ) ---> +( eval( d1, t ), eval( d2, t ) ) + * + * This function does this unfolding for a (possibly symbolic) evaluation + * head, where the argument "variable to model" vtm stores the model value of + * variables from this head. This allows us to track an explanation of the + * unfolding in the vector exp when track_exp is true. + * + * For example, if vtm[d] = C_+( C_x(), C_0() ) and track_exp is true, then + * this method applied to eval( d, t ) will return + * +( eval( d.0, t ), eval( d.1, t ) ), and is-C_+( d ) is added to exp. + * + * If the argument doRec is true, we do a multi-step unfolding instead of + * a single-step unfolding. For example, if vtm[d] = C_+( C_x(), C_0() ), + * then this method applied to eval(d,5) will return 5+0 = 0. + * + * Furthermore, notice that any-constant constructors are *never* expanded to + * their concrete model values. This means that the multi-step unfolding when + * vtm[d] = C_+( C_x(), any_constant(n) ), then this method applied to + * eval(d,5) will return 5 + d.2.1, where the latter term is a shared selector + * chain. In other words, this unfolding elaborates the connection between + * the builtin integer field d.2.1 of d and the builtin interpretation of + * this sygus term, for the given argument. + */ + Node unfold(Node en, + std::map& vtm, + std::vector& exp, + bool track_exp = true, + bool doRec = false); + /** + * Same as above, but without explanation tracking. This is used for concrete + * evaluation heads + */ + Node unfold(Node en); private: /** sygus term database associated with this utility */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 3f09a4346..5d4aaf7ae 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -105,7 +105,8 @@ Node SygusUnifRl::purifyLemma(Node n, { TNode cand = n[0]; Node tmp = n.substitute(cand, it->second); - nv = d_tds->evaluateWithUnfolding(tmp); + // should be concrete, can just use the rewriter + nv = Rewriter::rewrite(tmp); Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << tmp << " is " << nv << "\n"; } diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index e74068ace..07997221f 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_unif_strat.h" #include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/quantifiers/sygus/sygus_eval_unfold.h" #include "theory/quantifiers/sygus/sygus_unif.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -258,7 +259,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) Node eut = nm->mkNode(DT_SYGUS_EVAL, echildren); Trace("sygus-unif-debug2") << " Test evaluation of " << eut << "..." << std::endl; - eut = d_qe->getTermDatabaseSygus()->unfold(eut); + eut = d_qe->getTermDatabaseSygus()->getEvalUnfold()->unfold(eut); Trace("sygus-unif-debug2") << " ...got " << eut; Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl; diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 9f6954416..cbe907d41 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -321,8 +321,6 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj) bool addedLemma = false; for (const Node& lem : cclems) { - Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem - << std::endl; if (d_quantEngine->addLemma(lem)) { ++(d_statistics.d_cegqi_lemmas_ce); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 79b4c9caa..679d47779 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -953,107 +953,6 @@ unsigned TermDbSygus::getAnchorDepth( Node n ) { } } -Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp, bool track_exp ) { - if (en.getKind() != DT_SYGUS_EVAL) - { - Assert(en.isConst()); - return en; - } - Trace("sygus-db-debug") << "Unfold : " << en << std::endl; - Node ev = en[0]; - if (track_exp) - { - std::map::iterator itv = vtm.find(en[0]); - Assert(itv != vtm.end()); - if (itv != vtm.end()) - { - ev = itv->second; - } - Assert(en[0].getType() == ev.getType()); - Assert(ev.isConst()); - } - Assert(ev.getKind() == kind::APPLY_CONSTRUCTOR); - std::vector args; - for (unsigned i = 1, nchild = en.getNumChildren(); i < nchild; i++) - { - args.push_back(en[i]); - } - - Type headType = en[0].getType().toType(); - NodeManager* nm = NodeManager::currentNM(); - const Datatype& dt = static_cast(headType).getDatatype(); - unsigned i = datatypes::utils::indexOf(ev.getOperator()); - if (track_exp) - { - // explanation - Node ee = nm->mkNode( - kind::APPLY_TESTER, Node::fromExpr(dt[i].getTester()), en[0]); - if (std::find(exp.begin(), exp.end(), ee) == exp.end()) - { - exp.push_back(ee); - } - } - // if we are a symbolic constructor, unfolding returns the subterm itself - Node sop = Node::fromExpr(dt[i].getSygusOp()); - if (sop.getAttribute(SygusAnyConstAttribute())) - { - Trace("sygus-db-debug") << "...it is an any-constant constructor" - << std::endl; - Assert(dt[i].getNumArgs() == 1); - if (en[0].getKind() == APPLY_CONSTRUCTOR) - { - return en[0][0]; - } - else - { - return nm->mkNode( - APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, 0), en[0]); - } - } - - Assert(!dt.isParametric()); - std::map pre; - for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) - { - std::vector cc; - Node s; - // get the j^th subfield of en - if (en[0].getKind() == kind::APPLY_CONSTRUCTOR) - { - // if it is a concrete constructor application, as an optimization, - // just return the argument - s = en[0][j]; - } - else - { - s = nm->mkNode(kind::APPLY_SELECTOR_TOTAL, - dt[i].getSelectorInternal(headType, j), - en[0]); - } - cc.push_back(s); - if (track_exp) - { - // update vtm map - vtm[s] = ev[j]; - } - cc.insert(cc.end(), args.begin(), args.end()); - pre[j] = nm->mkNode(DT_SYGUS_EVAL, cc); - } - Node ret = mkGeneric(dt, i, pre); - // apply the appropriate substitution to ret - ret = datatypes::utils::applySygusArgs(dt, sop, ret, args); - // rewrite - ret = Rewriter::rewrite(ret); - return ret; -} - -Node TermDbSygus::unfold(Node en) -{ - std::map vtm; - std::vector exp; - return unfold(en, vtm, exp, false); -} - Node TermDbSygus::evaluateBuiltin(TypeNode tn, Node bn, std::vector& args, @@ -1105,6 +1004,8 @@ Node TermDbSygus::evaluateWithUnfolding( Trace("dt-eval-unfold-debug") << "Optimize: evaluate constant head " << ret << std::endl; // can just do direct evaluation here + // notice we prefer this code to the rewriter since it may use + // the evaluator std::vector args; bool success = true; for (unsigned i = 1, nchild = ret.getNumChildren(); i < nchild; i++) @@ -1127,7 +1028,7 @@ Node TermDbSygus::evaluateWithUnfolding( return rete; } } - ret = unfold( ret ); + ret = d_eval_unfold->unfold(ret); } if( ret.getNumChildren()>0 ){ std::vector< Node > children; @@ -1136,7 +1037,7 @@ Node TermDbSygus::evaluateWithUnfolding( } bool childChanged = false; for( unsigned i=0; i visited; - return evaluateWithUnfolding( n, visited ); + return evaluateWithUnfolding(n, visited); } bool TermDbSygus::isEvaluationPoint(Node n) const diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 0ec883537..76b5039f6 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -453,31 +453,6 @@ class TermDbSygus { static Node getAnchor( Node n ); static unsigned getAnchorDepth( Node n ); - public: - /** unfold - * - * This method returns the one-step unfolding of an evaluation function - * application. An example of a one step unfolding is: - * eval( C_+( d1, d2 ), t ) ---> +( eval( d1, t ), eval( d2, t ) ) - * - * This function does this unfolding for a (possibly symbolic) evaluation - * head, where the argument "variable to model" vtm stores the model value of - * variables from this head. This allows us to track an explanation of the - * unfolding in the vector exp when track_exp is true. - * - * For example, if vtm[d] = C_+( C_x(), C_0() ) and track_exp is true, then - * this method applied to eval( d, t ) will return - * +( eval( d.0, t ), eval( d.1, t ) ), and is-C_+( d ) is added to exp. - */ - Node unfold(Node en, - std::map& vtm, - std::vector& exp, - bool track_exp = true); - /** - * Same as above, but without explanation tracking. This is used for concrete - * evaluation heads - */ - Node unfold(Node en); }; }/* CVC4::theory::quantifiers namespace */ -- 2.30.2