From dcb73e70575406db5ef94eb48a9ad5b2bdf7b31a Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Thu, 26 May 2016 18:19:51 -0400 Subject: [PATCH] Fix for aig_bitblaster.cpp --- src/theory/bv/aig_bitblaster.cpp | 25 ++++++------------------- 1 file changed, 6 insertions(+), 19 deletions(-) diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp index 80a9396ac..098582433 100644 --- a/src/theory/bv/aig_bitblaster.cpp +++ b/src/theory/bv/aig_bitblaster.cpp @@ -19,7 +19,7 @@ #include "options/bv_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" - +#include "smt/smt_statistics_registry.h" #ifdef CVC4_USE_ABC // Function is defined as static in ABC. Not sure how else to do this. @@ -140,23 +140,10 @@ AigBitblaster::AigBitblaster() , d_bbAtoms() , d_aigOutputNode(NULL) { - 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"); - } + d_nullContext = new context::Context(); + d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, smtStatisticsRegistry(), "AigBitblaster"); + MinisatEmptyNotify* notify = new MinisatEmptyNotify(); + d_satSolver->setNotify(notify); } AigBitblaster::~AigBitblaster() { @@ -415,7 +402,7 @@ void AigBitblaster::assertToSatSolver(Cnf_Dat_t* pCnf) { prop::SatLiteral lit(sat_variables[index-1], int_lit < 0); clause.push_back(lit); } - d_satSolver->addClause(clause, false, RULE_INVALID); + d_satSolver->addClause(clause, false); } } -- 2.30.2