diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-03 15:34:17 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-03 15:34:17 -0500 |
commit | 053ee7b8058eccb84b909920ff92975faeda996c (patch) | |
tree | f2374e80abd943bb1188223e18254cf04c0c21de /src/theory | |
parent | b249f10578a078e032ed21bc7a3812b70d200c4d (diff) |
Eliminate option for sygus UF evaluation functions (#2262)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.cpp | 42 | ||||
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_eval_unfold.cpp | 14 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_rl.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_strat.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 10 |
9 files changed, 19 insertions, 68 deletions
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<Node>& 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<DatatypeType>(children[0].getType().toType()).getDatatype(); - Assert(dt.isSygus()); - std::vector<Node> 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<DatatypeType>(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<Node>& children); - /** make sygus evaluation function application */ - static Node mkSygusEvalApp(const std::vector<Node>& 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<Node, Node> vtm; std::vector<Node> 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<TNode, Node, TNodeHashFunction> visited; std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; std::stack<TNode> 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<Node>& 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; } |