generalized bv inequality reasoning to handle both strict and non-strict inequalities

1 files changed, 117 insertions, 49 deletions

diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 1a4b14ace..18bd75726 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -34,7 +34,8 @@ namespace bv {
 typedef unsigned TermId; 
 typedef unsigned ReasonId;
 extern const TermId UndefinedTermId;
-extern const ReasonId UndefinedReasonId; 
+extern const ReasonId UndefinedReasonId;
+extern const ReasonId AxiomReasonId; 
 
 class InequalityGraph {
 
@@ -44,24 +45,25 @@ class InequalityGraph {
   struct InequalityEdge {
     TermId next;
     ReasonId reason;
-    InequalityEdge(TermId n, ReasonId r)
-      : next(n), 
-        reason(r)
+    bool strict;
+    InequalityEdge(TermId n, bool s, ReasonId r)
+      : next(n),
+        reason(r),
+        strict(s)
     {}
   };
-  
+
   class InequalityNode {
     TermId d_id;
     unsigned d_bitwidth;
     bool d_isConstant;
     BitVector d_value;
   public:
-    InequalityNode(TermId id, unsigned bitwidth, bool isConst, BitVector val)
+    InequalityNode(TermId id, unsigned bitwidth, bool isConst, const BitVector val)
       : d_id(id),
         d_bitwidth(bitwidth),
         d_isConstant(isConst),
-        d_value(val)
-    {}
+        d_value(val)    {}
     TermId getId() const { return d_id; }
     unsigned getBitwidth() const { return d_bitwidth; }
     bool isConstant() const { return d_isConstant; }
@@ -69,17 +71,37 @@ class InequalityGraph {
     void setValue(const BitVector& val) { Assert (val.getSize() == d_bitwidth); d_value = val; }
   };
 
+  struct Explanation {
+    TermId parent;
+    ReasonId reason;
+
+    Explanation()
+      : parent(UndefinedTermId),
+        reason(UndefinedReasonId)
+    {}
+    
+    Explanation(TermId p, ReasonId r)
+      : parent(p),
+        reason(r)
+    {}
+  };
+
   struct PQueueElement {
     TermId id;
-    BitVector min_value;
-    PQueueElement(TermId id, BitVector min)
-      : id(id), 
-        min_value(min)
+    BitVector value; 
+    BitVector lower_bound;
+    Explanation explanation; 
+    PQueueElement(TermId id, const BitVector v, const BitVector& lb, Explanation exp)
+      : id(id),
+        value(v),
+        lower_bound(lb),
+        explanation(exp)
     {}
+    
     bool operator< (const PQueueElement& other) const {
-      return min_value < other.min_value; 
+      return value > other.value;
     }
-  }; 
+  };
   
   typedef __gnu_cxx::hash_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap;
   typedef __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap;
@@ -87,64 +109,110 @@ class InequalityGraph {
   typedef std::vector<InequalityEdge> Edges; 
   typedef __gnu_cxx::hash_set<TermId> TermIdSet;
 
-  typedef std::queue<TermId> TermIdQueue; 
-  typedef std::priority_queue<PQueueElement> BFSQueue;
-
+  typedef std::priority_queue<PQueueElement> BFSQueue; 
+  typedef __gnu_cxx::hash_map<TermId, Explanation> TermIdToExplanationMap; 
   
   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; 
+  ReasonToIdMap d_reasonToIdMap;
+  
+  std::vector<Node> d_termNodes;
   TermNodeToIdMap d_termNodeToIdMap;
 
+  TermIdToExplanationMap d_termToExplanation; 
+  
+  context::CDO<bool> d_inConflict;
+  std::vector<TNode> d_conflict;
+  bool d_signed; 
+
+
+  /** 
+   * Registers the term by creating its corresponding InequalityNode
+   * and adding the min <= term <= max default edges. 
+   * 
+   * @param term 
+   * 
+   * @return 
+   */
   TermId registerTerm(TNode term);
-  ReasonId registerReason(TNode reason);
-  TNode getReason(ReasonId id) const;
-  TermId getReasonId(TermId a, TermId b); 
-  TNode getTerm(TermId id) const; 
+  TNode getTermNode(TermId id) const; 
+  TermId getTermId(TNode node) 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]; }
+  ReasonId registerReason(TNode reason);
+  TNode getReasonNode(ReasonId id) const;
+  
+  bool hasExplanation(TermId id) const { return d_termToExplanation.find(id) != d_termToExplanation.end(); }
+  Explanation getExplanation(TermId id) const { Assert (hasExplanation(id)); return d_termToExplanation.find(id)->second; } 
+  void setExplanation(TermId id, Explanation exp) { d_termToExplanation[id] = exp; }
+  
+  Edges& getEdges(TermId id) { Assert (id < d_ineqEdges.size()); return d_ineqEdges[id]; }
   InequalityNode& getInequalityNode(TermId id) { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; }
   const InequalityNode& getInequalityNode(TermId id) const { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; }
-
-  const BitVector& getValue(TermId id) const { return getInequalityNode(id).getValue(); }
   unsigned getBitwidth(TermId id) const { return getInequalityNode(id).getBitwidth(); }
+  bool isConst(TermId id) const { return getInequalityNode(id).isConstant(); }
+  BitVector maxValue(unsigned bitwidth);
+  BitVector minValue(unsigned bitwidth);
+  TermId getMaxValueId(unsigned bitwidth);
+  TermId getMinValueId(unsigned bitwidth);
   
-  bool hasValue(TermId id) const;
-  bool initializeValues(TNode a, TNode b, TermId reason_id); 
-  TermId getMaxParent(TermId id); 
-  bool hasParents(TermId id); 
-
-  bool canReach(TermId from, TermId to);
-  void bfs(TermIdSet& seen, TermIdQueue& queue); 
+  const BitVector& getValue(TermId id) const { return getInequalityNode(id).getValue(); }
+    
+  void addEdge(TermId a, TermId b, bool strict, TermId reason);
   
-  void addEdge(TermId a, TermId b, TermId reason);
-  bool addInequalityInternal(TermId a, TermId b, ReasonId reason);
-  bool areLessThanInternal(TermId a, TermId b);
-  void getConflictInternal(std::vector<ReasonId>& conflict);
-  bool computeValuesBFS(BFSQueue& queue, TermIdSet& seen);
+  void setConflict(const std::vector<ReasonId>& conflict);
+  /** 
+   * If necessary update the value in the model of the current queue element. 
+   * 
+   * @param el current queue element we are updating
+   * @param start node we started with, to detect cycles
+   * @param seen 
+   * 
+   * @return 
+   */
+  bool updateValue(const PQueueElement& el, TermId start, const TermIdSet& seen);
+  /** 
+   * Update the current model starting with the start term. 
+   * 
+   * @param queue 
+   * @param start 
+   * @param seen 
+   * 
+   * @return 
+   */
+  bool computeValuesBFS(BFSQueue& queue, TermId start, TermIdSet& seen);
+  /** 
+   * Return the reasons why from <= to. If from is undefined we just
+   * explain the current value of to. 
+   * 
+   * @param from 
+   * @param to 
+   * @param explanation 
+   */
   void computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation); 
   
-  context::CDO<bool> d_inConflict;
-  std::vector<TNode> d_conflict;
-  void setConflict(const std::vector<ReasonId>& conflict);
-
 public:
   
-  InequalityGraph(context::Context* c)
+  InequalityGraph(context::Context* c, bool s = false)
     : d_context(c),
       d_ineqNodes(),
       d_ineqEdges(),
-      d_parentEdges(),
       d_inConflict(c, false),
-      d_conflict()
+      d_conflict(),
+      d_signed(s)
   {}
-  bool addInequality(TNode a, TNode b, TNode reason);
+  /** 
+   * 
+   * 
+   * @param a 
+   * @param b 
+   * @param diff 
+   * @param reason 
+   * 
+   * @return 
+   */
+  bool addInequality(TNode a, TNode b, bool strict, TNode reason);
   bool areLessThan(TNode a, TNode b);
   void getConflict(std::vector<TNode>& conflict);
 };