From b7054f0e092f54c9e385f4b55a81173602b74b42 Mon Sep 17 00:00:00 2001
From: lianah <lianahady@gmail.com>
Date: Mon, 18 Mar 2013 19:10:47 -0400
Subject: more work on inequality reasoning for bv

---
 src/theory/bv/bv_inequality_graph.h | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

(limited to 'src/theory/bv/bv_inequality_graph.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); 
 }; 
 
 }
-- 
cgit v1.2.3