Merged cryptominisat from experimental branch.

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 */