From a06b10cf51c22dd86bf266ef1494dded4b53e9f0 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Fri, 22 Oct 2021 17:56:39 +0300 Subject: [PATCH] Making `IntBlaster` inherit from `EnvObj` (#7431) This PR makes the IntBlaster class inherit from EnvObj, along with derived modifications. --- src/theory/bv/int_blaster.cpp | 21 +++++++++------- src/theory/bv/int_blaster.h | 8 ++++--- .../theory/theory_bv_int_blaster_white.cpp | 24 +++++++++++++++---- 3 files changed, 37 insertions(+), 16 deletions(-) diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp index 5b9e0bfc4..ba0e51595 100644 --- 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(1); }; +IntBlaster::~IntBlaster() {} + void IntBlaster::addRangeConstraint(Node node, uint64_t size, std::vector& lemmas) @@ -125,7 +128,7 @@ Node IntBlaster::intBlast(Node n, std::map& skolems) { // make sure the node is re-written - n = Rewriter::rewrite(n); + n = rewrite(n); // helper vector for traversal. std::vector 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 ce0d89fb7..ed8ed10c6 100644 --- 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; @@ -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 5fa1e10f2..39ae835e0 100644 --- 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(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 resultDomain = resultType.getArgTypes(); @@ -130,8 +142,12 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_with_children) // 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( - d_slvEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true); + env, options::SolveBVAsIntMode::SUM, 1, true); // bit-vector variables TypeNode bvType = d_nodeManager->mkBitVectorType(4); -- 2.30.2