Refactored CnfStream to work with the bv theory Bitblaster:

    * separated SatSolverInput interface class into two classes:
           - TheoryProxy for the sat solver to communicate with the theories
           - SatSolverInterface abstract class to communicate with the sat solver
    * instead of using #ifdef typedef for SatClauses and SatLiterals, now there are CVC4 SatLiteral/SatClause types and mappings between them and the internal sat solver clause/literal representation
    * added abstract classes for DPLLSatSolver and BVSatSolver different interfaces 

Replaced TheoryBV with bitblasting implementation:
    * all operators bitblasted
    * only operator elimination rewrite rules so far
  

1 files changed, 33 insertions, 270 deletions

diff --git a/src/prop/sat.h b/src/prop/sat.h
index 3f3166c14..a6bdcb309 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -29,6 +29,8 @@
 #include "util/options.h"
 #include "util/stats.h"
 
+#include "prop/sat_module.h"
+
 #ifdef __CVC4_USE_MINISAT
 
 #include "prop/minisat/core/Solver.h"
@@ -48,82 +50,10 @@ class CnfStream;
 
 /* Definitions of abstract types and conversion functions for SAT interface */
 
-#ifdef __CVC4_USE_MINISAT
-
-/** Type of the SAT variables */
-typedef Minisat::Var SatVariable;
-
-/** Type of the SAT literals */
-typedef Minisat::Lit SatLiteral;
-
-/** Type of the SAT clauses */
-typedef Minisat::vec<SatLiteral> SatClause;
-
-/** Type of a SAT variable assignment (T, F, unknown) */
-typedef Minisat::lbool SatLiteralValue;
-
 /**
- * Returns the variable of the literal.
- * @param lit the literal
+ * The proxy class that allows the SatSolver to communicate with the theories
  */
