diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Makefile.am | 8 | ||||
-rw-r--r-- | src/base/configuration.cpp | 4 | ||||
-rw-r--r-- | src/base/configuration.h | 2 | ||||
-rw-r--r-- | src/base/configuration_private.h | 6 | ||||
-rw-r--r-- | src/options/bv_bitblast_mode.cpp | 15 | ||||
-rw-r--r-- | src/options/bv_bitblast_mode.h | 7 | ||||
-rw-r--r-- | src/options/bv_options | 3 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 66 | ||||
-rw-r--r-- | src/options/options_handler.h | 6 | ||||
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 4 | ||||
-rw-r--r-- | src/prop/cryptominisat.cpp | 230 | ||||
-rw-r--r-- | src/prop/cryptominisat.h | 137 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 3 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 9 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.cpp | 7 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.h | 2 | ||||
-rw-r--r-- | src/theory/bv/aig_bitblaster.cpp | 21 | ||||
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 2 | ||||
-rw-r--r-- | src/theory/bv/eager_bitblaster.cpp | 23 |
19 files changed, 545 insertions, 10 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 908245e63..a3580989c 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -109,6 +109,8 @@ libcvc4_la_SOURCES = \ prop/sat_solver_factory.cpp \ prop/sat_solver_factory.h \ prop/sat_solver_types.h \ + prop/cryptominisat.h \ + prop/cryptominisat.cpp \ prop/theory_proxy.cpp \ prop/theory_proxy.h \ smt/boolean_terms.cpp \ @@ -474,6 +476,12 @@ libcvc4_la_LIBADD += $(ABC_LIBS) libcvc4_la_LDFLAGS += $(ABC_LDFLAGS) endif +if CVC4_USE_CRYPTOMINISAT +libcvc4_la_LIBADD += $(CRYPTOMINISAT_LIBS) +libcvc4_la_LDFLAGS += $(CRYPTOMINISAT_LDFLAGS) +endif + + BUILT_SOURCES = \ theory/rewriter_tables.h \ theory/theory_traits.h \ diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index ce8967a18..db19469fd 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -134,6 +134,10 @@ bool Configuration::isBuiltWithAbc() { return IS_ABC_BUILD; } +bool Configuration::isBuiltWithCryptominisat() { + return IS_CRYPTOMINISAT_BUILD; +} + bool Configuration::isBuiltWithReadline() { return IS_READLINE_BUILD; } diff --git a/src/base/configuration.h b/src/base/configuration.h index 498337c4c..5d499174f 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -93,6 +93,8 @@ public: static bool isBuiltWithAbc(); + static bool isBuiltWithCryptominisat(); + static bool isBuiltWithReadline(); static bool isBuiltWithCudd(); diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index 74ce00bdf..f0ef1a795 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -114,6 +114,12 @@ namespace CVC4 { # define IS_ABC_BUILD false #endif /* CVC4_USE_ABC */ +#if CVC4_USE_CRYPTOMINISAT +# define IS_CRYPTOMINISAT_BUILD true +#else /* CVC4_USE_CRYPTOMINISAT */ +# define IS_CRYPTOMINISAT_BUILD false +#endif /* CVC4_USE_CRYPTOMINISAT */ + #ifdef HAVE_LIBREADLINE # define IS_READLINE_BUILD true #else /* HAVE_LIBREADLINE */ diff --git a/src/options/bv_bitblast_mode.cpp b/src/options/bv_bitblast_mode.cpp index 9cf47fe33..f331345f7 100644 --- a/src/options/bv_bitblast_mode.cpp +++ b/src/options/bv_bitblast_mode.cpp @@ -53,4 +53,19 @@ std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode) { return out; } +std::ostream& operator<<(std::ostream& out, theory::bv::SatSolverMode solver) { + switch(solver) { + case theory::bv::SAT_SOLVER_MINISAT: + out << "SAT_SOLVER_MINISAT"; + break; + case theory::bv::SAT_SOLVER_CRYPTOMINISAT: + out << "SAT_SOLVER_CRYPTOMINISAT"; + break; + default: + out << "SatSolverMode:UNKNOWN![" << unsigned(solver) << "]"; + } + + return out; +} + }/* CVC4 namespace */ diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h index 4c8c4f626..3a6474104 100644 --- a/src/options/bv_bitblast_mode.h +++ b/src/options/bv_bitblast_mode.h @@ -60,12 +60,19 @@ enum BvSlicerMode { };/* enum BvSlicerMode */ +/** Enumeration of sat solvers that can be used. */ +enum SatSolverMode { + SAT_SOLVER_MINISAT, + SAT_SOLVER_CRYPTOMINISAT, +};/* enum SatSolver */ + }/* CVC4::theory::bv namespace */ }/* CVC4::theory namespace */ std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode); std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode); +std::ostream& operator<<(std::ostream& out, theory::bv::SatSolverMode mode); }/* CVC4 namespace */ diff --git a/src/options/bv_options b/src/options/bv_options index 8edc809e3..2e6fa2e7a 100644 --- a/src/options/bv_options +++ b/src/options/bv_options @@ -7,6 +7,9 @@ module BV "options/bv_options.h" Bitvector theory # Option to set the bit-blasting mode (lazy, eager) +expert-option bvSatSolver bv-sat-solver --bv-sat-solver=MODE CVC4::theory::bv::SatSolverMode :predicate satSolverEnabledBuild :handler stringToSatSolver :default CVC4::theory::bv::SAT_SOLVER_MINISAT :read-write :include "options/bv_bitblast_mode.h" + choose which sat solver to use, see --bv-sat-solver=help + option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :handler stringToBitblastMode :default CVC4::theory::bv::BITBLAST_MODE_LAZY :read-write :include "options/bv_bitblast_mode.h" choose bitblasting mode, see --bitblast=help diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 867feef6e..6a5f6cd39 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -821,6 +821,72 @@ void OptionsHandler::abcEnabledBuild(std::string option, std::string value) thro #endif /* CVC4_USE_ABC */ } +void OptionsHandler::satSolverEnabledBuild(std::string option, + bool value) throw(OptionException) { +#ifndef CVC4_USE_CRYPTOMINISAT + if(value) { + std::stringstream ss; + ss << "option `" << option << "' requires an cryptominisat-enabled build of CVC4; this binary was not built with cryptominisat support"; + throw OptionException(ss.str()); + } +#endif /* CVC4_USE_CRYPTOMINISAT */ +} + +void OptionsHandler::satSolverEnabledBuild(std::string option, + std::string value) throw(OptionException) { +#ifndef CVC4_USE_CRYPTOMINISAT + if(!value.empty()) { + std::stringstream ss; + ss << "option `" << option << "' requires an cryptominisat-enabled build of CVC4; this binary was not built with cryptominisat support"; + throw OptionException(ss.str()); + } +#endif /* CVC4_USE_CRYPTOMINISAT */ +} + +const std::string OptionsHandler::s_bvSatSolverHelp = "\ +Sat solvers currently supported by the --bv-sat-solver option:\n\ +\n\ +minisat (default)\n\ +\n\ +cryptominisat\n\ +"; + +theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option, + std::string optarg) throw(OptionException) { + if(optarg == "minisat") { + return theory::bv::SAT_SOLVER_MINISAT; + } else if(optarg == "cryptominisat") { + + if (options::incrementalSolving() && + options::incrementalSolving.wasSetByUser()) { + throw OptionException(std::string("Cryptominsat does not support incremental mode. \n\ + Try --bv-sat-solver=minisat")); + } + + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY && + options::bitblastMode.wasSetByUser()) { + throw OptionException(std::string("Cryptominsat does not support lazy bit-blsating. \n\ + Try --bv-sat-solver=minisat")); + } + if (!options::bitvectorToBool.wasSetByUser()) { + options::bitvectorToBool.set(true); + } + + // if (!options::bvAbstraction.wasSetByUser() && + // !options::skolemizeArguments.wasSetByUser()) { + // options::bvAbstraction.set(true); + // options::skolemizeArguments.set(true); + // } + return theory::bv::SAT_SOLVER_CRYPTOMINISAT; + } else if(optarg == "help") { + puts(s_bvSatSolverHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --bv-sat-solver: `") + + optarg + "'. Try --bv-sat-solver=help."); + } +} + const std::string OptionsHandler::s_bitblastingModeHelp = "\ Bit-blasting modes currently supported by the --bitblast option:\n\ \n\ diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 8f23219eb..5db2887c0 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -107,10 +107,15 @@ public: // theory/bv/options_handlers.h void abcEnabledBuild(std::string option, bool value) throw(OptionException); void abcEnabledBuild(std::string option, std::string value) throw(OptionException); + void satSolverEnabledBuild(std::string option, bool value) throw(OptionException); + void satSolverEnabledBuild(std::string option, std::string optarg) throw(OptionException); + theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg) throw(OptionException); theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException); void setBitblastAig(std::string option, bool arg) throw(OptionException); + theory::bv::SatSolverMode stringToSatSolver(std::string option, std::string optarg) throw(OptionException); + // theory/booleans/options_handlers.h theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException); @@ -193,6 +198,7 @@ public: /* Help strings */ static const std::string s_bitblastingModeHelp; + static const std::string s_bvSatSolverHelp; static const std::string s_booleanTermConversionModeHelp; static const std::string s_bvSlicerModeHelp; static const std::string s_cegqiFairModeHelp; diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 20724efd2..56a7c61e2 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -78,6 +78,10 @@ public: ClauseId addClause(SatClause& clause, bool removable); + ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) { + Unreachable("Minisat does not support native XOR reasoning"); + } + SatValue propagate(); SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp new file mode 100644 index 000000000..d8f25a786 --- /dev/null +++ b/src/prop/cryptominisat.cpp @@ -0,0 +1,230 @@ +/********************* */ +/*! \file cryptominisat.cpp + ** \verbatim + ** Original author: lianah + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2014 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief SAT Solver. + ** + ** Implementation of the cryptominisat for cvc4 (bitvectors). + **/ + +#include "prop/cryptominisat.h" + +#include "proof/clause_id.h" +#include "proof/sat_proof.h" + +using namespace CVC4; +using namespace prop; + +#ifdef CVC4_USE_CRYPTOMINISAT + +CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry, + const std::string& name) +: d_solver(new CMSat::SATSolver()) +, d_numVariables(0) +, d_okay(true) +, d_statistics(registry, name) +{ + d_true = newVar(); + d_false = newVar(); + + std::vector<CMSat::Lit> clause(1); + clause[0] = CMSat::Lit(d_true, false); + d_solver->add_clause(clause); + + clause[0] = CMSat::Lit(d_false, true); + d_solver->add_clause(clause); +} + + +CryptoMinisatSolver::~CryptoMinisatSolver() throw(AssertionException) { + delete d_solver; +} + +ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause, + bool rhs, + bool removable) { + Debug("sat::cryptominisat") << "Add xor clause " << clause <<" = " << rhs << "\n"; + + if (!d_okay) { + Debug("sat::cryptominisat") << "Solver unsat: not adding clause.\n"; + return ClauseIdError; + } + + ++(d_statistics.d_xorClausesAdded); + + // ensure all sat literals have positive polarity by pushing + // the negation on the result + std::vector<CMSat::Var> xor_clause; + for (unsigned i = 0; i < clause.size(); ++i) { + xor_clause.push_back(toInternalLit(clause[i]).var()); + rhs ^= clause[i].isNegated(); + } + bool res = d_solver->add_xor_clause(xor_clause, rhs); + d_okay &= res; + return ClauseIdError; +} + +ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){ + Debug("sat::cryptominisat") << "Add clause " << clause <<"\n"; + + if (!d_okay) { + Debug("sat::cryptominisat") << "Solver unsat: not adding clause.\n"; + return ClauseIdError; + } + + ++(d_statistics.d_clausesAdded); + + std::vector<CMSat::Lit> internal_clause; + toInternalClause(clause, internal_clause); + bool res = d_solver->add_clause(internal_clause); + d_okay &= res; + return ClauseIdError; +} + +bool CryptoMinisatSolver::ok() const { + return d_okay; +} + + +SatVariable CryptoMinisatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){ + d_solver->new_var(); + ++d_numVariables; + Assert (d_numVariables == d_solver->nVars()); + return d_numVariables - 1; +} + +SatVariable CryptoMinisatSolver::trueVar() { + return d_true; +} + +SatVariable CryptoMinisatSolver::falseVar() { + return d_false; +} + +void CryptoMinisatSolver::markUnremovable(SatLiteral lit) { + // cryptominisat supports dynamically adding back variables (?) + // so this is a no-op + return; +} + +void CryptoMinisatSolver::interrupt(){ + d_solver->interrupt_asap(); +} + +SatValue CryptoMinisatSolver::solve(){ + TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime); + ++d_statistics.d_statCallsToSolve; + return toSatLiteralValue(d_solver->solve()); +} + +SatValue CryptoMinisatSolver::solve(long unsigned int& resource) { + // CMSat::SalverConf conf = d_solver->getConf(); + Unreachable("Not sure how to set different limits for calls to solve in Cryptominisat"); + return solve(); +} + +SatValue CryptoMinisatSolver::value(SatLiteral l){ + const std::vector<CMSat::lbool> model = d_solver->get_model(); + CMSat::Var var = l.getSatVariable(); + Assert (var < model.size()); + CMSat::lbool value = model[var]; + return toSatLiteralValue(value); +} + +SatValue CryptoMinisatSolver::modelValue(SatLiteral l){ + return value(l); +} + +unsigned CryptoMinisatSolver::getAssertionLevel() const { + Unreachable("No interface to get assertion level in Cryptominisat"); + return -1; +} + +// converting from internal sat solver representation + +SatVariable CryptoMinisatSolver::toSatVariable(CMSat::Var var) { + if (var == CMSat::var_Undef) { + return undefSatVariable; + } + return SatVariable(var); +} + +CMSat::Lit CryptoMinisatSolver::toInternalLit(SatLiteral lit) { + if (lit == undefSatLiteral) { + return CMSat::lit_Undef; + } + return CMSat::Lit(lit.getSatVariable(), lit.isNegated()); +} + +SatLiteral CryptoMinisatSolver::toSatLiteral(CMSat::Lit lit) { + Assert (lit != CMSat::lit_Error); + if (lit == CMSat::lit_Undef) { + return undefSatLiteral; + } + + return SatLiteral(SatVariable(lit.var()), + lit.sign()); +} + +SatValue CryptoMinisatSolver::toSatLiteralValue(CMSat::lbool res) { + if(res == CMSat::l_True) return SAT_VALUE_TRUE; + if(res == CMSat::l_Undef) return SAT_VALUE_UNKNOWN; + Assert(res == CMSat::l_False); + return SAT_VALUE_FALSE; +} + +void CryptoMinisatSolver::toInternalClause(SatClause& clause, + std::vector<CMSat::Lit>& internal_clause) { + for (unsigned i = 0; i < clause.size(); ++i) { + internal_clause.push_back(toInternalLit(clause[i])); + } + Assert(clause.size() == internal_clause.size()); +} + +void CryptoMinisatSolver::toSatClause(std::vector<CMSat::Lit>& clause, + SatClause& sat_clause) { + for (unsigned i = 0; i < clause.size(); ++i) { + sat_clause.push_back(toSatLiteral(clause[i])); + } + Assert(clause.size() == sat_clause.size()); +} + + +// Satistics for CryptoMinisatSolver + +CryptoMinisatSolver::Statistics::Statistics(StatisticsRegistry* registry, + const std::string& prefix) : + d_registry(registry), + d_statCallsToSolve("theory::bv::"+prefix+"::cryptominisat::calls_to_solve", 0), + d_xorClausesAdded("theory::bv::"+prefix+"::cryptominisat::xor_clauses", 0), + d_clausesAdded("theory::bv::"+prefix+"::cryptominisat::clauses", 0), + d_solveTime("theory::bv::"+prefix+"::cryptominisat::solve_time"), + d_registerStats(!prefix.empty()) +{ + if (!d_registerStats) + return; + + d_registry->registerStat(&d_statCallsToSolve); + d_registry->registerStat(&d_xorClausesAdded); + d_registry->registerStat(&d_clausesAdded); + d_registry->registerStat(&d_solveTime); +} + +CryptoMinisatSolver::Statistics::~Statistics() { + if (!d_registerStats) + return; + d_registry->unregisterStat(&d_statCallsToSolve); + d_registry->unregisterStat(&d_xorClausesAdded); + d_registry->unregisterStat(&d_clausesAdded); + d_registry->unregisterStat(&d_solveTime); +} +#endif diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h new file mode 100644 index 000000000..29f8b7a2a --- /dev/null +++ b/src/prop/cryptominisat.h @@ -0,0 +1,137 @@ +/********************* */ +/*! \file cryptominisat.h + ** \verbatim + ** Original author: lianah + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2014 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief SAT Solver. + ** + ** Implementation of the cryptominisat sat solver for cvc4 (bitvectors). + **/ + +#include "cvc4_private.h" + +#pragma once + +#include "prop/sat_solver.h" + +#ifdef CVC4_USE_CRYPTOMINISAT +#include <cryptominisat4/cryptominisat.h> +namespace CVC4 { +namespace prop { + +class CryptoMinisatSolver : public SatSolver { + +private: + CMSat::SATSolver* d_solver; + unsigned d_numVariables; + bool d_okay; + SatVariable d_true; + SatVariable d_false; +public: + CryptoMinisatSolver(StatisticsRegistry* registry, + const std::string& name = ""); + ~CryptoMinisatSolver() throw(AssertionException); + + ClauseId addClause(SatClause& clause, bool removable); + ClauseId addXorClause(SatClause& clause, bool rhs, bool removable); + + bool nativeXor() { return true; } + + SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); + + SatVariable trueVar(); + SatVariable falseVar(); + + void markUnremovable(SatLiteral lit); + + void interrupt(); + + SatValue solve(); + SatValue solve(long unsigned int&); + bool ok() const; + SatValue value(SatLiteral l); + SatValue modelValue(SatLiteral l); + + unsigned getAssertionLevel() const; + + + // helper methods for converting from the internal Minisat representation + + static SatVariable toSatVariable(CMSat::Var var); + static CMSat::Lit toInternalLit(SatLiteral lit); + static SatLiteral toSatLiteral(CMSat::Lit lit); + static SatValue toSatLiteralValue(bool res); + static SatValue toSatLiteralValue(CMSat::lbool res); + + static void toInternalClause(SatClause& clause, std::vector<CMSat::Lit>& internal_clause); + static void toSatClause (std::vector<CMSat::Lit>& clause, SatClause& sat_clause); + + class Statistics { + public: + StatisticsRegistry* d_registry; + IntStat d_statCallsToSolve; + IntStat d_xorClausesAdded; + IntStat d_clausesAdded; + TimerStat d_solveTime; + bool d_registerStats; + Statistics(StatisticsRegistry* registry, + const std::string& prefix); + ~Statistics(); + }; + + Statistics d_statistics; +}; +} // CVC4::prop +} // CVC4 + +#else // CVC4_USE_CRYPTOMINISAT + +namespace CVC4 { +namespace prop { + +class CryptoMinisatSolver : public SatSolver { + +public: + CryptoMinisatSolver(const std::string& name = "") { Unreachable(); } + /** Assert a clause in the solver. */ + ClauseId addClause(SatClause& clause, bool removable) { + Unreachable(); + } + + /** Return true if the solver supports native xor resoning */ + bool nativeXor() { Unreachable(); } + + /** Add a clause corresponding to rhs = l1 xor .. xor ln */ + ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) { + Unreachable(); + } + + SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase) { Unreachable(); } + SatVariable trueVar() { Unreachable(); } + SatVariable falseVar() { Unreachable(); } + SatValue solve() { Unreachable(); } + SatValue solve(long unsigned int&) { Unreachable(); } + void interrupt() { Unreachable(); } + SatValue value(SatLiteral l) { Unreachable(); } + SatValue modelValue(SatLiteral l) { Unreachable(); } + unsigned getAssertionLevel() const { Unreachable(); } + bool ok() const { return false;}; + + +};/* class CryptoMinisatSolver */ +} // CVC4::prop +} // CVC4 + +#endif // CVC4_USE_CRYPTOMINISAT + + + + diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 535ce1a47..ec5297bb7 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -44,6 +44,9 @@ public: void initialize(context::Context* context, TheoryProxy* theoryProxy); ClauseId addClause(SatClause& clause, bool removable); + ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) { + Unreachable("Minisat does not support native XOR reasoning"); + } SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase); SatVariable trueVar() { return d_minisat->trueVar(); } diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 92696ae25..81fb94242 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -49,6 +49,12 @@ public: virtual ClauseId addClause(SatClause& clause, bool removable) = 0; + /** Return true if the solver supports native xor resoning */ + virtual bool nativeXor() { return false; } + + /** Add a clause corresponding to rhs = l1 xor .. xor ln */ + virtual ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) = 0; + /** * Create a new boolean variable in the solver. * @param isTheoryAtom is this a theory atom that needs to be asserted to theory @@ -84,7 +90,8 @@ public: /** Check if the solver is in an inconsistent state */ virtual bool ok() const = 0; - + + virtual void setProofLog( BitVectorProof * bvp ) {} };/* class SatSolver */ diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 092ec72f2..7fdc44e66 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -16,6 +16,7 @@ #include "prop/sat_solver_factory.h" +#include "prop/cryptominisat.h" #include "prop/minisat/minisat.h" #include "prop/bvminisat/bvminisat.h" @@ -26,6 +27,12 @@ BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatC return new BVMinisatSatSolver(registry, mainSatContext, name); } +SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry, + const std::string& name) { +return new CryptoMinisatSolver(registry, name); +} + + DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(StatisticsRegistry* registry) { return new MinisatSatSolver(registry); } diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index 7cc23a8e8..a04bcaaf4 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -35,6 +35,8 @@ public: StatisticsRegistry* registry, const std::string& name = ""); static DPLLSatSolverInterface* createDPLLMinisat(StatisticsRegistry* registry); + static SatSolver* createCryptoMinisat(StatisticsRegistry* registry, + const std::string& name = ""); };/* class SatSolverFactory */ 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() { diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 5fdc549d0..f9f5361d3 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -257,7 +257,7 @@ public: class EagerBitblaster : public TBitblaster<Node> { typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; // sat solver used for bitblasting and associated CnfStream - prop::BVSatSolverInterface* d_satSolver; + prop::SatSolver* d_satSolver; BitblastingRegistrar* d_bitblastingRegistrar; context::Context* d_nullContext; prop::CnfStream* d_cnfStream; 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; } |