Make Rewriter::rewrite non-static (#8828)

This furthermore eliminates smt::currentSolverEngine.

diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
index 15e93c927b35967c2a6c5c3979deb450b7b39740..4bc73514f37e72b497a7e420eccc0904be0ee5ee 100644 (file)
--- 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 4cafc74c8d3081eca5e2ff788d95726403cb4175..ce769c7adc53cf9d4b85b5bd51c77c8306c9acd4 100644 (file)
--- 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 3d11c13be12b0f8c8724dcda293ce0380973108e..967a407286925b6064c3a4a0483a6bc75f32c864 100644 (file)
--- 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 c369d7b14247c52fffda8e0eed83c0eb2a120d96..f942da5a198e443dbe2e347ab85f4f21a6fdcb29 100644 (file)
--- 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 efe985d78743364919a0f220880c5173483be1b9..82c1038a6bc365322d9747dbdd8366213703fc2c 100644 (file)
--- 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 2b2ef939d883dffcd6641f914974f304f7f38870..af9869dd6f423a81eae8b843a9ad13f2d2cab6ff 100644 (file)
--- 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 273ef036e7033605a843498610df197889b36f98..0fc50e64023477bee54f33d523870131c7813788 100644 (file)
--- 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 78da6031e671947545c8e7e2d603f69730445dc3..5f0ef75098bcb71f28e8355f3a5f14df8ff874a3 100644 (file)
--- 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<Node, Node> 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<Node, Node> 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<Node, Node> 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 98d471ab4568f624f92af4dc1581ac6e2b94af8e..6d42e15f3a5f456b25feb64ae320fa3015dcb22f 100644 (file)
--- 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 9236e044027956c4f076cc16a32c796efc3cf9f1..c4be4cf385a1ad3ec4b251fba603d6027f5324f2 100644 (file)
--- 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 981b9d3f140c873a940c72449538a66134e8ae1a..f3f718eac5cc538376b1d92c901a1790c021280c 100644 (file)
--- 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 48a44ecaed17f1ca8fa483b7495e8e24670e1cd4..9f47e503212ac8bce635032281402b7e79f3c983 100644 (file)
--- 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 d53fd2a0a3252a7f3d45b136bea03cef4fa2fffd..eb7f98af50f0c488633022cc63e7ceb0e3d8e0ae 100644 (file)
--- 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 d28f74d34991a3fa048334b087acd3973cf6d0b4..97756345f85ed643810024c138953c26793a5a4e 100644 (file)
--- 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<Node> lemmas;
   std::map<Node, Node> skolems;
@@ -53,10 +54,6 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_constants)
   Node bv7_4 = d_nodeManager->mkConst<BitVector>(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<Node> lemmas;
   std::map<Node, Node> 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<Node> lemmas;
   std::map<Node, Node> 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<Node> lemmas;
   std::map<Node, Node> 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<Node> lemmas;
   std::map<Node, Node> 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 a3ca50346dae1de25e0125460c9cb9c3cfe4004d..a3822256df668f6a4fb13b90413a17286949a70d 100644 (file)
--- 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 d00da636a14df47e1c9dfcd89d4464477806479c..1b36ebf6a43de17fcbb25387e03a015f72c8d51a 100644 (file)
--- 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 3d3bf94d59375dfe5a84eb5c5e6f8459be824bad..4834a163ad0f83087423ccbc290e5be6cfa7fdef 100644 (file)
--- 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 5402f668e62b6f5c5916c3d4b45215acc36425ca..ebd6f94d7edbbb14eb9f886ee4fc344bfec6ef21 100644 (file)
--- 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());