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
  

19 files changed, 110 insertions, 67 deletions

diff --git a/src/prop/minisat/core/Dimacs.h b/src/prop/minisat/core/Dimacs.h
index a05e900c1..6bd19fb5b 100644
--- a/src/prop/minisat/core/Dimacs.h
+++ b/src/prop/minisat/core/Dimacs.h
@@ -23,8 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include <stdio.h>
 
-#include "utils/ParseUtils.h"
-#include "core/SolverTypes.h"
+#include "prop/minisat/utils/ParseUtils.h"
+#include "prop/minisat/core/SolverTypes.h"
 
 namespace Minisat {
 
diff --git a/src/prop/minisat/core/Main.cc b/src/prop/minisat/core/Main.cc
index 4388c3e08..de73b7327 100644
--- a/src/prop/minisat/core/Main.cc
+++ b/src/prop/minisat/core/Main.cc
@@ -23,11 +23,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <signal.h>
 #include <zlib.h>
 
-#include "utils/System.h"
-#include "utils/ParseUtils.h"
-#include "utils/Options.h"
-#include "core/Dimacs.h"
-#include "core/Solver.h"
+#include "prop/minisat/utils/System.h"
+#include "prop/minisat/utils/ParseUtils.h"
+#include "prop/minisat/utils/Options.h"
+#include "prop/minisat/core/Dimacs.h"
+#include "prop/minisat/core/Solver.h"
 
 using namespace Minisat;
 
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index cdab47163..3fe9db10c 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -22,10 +22,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include <iostream>
 
-#include "mtl/Sort.h"
-#include "core/Solver.h"
+#include "prop/minisat/mtl/Sort.h"
+#include "prop/minisat/core/Solver.h"
 
 #include "prop/sat.h"
+#include "prop/sat_module.h"
 #include "util/output.h"
 #include "expr/command.h"
 #include "proof/proof_manager.h"
@@ -71,7 +72,7 @@ public:
 //=================================================================================================
 // Constructor/Destructor:
 
-Solver::Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bool enable_incremental) :
+Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enable_incremental) :
     proxy(proxy)
   , context(context)
   , assertionLevel(0)
@@ -177,8 +178,10 @@ CRef Solver::reason(Var x) {
     Lit l = mkLit(x, value(x) != l_True);
 
     // Get the explanation from the theory
-    SatClause explanation;
-    proxy->explainPropagation(l, explanation);
+    SatClause explanation_cl;
+    proxy->explainPropagation(DPLLMinisatSatSolver::toSatLiteral(l), explanation_cl);
+    vec<Lit> explanation;
+    DPLLMinisatSatSolver::toMinisatClause(explanation_cl, explanation); 
 
     // Sort the literals by trail index level
     lemma_lt lt(*this);
@@ -340,7 +343,7 @@ void Solver::cancelUntil(int level) {
         int currentLevel = decisionLevel();
         for(int i = variables_to_register.size() - 1; i >= 0 && variables_to_register[i].level > currentLevel; --i) {
           variables_to_register[i].level = currentLevel;
-          proxy->variableNotify(variables_to_register[i].var);
+          proxy->variableNotify(DPLLMinisatSatSolver::toSatVariable(variables_to_register[i].var));
         }
     }
 }
@@ -358,14 +361,15 @@ Lit Solver::pickBranchLit()
     Lit nextLit;
 
 #ifdef CVC4_REPLAY
-    nextLit = proxy->getNextReplayDecision();
+    nextLit = DPLLMinisatSatSolver::toMinisatLit(proxy->getNextReplayDecision());
+
     if (nextLit != lit_Undef) {
       return nextLit;
     }
 #endif /* CVC4_REPLAY */
 
     // Theory requests
-    nextLit = proxy->getNextDecisionRequest();
+    nextLit = DPLLMinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest());
     while (nextLit != lit_Undef) {
       if(value(var(nextLit)) == l_Undef) {
         Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl;
@@ -373,7 +377,7 @@ Lit Solver::pickBranchLit()
       } else {
         Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl;
       }
-      nextLit = proxy->getNextDecisionRequest();
+      nextLit = DPLLMinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest());
     }
 
     Var next = var_Undef;
