more work on inequality reasoning for bv

diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index 686cc7e831abe118f4468e781d4313382b700720..419acf6bae5c63a8938dc700c6394ff0cd62cdae 100644 (file)
--- 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 2ac22bb5b2b400d4abf12d0bf9898d344be38ac7..c319ba5f4b3370bcbe5d6051c8c7c78c362878fd 100644 (file)
--- 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 9e7566ebb317d4fa9a5cccabf44be55cb37d4909..73050ea7368fa2c1b7476c34e673cf0d5bd03ae2 100644 (file)
--- 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 7ccef5ff183183ec5a878eabda0e053ebc480aa2..3172a8c33e80afacb0c7f9adad1d0566f2fca9e8 100644 (file)
--- 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 63f9af9e4346ca3af04cc0221e6516940f3fbd63..71c6d0d4e6650e85ae4cb12500fa1deca39479a3 100644 (file)
--- 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 d457571e23c352603a092c9f8a3057eaed72822c..85077f10d83d6fced85268f51c506bf935da2d30 100644 (file)
--- 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"