From a8074075b507246379f7f24f2a13cc2340eb7fc9 Mon Sep 17 00:00:00 2001
From: Liana Hadarean <lianahady@gmail.com>
Date: Tue, 19 Mar 2013 23:39:25 -0400
Subject: [PATCH] fixed reversed concat in core theory

---
 src/theory/bv/bv_subtheory_core.cpp        |  6 +++---
 src/theory/bv/bv_subtheory_inequality.h    |  2 +-
 src/theory/bv/slicer.cpp                   | 17 ++++++++++-------
 src/theory/bv/theory_bv.cpp                |  2 +-
 test/regress/regress0/bv/core/slice-14.smt |  6 +++---
 5 files changed, 18 insertions(+), 15 deletions(-)

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index d8fc596c0..01378da56 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -50,7 +50,7 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
     d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true);
     d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true);
-    d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT);
+    d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT, true);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
@@ -197,8 +197,8 @@ bool CoreSolver::check(Theory::Effort e) {
 }
 
 bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
-  Debug("bv-slicer") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
-  Debug("bv-slicer") << "                     reason=" << reason << endl;
+  Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
+  Debug("bv-slicer-eq") << "                     reason=" << reason << endl;
   // Notify the equality engine 
   if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_CORE) ) {
     Trace("bitvector::core") << "     (assert " << fact << ")\n";  
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 92248205f..07c561c84 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -38,7 +38,7 @@ public:
   bool check(Theory::Effort e);
   void propagate(Theory::Effort e); 
   void explain(TNode literal, std::vector<TNode>& assumptions);
-  bool isInequalityTheory() { return false; }
+  bool isInequalityTheory() { return true; }
   virtual void collectModelInfo(TheoryModel* m) {}
 }; 
 
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index 92166224b..474c70052 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -657,15 +657,18 @@ void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp, std::ve
   }
   
   // construct actual extract nodes
-  Index current_low = 0;
-  Index current_high = 0; 
-  for (unsigned i = 0; i < nf.decomp.size(); ++i) {
-    Index current_size = d_unionFind.getBitwidth(nf.decomp[i]); 
-    current_high += current_size; 
-    Node current = Rewriter::rewrite(utils::mkExtract(node, current_high - 1, current_low));
-    current_low += current_size;
+  Index size = utils::getSize(node);
+  Index current_low = size - 1;
+  Index current_high = size - 1;
+  
+  for (int i = nf.decomp.size() - 1; i>=0 ; --i) {
+    Index current_size = d_unionFind.getBitwidth(nf.decomp[i]);
+    current_low = current_low - current_size; 
+    Node current = Rewriter::rewrite(utils::mkExtract(node, current_high, current_low+1));
+    current_high -= current_size;
     decomp.push_back(current); 
   }
+  
 
   Debug("bv-slicer") << "as [";
   for (unsigned i = 0; i < decomp.size(); ++i) {
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index a794d63a3..33f464400 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -128,7 +128,7 @@ void TheoryBV::check(Effort e)
 
   Assert (!ok == inConflict());
   if (!inConflict() && !d_coreSolver.isCoreTheory()) {
-    // if (!inConflict() && !d_inequalitySolver.isInequalityTheory()) {
+  // if (!inConflict() && !d_inequalitySolver.isInequalityTheory()) {
     ok = d_bitblastSolver.check(e); 
   }
   
diff --git a/test/regress/regress0/bv/core/slice-14.smt b/test/regress/regress0/bv/core/slice-14.smt
index b40f7938d..db3a3a7b3 100644
--- a/test/regress/regress0/bv/core/slice-14.smt
+++ b/test/regress/regress0/bv/core/slice-14.smt
@@ -1,8 +1,8 @@
 (benchmark slice
   :status unsat
   :logic QF_BV
-  :extrafuns ((x BitVec[16]))
-  :assumption (= (extract[15:1] x) (extract[14:0] x))
+  :extrafuns ((x BitVec[6]))
+  :assumption (= (extract[5:1] x) (extract[4:0] x))
   :assumption (= (extract[0:0] x) bv0[1])
-  :formula (not (= x bv0[16]))
+  :formula (not (= x bv0[6]))
 )
-- 
2.30.2