From cee1b99e1ad104c9790e63f3328837a75c599c8e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Feb 2022 10:37:03 -0600 Subject: [PATCH] Remove more static calls to rewrite (#8025) --- src/preprocessing/assertion_pipeline.cpp | 10 +++++----- src/preprocessing/assertion_pipeline.h | 5 +++-- src/smt/assertions.cpp | 2 +- src/theory/quantifiers/sygus/sygus_unif_rl.cpp | 7 ++++--- src/theory/strings/core_solver.cpp | 5 ++++- src/theory/strings/normal_form.cpp | 12 +++--------- src/theory/strings/theory_strings.cpp | 2 +- src/theory/uf/function_const.cpp | 3 --- test/unit/preprocessing/pass_bv_gauss_white.cpp | 6 +++--- 9 files changed, 24 insertions(+), 28 deletions(-) diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index 778931f70..5c43a0168 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -21,13 +21,13 @@ #include "proof/lazy_proof.h" #include "smt/preprocess_proof_generator.h" #include "theory/builtin/proof_checker.h" -#include "theory/rewriter.h" namespace cvc5 { namespace preprocessing { -AssertionPipeline::AssertionPipeline() - : d_realAssertionsEnd(0), +AssertionPipeline::AssertionPipeline(Env& env) + : EnvObj(env), + d_realAssertionsEnd(0), d_storeSubstsInAsserts(false), d_substsIndex(0), d_assumptionsStart(0), @@ -147,7 +147,7 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg) { NodeManager* nm = NodeManager::currentNM(); Node newConj = nm->mkNode(kind::AND, d_nodes[i], n); - Node newConjr = theory::Rewriter::rewrite(newConj); + Node newConjr = rewrite(newConj); Trace("assert-pipeline") << "Assertions: conjoin " << n << " to " << d_nodes[i] << std::endl; Trace("assert-pipeline-debug") << "conjoin " << n << " to " << d_nodes[i] @@ -200,7 +200,7 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg) } } d_nodes[i] = newConjr; - Assert(theory::Rewriter::rewrite(newConjr) == newConjr); + Assert(rewrite(newConjr) == newConjr); } } // namespace preprocessing diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index 5c75fba2b..6c220b756 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -23,6 +23,7 @@ #include "expr/node.h" #include "proof/trust_node.h" +#include "smt/env_obj.h" namespace cvc5 { @@ -40,10 +41,10 @@ using IteSkolemMap = std::unordered_map; * passes. It is assumed that all assertions after d_realAssertionsEnd were * generated by ITE removal. Hence, d_iteSkolemMap maps into only these. */ -class AssertionPipeline +class AssertionPipeline : protected EnvObj { public: - AssertionPipeline(); + AssertionPipeline(Env& env); size_t size() const { return d_nodes.size(); } diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 0191bcb82..136cdaf8c 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -42,7 +42,7 @@ Assertions::Assertions(Env& env, AbstractValues& absv) d_assertionListDefs(userContext()), d_globalDefineFunLemmasIndex(userContext(), 0), d_globalNegation(false), - d_assertions() + d_assertions(env) { } diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 51804f0ce..687c69f8f 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -1176,8 +1176,9 @@ Node SygusUnifRl::DecisionTreeInfo::PointSeparator::computeCond(Node cond, { return it->second; } + TermDbSygus* tds = d_dt->d_unif->d_tds; TypeNode tn = cond.getType(); - Node builtin_cond = d_dt->d_unif->d_tds->sygusToBuiltin(cond, tn); + Node builtin_cond = tds->sygusToBuiltin(cond, tn); // Retrieve evaluation point Assert(d_dt->d_unif->d_hd_to_pt.find(hd) != d_dt->d_unif->d_hd_to_pt.end()); std::vector pt = d_dt->d_unif->d_hd_to_pt[hd]; @@ -1192,7 +1193,7 @@ Node SygusUnifRl::DecisionTreeInfo::PointSeparator::computeCond(Node cond, } Trace("sygus-unif-rl-sep") << ")\n"; } - Node res = d_dt->d_unif->d_tds->evaluateBuiltin(tn, builtin_cond, pt); + Node res = tds->evaluateBuiltin(tn, builtin_cond, pt); Trace("sygus-unif-rl-sep") << "...got res = " << res << "\n"; // If condition is templated, recompute result accordingly Node templ = d_dt->d_template.first; @@ -1200,7 +1201,7 @@ Node SygusUnifRl::DecisionTreeInfo::PointSeparator::computeCond(Node cond, if (!templ.isNull()) { res = templ.substitute(templ_var, res); - res = Rewriter::rewrite(res); + res = tds->rewriteNode(res); Trace("sygus-unif-rl-sep") << "...after template res = " << res << std::endl; } diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 96cbf8848..ee54b0fce 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -1554,7 +1554,10 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, size_t cIndex = index; Node stra = nfc.collectConstantStringAt(cIndex); Assert(!stra.isNull()); - Node strb = nextConstStr; + stra = rewrite(stra); + Assert(stra.isConst()); + Node strb = rewrite(nextConstStr); + Assert(strb.isConst()); // Since `nc` is non-empty, we use the non-empty overlap size_t p = getSufficientNonEmptyOverlap(stra, strb, isRev); diff --git a/src/theory/strings/normal_form.cpp b/src/theory/strings/normal_form.cpp index 7a8df9f42..b2bc8ac5c 100644 --- a/src/theory/strings/normal_form.cpp +++ b/src/theory/strings/normal_form.cpp @@ -52,8 +52,7 @@ void NormalForm::reverse() void NormalForm::splitConstant(unsigned index, Node c1, Node c2) { - Assert(Rewriter::rewrite(NodeManager::currentNM()->mkNode( - STRING_CONCAT, d_isRev ? c2 : c1, d_isRev ? c1 : c2)) + Assert(Word::mkWordFlatten({d_isRev ? c2 : c1, d_isRev ? c1 : c2}) == d_nf[index]); d_nf.insert(d_nf.begin() + index + 1, c2); d_nf[index] = c1; @@ -152,14 +151,9 @@ Node NormalForm::collectConstantStringAt(size_t& index) { std::reverse(c.begin(), c.end()); } - Node cc = Rewriter::rewrite(utils::mkConcat(c, c[0].getType())); - Assert(cc.isConst()); - return cc; - } - else - { - return Node::null(); + return utils::mkConcat(c, c[0].getType()); } + return Node::null(); } void NormalForm::getExplanationForPrefixEq(NormalForm& nfi, diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index fdc743915..2f8b3b8ce 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -433,7 +433,7 @@ bool TheoryStrings::collectModelInfoType( argVal = nfe.d_nf[0][0]; } Assert(!argVal.isNull()) << "No value for " << nfe.d_nf[0][0]; - assignedValue = Rewriter::rewrite(nm->mkNode(SEQ_UNIT, argVal)); + assignedValue = rewrite(nm->mkNode(SEQ_UNIT, argVal)); Trace("strings-model") << "-> assign via seq.unit: " << assignedValue << std::endl; } diff --git a/src/theory/uf/function_const.cpp b/src/theory/uf/function_const.cpp index 181cb20ca..85fec7cb2 100644 --- a/src/theory/uf/function_const.cpp +++ b/src/theory/uf/function_const.cpp @@ -173,9 +173,6 @@ Node FunctionConst::getArrayRepresentationForLambdaRec(TNode n, { Trace("builtin-rewrite-debug2") << " process base : " << curr << std::endl; - // curr = Rewriter::rewrite(curr); - // Trace("builtin-rewrite-debug2") - // << " rewriten base : " << curr << std::endl; // Complex Boolean return cases, in which // (1) lambda x. (= x v1) v ... becomes // lambda x. (ite (= x v1) true [...]) diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp index eb462006c..1a36d682b 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.cpp +++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp @@ -2409,7 +2409,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique1) Node a = d_nodeManager->mkNode( kind::AND, d_nodeManager->mkNode(kind::AND, eq1, eq2), eq3); - AssertionPipeline apipe; + AssertionPipeline apipe(d_slvEngine->getEnv()); apipe.push_back(a); passes::BVGauss bgauss(d_preprocContext.get(), "bv-gauss-unit"); std::unordered_map res; @@ -2496,7 +2496,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique2) Node a = d_nodeManager->mkNode( kind::AND, d_nodeManager->mkNode(kind::AND, eq1, eq2), eq3); - AssertionPipeline apipe; + AssertionPipeline apipe(d_slvEngine->getEnv()); apipe.push_back(a); apipe.push_back(eq4); apipe.push_back(eq5); @@ -2548,7 +2548,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial) d_p), d_nine); - AssertionPipeline apipe; + AssertionPipeline apipe(d_slvEngine->getEnv()); apipe.push_back(eq1); apipe.push_back(eq2); passes::BVGauss bgauss(d_preprocContext.get(), "bv-gauss-unit"); -- 2.30.2