minor bug fixes

diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index 51775f72a96f46f61dffebf5de7a90158bd0d0c2..e499765725aa064a4e4f827bc7db90081f8e2cac 100644 (file)
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -29,6 +29,7 @@ using namespace std;
 
 void Base::decomposeNode(TNode node, std::vector<Node>& decomp) {
   Debug("bv-slicer") << "Base::decomposeNode " << node << "\n with base" << debugPrint() << endl;
+  
   Index low = 0;
   Index high = utils::getSize(node) - 1; 
   if (node.getKind() == kind::BITVECTOR_EXTRACT) {
@@ -237,7 +238,7 @@ void Slicer::splitEqualities(TNode node, std::vector<Node>& equalities) {
   if (base1 != Base(width)) {
     // we split the equalities according to the base
     int last = 0; 
-    for (unsigned i = 1; i < utils::getSize(t1); ++i) {
+    for (unsigned i = 0; i < utils::getSize(t1); ++i) {
       if (base1.isCutPoint(i)) {
         Node extract1 = Rewriter::rewrite(utils::mkExtract(t1, i, last));
         Node extract2 = Rewriter::rewrite(utils::mkExtract(t2, i, last));
@@ -255,13 +256,13 @@ void Slicer::splitEqualities(TNode node, std::vector<Node>& equalities) {
 void Slicer::processEquality(TNode node) {
   Assert (node.getKind() == kind::EQUAL);
   Debug("bv-slicer") << "theory::bv::Slicer::processEquality " << node << endl; 
-  std::vector<Node> equalities;
-  splitEqualities(node, equalities); 
-  for (unsigned i = 0; i < equalities.size(); ++i) {
-    Debug("bv-slicer") << "    splitEqualities " << node << endl;
-    registerSimpleEquality(equalities[i]); 
-    d_simpleEqualities.push_back(equalities[i]);
-  }
+  // std::vector<Node> equalities;
+  // splitEqualities(node, equalities); 
+  // for (unsigned i = 0; i < equalities.size(); ++i) {
+  //   Debug("bv-slicer") << "    splitEqualities " << node << endl;
+  registerSimpleEquality(node); 
+  d_simpleEqualities.push_back(node);
+  //  }
 }
 
 void Slicer::registerSimpleEquality(TNode eq) {
@@ -269,7 +270,10 @@ void Slicer::registerSimpleEquality(TNode eq) {
   Debug("bv-slicer") << "theory::bv::Slicer::registerSimpleEquality " << eq << endl;  
   TNode a = eq[0];
   TNode b = eq[1];
- 
+
+  if (a == b)
+    return;
+  
   RootId id_a = registerTerm(a);
   RootId id_b = registerTerm(b);
   
@@ -284,7 +288,7 @@ void Slicer::registerSimpleEquality(TNode eq) {
     low_b  = utils::getExtractLow(b);
   }
 
-  if (id_a == id_b) {
+  if (id_a == id_b ) {
     // we are in the special case a[i0:j0] = a[i1:j1]
     Index high_a = utils::getExtractHigh(a);
     Index high_b = utils::getExtractHigh(b);
@@ -446,50 +450,17 @@ void Slicer::computeCoarsestBase() {
   debugCheckBase(); 
 }
 
-void Slicer::getExtractOverBase(TNode node, std::vector<Node>& decomp) {
+// void Slicer::getExtractOverBase(TNode node, std::vector<Node>& decomp) {
   
-}
+// }
+
 
 void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp) {
-  if (node.getKind() == kind::BITVECTOR_CONCAT) {
-    for (unsigned i = 0; i < node.getNumChildren(); ++i) {
-      TNode root = node[i].getKind() == kind::BITVECTOR_EXTRACT ? node[i][0] : node[i]; 
-      Assert (isRootTerm(root)); 
-      Base base = getSliceBlock(getRootId(root))->getBase();
-      std::vector<Node> decomp_i; 
-      base.decomposeNode(node[i], decomp_i);
-      // TODO: add check for extract and finish this code here
-      
-      if (node[i].getKind() == kind::BITVECTOR_EXTRACT) {
-        unsigned low = utils::getExtractLow(node[i]); 
-        unsigned high = utils::getExtractHigh(node[i]); 
-        unsigned size = 0;
-        bool add = false;
-        for (int i = decomp_i.size() - 1; i >= 0; --i) {
-          int size_i = utils::getSize(decomp_i[i]);
-          if (low > size + size_i - 1 && !add) {
-            add = true; 
-            Node first = utils::mkExtract(decomp_i[i], size + size_i -1, low - size);
-            decomp.push_back(first); 
-          }
-          if (high < size + size_i - 1 && add) {
-            add = false;
-            Node last = utils::mkExtract(decomp_i[i], size + size_i - 1, high - size);
-            decomp.push_back(last); 
-          }
-          if(add) {
-            decomp.push_back(decomp_i[i]); 
-          }
-          size += size_i; 
-        }
-      }
-    }
-  } else {
-    TNode root = node.getKind() == kind::BITVECTOR_EXTRACT ? node[0] : node; 
-    Assert (isRootTerm(root)); 
-    Base base = getSliceBlock(getRootId(root))->getBase();
-    base.decomposeNode(node, decomp);
-  }
+  Assert (node.getKind() != kind::BITVECTOR_CONCAT); 
+  TNode root = node.getKind() == kind::BITVECTOR_EXTRACT ? node[0] : node; 
+  Assert (isRootTerm(root)); 
+  Base base = getSliceBlock(getRootId(root))->getBase();
+  base.decomposeNode(node, decomp);
 }
 
 void Slicer::debugCheckBase() {

diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index cb4636fef73d81255523770f08828d73d65d7f1a..fa9b65ce101b975657bc412231523a4491341a1e 100644 (file)
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -303,7 +303,7 @@ typedef std::vector<Splinter*> Splinters;
 typedef std::vector<SliceBlock*> SliceBlocks;
 
 class Slicer {
-  std::vector<TNode> d_simpleEqualities; /**< equalities of the form a[i0:j0] = b[i1:j1] */
+  std::vector<Node> d_simpleEqualities; /**< equalities of the form a[i0:j0] = b[i1:j1] */
   Roots d_roots;
   uint32_t d_numRoots; 
   NodeRootIdMap d_nodeRootMap;
@@ -323,9 +323,10 @@ public:
    */
   void processEquality(TNode node);
   bool isCoreTerm(TNode node); 
+  static void splitEqualities(TNode node, std::vector<Node>& equalities);
 private:
   void registerSimpleEquality(TNode node);
-  void splitEqualities(TNode node, std::vector<Node>& equalities);
+
   TNode addSimpleTerm(TNode t);
   bool isRootTerm(TNode node);
 

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index d537b8e606e6add76d0b785b010698daf2e92b0b..bb16e00cea69f5fd1b59e5dc03413f19a7fa9d76 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -210,6 +210,13 @@ Node TheoryBV::ppRewrite(TNode t)
     Node result = RewriteRule<BitwiseEq>::run<false>(t);
     return Rewriter::rewrite(result);
   }
+  
+  if (t.getKind() == kind::EQUAL) {
+    std::vector<Node> equalities;
+    Slicer::splitEqualities(t, equalities);
+    return utils::mkAnd(equalities); 
+  }
+  
   return t;
 }