summaryrefslogtreecommitdiff
path: root/src/prop/cryptominisat.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/cryptominisat.cpp')
-rw-r--r--src/prop/cryptominisat.cpp230
1 files changed, 230 insertions, 0 deletions
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback