diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-09 19:19:40 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-09 19:19:40 -0500 |
| commit | 92ed7681941b3b6d9c857724454860ac72d778d9 (patch) | |
| tree | 200455fb3d8046e9dc0e9c6ae8383e2b3a904bcc /src/theory/bv | |
| parent | 789f5b3c8c224deb48fe547303147e0d15e690ae (diff) | |
Towards proper use of resource managers (#4233)
Resource manager will be owned by SmtEngine in the future. This passes the resource manager cached by SmtEnginePrivate to the PropEngine created by SmtEngine instead of using the global pointer. It also makes a few preprocessing passes use the resource manager they already have access to and should use.
Diffstat (limited to 'src/theory/bv')
| -rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.cpp | 13 | ||||
| -rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.cpp | 16 |
2 files changed, 16 insertions, 13 deletions
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index c4e3513bf..bddde4cb7 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -63,12 +63,13 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c) default: Unreachable() << "Unknown SAT solver type"; } d_satSolver.reset(solver); - d_cnfStream.reset( - new prop::TseitinCnfStream(d_satSolver.get(), - d_bitblastingRegistrar.get(), - d_nullContext.get(), - options::proof(), - "EagerBitblaster")); + ResourceManager* rm = NodeManager::currentResourceManager(); + d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(), + d_bitblastingRegistrar.get(), + d_nullContext.get(), + rm, + options::proof(), + "EagerBitblaster")); } EagerBitblaster::~EagerBitblaster() {} diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 06afa126d..463ffae79 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -79,12 +79,13 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, d_satSolver.reset( prop::SatSolverFactory::createMinisat(c, smtStatisticsRegistry(), name)); - d_cnfStream.reset( - new prop::TseitinCnfStream(d_satSolver.get(), - d_nullRegistrar.get(), - d_nullContext.get(), - options::proof(), - "LazyBitblaster")); + ResourceManager* rm = NodeManager::currentResourceManager(); + d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(), + d_nullRegistrar.get(), + d_nullContext.get(), + rm, + options::proof(), + "LazyBitblaster")); d_satSolverNotify.reset( d_emptyNotify @@ -578,8 +579,9 @@ void TLazyBitblaster::clearSolver() { // recreate sat solver d_satSolver.reset( prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry())); + ResourceManager* rm = NodeManager::currentResourceManager(); d_cnfStream.reset(new prop::TseitinCnfStream( - d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get())); + d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get(), rm)); d_satSolverNotify.reset( d_emptyNotify ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify() |