fixed some more bugs

1 files changed, 19 insertions, 12 deletions

diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index b27b85e65..c7451c288 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -60,6 +60,11 @@ public:
   bool isEmpty() const;
   std::string debugPrint() const;
   Index getBitwidth() const { return d_size; }
+  void clear() {
+    for (unsigned i = 0; i < d_repr.size(); ++i) {
+      d_repr[i] = 0; 
+    }
+  }
   bool operator==(const Base& other) const {
     if (other.getBitwidth() != getBitwidth())
       return false;
@@ -110,40 +115,41 @@ struct NormalForm {
    * 
    * @return 
    */
-  TermId getTerm(Index i, const UnionFind& uf) const;
-  std::string debugPrint(const UnionFind& uf) const; 
+  std::pair<TermId, Index> getTerm(Index i, const UnionFind& uf) const;
+  std::string debugPrint(const UnionFind& uf) const;
+  void clear() { base.clear(); decomp.clear(); }
 };
 
 
 class UnionFind {
   class Node {
     Index d_bitwidth;
-    TermId d_ch1, d_ch2;
+    TermId d_ch1, d_ch0;
     TermId d_repr;
   public:
     Node(Index b)
   : d_bitwidth(b),
     d_ch1(UndefinedId),
-    d_ch2(UndefinedId), 
+    d_ch0(UndefinedId), 
     d_repr(UndefinedId)
     {}
     
     TermId getRepr() const { return d_repr; }
     Index getBitwidth() const { return d_bitwidth; }
-    bool hasChildren() const { return d_ch1 != UndefinedId && d_ch2 != UndefinedId; }
+    bool hasChildren() const { return d_ch1 != UndefinedId && d_ch0 != UndefinedId; }
 
     TermId getChild(Index i) const {
       Assert (i < 2);
-      return i == 0? d_ch1 : d_ch2;
+      return i == 0? d_ch0 : d_ch1;
     }
     void setRepr(TermId id) {
       Assert (! hasChildren());
       d_repr = id;
     }
-    void setChildren(TermId ch1, TermId ch2) {
+    void setChildren(TermId ch1, TermId ch0) {
       Assert (d_repr == UndefinedId && !hasChildren());
       d_ch1 = ch1;
-      d_ch2 = ch2; 
+      d_ch0 = ch0; 
     }
     std::string debugPrint() const;
   };
@@ -165,7 +171,7 @@ class UnionFind {
     return d_nodes[id].getChild(i); 
   }
   Index getCutPoint(TermId id) const {
-    return getBitwidth(getChild(id, 1)); 
+    return getBitwidth(getChild(id, 0)); 
   }
   bool hasChildren(TermId id) const {
     Assert (id < d_nodes.size());
@@ -176,9 +182,9 @@ class UnionFind {
     Assert (id < d_nodes.size());
     d_nodes[id].setRepr(new_repr); 
   }
-  void setChildren(TermId id, TermId ch1, TermId ch2) {
-    Assert (id < d_nodes.size() && getBitwidth(id) == getBitwidth(ch1) + getBitwidth(ch2));
-    d_nodes[id].setChildren(ch1, ch2); 
+  void setChildren(TermId id, TermId ch1, TermId ch0) {
+    Assert (id < d_nodes.size() && getBitwidth(id) == getBitwidth(ch1) + getBitwidth(ch0));
+    d_nodes[id].setChildren(ch1, ch0); 
   }
 
   
@@ -201,6 +207,7 @@ public:
     Assert (id < d_nodes.size());
     return d_nodes[id].getBitwidth(); 
   }
+  std::string debugPrint(TermId id); 
 
 };