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

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 11ddceaae..5303b6595 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -23,119 +23,42 @@
 
 #include "theory/theory.h"
 #include "context/context.h"
-#include "context/cdset.h"
 #include "context/cdlist.h"
-#include "theory/bv/equality_engine.h"
-#include "theory/bv/slice_manager.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "util/stats.h"
+
+namespace BVMinisat {
+class SimpSolver; 
+}
+
 
 namespace CVC4 {
 namespace theory {
 namespace bv {
 
+/// forward declarations 
+class Bitblaster;
+
 class TheoryBV : public Theory {
 
 public:
 
-  class EqualityNotify {
-    TheoryBV& d_theoryBV;
-  public:
-    EqualityNotify(TheoryBV& theoryBV)
-    : d_theoryBV(theoryBV) {}
-
-    bool operator () (size_t triggerId) {
-      return d_theoryBV.triggerEquality(triggerId);
-    }
-    void conflict(Node explanation) {
-      std::set<TNode> assumptions;
-      utils::getConjuncts(explanation, assumptions);
-      d_theoryBV.d_out->conflict(utils::mkConjunction(assumptions));
-    }
-  };
-
-  struct BVEqualitySettings {
-    static inline bool descend(TNode node) {
-      return node.getKind() == kind::BITVECTOR_CONCAT || node.getKind() == kind::BITVECTOR_EXTRACT;
-    }
-
-    /** Returns true if node1 has preference to node2 as a representative, otherwise node2 is used */
-    static inline bool mergePreference(TNode node1, unsigned node1size, TNode node2, unsigned node2size) {
-      if (node1.getKind() == kind::CONST_BITVECTOR) {
-        Assert(node2.getKind() != kind::CONST_BITVECTOR);
-        return true;
-      }
-      if (node2.getKind() == kind::CONST_BITVECTOR) {
-        Assert(node1.getKind() != kind::CONST_BITVECTOR);
-        return false;
-      }
-      if (node1.getKind() == kind::BITVECTOR_CONCAT) {
-        Assert(node2.getKind() != kind::BITVECTOR_CONCAT);
-        return true;
-      }
-      if (node2.getKind() == kind::BITVECTOR_CONCAT) {
-        Assert(node1.getKind() != kind::BITVECTOR_CONCAT);
-        return false;
-      }
-      return node2size < node1size;
-    }
-  };
-
-  typedef EqualityEngine<TheoryBV, EqualityNotify, BVEqualitySettings> BvEqualityEngine;
-
 private:
 
-  /** Equality reasoning engine */
-  BvEqualityEngine d_eqEngine;
-
-  /** Slice manager */
-  SliceManager<TheoryBV> d_sliceManager;
-
-  /** Equality triggers indexed by ids from the equality manager */
-  std::vector<Node> d_triggers;
-  
   /** The context we are using */
   context::Context* d_context;
 
   /** The asserted stuff */
-  context::CDSet<TNode, TNodeHashFunction> d_assertions;
-
-  /** Asserted dis-equalities */
-  context::CDList<TNode> d_disequalities;
-
-  struct Normalization {
-    context::CDList<Node> equalities;
-    context::CDList< std::set<TNode> > assumptions;
-    Normalization(context::Context* c, TNode eq)
-    : equalities(c), assumptions(c) {
-      equalities.push_back(eq);
-      assumptions.push_back(std::set<TNode>());
-    }
-  };
-
-  /** Map from equalities to their noramlization information */
-  typedef __gnu_cxx::hash_map<TNode, Normalization*, TNodeHashFunction> NormalizationMap;
-  NormalizationMap d_normalization;
-
-  /** Called by the equality managere on triggers */
-  bool triggerEquality(size_t triggerId);
-
+  context::CDList<TNode> d_assertions;
+  
+  /** Bitblaster */
+  Bitblaster* d_bitblaster; 
   Node d_true;
-
+    
 public:
 
-  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation)
-  : Theory(THEORY_BV, c, u, out, valuation), 
-    d_eqEngine(*this, c, "theory::bv::EqualityEngine"), 
-    d_sliceManager(*this, c), 
-    d_context(c),
-    d_assertions(c), 
-    d_disequalities(c)
-  {
-    d_true = utils::mkTrue();
-  }
-
-  BvEqualityEngine& getEqualityEngine() {
-    return d_eqEngine;
-  }
+  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
+  ~TheoryBV(); 
 
   void preRegisterTerm(TNode n);
 
@@ -150,6 +73,21 @@ public:
   Node getValue(TNode n);
 
   std::string identify() const { return std::string("TheoryBV"); }
+
+  //Node preprocessTerm(TNode term);
+  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); 
+private:
+  
+  class Statistics {
+  public:
+    AverageStat d_avgConflictSize;
+    IntStat     d_solveSubstitutions; 
+    Statistics();
+    ~Statistics(); 
+  }; 
+  
+  Statistics d_statistics;
+  
 };/* class TheoryBV */
 
 }/* CVC4::theory::bv namespace */