diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-11-15 17:52:15 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-11-15 17:52:15 -0800 |
commit | f45bad0112192abb47cd350abdb5414e385c38b1 (patch) | |
tree | 527136b5b49a1b2600e5ac3d9c96790c496ce12a /src/theory/bv/theory_bv.cpp | |
parent | 585682fbc2b622bc62db80578b76adf52709c7c7 (diff) |
Remove staticrmStatic
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 23ffabcd1..aa1aab6a6 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -44,13 +44,14 @@ namespace CVC4 { namespace theory { namespace bv { -TheoryBV::TheoryBV(context::Context* c, +TheoryBV::TheoryBV(Environment* env, + context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, std::string name) - : Theory(THEORY_BV, c, u, out, valuation, logicInfo, name), + : Theory(THEORY_BV, env, c, u, out, valuation, logicInfo, name), d_context(c), d_alreadyPropagatedSet(c), d_sharedTermsSet(c), @@ -78,29 +79,29 @@ TheoryBV::TheoryBV(context::Context* c, getExtTheory()->addFunctionKind(kind::BITVECTOR_TO_NAT); getExtTheory()->addFunctionKind(kind::INT_TO_BITVECTOR); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - d_eagerSolver.reset(new EagerBitblastSolver(c, this)); + d_eagerSolver.reset(new EagerBitblastSolver(env, c, this)); return; } if (options::bitvectorEqualitySolver() && !options::proof()) { - d_subtheories.emplace_back(new CoreSolver(c, this)); + d_subtheories.emplace_back(new CoreSolver(env, c, this)); d_subtheoryMap[SUB_CORE] = d_subtheories.back().get(); } if (options::bitvectorInequalitySolver() && !options::proof()) { - d_subtheories.emplace_back(new InequalitySolver(c, u, this)); + d_subtheories.emplace_back(new InequalitySolver(env, c, u, this)); d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get(); } if (options::bitvectorAlgebraicSolver() && !options::proof()) { - d_subtheories.emplace_back(new AlgebraicSolver(c, this)); + d_subtheories.emplace_back(new AlgebraicSolver(env, c, this)); d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get(); } - BitblastSolver* bb_solver = new BitblastSolver(c, this); + BitblastSolver* bb_solver = new BitblastSolver(env, c, this); if (options::bvAbstraction()) { bb_solver->setAbstraction(d_abstractionModule.get()); |