From e5c363fe467c0a29df2c36da74a27413103d584a Mon Sep 17 00:00:00 2001
From: Liana Hadarean <lianahady@gmail.com>
Date: Tue, 11 Dec 2012 16:10:02 -0500
Subject: [PATCH] fixed some slicer bugs; set up bv theory to run bit-blaster
 to check for correctness

---
 src/theory/bv/bv_subtheory_core.cpp |  2 +-
 src/theory/bv/slicer.cpp            | 21 +++++++++++++++------
 src/theory/bv/theory_bv.cpp         | 19 +++++++++++++++----
 src/theory/bv/theory_bv_utils.h     |  4 ++--
 4 files changed, 33 insertions(+), 13 deletions(-)

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 2252fc274..8343ac3a6 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -228,7 +228,7 @@ void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
 }
 
 bool CoreSolver::storePropagation(TNode literal) {
-  return d_bv->storePropagation(literal, SUB_EQUALITY);
+  return d_bv->storePropagation(literal, SUB_CORE);
 }
   
 void CoreSolver::conflict(TNode a, TNode b) {
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index 73cad53b8..9eb0548d2 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -138,20 +138,22 @@ void SliceBlock::computeBlockBase(std::vector<RootId>& queue)  {
         Splinter* bottom, *top = NULL;
         SplinterPointer sp;
         slice->split(i, sp, bottom, top);
-          
+        Assert (bottom != NULL && top != NULL); 
+        Assert (i > bottom->getLow()); 
+        unsigned delta = i - bottom->getLow();   
         if (sp != Undefined) {
           // if we do need to split something else split it
           Debug("bv-slicer") <<"    must split " << sp.debugPrint(); 
-          Slice* slice = d_slicer->getSlice(sp);
+          Slice* other_slice = d_slicer->getSlice(sp);
           Splinter* s = d_slicer->getSplinter(sp);
-          Index cutPoint = s->getLow() + i; 
+          Index cutPoint = s->getLow() + delta; 
           Splinter* new_bottom = new Splinter(cutPoint, s->getLow());
           Splinter* new_top = new Splinter(s->getHigh(), cutPoint + 1);
           new_bottom->setPointer(SplinterPointer(d_rootId, row, bottom->getLow()));
           new_top->setPointer(SplinterPointer(d_rootId, row, top->getLow()));
 
-          slice->addSplinter(new_bottom->getLow(), new_bottom);
-          slice->addSplinter(new_top->getLow(), new_top); 
+          other_slice->addSplinter(new_bottom->getLow(), new_bottom);
+          other_slice->addSplinter(new_top->getLow(), new_top); 
           
           bottom->setPointer(SplinterPointer(sp.term, sp.row, new_bottom->getLow()));
           top->setPointer(SplinterPointer(sp.term, sp.row, new_top->getLow()));
@@ -324,6 +326,9 @@ void Slicer::registerSimpleEquality(TNode eq) {
         slice->addSplinter(high+1, s); 
       }
       block_a->addSlice(slice);
+      d_rootBlocks[id_a] = block_a; 
+      Debug("bv-slicer") << "     updated block" << id_a << " to " << endl;
+      Debug("bv-slicer") << block_a->debugPrint() << endl;
       return; 
     }
   }
@@ -341,7 +346,11 @@ void Slicer::registerSimpleEquality(TNode eq) {
   SplinterPointer sp_b = SplinterPointer(id_b, row_b, low_b); 
 
   slice_a->getSplinter(low_a)->setPointer(sp_b);
-  slice_b->getSplinter(low_b)->setPointer(sp_a); 
+  slice_b->getSplinter(low_b)->setPointer(sp_a);
+  Debug("bv-slicer") << "     updated block" << id_a << " to " << endl;
+  Debug("bv-slicer") << block_a->debugPrint() << endl;
+  Debug("bv-slicer") << "     updated block" <<id_b << " to " << endl;
+  Debug("bv-slicer") << block_b->debugPrint() << endl;
 }
 
 Slice* Slicer::makeSlice(TNode node) {
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index c4e16545f..d537b8e60 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -126,13 +126,24 @@ void TheoryBV::check(Effort e)
   }
 
   // FIXME: this is not quite correct as it does not take into account cardinality constraints 
-  if (!d_coreSolver.isCoreTheory()) {
+
+  if (d_coreSolver.isCoreTheory()) {
+    // paranoid check to make sure results of bit-blaster agree with slicer for core theory
+    if (inConflict()) {
+      d_conflict = false;
+      d_bitblastSolver.addAssertions(new_assertions, Theory::EFFORT_FULL); 
+      Assert (inConflict()); 
+    } else {
+      d_bitblastSolver.addAssertions(new_assertions, Theory::EFFORT_FULL); 
+      Assert (!inConflict()); 
+    }
+  }
+  else {
     if (!inConflict()) {
       // sending assertions to the bitblast solver
       d_bitblastSolver.addAssertions(new_assertions, e);
     }
-  }
-
+  } 
   if (inConflict()) {
     sendConflict();
   }
@@ -252,7 +263,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
   // Ask the appropriate subtheory for the explanation
   if (propagatedBy(literal, SUB_CORE)) {
-    Debug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl;
+    Debug("bitvector::explain") << "TheoryBV::explain(" << literal << "): CORE" << std::endl;
     d_coreSolver.explain(literal, assumptions);
   } else {
     Assert(propagatedBy(literal, SUB_BITBLAST));
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 3f59be86d..565ec9704 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -73,11 +73,11 @@ inline Node mkAnd(std::vector<TNode>& children) {
   std::set<TNode> distinctChildren;
   distinctChildren.insert(children.begin(), children.end());
   
-  if (children.size() == 0) {
+  if (distinctChildren.size() == 0) {
     return mkTrue();
   }
   
-  if (children.size() == 1) {
+  if (distinctChildren.size() == 1) {
     return *children.begin();
   }
   
-- 
2.30.2