-inline SatVariable literalToVariable(SatLiteral lit) {
-  return Minisat::var(lit);
-}
-
-inline SatLiteral variableToLiteral(SatVariable var) {
-  return Minisat::mkLit(var);
-}
-
-inline bool literalSign(SatLiteral lit) {
-  return Minisat::sign(lit);
-}
-
-static inline size_t
-hashSatLiteral(const SatLiteral& literal) {
-  return (size_t) Minisat::toInt(literal);
-}
-
-inline std::string stringOfLiteralValue(SatLiteralValue val) {
-  if( val == l_False ) {
-    return "0";
-  } else if (val == l_True ) {
-    return "1";
-  } else { // unknown
-    return "_";
-  }
-}
-#endif /* __CVC4_USE_MINISAT */
-
-/** Interface encapsulating the "input" to the solver, e.g., from the
- * CNF converter.
- *
- * TODO: Is it possible to push the typedefs of SatClause and SatVariable
- * into here, somehow?
- */
-class SatInputInterface {
-public:
-  /** Virtual destructor to make g++ happy */
-  virtual ~SatInputInterface() { }
-  /** Assert a clause in the solver. */
-  virtual void addClause(SatClause& clause, bool removable) = 0;
-  /** Create a new boolean variable in the solver. */
-  virtual SatVariable newVar(bool theoryAtom = false) = 0;
-  /** Get the current user assertion level of the solver */
-  virtual int getAssertionLevel() const = 0;
-  /** Unregister the variable (of the literal) from solving */
-  virtual void unregisterVar(SatLiteral lit) = 0;
-  /** Register the variable (of the literal) for solving */
-  virtual void renewVar(SatLiteral lit, int level = -1) = 0;
-  /** Interrupt the solver */
-  virtual void interrupt() = 0;
-};
-
-/**
- * The proxy class that allows us to modify the internals of the SAT solver.
- * It's only accessible from the PropEngine, and should be treated with major
- * care.
- */
-class SatSolver : public SatInputInterface {
+class TheoryProxy {
 
   /** The prop engine we are using */
   PropEngine* d_propEngine;
@@ -143,96 +73,20 @@ class SatSolver : public SatInputInterface {
    */
   std::hash_set<Node, NodeHashFunction> d_shared;
 
-  /* Pointer to the concrete SAT solver. Including this via the
-     preprocessor saves us a level of indirection vs, e.g., defining a
-     sub-class for each solver. */
-
-#ifdef __CVC4_USE_MINISAT
-
-  /** Minisat solver */
-  Minisat::SimpSolver* d_minisat;
-
-  class Statistics {
-  private:
-    ReferenceStat<uint64_t> d_statStarts, d_statDecisions;
-    ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations;
-    ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals;
-    ReferenceStat<uint64_t> d_statLearntsLiterals,  d_statMaxLiterals;
-    ReferenceStat<uint64_t> d_statTotLiterals;
-  public:
-    Statistics() :
-      d_statStarts("sat::starts"),
-      d_statDecisions("sat::decisions"),
-      d_statRndDecisions("sat::rnd_decisions"),
-      d_statPropagations("sat::propagations"),
-      d_statConflicts("sat::conflicts"),
-      d_statClausesLiterals("sat::clauses_literals"),
-      d_statLearntsLiterals("sat::learnts_literals"),
-      d_statMaxLiterals("sat::max_literals"),
-      d_statTotLiterals("sat::tot_literals")
-    {
-      StatisticsRegistry::registerStat(&d_statStarts);
-      StatisticsRegistry::registerStat(&d_statDecisions);
-      StatisticsRegistry::registerStat(&d_statRndDecisions);
-      StatisticsRegistry::registerStat(&d_statPropagations);
-      StatisticsRegistry::registerStat(&d_statConflicts);
-      StatisticsRegistry::registerStat(&d_statClausesLiterals);
-      StatisticsRegistry::registerStat(&d_statLearntsLiterals);
-      StatisticsRegistry::registerStat(&d_statMaxLiterals);
-      StatisticsRegistry::registerStat(&d_statTotLiterals);
-    }
-    ~Statistics() {
-      StatisticsRegistry::unregisterStat(&d_statStarts);
-      StatisticsRegistry::unregisterStat(&d_statDecisions);
-      StatisticsRegistry::unregisterStat(&d_statRndDecisions);
-      StatisticsRegistry::unregisterStat(&d_statPropagations);
-      StatisticsRegistry::unregisterStat(&d_statConflicts);
-      StatisticsRegistry::unregisterStat(&d_statClausesLiterals);
-      StatisticsRegistry::unregisterStat(&d_statLearntsLiterals);
-      StatisticsRegistry::unregisterStat(&d_statMaxLiterals);
-      StatisticsRegistry::unregisterStat(&d_statTotLiterals);
-    }
-    void init(Minisat::SimpSolver* d_minisat){
-      d_statStarts.setData(d_minisat->starts);
-      d_statDecisions.setData(d_minisat->decisions);
-      d_statRndDecisions.setData(d_minisat->rnd_decisions);
-      d_statPropagations.setData(d_minisat->propagations);
-      d_statConflicts.setData(d_minisat->conflicts);
-      d_statClausesLiterals.setData(d_minisat->clauses_literals);
-      d_statLearntsLiterals.setData(d_minisat->learnts_literals);
-      d_statMaxLiterals.setData(d_minisat->max_literals);
-      d_statTotLiterals.setData(d_minisat->tot_literals);
-    }
-  };
-  Statistics d_statistics;
-
-#endif /* __CVC4_USE_MINISAT */
-
-protected:
-
 public:
-  /** Hash function for literals */
-  struct SatLiteralHashFunction {
-    inline size_t operator()(const SatLiteral& literal) const;
-  };
-
-  SatSolver(PropEngine* propEngine,
-            TheoryEngine* theoryEngine,
-            context::Context* context);
-
-  virtual ~SatSolver();
+  TheoryProxy(PropEngine* propEngine,
+              TheoryEngine* theoryEngine,
+              context::Context* context,
+              CnfStream* cnfStream);
 
-  SatLiteralValue solve(unsigned long& resource);
+  ~TheoryProxy();
 
-  void addClause(SatClause& clause, bool removable);
-
-  SatVariable newVar(bool theoryAtom = false);
 
   void theoryCheck(theory::Theory::Effort effort);
 
   void explainPropagation(SatLiteral l, SatClause& explanation);
 
-  void theoryPropagate(std::vector<SatLiteral>& output);
+  void theoryPropagate(SatClause& output);
 
   void enqueueTheoryLiteral(const SatLiteral& l);
 
@@ -240,20 +94,6 @@ public:
 
   bool theoryNeedCheck() const;
 
-  void setCnfStream(CnfStream* cnfStream);
-
-  /** Call value() during the search.*/
-  SatLiteralValue value(SatLiteral l);
-
-  /** Call modelValue() when the search is done.*/
-  SatLiteralValue modelValue(SatLiteral l);
-
-  int getAssertionLevel() const;
-
-  void push();
-
-  void pop();
-
   void removeClausesAboveLevel(int level);
 
   /**
@@ -265,8 +105,6 @@ public:
 
   void renewVar(SatLiteral lit, int level = -1);
 
-  void interrupt();
-
   TNode getNode(SatLiteral lit);
 
   void notifyRestart();
@@ -283,114 +121,26 @@ public:
 
 /* Functions that delegate to the concrete SAT solver. */
 
-#ifdef __CVC4_USE_MINISAT
-
-inline SatSolver::SatSolver(PropEngine* propEngine,
-                            TheoryEngine* theoryEngine,
-                            context::Context* context) :
+inline TheoryProxy::TheoryProxy(PropEngine* propEngine,
+                                TheoryEngine* theoryEngine,
+                                context::Context* context,
+                                CnfStream* cnfStream) :
   d_propEngine(propEngine),
-  d_cnfStream(NULL),
+  d_cnfStream(cnfStream),
   d_theoryEngine(theoryEngine),
-  d_context(context),
-  d_statistics()
-{
-  // Create the solver
-  d_minisat = new Minisat::SimpSolver(this, d_context,
-                                      Options::current()->incrementalSolving);
-  // Setup the verbosity
-  d_minisat->verbosity = (Options::current()->verbosity > 0) ? 1 : -1;
-
-  // Setup the random decision parameters
-  d_minisat->random_var_freq = Options::current()->satRandomFreq;
-  d_minisat->random_seed = Options::current()->satRandomSeed;
-
-  // Give access to all possible options in the sat solver
-  d_minisat->var_decay = Options::current()->satVarDecay;
-  d_minisat->clause_decay = Options::current()->satClauseDecay;
-  d_minisat->restart_first = Options::current()->satRestartFirst;
-  d_minisat->restart_inc = Options::current()->satRestartInc;
-
-  d_statistics.init(d_minisat);
-}
-
-inline SatSolver::~SatSolver() {
-  delete d_minisat;
-}
-
-inline SatLiteralValue SatSolver::solve(unsigned long& resource) {
-  Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
-  if(resource == 0) {
-    d_minisat->budgetOff();
-  } else {
-    d_minisat->setConfBudget(resource);
-  }
-  Minisat::vec<SatLiteral> empty;
-  unsigned long conflictsBefore = d_minisat->conflicts;
-  SatLiteralValue result = d_minisat->solveLimited(empty);
-  d_minisat->clearInterrupt();
-  resource = d_minisat->conflicts - conflictsBefore;
-  Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl;
-  return result;
-}
-
-inline void SatSolver::addClause(SatClause& clause, bool removable) {
-  d_minisat->addClause(clause, removable);
-}
-
-inline SatVariable SatSolver::newVar(bool theoryAtom) {
-  return d_minisat->newVar(true, true, theoryAtom);
-}
-
-inline SatLiteralValue SatSolver::value(SatLiteral l) {
-  return d_minisat->value(l);
-}
-
-inline SatLiteralValue SatSolver::modelValue(SatLiteral l) {
-  return d_minisat->modelValue(l);
-}
-
-inline void SatSolver::push() {
-  d_minisat->push();
-}
-
-inline void SatSolver::pop() {
-  d_minisat->pop();
-}
-
-inline int SatSolver::getAssertionLevel() const {
-  return d_minisat->getAssertionLevel();
-}
-
-inline void SatSolver::unregisterVar(SatLiteral lit) {
-  d_minisat->unregisterVar(lit);
-}
-
-inline void SatSolver::renewVar(SatLiteral lit, int level) {
-  d_minisat->renewVar(lit, level);
-}
-
-inline void SatSolver::interrupt() {
-  d_minisat->interrupt();
-}
-
-#endif /* __CVC4_USE_MINISAT */
-
-inline size_t
-SatSolver::SatLiteralHashFunction::operator()(const SatLiteral& literal) const {
-  return hashSatLiteral(literal);
-}
+  d_context(context)
+{}
 
 }/* CVC4::prop namespace */
 
 inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
-  const char * s = (prop::literalSign(lit)) ? "~" : " ";
-  out << s << prop::literalToVariable(lit);
+  out << lit.toString(); 
   return out;
 }
 
 inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) {
   out << "clause:";
-  for(int i = 0; i < clause.size(); ++i) {
+  for(unsigned i = 0; i < clause.size(); ++i) {
     out << " " << clause[i];
   }
   out << ";";
@@ -398,10 +148,23 @@ inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& claus
 }
 
 inline std::ostream& operator <<(std::ostream& out, prop::SatLiteralValue val) {
-  out << prop::stringOfLiteralValue(val);
+  std::string str; 
+  switch(val) {
+  case prop::SatValUnknown:
+    str = "_";
+  case prop::SatValTrue:
+    str = "1";
+  case prop::SatValFalse:
+    str = "0";
+  default:
+    str = "Error"; 
+
+  out << str;
   return out;
 }
 
+} /* prop namespace */
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PROP__SAT_H */