diff options
author | Liana Hadarean <lianahady@gmail.com> | 2016-05-24 22:30:41 -0700 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2016-05-24 22:30:48 -0700 |
commit | 2591fc4f57030b31c2c49d5c2dae9e96d3ce3afa (patch) | |
tree | 0296cb4f8194aef27813ef5251e88f475c9a6ffb /src/theory/bv/aig_bitblaster.cpp | |
parent | beaf8b212dfadb47328942c23a7649ab44a014cb (diff) |
Merged cryptominisat from experimental branch.
Diffstat (limited to 'src/theory/bv/aig_bitblaster.cpp')
-rw-r--r-- | src/theory/bv/aig_bitblaster.cpp | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp index 887daa1bd..80a9396ac 100644 --- a/src/theory/bv/aig_bitblaster.cpp +++ b/src/theory/bv/aig_bitblaster.cpp @@ -140,10 +140,23 @@ AigBitblaster::AigBitblaster() , d_bbAtoms() , d_aigOutputNode(NULL) { - d_nullContext = new context::Context(); - d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "AigBitblaster"); - MinisatEmptyNotify* notify = new MinisatEmptyNotify(); - d_satSolver->setNotify(notify); + d_nullContext = new context::Context(); + switch(options::bvSatSolver()) { + case SAT_SOLVER_MINISAT: { + prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat(d_nullContext, + "AigBitblaster"); + MinisatEmptyNotify* notify = new MinisatEmptyNotify(); + minisat->setNotify(notify); + d_satSolver = minisat; + break; + } + case SAT_SOLVER_CRYPTOMINISAT: + d_satSolver = prop::SatSolverFactory::createCryptoMinisat(smtStatisticsRegistry(), + "AigBitblaster"); + break; + default: + Unreachable("Unknown SAT solver type"); + } } AigBitblaster::~AigBitblaster() { |