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

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 4b16a02b9..c9306952b 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -29,7 +29,7 @@
 
 #include "expr/node.h"
 #include "prop/sat.h"
-#include "theory/registrar.h"
+#include "prop/registrar.h"
 
 #include <ext/hash_map>
 
@@ -48,7 +48,7 @@ class CnfStream {
 public:
 
   /** Cache of what nodes have been registered to a literal. */
-  typedef __gnu_cxx::hash_map<SatLiteral, TNode, SatSolver::SatLiteralHashFunction> NodeCache;
+  typedef __gnu_cxx::hash_map<SatLiteral, TNode, SatLiteralHashFunction> NodeCache;
 
   /** Per node translation information */
   struct TranslationInfo {
@@ -64,7 +64,7 @@ public:
 protected:
 
   /** The SAT solver we will be using */
-  SatInputInterface *d_satSolver;
+  SatSolverInterface *d_satSolver;
 
   TranslationCache d_translationCache;
   NodeCache d_nodeCache;
@@ -77,7 +77,7 @@ protected:
   const bool d_fullLitToNodeMap;
 
   /** The "registrar" for pre-registration of terms */
-  theory::Registrar d_registrar;
+  Registrar* d_registrar;
 
   /** Top level nodes that we translated */
   std::vector<TNode> d_translationTrail;
@@ -98,7 +98,7 @@ protected:
    * detection," when BIG FORMULA is later asserted, it is clausified
    * separately, and "lit" is never asserted as a unit clause.
    */
-  KEEP_STATISTIC(IntStat, d_fortunateLiterals, "prop::CnfStream::fortunateLiterals", 0);
+  //KEEP_STATISTIC(IntStat, d_fortunateLiterals, "prop::CnfStream::fortunateLiterals", 0);
 
   /** Remove nots from the node */
   TNode stripNot(TNode node) {
@@ -189,7 +189,7 @@ public:
    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
    * even for non-theory literals
    */
-  CnfStream(SatInputInterface* satSolver, theory::Registrar registrar, bool fullLitToNodeMap = false);
+  CnfStream(SatSolverInterface* satSolver, Registrar* registrar, bool fullLitToNodeMap = false);
 
   /**
    * Destructs a CnfStream.  This implementation does nothing, but we
@@ -289,7 +289,7 @@ public:
    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
    * even for non-theory literals
    */
-  TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar, bool fullLitToNodeMap = false);
+  TseitinCnfStream(SatSolverInterface* satSolver, Registrar* registrar, bool fullLitToNodeMap = false);
 
 private: