diff options
author | lianah <lianahady@gmail.com> | 2016-05-26 19:05:01 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2016-05-26 19:05:01 -0400 |
commit | d133e87221b0de3a4eb7c286cebda14548874e7c (patch) | |
tree | 7a2a01735c1e0e90d64c7e1f582a5120702f24e7 /src/theory/bv | |
parent | 5a97ae0820747af37f1cabce69e7649e88acb681 (diff) |
Changed aig_bitblaster to work with cryptominisat
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/aig_bitblaster.cpp | 22 | ||||
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 2 |
2 files changed, 19 insertions, 5 deletions
diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp index 098582433..37e9f4476 100644 --- a/src/theory/bv/aig_bitblaster.cpp +++ b/src/theory/bv/aig_bitblaster.cpp @@ -140,10 +140,24 @@ AigBitblaster::AigBitblaster() , d_bbAtoms() , d_aigOutputNode(NULL) { - d_nullContext = new context::Context(); - d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, smtStatisticsRegistry(), "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, + smtStatisticsRegistry(), + "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() { diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index f9f5361d3..929bccada 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -306,7 +306,7 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*> { static Abc_Ntk_t* abcAigNetwork; context::Context* d_nullContext; - prop::BVSatSolverInterface* d_satSolver; + prop::SatSolver* d_satSolver; TNodeAigMap d_aigCache; NodeAigMap d_bbAtoms; |