non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)

diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index e29ce201436732cc7cf99bb9be92ab644497da41..53be803caf1c1e1206a36b079b287ede1ec93ed1 100644 (file)
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -28,6 +28,7 @@ const TermId CVC4::theory::bv::UndefinedTermId = -1;
 const ReasonId CVC4::theory::bv::UndefinedReasonId = -1;
 const ReasonId CVC4::theory::bv::AxiomReasonId = -2;
 
+
 BitVector InequalityGraph::maxValue(unsigned bitwidth) {
   if (d_signed) {
     return BitVector(1, 0u).concat(~BitVector(bitwidth - 1, 0u)); 
@@ -78,7 +79,7 @@ TermId InequalityGraph::getMinValueId(unsigned bitwidth) {
 }
 
 bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) {
-  Debug("bv-inequality") << "InequlityGraph::addInequality " << a << " " << b << "\n"; 
+  Debug("bv-inequality") << "InequlityGraph::addInequality " << a << " " << b << "strict: " << strict << "\n"; 
 
   TermId id_a = registerTerm(a);
   TermId id_b = registerTerm(b);
@@ -89,7 +90,17 @@ bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason)
   BitVector b_val = getValue(id_b);
     
   unsigned bitwidth = utils::getSize(a); 
-  BitVector diff = strict ? BitVector(bitwidth, 1u) : BitVector(bitwidth, 0u); 
+  BitVector diff = strict ? BitVector(bitwidth, 1u) : BitVector(bitwidth, 0u);
+
+  if (a_val + diff < a_val) {
+    // we have an overflow
+    std::vector<ReasonId> conflict;
+    conflict.push_back(id_reason);
+    computeExplanation(UndefinedTermId, id_a, conflict);
+    setConflict(conflict);
+    return false; 
+  }
+  
   if (a_val + diff <= b_val) {
     // the inequality is true in the current partial model
     // we still add the edge because it may not be true later (cardinality)
@@ -117,7 +128,7 @@ bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason)
   return computeValuesBFS(queue, id_a, seen); 
 }
 
