started working on incremental slicer - not compiling

3 files changed, 78 insertions, 12 deletions

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index d678d7e31..3f2ede9e2 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -51,6 +51,7 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv, Slicer* slicer)
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
     d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT);
     d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS);
+    d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index f41612df3..3a6ca8a2f 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -216,6 +216,7 @@ void UnionFind::merge(TermId t1, TermId t2) {
 
   Assert (! hasChildren(t1) && ! hasChildren(t2));
   setRepr(t1, t2); 
+  recordOperation(UnionFind::MERGE, t1); 
   d_representatives.erase(t1);
   d_statistics.d_numRepresentatives += -1; 
 }
@@ -224,7 +225,7 @@ TermId UnionFind::find(TermId id) {
   TermId repr = getRepr(id); 
   if (repr != UndefinedId) {
     TermId find_id =  find(repr);
-    setRepr(id, find_id);
+    // setRepr(id, find_id);
     return find_id; 
   }
   return id; 
@@ -252,6 +253,7 @@ void UnionFind::split(TermId id, Index i) {
     TermId bottom_id = addTerm(i);
     TermId top_id = addTerm(getBitwidth(id) - i);
     setChildren(id, top_id, bottom_id);
+    recordOperation(UnionFind::SPLIT, id); 
 
   } else {
     Index cut = getCutPoint(id); 
@@ -415,6 +417,37 @@ void UnionFind::ensureSlicing(const ExtractTerm& term) {
   split(id, term.low);
 }
 
+void UnionFind::backtrack() {
+  for (int i = d_undoStack.size() -1; i >= d_undoStackIndex; ++i) {
+    Operation op = d_undoStack.back(); 
+    d_undoStack.pop_back();
+    if (op.op == UnionFind::MERGE) {
+      undoMerge(op.id); 
+    } else {
+      Assert (op.op == UnionFind::SPLIT);
+      undoSplit(op.id); 
+    }
+  }
+}
+
+void UnionFind::undoMerge(TermId id) {
+  Node& node = getNode(id);
+  Assert (getRepr(id) != id);
+  setRepr(id, id); 
+}
+
+void UnionFind::undoSplit(TermId id) {
+  Node& node = getNode(id);
+  Assert (hasChildren(node));
+  setChildren(id, UndefindId, UndefinedId); 
+}
+
+void UnionFind::recordOperation(OperationKind op, TermId term) {
+  ++d_undoStackIndex;
+  d_undoStack.push_back(Operation(op, term));
+  Assert (d_undoStack.size() == d_undoStackIndex); 
+}
+
 /**
  * Slicer
  * 
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index 88254b983..731141262 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -29,6 +29,10 @@
 #include "util/index.h"
 #include "expr/node.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "context/context.h"
+#include "context/cdhashset.h"
+#include "context/cdo.h"
+
 #ifndef __CVC4__THEORY__BV__SLICER_BV_H
 #define __CVC4__THEORY__BV__SLICER_BV_H
 
@@ -80,7 +84,7 @@ public:
  * UnionFind
  * 
  */
-typedef __gnu_cxx::hash_set<TermId> TermSet;
+typedef context::CDHashSet<uint32_t> CDTermSet;
 typedef std::vector<TermId> Decomposition; 
 
 struct ExtractTerm {
@@ -121,7 +125,7 @@ struct NormalForm {
 };
 
 
-class UnionFind {
+class UnionFind : public context::ContextNotifyObj {
   class Node {
     Index d_bitwidth;
     TermId d_ch1, d_ch0;
@@ -157,7 +161,7 @@ class UnionFind {
   /// 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;
+  CDTermSet d_representatives;
   
   void getDecomposition(const ExtractTerm& term, Decomposition& decomp);
   void handleCommonSlice(const Decomposition& d1, const Decomposition& d2, TermId common);
@@ -187,6 +191,28 @@ class UnionFind {
     d_nodes[id].setChildren(ch1, ch0); 
   }
 
+  /* Backtracking mechanisms */
+
+  enum OperationKind {
+    MERGE,
+    SPLIT
+  }; 
+
+  struct Operation {
+    OperationKind op;
+    TermId id;
+    Operation(OperationKind o, TermId i)
+      : op(o), id(i) {}
+  };
+
+  std::vector<Operation> d_undoStack;
+  context::CDO<unsigned> d_undoStackIndex;
+
+  void backtrack();
+  void undoMerge(TermId id);
+  void undoSplit(TermId id); 
+  void recordOperation(OperationKind op, TermId term);
+  
   class Statistics {
   public:
     IntStat d_numNodes; 
@@ -195,18 +221,18 @@ class UnionFind {
     IntStat d_numMerges;
     AverageStat d_avgFindDepth;
     ReferenceStat<unsigned> d_numAddedEqualities; 
-    //IntStat d_numAddedEqualities; 
     Statistics();
     ~Statistics();
   };
 
-  Statistics d_statistics
-;
-  
+  Statistics d_statistics;
 public:
-  UnionFind()
+  UnionFind(context::Context* ctx)
     : d_nodes(),
-      d_representatives()
+      d_representatives(ctx),
+      d_undoStack(),
+      d_undoStackIndex(ctx),
+      d_statistics()
   {}
 
   TermId addTerm(Index bitwidth);
@@ -223,6 +249,11 @@ public:
     return d_nodes[id].getBitwidth(); 
   }
   std::string debugPrint(TermId id);
+
+  void contextNotifyPop() {
+    backtrack();
+  }
+
   friend class Slicer; 
 };
 
@@ -233,16 +264,17 @@ class Slicer {
   UnionFind d_unionFind;
   ExtractTerm registerTerm(TNode node); 
 public:
-  Slicer()
+  Slicer(context::Context* ctx)
     : d_idToNode(),
       d_nodeToId(),
       d_coreTermCache(),
-      d_unionFind()
+      d_unionFind(ctx)
   {}
   
   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);
   static unsigned d_numAddedEqualities; 
 };