compiling implementation of new slicer finished; need to add debugging information and debug.

1 files changed, 71 insertions, 56 deletions

diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index 288b72bac..7ab40652d 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -26,7 +26,7 @@
 
 #include "util/bitvector.h"
 #include "util/statistics_registry.h"
-
+#include "util/index.h"
 #include "expr/node.h"
 #include "theory/bv/theory_bv_utils.h"
 #ifndef __CVC4__THEORY__BV__SLICER_BV_H
@@ -38,10 +38,11 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-typedef uint32_t TermId;
-typedef uint32_t Index;
 
 
+typedef Index TermId;
+extern const TermId UndefinedId;
+
 
 /** 
  * Base
@@ -51,13 +52,23 @@ class Base {
   Index d_size;
   std::vector<uint32_t> d_repr;
 public:
-  Base(uint32_t size);
+  Base(Index size);
   void sliceAt(Index index); 
   void sliceWith(const Base& other);
   bool isCutPoint(Index index) const;
   void diffCutPoints(const Base& other, Base& res) const;
   bool isEmpty() const;
   std::string debugPrint() const;
+  Index getBitwidth() const { return d_size; }
+  bool operator==(const Base& other) const {
+    if (other.getBitwidth() != getBitwidth())
+      return false;
+    for (unsigned i = 0; i < d_repr.size(); ++i) {
+      if (d_repr[i] != other.d_repr[i])
+        return false;
+    }
+    return true; 
+  }
 }; 
 
 /**
@@ -72,88 +83,80 @@ struct ExtractTerm {
   Index high;
   Index low;
   ExtractTerm(TermId i, Index h, Index l)
-    : id (i)
-      high(h)
+    : id (i),
+      high(h),
       low(l)
   {
-    Assert (h >= l && id != -1); 
+    Assert (h >= l && id != UndefinedId); 
   }
+  Index getBitwidth() const { return high - low + 1; } 
 };
 
+class UnionFind; 
+
 struct NormalForm {
   Base base;
   Decomposition decomp;
+
   NormalForm(Index bitwidth)
     : base(bitwidth),
       decomp()
   {}
+  /** 
+   * Returns the term in the decomposition on which the index i
+   * falls in
+   * @param i 
+   * 
+   * @return 
+   */
+  TermId getTerm(Index i, const UnionFind& uf) const; 
 };
 
 
 class UnionFind {
   class Node {
-    TermId d_repr;
-    TermId d_ch1, d_ch2;
     Index d_bitwidth;
+    TermId d_ch1, d_ch2;
+    TermId d_repr;    
   public:
     Node(Index b)
   : d_bitwidth(b),
-    d_ch1(-1),
-    d_ch2(-1), 
-    d_repr(-1)
+    d_ch1(UndefinedId),
+    d_ch2(UndefinedId), 
+    d_repr(UndefinedId)
     {}
     
     TermId getRepr() const { return d_repr; }
     Index getBitwidth() const { return d_bitwidth; }
-    bool hasChildren() const { return d_ch1 != -1 && d_ch2 != -1; }
+    bool hasChildren() const { return d_ch1 != UndefinedId && d_ch2 != UndefinedId; }
 
     TermId getChild(Index i) const {
       Assert (i < 2);
-      return i == 0? ch1 : ch2;
+      return i == 0? d_ch1 : d_ch2;
     }
-    Index getCutPoint() const {
-      Assert (d_ch1 != -1 && d_ch2 != -1);
-      return getNode(d_ch1).getBitwidth(); 
+    Index getCutPoint(const UnionFind& uf) const {
+      Assert (d_ch1 != UndefinedId && d_ch2 != UndefinedId);
+      return uf.getNode(d_ch1).getBitwidth(); 
     }
     void setRepr(TermId id) {
-      Assert (d_children.empty());
+      Assert (! hasChildren());
       d_repr = id;
     }
 
     void setChildren(TermId ch1, TermId ch2) {
-      Assert (d_repr == -1 && d_children.empty());
-      markAsNotTopLevel(ch1);
-      markAsNotTopLevel(ch2); 
-      d_children.push_back(ch1);
-      d_children.push_back(ch2); 
+      Assert (d_repr == UndefinedId && !hasChildren());
+      d_ch1 = ch1;
+      d_ch2 = ch2; 
     }
-    
-    // void setChildren(TermId ch1, TermId ch2, TermId ch3) {
-    //   Assert (d_repr == -1 && d_children.empty());
-    //   d_children.push_back(ch1);
-    //   d_children.push_back(ch2);
-    //   d_children.push_back(ch3); 
-    // }
-    
   };
 
+  /// map from TermId to the nodes that represent them 
   std::vector<Node> d_nodes;
-
+  /// a term is in this set if it is its own representative
   TermSet d_representatives;
-  TermSet d_topLevelTerms;
-  void markAsNotTopLevel(TermId id) {
-    if (d_topLevelTerms.find(id) != d_topLevelTerms.end())
-      d_topLevelTerms.erase(id); 
-  }
-
-  bool isTopLevel(TermId id) {
-    return d_topLevelTerms.find(id) != d_topLevelTerms.end(); 
-  }
   
-  Index getBitwidth(TermId id) {
-    Assert (id < d_nodes.size());
-    return d_nodes[id].getBitwidth(); 
-  }
+  void getDecomposition(const ExtractTerm& term, Decomposition& decomp);
+  void handleCommonSlice(const Decomposition& d1, const Decomposition& d2, TermId common);
   
 public:
   UnionFind()
@@ -162,32 +165,44 @@ public:
   {}
 
   TermId addTerm(Index bitwidth);
+  void unionTerms(const ExtractTerm& t1, const ExtractTerm& t2); 
   void merge(TermId t1, TermId t2);
-  TermId find(TermId t1); 
-  TermId split(TermId term, Index i);
-
-  void getNormalForm(ExtractTerm term, NormalForm& nf);
-  void alignSlicings(NormalForm& nf1, NormalForm& nf2);
+  TermId find(TermId t1) const ; 
+  void split(TermId term, Index i);
 
-  Node getNode(TermId id) {
+  void getNormalForm(const ExtractTerm& term, NormalForm& nf);
+  void alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2);
+  void ensureSlicing(const ExtractTerm& term);
+  
+  Node getNode(TermId id) const {
     Assert (id < d_nodes.size());
     return d_nodes[id]; 
   }
+  Index getBitwidth(TermId id) const {
+    Assert (id < d_nodes.size());
+    return d_nodes[id].getBitwidth(); 
+  }
+
 };
 
 class Slicer {
   __gnu_cxx::hash_map<TermId, TNode> d_idToNode;
-  __gnu_cxx::hash_map<TNode, TermId> d_nodeToId;
-  UnionFind d_unionFind();
- 
+  __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> d_nodeToId;
+  __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_coreTermCache; 
+  UnionFind d_unionFind;
+  ExtractTerm registerTerm(TNode node); 
 public:
   Slicer()
-    : d_topLevelTerms(),
+    : d_idToNode(),
+      d_nodeToId(),
+      d_coreTermCache(),
       d_unionFind()
   {}
   
-  void getBaseDecomposition(TNode node, std::vector<Node>& decomp) const;
+  void getBaseDecomposition(TNode node, std::vector<Node>& decomp);
   void processEquality(TNode eq);
+  bool isCoreTerm (TNode node);
+  static void splitEqualities(TNode node, std::vector<Node>& equalities); 
 }; 
 
 }/* CVC4::theory::bv namespace */