@@ -638,7 +642,7 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
     }
     if (theory[var(p)]) {
       // Enqueue to the theory
-      proxy->enqueueTheoryLiteral(p);
+      proxy->enqueueTheoryLiteral(DPLLMinisatSatSolver::toSatLiteral(p));
     }
 }
 
@@ -710,8 +714,13 @@ CRef Solver::propagate(TheoryCheckType type)
 }
 
 void Solver::propagateTheory() {
-  std::vector<Lit> propagatedLiterals;
-  proxy->theoryPropagate(propagatedLiterals);
+
+  SatClause propagatedLiteralsClause; 
+  proxy->theoryPropagate(propagatedLiteralsClause);
+  
+  vec<Lit> propagatedLiterals;
+  DPLLMinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals); 
+
   int oldTrailSize = trail.size();
   Debug("minisat") << "old trail size is " << oldTrailSize << ", propagating " << propagatedLiterals.size() << " lits..." << std::endl;
   for (unsigned i = 0, i_end = propagatedLiterals.size(); i < i_end; ++ i) {
@@ -1069,7 +1078,7 @@ lbool Solver::search(int nof_conflicts)
                 }
 
 #ifdef CVC4_REPLAY
-                proxy->logDecision(next);
+                proxy->logDecision(DPLLMinisatSatSolver::toSatLiteral(next));
 #endif /* CVC4_REPLAY */
             }
 
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index a3d449a36..426268b4b 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -25,11 +25,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include <iostream>
 
-#include "mtl/Vec.h"
-#include "mtl/Heap.h"
-#include "mtl/Alg.h"
-#include "utils/Options.h"
-#include "core/SolverTypes.h"
+#include "prop/minisat/mtl/Vec.h"
+#include "prop/minisat/mtl/Heap.h"
+#include "prop/minisat/mtl/Alg.h"
+#include "prop/minisat/utils/Options.h"
+#include "prop/minisat/core/SolverTypes.h"
 
 #include "context/context.h"
 #include "theory/theory.h"
@@ -40,7 +40,7 @@ namespace CVC4 {
 class SatProof;
 
 namespace prop {
-  class SatSolver;
+  class TheoryProxy;
 }/* CVC4::prop namespace */
 
 }/* CVC4 namespace */
@@ -53,22 +53,22 @@ namespace Minisat {
 class Solver {
 
   /** The only two CVC4 entry points to the private solver data */
-  friend class CVC4::prop::SatSolver;
+  friend class CVC4::prop::TheoryProxy;
   friend class CVC4::SatProof; 
 protected:
 
   /** The pointer to the proxy that provides interfaces to the SMT engine */
-  CVC4::prop::SatSolver* proxy;
+  CVC4::prop::TheoryProxy* proxy;
 
   /** The context from the SMT solver */
   CVC4::context::Context* context;
 
   /** The current assertion level (user) */
   int assertionLevel; 
-
+public:
   /** Returns the current user assertion level */
   int getAssertionLevel() const { return assertionLevel; }
-
+protected:
   /** Do we allow incremental solving */
   bool enable_incremental;  
 
@@ -102,7 +102,7 @@ public:
 
     // Constructor/Destructor:
     //
-    Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bool enableIncremental = false);
+    Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enableIncremental = false);
     CVC4_PUBLIC virtual ~Solver();
 
     // Problem specification:
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index 57ca95a41..85e1b9750 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -25,11 +25,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include <assert.h>
 #include "util/output.h"
