diff options
Diffstat (limited to 'src/theory/bv/eager_bitblaster.cpp')
-rw-r--r-- | src/theory/bv/eager_bitblaster.cpp | 23 |
1 files changed, 19 insertions, 4 deletions
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index a103d1f63..53fb4f94b 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -47,15 +47,30 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) { d_bitblastingRegistrar = new BitblastingRegistrar(this); d_nullContext = new context::Context(); - - d_satSolver = prop::SatSolverFactory::createMinisat( - d_nullContext, smtStatisticsRegistry(), "EagerBitblaster"); + + switch(options::bvSatSolver()) { + case SAT_SOLVER_MINISAT: { + prop::BVSatSolverInterface* minisat = + prop::SatSolverFactory::createMinisat(d_nullContext, + smtStatisticsRegistry(), + "EagerBitblaster"); + MinisatEmptyNotify* notify = new MinisatEmptyNotify(); + minisat->setNotify(notify); + d_satSolver = minisat; + break; + } + case SAT_SOLVER_CRYPTOMINISAT: + d_satSolver = prop::SatSolverFactory::createCryptoMinisat(smtStatisticsRegistry(), + "EagerBitblaster"); + break; + default: + Unreachable("Unknown SAT solver type"); + } d_cnfStream = new prop::TseitinCnfStream( d_satSolver, d_bitblastingRegistrar, d_nullContext, options::proof(), "EagerBitblaster"); - d_satSolver->setNotify(&d_notify); d_bvp = NULL; } |