more work on inequality reasoning for bv

6 files changed, 31 insertions, 14 deletions

diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index 686cc7e83..419acf6ba 100644
--- a/src/theory/bv/Makefile.am
+++ b/src/theory/bv/Makefile.am
@@ -13,12 +13,12 @@ libbv_la_SOURCES = \
 	bitblaster.h \
 	bitblaster.cpp \
 	bv_subtheory.h \
-	bv_subtheory_eq.h \
-	bv_subtheory_eq.cpp \
 	bv_subtheory_core.h \
 	bv_subtheory_core.cpp \
 	bv_subtheory_bitblast.h \
 	bv_subtheory_bitblast.cpp \
+	bv_subtheory_inequality.h \
+	bv_subtheory_inequality.cpp \
 	bitblast_strategies.h \
 	bitblast_strategies.cpp \
 	slicer.h \
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 2ac22bb5b..c319ba5f4 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -35,6 +35,24 @@ typedef unsigned ReasonId;
 
 class InequalityGraph {
   context::Context d_context;
+
+  struct InequalityEdge {
+    TermId next;
+    ReasonId reason;
+    InequalityEdge(TermId n, ReasonId r)
+      : next(n)
+        reason(r)
+    {}
+  };
+  
+  class InequalityNode {
+    TermId d_id;
+    unsigned d_bitwidth;
+    bool d_isConstant;
+    BitVector d_value;
+  };
+  std::vector<InequalityNode> d_nodes;
+  std::vector< std::vector<InequalityEdge> > d_nodeEdges;
   
 public:
   
@@ -44,7 +62,9 @@ public:
   bool addInequality(TermId a, TermId b, ReasonId reason);
   bool propagate();
   bool areLessThan(TermId a, TermId b);
-  void getConflict(std::vector<ReasonId>& conflict); 
+  void getConflict(std::vector<ReasonId>& conflict);
+  TermId addTerm(unsigned bitwidth);
+  TermId addTerm(const BitVector& value); 
 }; 
 
 }
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 9e7566ebb..73050ea73 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -61,6 +61,7 @@ const bool d_useSatPropagation = true;
 // forward declaration 
 class TheoryBV; 
 
+typedef context::CDQueue<TNode> AssertionQueue; 
 /**
  * Abstract base class for bit-vector subtheory solvers
  *
@@ -74,7 +75,7 @@ protected:
 
   /** The bit-vector theory */
   TheoryBV* d_bv;
-  context::CDQueue<TNode> d_assertionQueue;
+  AssertionQueue d_assertionQueue;
   context::CDO<uint32_t>  d_assertionIndex; 
 public:
   
@@ -88,7 +89,7 @@ public:
   virtual bool check(Theory::Effort e) = 0; 
   virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0;
   virtual void preRegister(TNode node) {}
-  virtual void propagate(Effort e) {}
+  virtual void propagate(Theory::Effort e) {}
   virtual void collectModelInfo(TheoryModel* m) = 0;
   bool done() { return d_assertionQueue.size() == d_assertionIndex; }
   TNode get() {
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 7ccef5ff1..3172a8c33 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -33,6 +33,6 @@ void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
   
 }
 
-bool InequalitySolver::propagate(Theory::Effort e) {
+void InequalitySolver::propagate(Theory::Effort e) {
   
 }
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 63f9af9e4..71c6d0d4e 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -19,18 +19,15 @@
 #ifndef __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
 #define __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
 
-#include "context/context.h"
-#include "context/cdqueue.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/theory.h"
-
+#include "theory/bv/theory_bv.h"
+#include "theory/bv/bv_subtheory.h"
 namespace CVC4 {
 namespace theory {
 
 
 namespace bv {
 
-class InequalitySolver {
+class InequalitySolver: public SubtheorySolver {
 
 public:
   
@@ -39,7 +36,7 @@ public:
   {}
   
   bool check(Theory::Effort e);
-  void propagate(Effort e); 
+  void propagate(Theory::Effort e); 
   void explain(TNode literal, std::vector<TNode>& assumptions); 
 }; 
 
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index d457571e2..85077f10d 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -26,7 +26,6 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "util/statistics_registry.h"
 #include "theory/bv/bv_subtheory.h"
-#include "theory/bv/bv_subtheory_eq.h"
 #include "theory/bv/bv_subtheory_core.h"
 #include "theory/bv/bv_subtheory_bitblast.h"
 #include "theory/bv/slicer.h"