Making `IntBlaster` inherit from `EnvObj` (#7431)

This PR makes the IntBlaster class inherit from EnvObj, along with derived modifications.

diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
index 5b9e0bfc4de973228583869f78ea672e4c54ca99..ba0e51595478ce14413e85ac12008d625cb95e30 100644 (file)
--- a/src/theory/bv/int_blaster.cpp
+++ b/src/theory/bv/int_blaster.cpp
@@ -27,7 +27,7 @@
 #include "options/option_exception.h"
 #include "options/uf_options.h"
 #include "theory/bv/theory_bv_utils.h"
-#include "theory/rewriter.h"
+#include "theory/logic_info.h"
 #include "util/bitvector.h"
 #include "util/iand.h"
 #include "util/rational.h"
@@ -42,17 +42,18 @@ Rational intpow2(uint64_t b) { return Rational(Integer(2).pow(b), Integer(1)); }
 
 }  // namespace
 
-IntBlaster::IntBlaster(context::Context* c,
+IntBlaster::IntBlaster(Env& env,
                        options::SolveBVAsIntMode mode,
                        uint64_t granularity,
                        bool introduceFreshIntVars)
-    : d_binarizeCache(c),
-      d_intblastCache(c),
-      d_rangeAssertions(c),
-      d_bitwiseAssertions(c),
+    : EnvObj(env),
+      d_binarizeCache(userContext()),
+      d_intblastCache(userContext()),
+      d_rangeAssertions(userContext()),
+      d_bitwiseAssertions(userContext()),
       d_mode(mode),
       d_granularity(granularity),
-      d_context(c),
+      d_context(userContext()),
       d_introduceFreshIntVars(introduceFreshIntVars)
 {
   d_nm = NodeManager::currentNM();
@@ -60,6 +61,8 @@ IntBlaster::IntBlaster(context::Context* c,
   d_one = d_nm->mkConst<Rational>(1);
 };
 
+IntBlaster::~IntBlaster() {}
+
 void IntBlaster::addRangeConstraint(Node node,
                                     uint64_t size,
                                     std::vector<Node>& lemmas)
@@ -125,7 +128,7 @@ Node IntBlaster::intBlast(Node n,
                           std::map<Node, Node>& skolems)
 {
   // make sure the node is re-written
-  n = Rewriter::rewrite(n);
+  n = rewrite(n);
 
   // helper vector for traversal.
   std::vector<Node> toVisit;
@@ -500,7 +503,7 @@ Node IntBlaster::translateWithChildren(
        * of the bounds that were relevant for the original
        * bit-vectors.
        */
-      if (childrenTypesChanged(original) && options::ufHo())
+      if (childrenTypesChanged(original) && logicInfo().isHigherOrder())
       {
         throw OptionException("bv-to-int does not support higher order logic ");
       }

diff --git a/src/theory/bv/int_blaster.h b/src/theory/bv/int_blaster.h
index ce0d89fb742a928b65faecfecd13665e5d2f90ab..ed8ed10c652a29a54b072f5268817563c9aad21f 100644 (file)
--- a/src/theory/bv/int_blaster.h
+++ b/src/theory/bv/int_blaster.h
@@ -21,8 +21,8 @@
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/cdo.h"
-#include "context/context.h"
 #include "options/smt_options.h"
+#include "smt/env_obj.h"
 #include "theory/arith/nl/iand_utils.h"
 
 namespace cvc5 {
@@ -91,7 +91,7 @@ namespace cvc5 {
 ** op.
 **
 **/
-class IntBlaster
+class IntBlaster : protected EnvObj
 {
   using CDNodeMap = context::CDHashMap<Node, Node>;
 
@@ -105,11 +105,13 @@ class IntBlaster
    * translated to integer variables, or are directly casted using `bv2nat`
    * operator. not purely bit-vector nodes.
    */
-  IntBlaster(context::Context* context,
+  IntBlaster(Env& env,
              options::SolveBVAsIntMode mode,
              uint64_t granluarity = 1,
              bool introduceFreshIntVars = true);
 
+  ~IntBlaster();
+
   /**
    * The result is an integer term and is computed
    * according to the translation specified above.

diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp
index 5fa1e10f26d1abc3733ca0b6f3f89c6d59d55349..39ae835e0b1e38b38142cc5e06ced527819e9992 100644 (file)
--- a/test/unit/theory/theory_bv_int_blaster_white.cpp
+++ b/test/unit/theory/theory_bv_int_blaster_white.cpp
@@ -57,8 +57,12 @@ 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(
-      d_slvEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, false);
+      env, options::SolveBVAsIntMode::SUM, 1, false);
   Node result = intBlaster.translateNoChildren(bv7_4, lemmas, skolems);
   Node seven = d_nodeManager->mkConst(Rational(7));
   ASSERT_EQ(seven, result);
@@ -79,8 +83,12 @@ 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(
-      d_slvEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true);
+      env, options::SolveBVAsIntMode::SUM, 1, true);
   Node result = intBlaster.translateNoChildren(bv, lemmas, skolems);
   ASSERT_TRUE(result.isVar() && result.getType().isInteger());
 
@@ -106,8 +114,12 @@ 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(
-      d_slvEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true);
+      env, options::SolveBVAsIntMode::SUM, 1, true);
   Node result = intBlaster.translateNoChildren(f, lemmas, skolems);
   TypeNode resultType = result.getType();
   std::vector<TypeNode> resultDomain = resultType.getArgTypes();
@@ -130,8 +142,12 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_with_children)
   // 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(
-      d_slvEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true);
+      env, options::SolveBVAsIntMode::SUM, 1, true);
 
   // bit-vector variables
   TypeNode bvType = d_nodeManager->mkBitVectorType(4);