-#include "mtl/IntTypes.h"
-#include "mtl/Alg.h"
-#include "mtl/Vec.h"
-#include "mtl/Map.h"
-#include "mtl/Alloc.h"
+#include "prop/minisat/mtl/IntTypes.h"
+#include "prop/minisat/mtl/Alg.h"
+#include "prop/minisat/mtl/Vec.h"
+#include "prop/minisat/mtl/Map.h"
+#include "prop/minisat/mtl/Alloc.h"
 
 namespace Minisat {
 
@@ -119,6 +119,40 @@ inline lbool toLbool(int   v) { return lbool((uint8_t)v);  }
 
 class Clause;
 typedef RegionAllocator<uint32_t>::Ref CRef;
+
+/* convenience printing functions */
+
+
+inline std::ostream& operator <<(std::ostream& out, Minisat::Lit lit) {
+  const char * s = (Minisat::sign(lit)) ? "~" : " ";
+  out << s << Minisat::var(lit);
+  return out;
+}
+
+inline std::ostream& operator <<(std::ostream& out, Minisat::vec<Minisat::Lit>& clause) {
+  out << "clause:";
+  for(int i = 0; i < clause.size(); ++i) {
+    out << " " << clause[i];
+  }
+  out << ";";
+  return out;
+}
+
+inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) {
+  std::string val_str; 
+  if( val == l_False ) {
+    val_str = "0";
+  } else if (val == l_True ) {
+    val_str = "1";
+  } else { // unknown
+    val_str = "_";
+  }
+
+  out << val_str;
+  return out;
+}
+
+
 } /* Minisat */
 
 
diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h
index bb1ee5ad2..6c3a18450 100644
--- a/src/prop/minisat/mtl/Alg.h
+++ b/src/prop/minisat/mtl/Alg.h
@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Alg_h
 #define Minisat_Alg_h
 
