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/prop | |
parent | beaf8b212dfadb47328942c23a7649ab44a014cb (diff) |
Merged cryptominisat from experimental branch.
Diffstat (limited to 'src/prop')
-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 |
7 files changed, 391 insertions, 1 deletions
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 */ |