From 704fd545440023a0deaa328a9de9c11ac5fe963c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 8 Sep 2021 20:16:11 -0500 Subject: Remove deprecated SyGuS method evaluateWithUnfolding (#7155) This was a predecessor to the evaluator and TermDbSygus::rewriteNode that is no longer necessary. This refactors the code so that evaluateWithUnfolding is replaced by rewriteNode as necessary throughout the SyGuS solver. Note that in a few places, the extended rewriter was being used where TermDbSygus::rewriteNode (which also evaluates recursive function definitions) should have been used. --- src/theory/quantifiers/sygus/cegis.cpp | 4 +- src/theory/quantifiers/sygus/sygus_eval_unfold.cpp | 9 +--- src/theory/quantifiers/sygus/sygus_eval_unfold.h | 5 -- src/theory/quantifiers/sygus/sygus_invariance.cpp | 7 +-- src/theory/quantifiers/sygus/sygus_invariance.h | 5 -- .../quantifiers/sygus/sygus_repair_const.cpp | 2 +- src/theory/quantifiers/sygus/sygus_unif_strat.cpp | 2 +- .../quantifiers/sygus/term_database_sygus.cpp | 63 ++++------------------ src/theory/quantifiers/sygus/term_database_sygus.h | 15 ------ 9 files changed, 15 insertions(+), 97 deletions(-) diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 8d1bfd9b6..708bffe80 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -345,7 +345,7 @@ void Cegis::addRefinementLemma(Node lem) d_rl_vals.end()); } // rewrite with extended rewriter - slem = extendedRewrite(slem); + slem = d_tds->rewriteNode(slem); // collect all variables in slem expr::getSymbols(slem, d_refinement_lemma_vars); std::vector waiting; @@ -509,7 +509,7 @@ bool Cegis::getRefinementEvalLemmas(const std::vector& vs, 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); + Node lemcsu = d_tds->rewriteNode(lemcs); Trace("sygus-cref-eval2") << "...after unfolding is : " << lemcsu << std::endl; if (lemcsu.isConst() && !lemcsu.getConst()) diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 0ef1e7f17..7af1ef45b 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -180,7 +180,7 @@ void SygusEvalUnfold::registerModelValue(Node a, Node conj = nm->mkNode(DT_SYGUS_EVAL, eval_children); eval_children[0] = vn; Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children); - res = d_tds->evaluateWithUnfolding(eval_fun); + res = d_tds->rewriteNode(eval_fun); Trace("sygus-eval-unfold") << "Evaluate with unfolding returns " << res << std::endl; esit.init(conj, n, res); @@ -324,13 +324,6 @@ Node SygusEvalUnfold::unfold(Node en, 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 cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h index bb181996a..c30d4dae7 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h @@ -122,11 +122,6 @@ class SygusEvalUnfold 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_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index 29557fe5c..8048330e4 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -49,11 +49,6 @@ void EvalSygusInvarianceTest::init(Node conj, Node var, Node res) d_result = res; } -Node EvalSygusInvarianceTest::doEvaluateWithUnfolding(TermDbSygus* tds, Node n) -{ - return tds->evaluateWithUnfolding(n, d_visited); -} - bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) { TNode tnvn = nvn; @@ -61,7 +56,7 @@ bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) for (const Node& c : d_terms) { Node conj_subs = c.substitute(d_var, tnvn, cache); - Node conj_subs_unfold = doEvaluateWithUnfolding(tds, conj_subs); + Node conj_subs_unfold = tds->rewriteNode(conj_subs); Trace("sygus-cref-eval2-debug") << " ...check unfolding : " << conj_subs_unfold << std::endl; Trace("sygus-cref-eval2-debug") diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index ca5f057b1..afb59bf73 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -111,9 +111,6 @@ class EvalSygusInvarianceTest : public SygusInvarianceTest */ void init(Node conj, Node var, Node res); - /** do evaluate with unfolding, using the cache of this class */ - Node doEvaluateWithUnfolding(TermDbSygus* tds, Node n); - protected: /** does d_terms{ d_var -> nvn } still rewrite to d_result? */ bool invariant(TermDbSygus* tds, Node nvn, Node x) override; @@ -137,8 +134,6 @@ class EvalSygusInvarianceTest : public SygusInvarianceTest * disjunctively, i.e. if one child test succeeds, the overall test succeeds. */ bool d_is_conjunctive; - /** cache of n -> the simplified form of eval( n ) */ - std::unordered_map d_visited; }; /** EquivSygusInvarianceTest diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index bcd826799..b7611784d 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -444,7 +444,7 @@ Node SygusRepairConst::getFoQuery(Node body, Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl; Trace("sygus-repair-const") << " Unfold the specification..." << std::endl; - body = d_tds->evaluateWithUnfolding(body); + body = d_tds->rewriteNode(body); Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl; Trace("sygus-repair-const") << " Introduce first-order vars..." << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 10db1ef9e..6b023075b 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -264,7 +264,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_tds->getEvalUnfold()->unfold(eut); + eut = d_tds->rewriteNode(eut); Trace("sygus-unif-debug2") << " ...got " << eut; Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl; diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 9c9a90255..035db433e 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -739,7 +739,15 @@ SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn) Node TermDbSygus::rewriteNode(Node n) const { - Node res = Rewriter::rewrite(n); + Node res; + if (options().quantifiers.sygusExtRew) + { + res = extendedRewrite(n); + } + else + { + res = rewrite(n); + } if (res.isConst()) { // constant, we are done @@ -1001,59 +1009,6 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn, return rewriteNode(res); } -Node TermDbSygus::evaluateWithUnfolding(Node n, - std::unordered_map& visited) -{ - std::unordered_map::iterator it = visited.find(n); - if( it==visited.end() ){ - Node ret = n; - while (ret.getKind() == DT_SYGUS_EVAL - && ret[0].getKind() == APPLY_CONSTRUCTOR) - { - if (ret == n && ret[0].isConst()) - { - // use rewriting, possibly involving recursive functions - ret = rewriteNode(ret); - } - else - { - ret = d_eval_unfold->unfold(ret); - } - } - if( ret.getNumChildren()>0 ){ - std::vector< Node > children; - if( ret.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( ret.getOperator() ); - } - bool childChanged = false; - for( unsigned i=0; imkNode( ret.getKind(), children ); - } - if (options::sygusExtRew()) - { - ret = extendedRewrite(ret); - } - // use rewriting, possibly involving recursive functions - ret = rewriteNode(ret); - } - visited[n] = ret; - return ret; - }else{ - return it->second; - } -} - -Node TermDbSygus::evaluateWithUnfolding(Node n) -{ - std::unordered_map visited; - return evaluateWithUnfolding(n, visited); -} - bool TermDbSygus::isEvaluationPoint(Node n) const { if (n.getKind() != DT_SYGUS_EVAL) diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index a44ebd297..7b05c70e4 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -271,21 +271,6 @@ class TermDbSygus : protected EnvObj Node bn, const std::vector& args, bool tryEval = true); - /** evaluate with unfolding - * - * n is any term that may involve sygus evaluation functions. This function - * returns the result of unfolding the evaluation functions within n and - * rewriting the result. For example, if eval_A is the evaluation function - * for the datatype: - * A -> C_0 | C_1 | C_x | C_+( C_A, C_A ) - * corresponding to grammar: - * A -> 0 | 1 | x | A + A - * then calling this function on eval( C_+( x, 1 ), 4 ) = y returns 5 = y. - * The node returned by this function is in (extended) rewritten form. - */ - Node evaluateWithUnfolding(Node n); - /** 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 -- cgit v1.2.3