implementing more inequality graph stuff; work in progress doesn't compile

1 files changed, 72 insertions, 11 deletions

diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index c319ba5f4..2c7d3f8a3 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -33,14 +33,17 @@ namespace bv {
 typedef unsigned TermId; 
 typedef unsigned ReasonId;
 
+
 class InequalityGraph {
-  context::Context d_context;
+
+
+  context::Context* d_context;
 
   struct InequalityEdge {
     TermId next;
     ReasonId reason;
     InequalityEdge(TermId n, ReasonId r)
-      : next(n)
+      : next(n), 
         reason(r)
     {}
   };
@@ -50,21 +53,79 @@ class InequalityGraph {
     unsigned d_bitwidth;
     bool d_isConstant;
     BitVector d_value;
+  public:
+    InequalityNode(TermId id, unsigned bitwidth, bool isConst = false)
+      : d_id(id),
+        d_bitwidth(bitwidth),
+        d_isConstant(isConst),
+        d_value(BitVector(bitwidth, 0u))
+    {}
+    TermId getId() const { return d_id; }
+    unsigned getBitwidth() const { return d_bitwidth; }
+    bool isConstant() const { return d_isConstant; }
+    const BitVector& getValue() const { return d_value; }
   };
-  std::vector<InequalityNode> d_nodes;
-  std::vector< std::vector<InequalityEdge> > d_nodeEdges;
+
+  struct PQueueElement {
+    TermId id;
+    BitVector min_value;
+    PQueueElement(TermId id, BitVector min)
+      : id(id), 
+        min_value(min)
+    {}
+    bool operator< (const PQueueElement& other) const {
+      return min_value < other.min_value; 
+    }
+  }; 
   
+  typedef __gnu_cxx::hash_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap;
+  typedef __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap;
+
+  typedef std::vector<InequalityEdge> Edges; 
+  typedef __gnu_cxx::hash_set<TermId> TermIdSet;
+
+  typedef std::queue<PQueueElement> BFSQueue;
+
+  
+  std::vector<InequalityNode> d_ineqNodes;
+
+  std::vector< Edges > d_ineqEdges;
+  std::vector< Edges > d_parentEdges;
+  
+  std::vector<TNode> d_reasonNodes;
+  std::vector<TNode> d_termNodes;
+  ReasonToIdMap d_reasonToIdMap; 
+  TermNodeToIdMap d_termNodeToIdMap;
+
+  TermId registerTerm(TNode term);
+  ReasonId registerReason(TNode reason);
+  TNode getReason(ReasonId id) const;
+  TNode getTerm(TermId id) const; 
+
+  Edges& getOutEdges(TermId id) { Assert (id < d_ineqEdges.size()); return d_ineqEdges[id]; }
+  Edges& getInEdges(TermId id) { Assert (id < d_parentEdges.size()); return d_parentEdges[id]; }
+  InequalityNode& getInequalityNode(TermId id) { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; }
+  const BitVector& getValue(TermId id) const { return getInequalityNode().getValue(); }
+  bool addInequalityInternal(TermId a, TermId b, ReasonId reason);
+  bool areLessThanInternal(TermId a, TermId b);
+  void getConflictInternal(std::vector<ReasonId>& conflict);
+
+  context::CDO<bool> d_inConflict;
+  context::CDList<TNode> d_conflict;
+  void setConflict(const std::vector<ReasonId>& conflict); 
 public:
   
   InequalityGraph(context::Context* c)
-    : d_context(c)
+    : d_context(c),
+      d_ineqNodes(),
+      d_ineqEdges(),
+      d_parentEdges(),
+      d_inConflict(c, false),
+      d_conflict(c)
   {}
-  bool addInequality(TermId a, TermId b, ReasonId reason);
-  bool propagate();
-  bool areLessThan(TermId a, TermId b);
-  void getConflict(std::vector<ReasonId>& conflict);
-  TermId addTerm(unsigned bitwidth);
-  TermId addTerm(const BitVector& value); 
+  bool addInequality(TNode a, TNode b, TNode reason);
+  bool areLessThan(TNode a, TNode b);
+  void getConflict(std::vector<TNode>& conflict);
 }; 
 
 }