more bugfixes for bitvectors

4 files changed, 198 insertions, 76 deletions

diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h
index aeb28ab7b..d020ef362 100644
--- a/src/theory/bv/cd_set_collection.h
+++ b/src/theory/bv/cd_set_collection.h
@@ -40,10 +40,19 @@ class BacktrackableSetCollection {
   /** Backtrackable number of nodes that have been inserted */
   context::CDO<unsigned> d_nodesInserted;
 
+  /** Check if the reference is valid in the current context */
+  inline bool isValid(reference_type set) const {
+    return d_nodesInserted == d_memory.size() && (set == null || set < d_memory.size());
+  }
+
   /** Backtrack */
   void backtrack() {
     while (d_nodesInserted < d_memory.size()) {
       const tree_entry_type& node = d_memory.back();
+
+      Debug("cd_set_collection") << "BacktrackableSetCollection::backtrack(): removing " << node.getValue()
+                                 << " from " << internalToString(getRoot(d_memory.size()-1)) << std::endl;
+
       if (node.hasParent()) {
         if (node.isLeft()) {
           d_memory[node.getParent()].removeLeft();
@@ -64,7 +73,7 @@ class BacktrackableSetCollection {
    */
   reference_type newElement(const value_type& value, reference_type left, reference_type right, reference_type parent, bool isLeft) {
     reference_type index = d_memory.size();
-    d_memory.push_back(tree_entry_type(value, left, right, value, isLeft));
+    d_memory.push_back(tree_entry_type(value, left, right, parent, isLeft));
     d_nodesInserted = d_nodesInserted + 1;
     return index;
   }
@@ -91,6 +100,7 @@ class BacktrackableSetCollection {
    */
   reference_type max(reference_type set) const {
     Assert(set != null);
+    Assert(isValid(set));
     while (d_memory[set].hasRight()) {
       set = d_memory[set].getRight();
     }
@@ -102,12 +112,54 @@ class BacktrackableSetCollection {
    */
   reference_type min(reference_type set) const {
     Assert(set != null);
+    Assert(isValid(set));
     while (d_memory[set].hasLeft()) {
       set = d_memory[set].getLeft();
     }
     return set;
   }
 
+  /**
+   * REturns the root of the tree
+   */
+  reference_type getRoot(reference_type set) const {
+    // We don't check validity as this is used in backtracking
+    while (set != null && d_memory[set].hasParent()) {
+      Assert(set > d_memory[set].getParent());
+      set = d_memory[set].getParent();
+    }
+    return set;
+  }
+
+  /**
+   * Print the list of elements to the output.
+   */
+  void internalPrint(std::ostream& out, reference_type set) const {
+    if (set == null) {
+      return;
+    }
+    const tree_entry_type& current = d_memory[set];
+    if (current.hasLeft()) {
+      internalPrint(out, current.getLeft());
+      out << ",";
+    }
+    out << current.getValue();
+    if (current.hasRight()) {
+      out << ",";
+      internalPrint(out, current.getRight());
+    }
+  }
+
+  /**
+   * String representation of a set.
+   */
+  std::string internalToString(reference_type set) const {
+    std::stringstream out;
+    internalPrint(out, set);
+    return out.str();
+  }
+
+
 public:
 
   BacktrackableSetCollection(context::Context* context)
@@ -118,6 +170,20 @@ public:
     return d_memory.size();
   }
 
+  size_t size(reference_type set) const {
+    backtrack();
+    Assert(isValid(set));
+    if (set == null) return 0;
+    size_t n = 1;
+    if (d_memory[set].hasLeft()) {
+      n += size(d_memory[set].getLeft());
+    }
+    if (d_memory[set].hasRight()) {
+      n += size(d_memory[set].getRight());
+    }
+    return n;
+  }
+
   reference_type newSet(const value_type& value) {
     backtrack();
     return newElement(value, null, null, null, false);
@@ -125,6 +191,7 @@ public:
 
   void insert(reference_type& root, const value_type& value) {
     backtrack();
+    Assert(isValid(root));
     if (root == null) {
       root = newSet(value);
       return;
@@ -133,20 +200,24 @@ public:
     reference_type parent = null;
     reference_type current = root;
     while (true) {
-      parent = current;
+      Assert(isValid(current));
       if (value < d_memory[current].getValue()) {
         if (d_memory[current].hasLeft()) {
+          parent = current;
           current = d_memory[current].getLeft();
         } else {
-          d_memory[current].setLeft(newElement(value, null, null, parent, true));
+          d_memory[current].setLeft(newElement(value, null, null, current, true));
+          Assert(d_memory[current].hasLeft());
           return;
         }
       } else {
-        Assert(value != d_memory[root].getValue());
+        Assert(value != d_memory[current].getValue());
         if (d_memory[current].hasRight()) {
+          parent = current;
           current = d_memory[current].getRight();
         } else {
-          d_memory[parent].setRight(newElement(value, null, null, parent, false));
+          d_memory[current].setRight(newElement(value, null, null, current, false));
+          Assert(d_memory[current].hasRight());
           return;
         }
       }
@@ -158,6 +229,7 @@ public:
    */
   const_value_reference maxElement(reference_type set) const {
     Assert(set != null);
+    Assert(isValid(set));
     backtrack();
     return d_memory[max(set)].getValue();
   }
@@ -167,6 +239,7 @@ public:
    */
   const_value_reference minElement(reference_type set) const {
     Assert(set != null);
+    Assert(isValid(set));
     backtrack();
     return d_memory[min(set)].getValue();
   }
@@ -176,6 +249,7 @@ public:
    */
   const_value_reference prev(reference_type set, const_value_reference value) {
     backtrack();
+    Assert(isValid(set));
 
     const_value_reference candidate_value;
     bool candidate_found = false;
@@ -202,6 +276,7 @@ public:
 
   const_value_reference next(reference_type set, const_value_reference value) {
     backtrack();
+    Assert(isValid(set));
 
     const_value_reference candidate_value;
     bool candidate_found = false;
@@ -232,6 +307,8 @@ public:
   unsigned count(reference_type set, const_value_reference lowerBound, const_value_reference upperBound) const {
     Assert(lowerBound <= upperBound);
     backtrack();
+    Assert(isValid(set));
+
     // Empty set no elements
     if (set == null) {
       return 0;
@@ -260,6 +337,7 @@ public:
    */
   bool contains(reference_type set, const_value_reference value) const {
     backtrack();
+    Assert(isValid(set));
     return count(set, value, value) > 0;
   }
 
@@ -270,6 +348,7 @@ public:
   void getElements(reference_type set, const_value_reference lowerBound, const_value_reference upperBound, std::vector<value_type>& output) const {
     Assert(lowerBound <= upperBound);
     backtrack();
+    Assert(isValid(set));
 
     Debug("set_collection") << "BacktrackableSetCollection::getElements(" << toString(set) << "," << lowerBound << "," << upperBound << ")" << std::endl;
 
@@ -298,6 +377,8 @@ public:
    */
   void print(std::ostream& out, reference_type set) const {
     backtrack();
+    Assert(isValid(set));
+
     if (set == null) {
       return;
     }
@@ -317,6 +398,9 @@ public:
    * String representation of a set.
    */
   std::string toString(reference_type set) const {
+    backtrack();
+    Assert(isValid(set));
+
     std::stringstream out;
     print(out, set);
     return out.str();
diff --git a/src/theory/bv/slice_manager.h b/src/theory/bv/slice_manager.h
index 96a0067dc..ed516fa31 100644
--- a/src/theory/bv/slice_manager.h
+++ b/src/theory/bv/slice_manager.h
@@ -122,7 +122,7 @@ public:
   typedef context::BacktrackableSetCollection<std::vector<slice_point>, slice_point, set_reference> set_collection;
 
   /** The map type from nodes to their references */
-  typedef std::map<Node, set_reference> slicing_map;
+  typedef context::CDMap<Node, set_reference, NodeHashFunction> slicing_map;
 
   /** The equality engine theory of bit-vectors is using */
   typedef typename TheoryBitvector::BvEqualityEngine EqualityEngine;
@@ -150,7 +150,11 @@ private:
 public:
 
   SliceManager(TheoryBitvector& theoryBitvector, context::Context* context)
-  : d_theoryBitvector(theoryBitvector), d_equalityEngine(theoryBitvector.getEqualityEngine()), d_setCollection(context) {
+  : d_theoryBitvector(theoryBitvector),
+    d_equalityEngine(theoryBitvector.getEqualityEngine()),
+    d_setCollection(context),
+    d_nodeSlicing(context)
+  {
   }
 
   /**
@@ -207,68 +211,6 @@ private:
   inline bool addSlice(Node term, unsigned slicePoint);
 };
 
-
-template <class TheoryBitvector>
-bool SliceManager<TheoryBitvector>::addSlice(Node node, unsigned slicePoint) {
-  Debug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << ")" << std::endl;
-
-  bool ok = true;
-
-  int low  = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractLow(node) : 0;
-  int high = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractHigh(node) + 1: utils::getSize(node);
-  slicePoint += low;
-
-  TNode nodeBase = baseTerm(node);
-
-  set_reference sliceSet;
-  slicing_map::iterator find = d_nodeSlicing.find(nodeBase);
-  if (find == d_nodeSlicing.end()) {
-    sliceSet = d_nodeSlicing[nodeBase] = d_setCollection.newSet(slicePoint);
-    d_setCollection.insert(sliceSet, low);
-    d_setCollection.insert(sliceSet, high);
-  } else {
-    sliceSet = find->second;
-  }
-
-  // What are the points surrounding the new slice point
-  int prev = d_setCollection.prev(sliceSet, slicePoint);
-  int next = d_setCollection.next(sliceSet, slicePoint);
-
-  // Add the slice to the set
-  d_setCollection.insert(sliceSet, slicePoint);
-  Debug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << "): current set " << d_setCollection.toString(sliceSet) << std::endl;
-
-  // Add the terms and the equality to the equality engine
-  Node t1 = utils::mkExtract(nodeBase, next - 1, slicePoint);
-  Node t2 = utils::mkExtract(nodeBase, slicePoint - 1, prev);
-  Node nodeSlice = (next == high && prev == low) ? node : utils::mkExtract(nodeBase, next - 1, prev);
-  Node concat = utils::mkConcat(t1, t2);
-
-  d_equalityEngine.addTerm(t1);
-  d_equalityEngine.addTerm(t2);
-  d_equalityEngine.addTerm(nodeSlice);
-  d_equalityEngine.addTerm(concat);
-
-  // We are free to add this slice, unless the slice has a representative that's already a concat
-  TNode nodeSliceRepresentative = d_equalityEngine.getRepresentative(nodeSlice);
-  if (nodeSliceRepresentative.getKind() != kind::BITVECTOR_CONCAT) {
-    // Add the slice to the equality engine
-    ok = d_equalityEngine.addEquality(nodeSlice, concat, utils::mkTrue());
-  } else {
-    // If the representative is a concat, we must solve it
-    // There is no need do add nodeSlice = concat as we will solve the representative of nodeSlice
-    std::set<TNode> assumptions;
-    std::vector<TNode> equalities;
-    d_equalityEngine.getExplanation(nodeSlice, nodeSliceRepresentative, equalities);
-    assumptions.insert(equalities.begin(), equalities.end());
-    ok = solveEquality(nodeSliceRepresentative, concat, assumptions);
-  }
-
-  Debug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << ") => " << d_setCollection.toString(d_nodeSlicing[nodeBase]) << std::endl;
-
-  return ok;
-}
-
 template <class TheoryBitvector>
 bool SliceManager<TheoryBitvector>::solveEquality(TNode lhs, TNode rhs) {
   std::set<TNode> assumptions;
@@ -541,11 +483,13 @@ bool SliceManager<TheoryBitvector>::isSliced(TNode node) const {
     if (find == d_nodeSlicing.end()) {
       result = nodeKind != kind::BITVECTOR_EXTRACT;
     } else {
+      set_reference sliceSet = (*find).second;
+      Assert(d_setCollection.size(sliceSet) >= 2);
       // The term is not sliced if one of the borders is not in the slice set or
       // there is a point between the borders      
       result = 
-	d_setCollection.contains(find->second, low) && d_setCollection.contains(find->second, high + 1) &&
-        (low == high || d_setCollection.count(find->second, low + 1, high) == 0);
+	d_setCollection.contains(sliceSet, low) && d_setCollection.contains(sliceSet, high + 1) &&
+        (low == high || d_setCollection.count(sliceSet, low + 1, high) == 0);
     }
   }
 
@@ -554,6 +498,68 @@ bool SliceManager<TheoryBitvector>::isSliced(TNode node) const {
 }
 
 template <class TheoryBitvector>
+bool SliceManager<TheoryBitvector>::addSlice(Node node, unsigned slicePoint) {
+  Debug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << ")" << std::endl;
+
+  bool ok = true;
+
+  int low  = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractLow(node) : 0;
+  int high = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractHigh(node) + 1: utils::getSize(node);
+  slicePoint += low;
+
+  TNode nodeBase = baseTerm(node);
+
+  set_reference sliceSet;
+  slicing_map::iterator find = d_nodeSlicing.find(nodeBase);
+  if (find == d_nodeSlicing.end()) {
+    d_nodeSlicing[nodeBase] = sliceSet = d_setCollection.newSet(0);
+    d_setCollection.insert(sliceSet, utils::getSize(nodeBase));
+  } else {
+    sliceSet = (*find).second;
+  }
+
+  Assert(d_setCollection.size(sliceSet) >= 2);
+
+  // What are the points surrounding the new slice point
+  int prev = d_setCollection.prev(sliceSet, slicePoint);
+  int next = d_setCollection.next(sliceSet, slicePoint);
+
+  // Add the slice to the set
+  d_setCollection.insert(sliceSet, slicePoint);
+  Debug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << "): current set " << d_setCollection.toString(sliceSet) << std::endl;
+
+  // Add the terms and the equality to the equality engine
+  Node t1 = utils::mkExtract(nodeBase, next - 1, slicePoint);
+  Node t2 = utils::mkExtract(nodeBase, slicePoint - 1, prev);
+  Node nodeSlice = (next == high && prev == low) ? node : utils::mkExtract(nodeBase, next - 1, prev);
+  Node concat = utils::mkConcat(t1, t2);
+
+  d_equalityEngine.addTerm(t1);
+  d_equalityEngine.addTerm(t2);
+  d_equalityEngine.addTerm(nodeSlice);
+  d_equalityEngine.addTerm(concat);
+
+  // We are free to add this slice, unless the slice has a representative that's already a concat
+  TNode nodeSliceRepresentative = d_equalityEngine.getRepresentative(nodeSlice);
+  if (nodeSliceRepresentative.getKind() != kind::BITVECTOR_CONCAT) {
+    // Add the slice to the equality engine
+    ok = d_equalityEngine.addEquality(nodeSlice, concat, utils::mkTrue());
+  } else {
+    // If the representative is a concat, we must solve it
+    // There is no need do add nodeSlice = concat as we will solve the representative of nodeSlice
+    std::set<TNode> assumptions;
+    std::vector<TNode> equalities;
+    d_equalityEngine.getExplanation(nodeSlice, nodeSliceRepresentative, equalities);
+    assumptions.insert(equalities.begin(), equalities.end());
+    ok = solveEquality(nodeSliceRepresentative, concat, assumptions);
+  }
+
+  Debug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << ") => " << d_setCollection.toString(d_nodeSlicing[nodeBase]) << std::endl;
+
+  return ok;
+}
+
+template <class TheoryBitvector>
 inline bool SliceManager<TheoryBitvector>::slice(TNode node, std::vector<Node>& sliced) {
 
   Debug("slicing") << "SliceManager::slice(" << node << ")" << std::endl;
@@ -572,18 +578,19 @@ inline bool SliceManager<TheoryBitvector>::slice(TNode node, std::vector<Node>&
   Assert(nodeBase.getKind() != kind::CONST_BITVECTOR);
 
   // The nodes slice set
-  set_collection::reference_type nodeSliceSet;
+  set_reference nodeSliceSet;
 
   // Find the current one or construct it
   slicing_map::iterator findSliceSet = d_nodeSlicing.find(nodeBase);
   if (findSliceSet == d_nodeSlicing.end()) {
-    nodeSliceSet = d_setCollection.newSet(utils::getSize(nodeBase));
-    d_setCollection.insert(nodeSliceSet, 0);
-    d_nodeSlicing[nodeBase] = nodeSliceSet;
+    d_nodeSlicing[nodeBase] = nodeSliceSet = d_setCollection.newSet(0);
+    d_setCollection.insert(nodeSliceSet, utils::getSize(nodeBase));
   } else {
     nodeSliceSet = d_nodeSlicing[nodeBase];
   }
 
+  Assert(d_setCollection.size(nodeSliceSet) >= 2);
+
   Debug("slicing") << "SliceManager::slice(" << node << "): current: " << d_setCollection.toString(nodeSliceSet) << std::endl;
   std::vector<size_t> slicePoints;
   if (low + 1 < high) {
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 2d823383c..2d989a563 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -89,6 +89,8 @@ void TheoryBV::check(Effort e) {
         assumptions.insert(assertion);
         d_out->conflict(mkConjunction(assumptions));
         return;
+      } else {
+        d_disequalities.push_back(assertion);
       }
       break;
     }
@@ -96,6 +98,32 @@ void TheoryBV::check(Effort e) {
       Unhandled();
     }
   }
+
+  if (fullEffort(e)) {
+
+    Debug("bitvector") << "TheoryBV::check(" << e << "): checking dis-equalities" << std::endl;
+
+    for (unsigned i = 0, i_end = d_disequalities.size(); i < i_end; ++ i) {
+
+      Debug("bitvector") << "TheoryBV::check(" << e << "): checking " << d_disequalities[i] << std::endl;
+
+      TNode equality = d_disequalities[i][0];
+      // Assumptions
+      std::set<TNode> assumptions;
+      Node lhsNormalized = d_eqEngine.normalize(equality[0], assumptions);
+      Node rhsNormalized = d_eqEngine.normalize(equality[1], assumptions);
+
+      Debug("bitvector") << "TheoryBV::check(" << e << "): normalizes to " << lhsNormalized << " = " << rhsNormalized << std::endl;
+
+      // No need to slice the equality, the whole thing *should* be deduced
+      if (lhsNormalized == rhsNormalized) {
+        Debug("bitvector") << "TheoryBV::check(" << e << "): conflict with " << utils::setToString(assumptions) << std::endl;
+        assumptions.insert(d_disequalities[i]);
+        d_out->conflict(mkConjunction(assumptions));
+        return;
+      }
+    }
+  }
 }
 
 bool TheoryBV::triggerEquality(size_t triggerId) {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 8eaa332eb..474c4d0cd 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -93,13 +93,16 @@ private:
   /** The asserted stuff */
   context::CDSet<TNode, TNodeHashFunction> d_assertions;
 
+  /** Asserted dis-equalities */
+  context::CDList<TNode> d_disequalities;
+
   /** Called by the equality managere on triggers */
   bool triggerEquality(size_t triggerId);
 
 public:
 
   TheoryBV(context::Context* c, OutputChannel& out) :
-    Theory(THEORY_BV, c, out), d_eqEngine(*this, c, "theory::bv::EqualityEngine"), d_sliceManager(*this, c), d_assertions(c) {
+    Theory(THEORY_BV, c, out), d_eqEngine(*this, c, "theory::bv::EqualityEngine"), d_sliceManager(*this, c), d_assertions(c), d_disequalities(c) {
   }
 
   BvEqualityEngine& getEqualityEngine() {