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, 2 insertions, 3 deletions

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 0b5be4647..4f83888fc 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -27,7 +27,6 @@
 #include "util/options.h"
 #include "util/result.h"
 #include "smt/modal_exception.h"
-
 #include <sys/time.h>
 
 namespace CVC4 {
@@ -37,7 +36,7 @@ class TheoryEngine;
 namespace prop {
 
 class CnfStream;
-class SatSolver;
+class DPLLSatSolverInterface;
 
 class PropEngine;
 
@@ -132,7 +131,7 @@ class PropEngine {
   context::Context* d_context;
 
   /** The SAT solver proxy */
-  SatSolver* d_satSolver;
+  DPLLSatSolverInterface* d_satSolver;
 
   /** List of all of the assertions that need to be made */
   std::vector<Node> d_assertionList;