diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 1 | ||||
-rw-r--r-- | src/theory/bv/eager_bitblaster.cpp | 17 | ||||
-rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 9 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 4 |
5 files changed, 16 insertions, 19 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 66eea0997..9c6c4af9b 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -26,7 +26,6 @@ #include "context/cdhashmap.h" #include "expr/node.h" #include "prop/sat_solver.h" -#include "smt/smt_globals.h" #include "theory/theory_registrar.h" #include "theory/valuation.h" #include "util/resource_manager.h" diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index 2e4f06c38..dd561667c 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -43,16 +43,13 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) d_bitblastingRegistrar = new BitblastingRegistrar(this); d_nullContext = new context::Context(); - d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, - smtStatisticsRegistry(), - "EagerBitblaster"); - d_cnfStream = new prop::TseitinCnfStream(d_satSolver, - d_bitblastingRegistrar, - d_nullContext, - d_bv->globals(), - options::proof(), - "EagerBitblaster"); - + d_satSolver = prop::SatSolverFactory::createMinisat( + d_nullContext, smtStatisticsRegistry(), "EagerBitblaster"); + + d_cnfStream = new prop::TseitinCnfStream( + d_satSolver, d_bitblastingRegistrar, d_nullContext, options::proof(), + "EagerBitblaster"); + MinisatEmptyNotify* notify = new MinisatEmptyNotify(); d_satSolver->setNotify(notify); d_bvp = NULL; diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index 9268e2152..ca21e98c4 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -56,13 +56,13 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar, d_nullContext, - d_bv->globals(), options::proof(), "LazyBitblaster"); d_satSolverNotify = d_emptyNotify ? (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : - (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, this); + (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, + this); d_satSolver->setNotify(d_satSolverNotify); } @@ -526,11 +526,12 @@ void TLazyBitblaster::clearSolver() { d_satSolver = prop::SatSolverFactory::createMinisat( d_ctx, smtStatisticsRegistry()); d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar, - d_nullContext, d_bv->globals()); + d_nullContext); d_satSolverNotify = d_emptyNotify ? (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : - (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this); + (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, + this); d_satSolver->setNotify(d_satSolverNotify); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 8f7e975cd..191f70638 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -44,8 +44,8 @@ namespace bv { TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, SmtGlobals* globals) - : Theory(THEORY_BV, c, u, out, valuation, logicInfo, globals), + const LogicInfo& logicInfo) + : Theory(THEORY_BV, c, u, out, valuation, logicInfo), d_context(c), d_alreadyPropagatedSet(c), d_sharedTermsSet(c), diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 27138abfc..1da15abf8 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -22,7 +22,6 @@ #include "context/cdhashset.h" #include "context/cdlist.h" #include "context/context.h" -#include "smt/smt_globals.h" #include "theory/bv/bv_subtheory.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory.h" @@ -56,7 +55,8 @@ class TheoryBV : public Theory { public: - TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals); + TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo); ~TheoryBV(); |