fixed reversed concat in core theory

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index d8fc596c0b9f0aadd75310f3cd8f542d98cc51d5..01378da56e6023ee0ee2b4799e4f0951ff2ad0c5 100644 (file)
--- 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 92248205f63d8ede2599266c95dc2710cf9029a1..07c561c848481ee1cedfdca8e5b855a6a4655eca 100644 (file)
--- 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 92166224b19b578a7b9783eb4367ca78c0caa977..474c70052067e309d515e3c806ffad5015d0e9c0 100644 (file)
--- 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 a794d63a305ef1f1cec9ab1be3608e8068dbaeaa..33f46440006fb5441ee70700193ca509a9eef672 100644 (file)
--- 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 b40f7938d2547441d2445721c42517951811dd02..db3a3a7b3fc42c85eda8d8ac39e3804d620f1b53 100644 (file)
--- 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]))
 )