From 52bdeff9adb7ebaaf54dec3232f7b896f86e9834 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 27 May 2022 10:53:07 -0500 Subject: [PATCH] Make Rewriter::rewrite non-static (#8828) This furthermore eliminates smt::currentSolverEngine. --- src/preprocessing/preprocessing_pass.cpp | 2 +- src/smt/listeners.cpp | 1 - src/smt/solver_engine_scope.cpp | 10 +----- src/smt/solver_engine_scope.h | 3 -- src/theory/evaluator.cpp | 4 +-- src/theory/rewriter.cpp | 11 ++----- src/theory/rewriter.h | 11 +------ .../preprocessing/pass_bv_gauss_white.cpp | 28 +++++++++------- test/unit/theory/regexp_operation_black.cpp | 19 ++++++----- test/unit/theory/strings_rewriter_white.cpp | 5 +-- test/unit/theory/theory_arith_white.cpp | 27 ++++++++------- .../theory/theory_bags_rewriter_white.cpp | 8 +++-- test/unit/theory/theory_black.cpp | 33 ++++++++++--------- .../theory/theory_bv_int_blaster_white.cpp | 25 +++----------- test/unit/theory/theory_bv_rewriter_white.cpp | 18 ++++++---- test/unit/theory/theory_engine_white.cpp | 6 ++-- .../theory/theory_sets_rewriter_white.cpp | 5 +-- .../theory_sets_type_enumerator_white.cpp | 3 +- 18 files changed, 100 insertions(+), 119 deletions(-) diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp index 15e93c927..4bc73514f 100644 --- a/src/preprocessing/preprocessing_pass.cpp +++ b/src/preprocessing/preprocessing_pass.cpp @@ -45,7 +45,7 @@ PreprocessingPass::PreprocessingPass(PreprocessingPassContext* preprocContext, { } -PreprocessingPass::~PreprocessingPass() { Assert(smt::solverEngineInScope()); } +PreprocessingPass::~PreprocessingPass() {} } // namespace preprocessing } // namespace cvc5::internal diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index 4cafc74c8..ce769c7ad 100644 --- a/src/smt/listeners.cpp +++ b/src/smt/listeners.cpp @@ -26,7 +26,6 @@ ResourceOutListener::ResourceOutListener(SolverEngine& slv) : d_slv(slv) {} void ResourceOutListener::notify() { SolverEngineScope scope(&d_slv); - Assert(smt::solverEngineInScope()); d_slv.interrupt(); } diff --git a/src/smt/solver_engine_scope.cpp b/src/smt/solver_engine_scope.cpp index 3d11c13be..967a40728 100644 --- a/src/smt/solver_engine_scope.cpp +++ b/src/smt/solver_engine_scope.cpp @@ -28,14 +28,6 @@ namespace smt { thread_local SolverEngine* s_slvEngine_current = nullptr; -SolverEngine* currentSolverEngine() -{ - Assert(s_slvEngine_current != nullptr); - return s_slvEngine_current; -} - -bool solverEngineInScope() { return s_slvEngine_current != nullptr; } - ResourceManager* currentResourceManager() { return s_slvEngine_current->getResourceManager(); @@ -60,7 +52,7 @@ SolverEngineScope::~SolverEngineScope() StatisticsRegistry& SolverEngineScope::currentStatisticsRegistry() { - Assert(solverEngineInScope()); + Assert(s_slvEngine_current != nullptr); return s_slvEngine_current->getStatisticsRegistry(); } diff --git a/src/smt/solver_engine_scope.h b/src/smt/solver_engine_scope.h index c369d7b14..f942da5a1 100644 --- a/src/smt/solver_engine_scope.h +++ b/src/smt/solver_engine_scope.h @@ -31,9 +31,6 @@ class StatisticsRegistry; namespace smt { -SolverEngine* currentSolverEngine(); -bool solverEngineInScope(); - /** get the current resource manager */ ResourceManager* currentResourceManager(); diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index efe985d78..82c1038a6 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -184,10 +184,10 @@ Node Evaluator::eval(TNode n, } // should be the same as substitution + rewriting, or possibly null if // d_rr is nullptr or non-constant - Assert(((ret.isNull() || !ret.isConst()) && d_rr == nullptr) + Assert(ret.isNull() || !ret.isConst() || d_rr == nullptr || ret == d_rr->rewrite(n.substitute( - args.begin(), args.end(), vals.begin(), vals.end()))); + args.begin(), args.end(), vals.begin(), vals.end()))); return ret; } diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 2b2ef939d..af9869dd6 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -93,7 +93,7 @@ Node Rewriter::rewrite(TNode node) { // eagerly for the sake of efficiency here. return node; } - return getInstance()->rewriteTo(theoryOf(node), node); + return rewriteTo(theoryOf(node), node); } Node Rewriter::extendedRewrite(TNode node, bool aggr) @@ -110,11 +110,11 @@ TrustNode Rewriter::rewriteWithProof(TNode node, if (isExtEq) { // theory rewriter is responsible for rewriting the equality - TheoryRewriter* tr = getInstance()->d_theoryRewriters[theoryOf(node)]; + TheoryRewriter* tr = d_theoryRewriters[theoryOf(node)]; Assert(tr != nullptr); return tr->rewriteEqualityExtWithProof(node); } - Node ret = getInstance()->rewriteTo(theoryOf(node), node, d_tpg.get()); + Node ret = rewriteTo(theoryOf(node), node, d_tpg.get()); return TrustNode::mkTrustRewrite(node, ret, d_tpg.get()); } @@ -152,11 +152,6 @@ TheoryRewriter* Rewriter::getTheoryRewriter(theory::TheoryId theoryId) return d_theoryRewriters[theoryId]; } -Rewriter* Rewriter::getInstance() -{ - return smt::currentSolverEngine()->getRewriter(); -} - Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node, TConvProofGenerator* tcpg) diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 273ef036e..0fc50e640 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -40,12 +40,10 @@ class Rewriter { Rewriter(); /** - * !!! Temporary until static access to rewriter is eliminated. - * * Rewrites the node using theoryOf() to determine which rewriter to * use on the node. */ - static Node rewrite(TNode node); + Node rewrite(TNode node); /** * Rewrites the equality node using theoryOf() to determine which rewriter to @@ -102,13 +100,6 @@ class Rewriter { TheoryRewriter* getTheoryRewriter(theory::TheoryId theoryId); private: - /** - * Get the rewriter associated with the SolverEngine in scope. - * - * TODO(#3468): Get rid of this function (it relies on there being an - * singleton with the current SolverEngine in scope) - */ - static Rewriter* getInstance(); /** Returns the appropriate cache for a node */ Node getPreRewriteCache(theory::TheoryId theoryId, TNode node); diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp index 78da6031e..5f0ef7509 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.cpp +++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp @@ -1871,6 +1871,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial6) TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial) { + Rewriter* rr = d_slvEngine->getRewriter(); std::unordered_map res; BVGauss::Result ret; @@ -1925,9 +1926,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial) ASSERT_EQ(ret, BVGauss::Result::PARTIAL); ASSERT_EQ(res.size(), 2); - x = Rewriter::rewrite(x); - y = Rewriter::rewrite(y); - z = Rewriter::rewrite(z); + x = rr->rewrite(x); + y = rr->rewrite(y); + z = rr->rewrite(z); Node x1 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, @@ -1986,8 +1987,8 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial) * 9 0 1 7 --> 1 0 5 2 * 3 1 0 9 0 1 7 3 */ - ASSERT_EQ(res[Rewriter::rewrite(y)], y3); - ASSERT_EQ(res[Rewriter::rewrite(z)], z3); + ASSERT_EQ(res[rr->rewrite(y)], y3); + ASSERT_EQ(res[rr->rewrite(z)], z3); } else if (res.find(y) == res.end()) { @@ -2022,6 +2023,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial) TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial) { + Rewriter* rr = d_slvEngine->getRewriter(); std::unordered_map res; BVGauss::Result ret; @@ -2096,9 +2098,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial) ASSERT_EQ(ret, BVGauss::Result::PARTIAL); ASSERT_EQ(res.size(), 2); - x_mul_xx = Rewriter::rewrite(x_mul_xx); - y_mul_yy = Rewriter::rewrite(y_mul_yy); - z_mul_zz = Rewriter::rewrite(z_mul_zz); + x_mul_xx = rr->rewrite(x_mul_xx); + y_mul_yy = rr->rewrite(y_mul_yy); + z_mul_zz = rr->rewrite(z_mul_zz); Node x1 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, @@ -2241,6 +2243,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid1) TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid2) { + Rewriter* rr = d_slvEngine->getRewriter(); std::unordered_map res; BVGauss::Result ret; @@ -2295,9 +2298,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid2) ASSERT_EQ(ret, BVGauss::Result::UNIQUE); ASSERT_EQ(res.size(), 3); - n1 = Rewriter::rewrite(n1); - n2 = Rewriter::rewrite(n2); - z = Rewriter::rewrite(z); + n1 = rr->rewrite(n1); + n2 = rr->rewrite(n2); + z = rr->rewrite(z); ASSERT_EQ(res[n1], bv::utils::mkConst(48, 4)); ASSERT_EQ(res[n2], bv::utils::mkConst(48, 2)); @@ -3005,6 +3008,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw5a) TEST_F(TestPPWhiteBVGauss, get_min_bw5b) { + Rewriter* rr = d_slvEngine->getRewriter(); /* (bvadd * (bvadd * (bvadd @@ -3105,7 +3109,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw5b) kind::BITVECTOR_MULT, bv::utils::mkConst(20, 83), ww)); ASSERT_EQ(d_bv_gauss->getMinBwExpr(plus7), 19); - ASSERT_EQ(d_bv_gauss->getMinBwExpr(Rewriter::rewrite(plus7)), 17); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(rr->rewrite(plus7)), 17); } } // namespace test } // namespace cvc5::internal diff --git a/test/unit/theory/regexp_operation_black.cpp b/test/unit/theory/regexp_operation_black.cpp index 98d471ab4..6d42e15f3 100644 --- a/test/unit/theory/regexp_operation_black.cpp +++ b/test/unit/theory/regexp_operation_black.cpp @@ -44,16 +44,18 @@ class TestTheoryBlackRegexpOperation : public TestSmt void includes(Node r1, Node r2) { - r1 = Rewriter::rewrite(r1); - r2 = Rewriter::rewrite(r2); + Rewriter* rr = d_slvEngine->getRewriter(); + r1 = rr->rewrite(r1); + r2 = rr->rewrite(r2); std::cout << r1 << " includes " << r2 << std::endl; ASSERT_TRUE(RegExpEntail::regExpIncludes(r1, r2)); } void doesNotInclude(Node r1, Node r2) { - r1 = Rewriter::rewrite(r1); - r2 = Rewriter::rewrite(r2); + Rewriter* rr = d_slvEngine->getRewriter(); + r1 = rr->rewrite(r1); + r2 = rr->rewrite(r2); std::cout << r1 << " does not include " << r2 << std::endl; ASSERT_FALSE(RegExpEntail::regExpIncludes(r1, r2)); } @@ -88,6 +90,7 @@ TEST_F(TestTheoryBlackRegexpOperation, basic) TEST_F(TestTheoryBlackRegexpOperation, star_wildcards) { + Rewriter* rr = d_slvEngine->getRewriter(); Node sigma = d_nodeManager->mkNode(REGEXP_ALLCHAR); Node sigmaStar = d_nodeManager->mkNode(REGEXP_STAR, sigma); Node a = d_nodeManager->mkNode(STRING_TO_REGEXP, @@ -100,9 +103,9 @@ TEST_F(TestTheoryBlackRegexpOperation, star_wildcards) Node _abc_ = d_nodeManager->mkNode(REGEXP_CONCAT, sigmaStar, abc, sigmaStar); Node _asc_ = d_nodeManager->mkNode(REGEXP_CONCAT, {sigmaStar, a, sigma, c, sigmaStar}); - Node _sc_ = Rewriter::rewrite( + Node _sc_ = rr->rewrite( d_nodeManager->mkNode(REGEXP_CONCAT, {sigmaStar, sigma, c, sigmaStar})); - Node _as_ = Rewriter::rewrite( + Node _as_ = rr->rewrite( d_nodeManager->mkNode(REGEXP_CONCAT, {sigmaStar, a, sigma, sigmaStar})); Node _assc_ = d_nodeManager->mkNode( REGEXP_CONCAT, @@ -111,9 +114,9 @@ TEST_F(TestTheoryBlackRegexpOperation, star_wildcards) d_nodeManager->mkNode(REGEXP_CONCAT, {sigmaStar, c, sigma, a, sigmaStar}); Node _c_a_ = d_nodeManager->mkNode(REGEXP_CONCAT, {sigmaStar, c, sigmaStar, a, sigmaStar}); - Node _s_s_ = Rewriter::rewrite(d_nodeManager->mkNode( + Node _s_s_ = rr->rewrite(d_nodeManager->mkNode( REGEXP_CONCAT, {sigmaStar, sigma, sigmaStar, sigma, sigmaStar})); - Node _a_abc_ = Rewriter::rewrite(d_nodeManager->mkNode( + Node _a_abc_ = rr->rewrite(d_nodeManager->mkNode( REGEXP_CONCAT, {sigmaStar, a, sigmaStar, abc, sigmaStar})); includes(_asc_, _abc_); diff --git a/test/unit/theory/strings_rewriter_white.cpp b/test/unit/theory/strings_rewriter_white.cpp index 9236e0440..c4be4cf38 100644 --- a/test/unit/theory/strings_rewriter_white.cpp +++ b/test/unit/theory/strings_rewriter_white.cpp @@ -38,6 +38,7 @@ class TestTheoryWhiteStringsRewriter : public TestSmt TEST_F(TestTheoryWhiteStringsRewriter, rewrite_leq) { + Rewriter* rr = d_slvEngine->getRewriter(); TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); @@ -51,12 +52,12 @@ TEST_F(TestTheoryWhiteStringsRewriter, rewrite_leq) { Node leq = d_nodeManager->mkNode(STRING_LEQ, ax, bcy); - ASSERT_EQ(Rewriter::rewrite(leq), d_nodeManager->mkConst(true)); + ASSERT_EQ(rr->rewrite(leq), d_nodeManager->mkConst(true)); } { Node leq = d_nodeManager->mkNode(STRING_LEQ, bcy, ax); - ASSERT_EQ(Rewriter::rewrite(leq), d_nodeManager->mkConst(false)); + ASSERT_EQ(rr->rewrite(leq), d_nodeManager->mkConst(false)); } } diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp index 981b9d3f1..f3f718eac 100644 --- a/test/unit/theory/theory_arith_white.cpp +++ b/test/unit/theory/theory_arith_white.cpp @@ -53,7 +53,8 @@ class TestTheoryWhiteArith : public TestSmtNoFinishInit void fakeTheoryEnginePreprocess(TNode input) { - Assert(input == Rewriter::rewrite(input)); + Rewriter* rr = d_slvEngine->getRewriter(); + Assert(input == rr->rewrite(input)); d_slvEngine->getTheoryEngine()->preRegister(input); } @@ -67,11 +68,12 @@ class TestTheoryWhiteArith : public TestSmtNoFinishInit TEST_F(TestTheoryWhiteArith, assert) { + Rewriter* rr = d_slvEngine->getRewriter(); Node x = d_nodeManager->mkVar(*d_realType); Node c = d_nodeManager->mkConstReal(d_zero); Node gt = d_nodeManager->mkNode(GT, x, c); - Node leq = Rewriter::rewrite(gt.notNode()); + Node leq = rr->rewrite(gt.notNode()); fakeTheoryEnginePreprocess(leq); d_arith->assertFact(leq, true); @@ -81,6 +83,7 @@ TEST_F(TestTheoryWhiteArith, assert) TEST_F(TestTheoryWhiteArith, int_normal_form) { + Rewriter* rr = d_slvEngine->getRewriter(); Node x = d_nodeManager->mkVar(*d_intType); Node xr = d_nodeManager->mkVar(*d_realType); Node c0 = d_nodeManager->mkConstInt(d_zero); @@ -91,37 +94,37 @@ TEST_F(TestTheoryWhiteArith, int_normal_form) Node geq1 = d_nodeManager->mkNode(GEQ, x, c1); Node geq2 = d_nodeManager->mkNode(GEQ, x, c2); - ASSERT_EQ(Rewriter::rewrite(geq0), geq0); - ASSERT_EQ(Rewriter::rewrite(geq1), geq1); + ASSERT_EQ(rr->rewrite(geq0), geq0); + ASSERT_EQ(rr->rewrite(geq1), geq1); Node gt0 = d_nodeManager->mkNode(GT, x, c0); Node gt1 = d_nodeManager->mkNode(GT, x, c1); - ASSERT_EQ(Rewriter::rewrite(gt0), Rewriter::rewrite(geq1)); - ASSERT_EQ(Rewriter::rewrite(gt1), Rewriter::rewrite(geq2)); + ASSERT_EQ(rr->rewrite(gt0), rr->rewrite(geq1)); + ASSERT_EQ(rr->rewrite(gt1), rr->rewrite(geq2)); Node lt0 = d_nodeManager->mkNode(LT, x, c0); Node lt1 = d_nodeManager->mkNode(LT, x, c1); - ASSERT_EQ(Rewriter::rewrite(lt0), Rewriter::rewrite(geq0.notNode())); - ASSERT_EQ(Rewriter::rewrite(lt1), Rewriter::rewrite(geq1.notNode())); + ASSERT_EQ(rr->rewrite(lt0), rr->rewrite(geq0.notNode())); + ASSERT_EQ(rr->rewrite(lt1), rr->rewrite(geq1.notNode())); Node leq0 = d_nodeManager->mkNode(LEQ, x, c0); Node leq1 = d_nodeManager->mkNode(LEQ, x, c1); - ASSERT_EQ(Rewriter::rewrite(leq0), Rewriter::rewrite(geq1.notNode())); - ASSERT_EQ(Rewriter::rewrite(leq1), Rewriter::rewrite(geq2.notNode())); + ASSERT_EQ(rr->rewrite(leq0), rr->rewrite(geq1.notNode())); + ASSERT_EQ(rr->rewrite(leq1), rr->rewrite(geq2.notNode())); // (abs x) --> (abs x) Node absX = d_nodeManager->mkNode(ABS, x); - ASSERT_EQ(Rewriter::rewrite(absX), absX); + ASSERT_EQ(rr->rewrite(absX), absX); // (exp (+ 2 + x)) --> (* (exp x) (exp 1) (exp 1)) Node cr0 = d_nodeManager->mkConstReal(d_zero); Node t = d_nodeManager->mkNode(EXPONENTIAL, d_nodeManager->mkNode(ADD, c2, xr)) .eqNode(cr0); - ASSERT_EQ(Rewriter::rewrite(Rewriter::rewrite(t)), Rewriter::rewrite(t)); + ASSERT_EQ(rr->rewrite(rr->rewrite(t)), rr->rewrite(t)); } } // namespace test } // namespace cvc5::internal diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index 48a44ecae..9f47e5032 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -687,6 +687,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, to_set) TEST_F(TestTheoryWhiteBagsRewriter, map) { + Rewriter* rr = d_slvEngine->getRewriter(); TypeNode bagStringType = d_nodeManager->mkBagType(d_nodeManager->stringType()); Node emptybagString = d_nodeManager->mkConst(EmptyBag(bagStringType)); @@ -719,7 +720,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, map) // (bag.union_disjoint (bag "a" 3) (bag "b" 4))) = // (bag "" 7)) Node n2 = d_nodeManager->mkNode(BAG_MAP, lambda, unionDisjointAB); - Node rewritten = Rewriter::rewrite(n2); + Node rewritten = rr->rewrite(n2); Node bag = d_nodeManager->mkNode( BAG_MAKE, empty, d_nodeManager->mkConstInt(Rational(7))); // - (bag.map f (bag.union_disjoint K1 K2)) = @@ -729,7 +730,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, map) Node f = d_skolemManager->mkDummySkolem("f", lambda.getType()); Node unionDisjointK1K2 = d_nodeManager->mkNode(BAG_UNION_DISJOINT, k1, k2); Node n3 = d_nodeManager->mkNode(BAG_MAP, f, unionDisjointK1K2); - Node rewritten3 = Rewriter::rewrite(n3); + Node rewritten3 = rr->rewrite(n3); Node mapK1 = d_nodeManager->mkNode(BAG_MAP, f, k1); Node mapK2 = d_nodeManager->mkNode(BAG_MAP, f, k2); Node unionDisjointMapK1K2 = @@ -739,6 +740,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, map) TEST_F(TestTheoryWhiteBagsRewriter, fold) { + Rewriter* rr = d_slvEngine->getRewriter(); TypeNode bagIntegerType = d_nodeManager->mkBagType(d_nodeManager->integerType()); Node emptybag = d_nodeManager->mkConst(EmptyBag(bagIntegerType)); @@ -775,7 +777,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, fold) bag = d_nodeManager->mkNode(BAG_MAKE, ten, n); Node node3 = d_nodeManager->mkNode(BAG_FOLD, f, one, bag); Node result3 = d_nodeManager->mkConstInt(Rational(21)); - Node response3 = Rewriter::rewrite(node3); + Node response3 = rr->rewrite(node3); ASSERT_TRUE(response3 == result3); // (bag.fold f t (bag.union_disjoint A B)) = diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp index d53fd2a0a..eb7f98af5 100644 --- a/test/unit/theory/theory_black.cpp +++ b/test/unit/theory/theory_black.cpp @@ -39,6 +39,7 @@ class TestTheoryBlack : public TestSmt TEST_F(TestTheoryBlack, array_const) { + Rewriter* rr = d_slvEngine->getRewriter(); TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(), d_nodeManager->integerType()); Node zero = d_nodeManager->mkConstInt(Rational(0)); @@ -48,18 +49,18 @@ TEST_F(TestTheoryBlack, array_const) Node arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); ASSERT_FALSE(arr.isConst()); - arr = Rewriter::rewrite(arr); + arr = rr->rewrite(arr); ASSERT_TRUE(arr.isConst()); arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); ASSERT_TRUE(arr.isConst()); Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); - arr2 = Rewriter::rewrite(arr2); + arr2 = rr->rewrite(arr2); ASSERT_TRUE(arr2.isConst()); arr2 = d_nodeManager->mkNode(STORE, arr, one, one); - arr2 = Rewriter::rewrite(arr2); + arr2 = rr->rewrite(arr2); ASSERT_TRUE(arr2.isConst()); arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); - arr2 = Rewriter::rewrite(arr2); + arr2 = rr->rewrite(arr2); ASSERT_TRUE(arr2.isConst()); arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1), @@ -71,22 +72,22 @@ TEST_F(TestTheoryBlack, array_const) arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); ASSERT_FALSE(arr.isConst()); - arr = Rewriter::rewrite(arr); + arr = rr->rewrite(arr); ASSERT_TRUE(arr.isConst()); arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); - arr = Rewriter::rewrite(arr); + arr = rr->rewrite(arr); ASSERT_TRUE(arr.isConst()); arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); ASSERT_FALSE(arr2.isConst()); - arr2 = Rewriter::rewrite(arr2); + arr2 = rr->rewrite(arr2); ASSERT_TRUE(arr2.isConst()); arr2 = d_nodeManager->mkNode(STORE, arr, one, one); ASSERT_FALSE(arr2.isConst()); - arr2 = Rewriter::rewrite(arr2); + arr2 = rr->rewrite(arr2); ASSERT_TRUE(arr2.isConst()); arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); ASSERT_FALSE(arr2.isConst()); - arr2 = Rewriter::rewrite(arr2); + arr2 = rr->rewrite(arr2); ASSERT_TRUE(arr2.isConst()); arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(2), @@ -102,31 +103,31 @@ TEST_F(TestTheoryBlack, array_const) ASSERT_TRUE(arr.isConst()); arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); ASSERT_FALSE(arr2.isConst()); - arr2 = Rewriter::rewrite(arr2); + arr2 = rr->rewrite(arr2); ASSERT_TRUE(arr2.isConst()); arr = d_nodeManager->mkNode(STORE, storeAll, one, three); ASSERT_TRUE(arr.isConst()); arr2 = d_nodeManager->mkNode(STORE, arr, one, one); ASSERT_FALSE(arr2.isConst()); - arr2 = Rewriter::rewrite(arr2); + arr2 = rr->rewrite(arr2); ASSERT_TRUE(arr2 == storeAll); arr2 = d_nodeManager->mkNode(STORE, arr, zero, zero); ASSERT_FALSE(arr2.isConst()); - ASSERT_TRUE(Rewriter::rewrite(arr2).isConst()); + ASSERT_TRUE(rr->rewrite(arr2).isConst()); arr2 = d_nodeManager->mkNode(STORE, arr2, two, two); ASSERT_FALSE(arr2.isConst()); - ASSERT_TRUE(Rewriter::rewrite(arr2).isConst()); + ASSERT_TRUE(rr->rewrite(arr2).isConst()); arr2 = d_nodeManager->mkNode(STORE, arr2, three, one); ASSERT_FALSE(arr2.isConst()); - ASSERT_TRUE(Rewriter::rewrite(arr2).isConst()); + ASSERT_TRUE(rr->rewrite(arr2).isConst()); arr2 = d_nodeManager->mkNode(STORE, arr2, three, three); ASSERT_FALSE(arr2.isConst()); - ASSERT_TRUE(Rewriter::rewrite(arr2).isConst()); + ASSERT_TRUE(rr->rewrite(arr2).isConst()); arr2 = d_nodeManager->mkNode(STORE, arr2, two, zero); ASSERT_FALSE(arr2.isConst()); - arr2 = Rewriter::rewrite(arr2); + arr2 = rr->rewrite(arr2); ASSERT_TRUE(arr2.isConst()); } } // namespace test diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp index d28f74d34..97756345f 100644 --- a/test/unit/theory/theory_bv_int_blaster_white.cpp +++ b/test/unit/theory/theory_bv_int_blaster_white.cpp @@ -44,6 +44,7 @@ class TestTheoryWhiteBvIntblaster : public TestSmtNoFinishInit TEST_F(TestTheoryWhiteBvIntblaster, intblaster_constants) { + Env& env = d_slvEngine->getEnv(); // place holders for lemmas and skolem std::vector lemmas; std::map skolems; @@ -53,10 +54,6 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_constants) Node bv7_4 = d_nodeManager->mkConst(c1); // translating it to integers should yield 7. - Options opts; - Env env(d_nodeManager, &opts); - env.d_logic.setLogicString("QF_UFBV"); - env.d_logic.lock(); IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1); Node result = intBlaster.translateNoChildren(bv7_4, lemmas, skolems); Node seven = d_nodeManager->mkConstInt(Rational(7)); @@ -69,6 +66,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_constants) TEST_F(TestTheoryWhiteBvIntblaster, intblaster_symbolic_constant) { + Env& env = d_slvEngine->getEnv(); // place holders for lemmas and skolem std::vector lemmas; std::map skolems; @@ -78,10 +76,6 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_symbolic_constant) Node bv = d_nodeManager->mkVar("bv1", bvType); // translating it to integers should yield an integer variable. - Options opts; - Env env(d_nodeManager, &opts); - env.d_logic.setLogicString("QF_UFBV"); - env.d_logic.lock(); IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1); Node result = intBlaster.translateNoChildren(bv, lemmas, skolems); ASSERT_TRUE(result.isVar() && result.getType().isInteger()); @@ -93,6 +87,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_symbolic_constant) TEST_F(TestTheoryWhiteBvIntblaster, intblaster_uf) { + Env& env = d_slvEngine->getEnv(); // place holders for lemmas and skolem std::vector lemmas; std::map skolems; @@ -108,10 +103,6 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_uf) Node f = d_nodeManager->mkVar("f", funType); // translating it to integers should yield an Int x Int -> Bool function - Options opts; - Env env(d_nodeManager, &opts); - env.d_logic.setLogicString("QF_UFBV"); - env.d_logic.lock(); IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1); Node result = intBlaster.translateNoChildren(f, lemmas, skolems); TypeNode resultType = result.getType(); @@ -132,13 +123,10 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_uf) */ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_with_children) { + Env& env = d_slvEngine->getEnv(); // place holders for lemmas and skolem std::vector lemmas; std::map skolems; - Options opts; - Env env(d_nodeManager, &opts); - env.d_logic.setLogicString("QF_UFBV"); - env.d_logic.lock(); IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1); // bit-vector variables @@ -283,13 +271,10 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_with_children) */ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_bitwise) { + Env& env = d_slvEngine->getEnv(); // place holders for lemmas and skolem std::vector lemmas; std::map skolems; - Options opts; - Env env(d_nodeManager, &opts); - env.d_logic.setLogicString("QF_UFBV"); - env.d_logic.lock(); IntBlaster intBlaster(env, options::SolveBVAsIntMode::BITWISE, 1); // bit-vector variables diff --git a/test/unit/theory/theory_bv_rewriter_white.cpp b/test/unit/theory/theory_bv_rewriter_white.cpp index a3ca50346..a3822256d 100644 --- a/test/unit/theory/theory_bv_rewriter_white.cpp +++ b/test/unit/theory/theory_bv_rewriter_white.cpp @@ -44,6 +44,7 @@ class TestTheoryWhiteBvRewriter : public TestSmt TEST_F(TestTheoryWhiteBvRewriter, rewrite_to_fixpoint) { + Rewriter* rr = d_slvEngine->getRewriter(); TypeNode boolType = d_nodeManager->booleanType(); TypeNode bvType = d_nodeManager->mkBitVectorType(1); @@ -62,12 +63,13 @@ TEST_F(TestTheoryWhiteBvRewriter, rewrite_to_fixpoint) d_nodeManager->mkNode(BITVECTOR_ITE, boolToBv(b3), zero, bv), bv), bv); - Node nr = Rewriter::rewrite(n); - ASSERT_EQ(nr, Rewriter::rewrite(nr)); + Node nr = rr->rewrite(n); + ASSERT_EQ(nr, rr->rewrite(nr)); } TEST_F(TestTheoryWhiteBvRewriter, rewrite_concat_to_fixpoint) { + Rewriter* rr = d_slvEngine->getRewriter(); TypeNode boolType = d_nodeManager->booleanType(); TypeNode bvType = d_nodeManager->mkBitVectorType(4); @@ -80,12 +82,13 @@ TEST_F(TestTheoryWhiteBvRewriter, rewrite_concat_to_fixpoint) BITVECTOR_CONCAT, bv::utils::mkExtract(d_nodeManager->mkNode(BITVECTOR_CONCAT, x, y), 7, 0), z); - Node nr = Rewriter::rewrite(n); - ASSERT_EQ(nr, Rewriter::rewrite(nr)); + Node nr = rr->rewrite(n); + ASSERT_EQ(nr, rr->rewrite(nr)); } TEST_F(TestTheoryWhiteBvRewriter, rewrite_bv_ite) { + Rewriter* rr = d_slvEngine->getRewriter(); TypeNode boolType = d_nodeManager->booleanType(); TypeNode bvType = d_nodeManager->mkBitVectorType(1); @@ -95,19 +98,20 @@ TEST_F(TestTheoryWhiteBvRewriter, rewrite_bv_ite) Node ite = d_nodeManager->mkNode(BITVECTOR_ITE, c2, zero, zero); Node n = d_nodeManager->mkNode(BITVECTOR_ITE, c1, ite, ite); - Node nr = Rewriter::rewrite(n); - ASSERT_EQ(nr, Rewriter::rewrite(nr)); + Node nr = rr->rewrite(n); + ASSERT_EQ(nr, rr->rewrite(nr)); } TEST_F(TestTheoryWhiteBvRewriter, rewrite_bv_comp) { + Rewriter* rr = d_slvEngine->getRewriter(); TypeNode bvType = d_nodeManager->mkBitVectorType(1); Node zero = d_nodeManager->mkConst(BitVector(1, 0u)); Node x = d_nodeManager->mkVar("x", bvType); Node lhs = d_nodeManager->mkNode(BITVECTOR_NOT, x); Node rhs = d_nodeManager->mkNode(BITVECTOR_AND, zero, zero); Node n = d_nodeManager->mkNode(BITVECTOR_COMP, lhs, rhs); - Node nr = Rewriter::rewrite(n); + Node nr = rr->rewrite(n); // bvcomp(bvnot(x), bvand(0, 0)) ---> x ASSERT_EQ(nr, x); } diff --git a/test/unit/theory/theory_engine_white.cpp b/test/unit/theory/theory_engine_white.cpp index d00da636a..1b36ebf6a 100644 --- a/test/unit/theory/theory_engine_white.cpp +++ b/test/unit/theory/theory_engine_white.cpp @@ -75,6 +75,7 @@ class TestTheoryWhiteEngine : public TestSmt TEST_F(TestTheoryWhiteEngine, rewriter_simple) { + Rewriter* rr = d_slvEngine->getRewriter(); Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType()); Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType()); Node z = d_nodeManager->mkVar("z", d_nodeManager->integerType()); @@ -90,7 +91,7 @@ TEST_F(TestTheoryWhiteEngine, rewriter_simple) // do a full rewrite; DummyTheory::preRewrite() and DummyTheory::postRewrite() // assert that the rewrite calls that are made match the expected sequence // set up above - nOut = Rewriter::rewrite(n); + nOut = rr->rewrite(n); // assert that the rewritten node is what we expect ASSERT_EQ(nOut, nExpected); @@ -98,6 +99,7 @@ TEST_F(TestTheoryWhiteEngine, rewriter_simple) TEST_F(TestTheoryWhiteEngine, rewriter_complex) { + Rewriter* rr = d_slvEngine->getRewriter(); Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType()); Node y = d_nodeManager->mkVar("y", d_nodeManager->realType()); TypeNode u = d_nodeManager->mkSort("U"); @@ -137,7 +139,7 @@ TEST_F(TestTheoryWhiteEngine, rewriter_complex) // do a full rewrite; DummyTheory::preRewrite() and DummyTheory::postRewrite() // assert that the rewrite calls that are made match the expected sequence // set up above - nOut = Rewriter::rewrite(n); + nOut = rr->rewrite(n); // assert that the rewritten node is what we expect ASSERT_EQ(nOut, nExpected); diff --git a/test/unit/theory/theory_sets_rewriter_white.cpp b/test/unit/theory/theory_sets_rewriter_white.cpp index 3d3bf94d5..4834a163a 100644 --- a/test/unit/theory/theory_sets_rewriter_white.cpp +++ b/test/unit/theory/theory_sets_rewriter_white.cpp @@ -43,6 +43,7 @@ class TestTheoryWhiteSetsRewriter : public TestSmt TEST_F(TestTheoryWhiteSetsRewriter, map) { + Rewriter* rr = d_slvEngine->getRewriter(); Node one = d_nodeManager->mkConstInt(Rational(1)); TypeNode stringType = d_nodeManager->stringType(); TypeNode integerType = d_nodeManager->integerType(); @@ -71,7 +72,7 @@ TEST_F(TestTheoryWhiteSetsRewriter, map) // (lambda ((x String)) 1) // (set.union (set.singleton "a") (set.singleton "b"))) = (set.singleton 1)) Node n2 = d_nodeManager->mkNode(SET_MAP, lambda, unionAB); - Node rewritten2 = Rewriter::rewrite(n2); + Node rewritten2 = rr->rewrite(n2); Node bag = d_nodeManager->mkNode(SET_SINGLETON, one); ASSERT_TRUE(rewritten2 == bag); @@ -82,7 +83,7 @@ TEST_F(TestTheoryWhiteSetsRewriter, map) Node f = d_skolemManager->mkDummySkolem("f", lambda.getType()); Node unionK1K2 = d_nodeManager->mkNode(SET_UNION, k1, k2); Node n3 = d_nodeManager->mkNode(SET_MAP, f, unionK1K2); - Node rewritten3 = Rewriter::rewrite(n3); + Node rewritten3 = rr->rewrite(n3); Node mapK1 = d_nodeManager->mkNode(SET_MAP, f, k1); Node mapK2 = d_nodeManager->mkNode(SET_MAP, f, k2); Node unionMapK1K2 = d_nodeManager->mkNode(SET_UNION, mapK1, mapK2); diff --git a/test/unit/theory/theory_sets_type_enumerator_white.cpp b/test/unit/theory/theory_sets_type_enumerator_white.cpp index 5402f668e..ebd6f94d7 100644 --- a/test/unit/theory/theory_sets_type_enumerator_white.cpp +++ b/test/unit/theory/theory_sets_type_enumerator_white.cpp @@ -41,6 +41,7 @@ class TestTheoryWhiteSetsTypeEnumerator : public TestSmt TEST_F(TestTheoryWhiteSetsTypeEnumerator, set_of_booleans) { + Rewriter* rr = d_slvEngine->getRewriter(); TypeNode boolType = d_nodeManager->booleanType(); SetEnumerator setEnumerator(d_nodeManager->mkSetType(boolType)); ASSERT_FALSE(setEnumerator.isFinished()); @@ -59,7 +60,7 @@ TEST_F(TestTheoryWhiteSetsTypeEnumerator, set_of_booleans) addAndCheckUnique(actual2, elems); ASSERT_FALSE(setEnumerator.isFinished()); - Node actual3 = Rewriter::rewrite(*++setEnumerator); + Node actual3 = rr->rewrite(*++setEnumerator); addAndCheckUnique(actual3, elems); ASSERT_FALSE(setEnumerator.isFinished()); -- 2.30.2