-#include "mtl/Vec.h"
+#include "prop/minisat/mtl/Vec.h"
 
 namespace Minisat {
 
diff --git a/src/prop/minisat/mtl/Alloc.h b/src/prop/minisat/mtl/Alloc.h
index 76322b8b6..71f9f7281 100644
--- a/src/prop/minisat/mtl/Alloc.h
+++ b/src/prop/minisat/mtl/Alloc.h
@@ -21,8 +21,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Alloc_h
 #define Minisat_Alloc_h
 
-#include "mtl/XAlloc.h"
-#include "mtl/Vec.h"
+#include "prop/minisat/mtl/XAlloc.h"
+#include "prop/minisat/mtl/Vec.h"
 
 namespace Minisat {
 
diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h
index 226407e77..5b9fb5822 100644
--- a/src/prop/minisat/mtl/Heap.h
+++ b/src/prop/minisat/mtl/Heap.h
@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Heap_h
 #define Minisat_Heap_h
 
-#include "mtl/Vec.h"
+#include "prop/minisat/mtl/Vec.h"
 
 namespace Minisat {
 
diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h
index 8a82d0e28..dda6c73d1 100644
--- a/src/prop/minisat/mtl/Map.h
+++ b/src/prop/minisat/mtl/Map.h
@@ -20,8 +20,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Map_h
 #define Minisat_Map_h
 
-#include "mtl/IntTypes.h"
-#include "mtl/Vec.h"
+#include "prop/minisat/mtl/IntTypes.h"
+#include "prop/minisat/mtl/Vec.h"
 
 namespace Minisat {
 
diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h
index 17567d694..2c818fcc9 100644
--- a/src/prop/minisat/mtl/Queue.h
+++ b/src/prop/minisat/mtl/Queue.h
@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Queue_h
 #define Minisat_Queue_h
 
-#include "mtl/Vec.h"
+#include "prop/minisat/mtl/Vec.h"
 
 namespace Minisat {
 
diff --git a/src/prop/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h
index e9313ef86..644c39789 100644
--- a/src/prop/minisat/mtl/Sort.h
+++ b/src/prop/minisat/mtl/Sort.h
@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Sort_h
 #define Minisat_Sort_h
 
-#include "mtl/Vec.h"
+#include "prop/minisat/mtl/Vec.h"
 
 //=================================================================================================
 // Some sorting algorithms for vec's
diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h
index 9e220852e..faf3c67f9 100644
--- a/src/prop/minisat/mtl/Vec.h
+++ b/src/prop/minisat/mtl/Vec.h
@@ -24,8 +24,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <assert.h>
 #include <new>
 
-#include "mtl/IntTypes.h"
-#include "mtl/XAlloc.h"
+#include "prop/minisat/mtl/IntTypes.h"
+#include "prop/minisat/mtl/XAlloc.h"
 
 namespace Minisat {
 
diff --git a/src/prop/minisat/simp/Main.cc b/src/prop/minisat/simp/Main.cc
index e59d73be0..ff0f589cd 100644
--- a/src/prop/minisat/simp/Main.cc
+++ b/src/prop/minisat/simp/Main.cc
@@ -24,11 +24,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <zlib.h>
 #include <sys/resource.h>
 
-#include "utils/System.h"
-#include "utils/ParseUtils.h"
-#include "utils/Options.h"
-#include "core/Dimacs.h"
-#include "simp/SimpSolver.h"
+#include "prop/minisat/utils/System.h"
+#include "prop/minisat/utils/ParseUtils.h"
+#include "prop/minisat/utils/Options.h"
+#include "prop/minisat/core/Dimacs.h"
+#include "prop/minisat/simp/SimpSolver.h"
 
 using namespace Minisat;
 
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 6045fc881..2b5468186 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -18,9 +18,9 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#include "mtl/Sort.h"
-#include "simp/SimpSolver.h"
-#include "utils/System.h"
+#include "prop/minisat/mtl/Sort.h"
+#include "prop/minisat/simp/SimpSolver.h"
+#include "prop/minisat/utils/System.h"
 #include "proof/proof.h"
 using namespace Minisat;
 using namespace CVC4;
@@ -44,7 +44,7 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of
 // Constructor/Destructor:
 
 
-SimpSolver::SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bool enableIncremental) :
+SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enableIncremental) :
     Solver(proxy, context, enableIncremental)
   , grow               (opt_grow)
   , clause_lim         (opt_clause_lim)
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 68ea6e463..97f5c2265 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -23,13 +23,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "cvc4_private.h"
 
-#include "mtl/Queue.h"
-#include "core/Solver.h"
+#include "prop/minisat/mtl/Queue.h"
+#include "prop/minisat/core/Solver.h"
 
 
 namespace CVC4 {
 namespace prop {
-  class SatSolver;
+  class TheoryProxy;
 }
 }
 
@@ -41,7 +41,7 @@ class SimpSolver : public Solver {
  public:
     // Constructor/Destructor:
     //
-    SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bool enableIncremental = false);
+    SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enableIncremental = false);
     CVC4_PUBLIC ~SimpSolver();
 
     // Problem specification:
diff --git a/src/prop/minisat/utils/Options.cc b/src/prop/minisat/utils/Options.cc
index ec5a6e930..94c6719c3 100644
--- a/src/prop/minisat/utils/Options.cc
+++ b/src/prop/minisat/utils/Options.cc
@@ -17,9 +17,9 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#include "mtl/Sort.h"
-#include "utils/Options.h"
-#include "utils/ParseUtils.h"
+#include "prop/minisat/mtl/Sort.h"
+#include "prop/minisat/utils/Options.h"
+#include "prop/minisat/utils/ParseUtils.h"
 
 using namespace Minisat;
 
diff --git a/src/prop/minisat/utils/Options.h b/src/prop/minisat/utils/Options.h
index 9c1f40699..d2611be94 100644
--- a/src/prop/minisat/utils/Options.h
+++ b/src/prop/minisat/utils/Options.h
@@ -25,9 +25,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <math.h>
 #include <string.h>
 
-#include "mtl/IntTypes.h"
-#include "mtl/Vec.h"
-#include "utils/ParseUtils.h"
+#include "prop/minisat/mtl/IntTypes.h"
+#include "prop/minisat/mtl/Vec.h"
+#include "prop/minisat/utils/ParseUtils.h"
 
 namespace Minisat {
 
diff --git a/src/prop/minisat/utils/System.cc b/src/prop/minisat/utils/System.cc
index a7cf53f55..5856e4897 100644
--- a/src/prop/minisat/utils/System.cc
+++ b/src/prop/minisat/utils/System.cc
@@ -18,7 +18,7 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#include "utils/System.h"
+#include "prop/minisat/utils/System.h"
 
 #if defined(__linux__)
 
diff --git a/src/prop/minisat/utils/System.h b/src/prop/minisat/utils/System.h
index 17581927a..f5381e568 100644
--- a/src/prop/minisat/utils/System.h
+++ b/src/prop/minisat/utils/System.h
@@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <fpu_control.h>
 #endif
 
-#include "mtl/IntTypes.h"
+#include "prop/minisat/mtl/IntTypes.h"
 
 //-------------------------------------------------------------------------------------------------