-bool InequalityGraph::updateValue(const PQueueElement& el, TermId start, const TermIdSet& seen) {
+bool InequalityGraph::updateValue(const PQueueElement& el, TermId start, const TermIdSet& seen, bool& changed) {
   TermId id = el.id;
   const BitVector& lower_bound = el.lower_bound; 
   InequalityNode& ineqNode = getInequalityNode(id);
@@ -138,7 +149,7 @@ bool InequalityGraph::updateValue(const PQueueElement& el, TermId start, const T
     // if not constant we can update the value
     if (ineqNode.getValue() < lower_bound) {
       // if we are updating the term we started with we must be in a cycle
-      if (seen.count(id)) {
+      if (seen.count(id) && id == start) {
         TermId parent = el.explanation.parent;
         ReasonId reason = el.explanation.reason;
         std::vector<TermId> conflict;
@@ -151,6 +162,7 @@ bool InequalityGraph::updateValue(const PQueueElement& el, TermId start, const T
       Debug("bv-inequality-internal") << "Updating " << getTermNode(id) 
                                       << "  from " << ineqNode.getValue() << "\n"
                                       << "  to " << lower_bound << "\n";
+      changed = true; 
       ineqNode.setValue(lower_bound);
       setExplanation(id, el.explanation); 
     }
@@ -164,17 +176,28 @@ bool InequalityGraph::computeValuesBFS(BFSQueue& queue, TermId start, TermIdSet&
 
   const PQueueElement current = queue.top();
   queue.pop();
-  
-  if (!updateValue(current, start, seen)) {
+  Debug("bv-inequality-internal") << "InequalityGraph::computeValuesBFS proceessing " << getTermNode(current.id) << " " << current.toString() << "\n";
+  bool updated_current = false; 
+  if (!updateValue(current, start, seen, updated_current)) {
     return false; 
   }
-  if (seen.count(current.id) && current.id != getMaxValueId(getBitwidth(current.id))) {
+  if (seen.count(current.id) && current.id == start) {
+    // we know what we didn't update start or we would have had a conflict 
     Debug("bv-inequality-internal") << "InequalityGraph::computeValuesBFS equal cycle."; 
     // this means we are in a cycle where all the values are forced to be equal
+    // TODO: make sure we collapse this cycle into one big node. 
+    return computeValuesBFS(queue, start, seen); 
+  }
+  
+  if (!updated_current && !(seen.count(current.id) == 0 && current.id == start)) {
+    // if we didn't update current we don't need to readd to the queue it's children 
+    seen.insert(current.id);
+    Debug("bv-inequality-internal") << "  unchanged " << getTermNode(current.id) << "\n";  
     return computeValuesBFS(queue, start, seen); 
   }
   
-  seen.insert(current.id); 
+  seen.insert(current.id);
+  
   const BitVector& current_value = getValue(current.id);
   
   unsigned size = getBitwidth(current.id);
@@ -186,8 +209,19 @@ bool InequalityGraph::computeValuesBFS(BFSQueue& queue, TermId start, TermIdSet&
     TermId next = it->next;
     const BitVector increment = it->strict ? one : zero; 
     const BitVector& next_lower_bound = current_value + increment;
+    if (next_lower_bound < current_value) {
+      // it means we have an overflow and hence a conflict
+        std::vector<TermId> conflict;
+        conflict.push_back(it->reason);
+        computeExplanation(start, current.id, conflict);
+        Debug("bv-inequality") << "InequalityGraph::addInequality conflict: cycle \n"; 
+        setConflict(conflict); 
+        return false; 
+    }
     const BitVector& value = getValue(next); 
-    queue.push(PQueueElement(next, value, next_lower_bound, Explanation(current.id, it->reason)));
+    PQueueElement el = PQueueElement(next, value, next_lower_bound, Explanation(current.id, it->reason)); 
+    queue.push(el);
+    Debug("bv-inequality-internal") << "   enqueue " << getTermNode(el.id) << " " << el.toString() << "\n"; 
   }
   return computeValuesBFS(queue, start, seen); 
 }
@@ -209,16 +243,13 @@ void InequalityGraph::addEdge(TermId a, TermId b, bool strict, TermId reason) {
 }
 
 TermId InequalityGraph::registerTerm(TNode term) {
-  Debug("bv-inequality-internal") << "InequalityGraph::registerTerm " << term << "\n"; 
-
-
   if (d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end()) {
     return d_termNodeToIdMap[term]; 
   }
 
   // store in node mapping
   TermId id = d_termNodes.size();
-  Debug("bv-inequality-internal") << " with id " << id << "\n";
+  Debug("bv-inequality-internal") << "InequalityGraph::registerTerm " << term << " => id"<< id << "\n"; 
   
   d_termNodes.push_back(term);
   d_termNodeToIdMap[term] = id;
@@ -285,6 +316,13 @@ void InequalityGraph::getConflict(std::vector<TNode>& conflict) {
   }
 }
 
+std::string InequalityGraph::PQueueElement::toString() const {
+  ostringstream os;
+  os << "(id: " << id <<", value: " << value.toString(10) << ", lower_bound: " << lower_bound.toString(10) <<")"; 
+  return os.str(); 
+}
+
+
 // bool InequalityGraph::initializeValues(TNode a, TNode b, bool strict, TermId reason_id) {
 //   TermId id_a = registerTerm(a);
 //   TermId id_b = registerTerm(b);

diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 18bd757266f77bb3535899234a00f7e879644a5d..6eb88ec79bbb9f728899acd1e443f28b53fd6436 100644 (file)
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -101,6 +101,7 @@ class InequalityGraph {
     bool operator< (const PQueueElement& other) const {
       return value > other.value;
     }
+    std::string toString() const; 
   };
   
   typedef __gnu_cxx::hash_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap;
@@ -171,7 +172,7 @@ class InequalityGraph {
    * 
    * @return 
    */
-  bool updateValue(const PQueueElement& el, TermId start, const TermIdSet& seen);
+  bool updateValue(const PQueueElement& el, TermId start, const TermIdSet& seen, bool& changed);
   /** 
    * Update the current model starting with the start term. 
    * 

diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 6b4b1a1343ff548c313bca4e90cd3ccda33f2866..f856c94106dbe0eb5e520250c5665ba51a26cfce 100644 (file)
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -30,7 +30,13 @@ bool InequalitySolver::check(Theory::Effort e) {
   bool ok = true; 
   while (!done() && ok) {
     TNode fact = get();
-    
+    if (fact.getKind() == kind::EQUAL) {
+      TNode a = fact[0];
+      TNode b = fact[1];
+      ok = d_inequalityGraph.addInequality(a, b, false, fact);
+      if (ok)
+        ok = d_inequalityGraph.addInequality(b, a, false, fact); 
+    }
     if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULE) {
       TNode a = fact[0][1];
       TNode b = fact[0][0]; 

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index a794d63a305ef1f1cec9ab1be3608e8068dbaeaa..bc8e39e67b5562e72e1a66ef1c55dc7ead4a1857 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -122,15 +122,15 @@ void TheoryBV::check(Effort e)
   }
   Assert (!ok == inConflict()); 
 
-  // if (!inConflict() && !d_coreSolver.isCoreTheory()) {
-  //   ok = d_inequalitySolver.check(e); 
-  // }
-
-  Assert (!ok == inConflict());
   if (!inConflict() && !d_coreSolver.isCoreTheory()) {
-    // if (!inConflict() && !d_inequalitySolver.isInequalityTheory()) {
-    ok = d_bitblastSolver.check(e); 
+    ok = d_inequalitySolver.check(e); 
   }
+
+  Assert (!ok == inConflict());
+  // if (!inConflict() && !d_coreSolver.isCoreTheory()) {
+  // if (!inConflict() && !d_inequalitySolver.isInequalityTheory()) {
+  //   ok = d_bitblastSolver.check(e); 
+  // }
   
   Assert (!ok == inConflict()); 
   if (inConflict()) {

diff --git a/test/regress/regress0/bv/inequality04.smt2 b/test/regress/regress0/bv/inequality04.smt2
index 7b5dbd7d5c5e2a1106d3b7f7ce66ff15223a1dcd..35607eaef53f9886d20a9af535c886a4fedab307 100644 (file)
--- a/test/regress/regress0/bv/inequality04.smt2
+++ b/test/regress/regress0/bv/inequality04.smt2
@@ -12,7 +12,7 @@
         (bvule v0 v1)
         (bvule v1 v2)
         (bvule v2 v0)
-        (bvule (_ bv4 16) v0)
+        (bvult (_ bv4 16) v0)
         (bvult v2 (_ bv5 16))
         ))
 (check-sat)