CBQI BV: Added EXTRACT handling. (#1240)

This adds inverse handling for BITVECTOR_EXTRACT. Fixes previously disabled regressions. These regressions are now enabled.

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 0795c3068cb1ee3cd37b3c05971fbfd52b94f065..8a65338a61329cd331c3bc26dd21b2dd875e8f3c 100644 (file)
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -34,7 +34,10 @@ static Node dropChild(Node n, unsigned index) {
   unsigned nchildren = n.getNumChildren();
   Assert(index < nchildren);
   Kind k = n.getKind();
-  Assert(k == AND || k == OR || k == BITVECTOR_MULT || k == BITVECTOR_PLUS);
+  Assert(k == BITVECTOR_AND
+         || k == BITVECTOR_OR
+         || k == BITVECTOR_MULT
+         || k == BITVECTOR_PLUS);
   NodeBuilder<> nb(NodeManager::currentNM(), k);
   for (unsigned i = 0; i < nchildren; ++i) {
     if (i == index) continue;
@@ -268,6 +271,7 @@ Node BvInverter::solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk,
     Assert(index < sv_t.getNumChildren());
     path.pop_back();
     Kind k = sv_t.getKind();
+    unsigned nchildren = sv_t.getNumChildren();
 
     /* inversions  */
     if (k == BITVECTOR_CONCAT) {
@@ -280,17 +284,22 @@ Node BvInverter::solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk,
       upper = bv::utils::getSize(t) - 1;
       lower = 0;
       NodeBuilder<> nb(nm, BITVECTOR_CONCAT);
-      for (unsigned i = 0; i < sv_t.getNumChildren(); i++) {
+      for (unsigned i = 0; i < nchildren; i++) {
         if (i < index)
           upper -= bv::utils::getSize(sv_t[i]);
         else if (i > index)
           lower += bv::utils::getSize(sv_t[i]);
       }
       t = bv::utils::mkExtract(t, upper, lower);
+    } else if (k == BITVECTOR_EXTRACT) {
+      Trace("bv-invert") << "bv-invert : Unsupported for index " << index
+                         << ", from " << sv_t << std::endl;
+      return Node::null();
+    } else if (k == BITVECTOR_NEG || k == BITVECTOR_NOT) {
+      t = NodeManager::currentNM()->mkNode(k, t);
     } else {
-      Node s = sv_t.getNumChildren() == 2
-        ? sv_t[1 - index]
-        : dropChild(sv_t, index);
+      Assert (nchildren >= 2);
+      Node s = nchildren == 2 ? sv_t[1 - index] : dropChild(sv_t, index);
       /* Note: All n-ary kinds except for CONCAT (i.e., AND, OR, MULT, PLUS)
        *       are commutative (no case split based on index). */
       if (k == BITVECTOR_PLUS) {
@@ -327,9 +336,7 @@ Node BvInverter::solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk,
         Node x = getSolveVariable(solve_tn);
         Node scl, scr;
         if (index == 0) {
-          /* x % s = t
-           * with side condition:
-           * TODO  */
+          /* x % s = t is rewritten to x - x / y * y */
           Trace("bv-invert") << "bv-invert : Unsupported for index " << index
                              << ", from " << sv_t << std::endl;
           return Node::null();
@@ -501,10 +508,8 @@ Node BvInverter::solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk,
         Node skv = getInversionNode(sc, solve_tn);
         /* now solving with the skolem node as the RHS */
         t = skv;
-      } else if (k == BITVECTOR_NEG || k == BITVECTOR_NOT) {
-        t = NodeManager::currentNM()->mkNode(k, t);
-        //}else if( k==BITVECTOR_ASHR ){
-        // TODO
+      //}else if( k==BITVECTOR_ASHR ){
+      // TODO
       } else {
         Trace("bv-invert") << "bv-invert : Unknown kind for bit-vector term "
                            << k

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index ec24fdd8b247aa18c34e673fa81b9e373083ff14..a2f5c18b52586a746a1e6fef8ccfa89d90c95bd2 100644 (file)
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -104,11 +104,9 @@ TESTS =    \
        qbv-test-urem-rewrite.smt2 \
        qbv-inequality2.smt2 \
        qbv-test-invert-bvult-1.smt2 \
-       intersection-example-onelane.proof-node22337.smt2 
-       
-# solved, but fail an assertion due to unhandled EXTRACT case
-#      nested9_true-unreach-call.i_575.smt2 
-#      small-pipeline-fixpoint-3.smt2
+       intersection-example-onelane.proof-node22337.smt2 \
+       nested9_true-unreach-call.i_575.smt2 \
+       small-pipeline-fixpoint-3.smt2
  
 
 # regression can be solved with --finite-model-find --fmf-inst-engine