From 053ee7b8058eccb84b909920ff92975faeda996c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 3 Aug 2018 15:34:17 -0500 Subject: [PATCH] Eliminate option for sygus UF evaluation functions (#2262) --- src/expr/datatype.cpp | 21 ---------- src/expr/datatype.h | 13 ------ src/options/datatypes_options.toml | 9 ---- src/theory/datatypes/datatypes_rewriter.cpp | 42 ------------------- src/theory/datatypes/datatypes_rewriter.h | 4 -- .../quantifiers/sygus/sygus_eval_unfold.cpp | 14 +++---- .../quantifiers/sygus/sygus_grammar_cons.cpp | 3 +- src/theory/quantifiers/sygus/sygus_pbe.cpp | 4 +- .../quantifiers/sygus/sygus_repair_const.cpp | 2 +- .../quantifiers/sygus/sygus_unif_rl.cpp | 4 +- .../quantifiers/sygus/sygus_unif_strat.cpp | 4 +- .../quantifiers/sygus/term_database_sygus.cpp | 10 ++--- 12 files changed, 19 insertions(+), 111 deletions(-) diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 8747c530e..ae61d5f33 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -154,23 +154,6 @@ void Datatype::resolve(ExprManager* em, } d_record = new Record(fields); } - - //make the sygus evaluation function - if( isSygus() ){ - PrettyCheckArgument(d_params.empty(), this, "sygus types cannot be parametric"); - NodeManager* nm = NodeManager::fromExprManager(em); - std::string name = "eval_" + getName(); - std::vector evalType; - evalType.push_back(TypeNode::fromType(d_self)); - if( !d_sygus_bvl.isNull() ){ - for(size_t j = 0; j < d_sygus_bvl.getNumChildren(); ++j) { - evalType.push_back(TypeNode::fromType(d_sygus_bvl[j].getType())); - } - } - evalType.push_back(TypeNode::fromType(d_sygus_type)); - TypeNode eval_func_type = nm->mkFunctionType(evalType); - d_sygus_eval = nm->mkSkolem(name, eval_func_type, "sygus evaluation function").toExpr(); - } } void Datatype::addConstructor(const DatatypeConstructor& c) { @@ -683,10 +666,6 @@ bool Datatype::getSygusAllowAll() const { return d_sygus_allow_all; } -Expr Datatype::getSygusEvaluationFunc() const { - return d_sygus_eval; -} - bool Datatype::involvesExternalType() const{ return d_involvesExt; } diff --git a/src/expr/datatype.h b/src/expr/datatype.h index c2cf80158..a3519f405 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -920,17 +920,6 @@ public: * to setSygus). */ bool getSygusAllowAll() const; - /** get sygus evaluation function - * - * This gets the evaluation function for this datatype - * for the deep embedding. This is a function of type: - * D x T1 x ... x Tn -> T - * where: - * D is the datatype type for this datatype, - * T1...Tn are the types of the variables in getSygusVarList(), - * T is getSygusType(). - */ - Expr getSygusEvaluationFunc() const; /** involves external type * Get whether this datatype has a subfield @@ -979,8 +968,6 @@ public: bool d_sygus_allow_const; /** whether all terms are allowed as solutions */ bool d_sygus_allow_all; - /** the evaluation function for this sygus datatype */ - Expr d_sygus_eval; /** the cardinality of this datatype * "mutable" because computing the cardinality can be expensive, diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml index 0c521bb93..2394a1b5d 100644 --- a/src/options/datatypes_options.toml +++ b/src/options/datatypes_options.toml @@ -184,12 +184,3 @@ header = "options/datatypes_options.h" default = "-1" read_only = true help = "tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)" - -[[option]] - name = "sygusEvalBuiltin" - category = "regular" - long = "sygus-eval-builtin" - type = "bool" - default = "true" - read_only = true - help = "use builtin kind for evaluation functions in sygus" diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 443cd0bd0..8366fe4e1 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -256,48 +256,6 @@ Node DatatypesRewriter::mkSygusTerm(const Datatype& dt, Trace("dt-sygus-util") << "...return " << ret << std::endl; return ret; } -Node DatatypesRewriter::mkSygusEvalApp(const std::vector& children) -{ - if (options::sygusEvalBuiltin()) - { - return NodeManager::currentNM()->mkNode(DT_SYGUS_EVAL, children); - } - // otherwise, using APPLY_UF - Assert(!children.empty()); - Assert(children[0].getType().isDatatype()); - const Datatype& dt = - static_cast(children[0].getType().toType()).getDatatype(); - Assert(dt.isSygus()); - std::vector schildren; - schildren.push_back(Node::fromExpr(dt.getSygusEvaluationFunc())); - schildren.insert(schildren.end(), children.begin(), children.end()); - return NodeManager::currentNM()->mkNode(APPLY_UF, schildren); -} - -bool DatatypesRewriter::isSygusEvalApp(Node n) -{ - if (options::sygusEvalBuiltin()) - { - return n.getKind() == DT_SYGUS_EVAL; - } - // otherwise, using APPLY_UF - if (n.getKind() != APPLY_UF || n.getNumChildren() == 0) - { - 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(); -} RewriteResponse DatatypesRewriter::preRewrite(TNode in) { diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index b99c5fb53..7d91544e1 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -130,10 +130,6 @@ public: static Node mkSygusTerm(const Datatype& dt, unsigned i, const std::vector& children); - /** make sygus evaluation function application */ - static Node mkSygusEvalApp(const std::vector& children); - /** is sygus evaluation function */ - static bool isSygusEvalApp(Node n); /** * Get the builtin sygus operator for constructor term n of sygus datatype * type. For example, if n is the term C_+( d1, d2 ) where C_+ is a sygus diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 36cbb89fe..ac7467c00 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -32,7 +32,7 @@ void SygusEvalUnfold::registerEvalTerm(Node n) { Assert(options::sygusEvalUnfold()); // is this a sygus evaluation function application? - if (!datatypes::DatatypesRewriter::isSygusEvalApp(n)) + if (n.getKind() != DT_SYGUS_EVAL) { return; } @@ -140,15 +140,13 @@ void SygusEvalUnfold::registerModelValue(Node a, } if (do_unfold) { - // TODO (#1949) : this is replicated for different values, possibly - // do better caching + // note that this is replicated for different values std::map vtm; std::vector exp; vtm[n] = vn; eval_children.insert( eval_children.end(), it->second[i].begin(), it->second[i].end()); - Node eval_fun = - datatypes::DatatypesRewriter::mkSygusEvalApp(eval_children); + Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children); eval_children.resize(1); res = d_tds->unfold(eval_fun, vtm, exp); expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp); @@ -158,11 +156,9 @@ void SygusEvalUnfold::registerModelValue(Node a, EvalSygusInvarianceTest esit; eval_children.insert( eval_children.end(), it->second[i].begin(), it->second[i].end()); - Node conj = - datatypes::DatatypesRewriter::mkSygusEvalApp(eval_children); + Node conj = nm->mkNode(DT_SYGUS_EVAL, eval_children); eval_children[0] = vn; - Node eval_fun = - datatypes::DatatypesRewriter::mkSygusEvalApp(eval_children); + Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children); res = d_tds->evaluateWithUnfolding(eval_fun); esit.init(conj, n, res); eval_children.resize(1); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index efffa046f..deea1c261 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -268,6 +268,7 @@ Node CegGrammarConstructor::process(Node q, } Node CegGrammarConstructor::convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars ){ + NodeManager* nm = NodeManager::currentNM(); std::unordered_map visited; std::unordered_map::iterator it; std::stack visit; @@ -323,7 +324,7 @@ Node CegGrammarConstructor::convertToEmbedding( Node n, std::map< Node, Node >& if (makeEvalFun) { // will make into an application of an evaluation function - ret = datatypes::DatatypesRewriter::mkSygusEvalApp(children); + ret = nm->mkNode(DT_SYGUS_EVAL, children); } else if (childChanged) { diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 56d2cf2b5..6a82b9dad 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -48,7 +48,7 @@ void CegConjecturePbe::collectExamples( Node n, std::map< Node, bool >& visited, Node neval; Node n_output; bool neval_is_evalapp = false; - if (datatypes::DatatypesRewriter::isSygusEvalApp(n)) + if (n.getKind() == DT_SYGUS_EVAL) { neval = n; if( hasPol ){ @@ -57,7 +57,7 @@ void CegConjecturePbe::collectExamples( Node n, std::map< Node, bool >& visited, neval_is_evalapp = true; }else if( n.getKind()==EQUAL && hasPol && !pol ){ for( unsigned r=0; r<2; r++ ){ - if (datatypes::DatatypesRewriter::isSygusEvalApp(n[r])) + if (n[r].getKind() == DT_SYGUS_EVAL) { neval = n[r]; if( n[1-r].isConst() ){ diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 71449029b..514f42fb1 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -463,7 +463,7 @@ Node SygusRepairConst::getFoQuery(const std::vector& candidates, if (it == visited.end()) { visited[cur] = Node::null(); - if (datatypes::DatatypesRewriter::isSygusEvalApp(cur)) + if (cur.getKind() == DT_SYGUS_EVAL) { Node v = cur[0]; if (std::find(sk_vars.begin(), sk_vars.end(), v) != sk_vars.end()) diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 759ee6ffa..183f40b66 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -81,7 +81,7 @@ Node SygusUnifRl::purifyLemma(Node n, // We retrive model value now because purified node may not have a value Node nv = n; // Whether application of a function-to-synthesize - bool fapp = datatypes::DatatypesRewriter::isSygusEvalApp(n); + bool fapp = (n.getKind() == DT_SYGUS_EVAL); bool u_fapp = false; bool nu_fapp = false; if (fapp) @@ -194,7 +194,7 @@ Node SygusUnifRl::purifyLemma(Node n, children[0] = new_f; Trace("sygus-unif-rl-purify-debug") << "Make sygus eval app " << children << std::endl; - np = datatypes::DatatypesRewriter::mkSygusEvalApp(children); + np = nm->mkNode(DT_SYGUS_EVAL, children); d_app_to_purified[nb] = np; } else diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 6e01ff084..3cbac1eaa 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -254,7 +254,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) { echildren.push_back(sbv); } - Node eut = datatypes::DatatypesRewriter::mkSygusEvalApp(echildren); + Node eut = nm->mkNode(DT_SYGUS_EVAL, echildren); Trace("sygus-unif-debug2") << " Test evaluation of " << eut << "..." << std::endl; eut = d_qe->getTermDatabaseSygus()->unfold(eut); @@ -296,7 +296,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) echildren[0] = sks[k]; Trace("sygus-unif-debug2") << "...set eval dt to " << sks[k] << std::endl; - Node esk = datatypes::DatatypesRewriter::mkSygusEvalApp(echildren); + Node esk = nm->mkNode(DT_SYGUS_EVAL, echildren); vs.push_back(esk); Node tvar = nm->mkSkolem("templ", esk.getType()); templ_var_index[tvar] = k; diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 99ab54a2c..54e731694 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -1557,7 +1557,7 @@ unsigned TermDbSygus::getAnchorDepth( Node n ) { } Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp, bool track_exp ) { - if (!datatypes::DatatypesRewriter::isSygusEvalApp(en)) + if (en.getKind() != DT_SYGUS_EVAL) { Assert(en.isConst()); return en; @@ -1640,7 +1640,7 @@ Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Nod vtm[s] = ev[j]; } cc.insert(cc.end(), args.begin(), args.end()); - pre[j] = datatypes::DatatypesRewriter::mkSygusEvalApp(cc); + pre[j] = nm->mkNode(DT_SYGUS_EVAL, cc); } Node ret = mkGeneric(dt, i, pre); // if it is a variable, apply the substitution @@ -1667,7 +1667,7 @@ Node TermDbSygus::getEagerUnfold( Node n, std::map< Node, Node >& visited ) { if( itv==visited.end() ){ Trace("cegqi-eager-debug") << "getEagerUnfold " << n << std::endl; Node ret; - if (datatypes::DatatypesRewriter::isSygusEvalApp(n)) + if (n.getKind() == DT_SYGUS_EVAL) { TypeNode tn = n[0].getType(); Trace("cegqi-eager-debug") << "check " << n[0].getType() << std::endl; @@ -1771,7 +1771,7 @@ Node TermDbSygus::evaluateWithUnfolding( visited.find(n); if( it==visited.end() ){ Node ret = n; - while (datatypes::DatatypesRewriter::isSygusEvalApp(ret) + while (ret.getKind() == DT_SYGUS_EVAL && ret[0].getKind() == APPLY_CONSTRUCTOR) { ret = unfold( ret ); @@ -1806,7 +1806,7 @@ Node TermDbSygus::evaluateWithUnfolding( Node n ) { bool TermDbSygus::isEvaluationPoint(Node n) const { - if (!datatypes::DatatypesRewriter::isSygusEvalApp(n)) + if (n.getKind() != DT_SYGUS_EVAL) { return false; } -- 2.30.2