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

diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index 419acf6bae5c63a8938dc700c6394ff0cd62cdae..29284ff5ab295c2570097df4494991c489e1caf9 100644 (file)
--- a/src/theory/bv/Makefile.am
+++ b/src/theory/bv/Makefile.am
@@ -19,6 +19,8 @@ libbv_la_SOURCES = \
        bv_subtheory_bitblast.cpp \
        bv_subtheory_inequality.h \
        bv_subtheory_inequality.cpp \
+       bv_inequality_graph.h \
+       bv_inequality_graph.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 c319ba5f4b3370bcbe5d6051c8c7c78c362878fd..2c7d3f8a3dc3fa479f3aba03f4459180dd5d04eb 100644 (file)
--- 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);
 }; 
 
 }

diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 3172a8c33e80afacb0c7f9adad1d0566f2fca9e8..ff1287b3d5c66019877869cbf9d644fe5542afa5 100644 (file)
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -27,12 +27,34 @@ using namespace CVC4::theory::bv;
 using namespace CVC4::theory::bv::utils;
 
 bool InequalitySolver::check(Theory::Effort e) {
-  
+  bool ok = true; 
+  while (!done() && ok) {
+    TNode fact = get();
+     if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULE) {
+       TNode a = fact[0][1];
+       TNode b = fact[0][0]; 
+       ok = d_inequalityGraph.addInequality(a, b, fact);
+    }
+    if (fact.getKind() == kind::BITVECTOR_ULT) {
+      TNode a = fact[0];
+      Tnode b = fact[0]; 
+      ok = d_inequalityGraph.addInequality(a, b, fact);
+    }
+  }
+  if (!ok) {
+    std::vector<TNode> conflict;
+    d_inequalityGraph.getConflict(conflict); 
+    d_bv->setConflict(utils::mkConjunction(conflict));
+    return false; 
+  }
+  return true; 
 }
+
 void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
-  
+  Assert (false); 
 }
 
 void InequalitySolver::propagate(Theory::Effort e) {
-  
+  Assert (false); 
 }
+

diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 71c6d0d4e6650e85ae4cb12500fa1deca39479a3..445d5532d5b2305bd952a9c52ed2db48fe61005f 100644 (file)
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -21,18 +21,19 @@
 
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/bv_subtheory.h"
+#include "theory/bv/bv_inequality_graph.h"
+
 namespace CVC4 {
 namespace theory {
-
-
 namespace bv {
 
 class InequalitySolver: public SubtheorySolver {
-
+  InequalityGraph d_inequalityGraph;
 public:
   
   InequalitySolver(context::Context* c, TheoryBV* bv)
-    : SubtheorySolver(c, bv)
+    : SubtheorySolver(c, bv),
+      d_inequalityGraph()
   {}
   
   bool check(Theory::Effort e);