Bv2int fail on demand

Postpone failure in bv-to-int preprocessing pass.

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 75136913c184910f10dfac8d3e04d6a19707dd93..cb78b089705b9ba6b2a82dad4a0b70b6209da646 100644 (file)
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "options/uf_options.h"
 #include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/rewriter.h"
@@ -315,9 +316,7 @@ Node BVToInt::bvToInt(Node n)
             }
             else
             {
-              // Boolean variables are left unchanged.
-              AlwaysAssert(current.getType() == d_nm->booleanType()
-                           || current.getType().isSort());
+              // variables other than bit-vector variables are left intact
               d_bvToIntCache[current] = current;
             }
           }
@@ -696,6 +695,8 @@ Node BVToInt::bvToInt(Node n)
                * We cache both the term itself (e.g., f(a)) and the function
                * symbol f.
                */
+
+              //Construct the function itself
               Node bvUF = current.getOperator();
               Node intUF;
               TypeNode tn = current.getOperator().getType();
@@ -729,38 +730,57 @@ Node BVToInt::bvToInt(Node n)
                 // Insert the function symbol itself to the cache
                 d_bvToIntCache[bvUF] = intUF;
               }
-              translated_children.insert(translated_children.begin(), intUF);
-              // Insert the term to the cache
-              d_bvToIntCache[current] =
-                  d_nm->mkNode(kind::APPLY_UF, translated_children);
+              if (childrenTypesChanged(current) && options::ufHo()) {
               /**
-               * Add range constraints if necessary.
-               * If the original range was a BV sort, the current application of
-               * the fucntion Must be within the range determined by the
-               * bitwidth.
+               * higher order logic allows comparing between functions
+               * The current translation does not support this,
+               * as the translated functions may be different outside
+               * of the bounds that were relevant for the original
+               * bit-vectors.
                */
-              if (bvRange.isBitVector())
-              {
-                d_rangeAssertions.insert(
-                    mkRangeConstraint(d_bvToIntCache[current],
-                                      current.getType().getBitVectorSize()));
+                  throw TypeCheckingException(
+                      current.toExpr(),
+                      string("Cannot translate to Int: ") + current.toString());
               }
-              break;
+              else {
+                translated_children.insert(translated_children.begin(), intUF);
+                // Insert the term to the cache
+                d_bvToIntCache[current] =
+                    d_nm->mkNode(kind::APPLY_UF, translated_children);
+                /**
+                 * Add range constraints if necessary.
+                 * If the original range was a BV sort, the current application of
+                 * the function Must be within the range determined by the
+                 * bitwidth.
+                 */
+                if (bvRange.isBitVector())
+                {
+                  d_rangeAssertions.insert(
+                      mkRangeConstraint(d_bvToIntCache[current],
+                                        current.getType().getBitVectorSize()));
+                }
+              }
+                break;
             }
             default:
             {
-              if (Theory::theoryOf(current) == THEORY_BOOL)
-              {
+              if (childrenTypesChanged(current)) {
+                /**
+                 * This is "failing on demand":
+                 * We throw an exception if we encounter a case
+                 * that we do not know how to translate,
+                 * only if we actually need to construct a new
+                 * node for such a case.
+                 */
+                  throw TypeCheckingException(
+                      current.toExpr(),
+                      string("Cannot translate to Int: ") + current.toString());
+              }
+              else {
                 d_bvToIntCache[current] =
                     d_nm->mkNode(oldKind, translated_children);
-                break;
-              }
-              else
-              {
-                // Currently, only QF_UFBV formulas are handled.
-                // In the future, more theories should be supported, e.g., arrays.
-                Unimplemented();
               }
+              break;
             }
           }
         }
@@ -771,6 +791,19 @@ Node BVToInt::bvToInt(Node n)
   return d_bvToIntCache[n];
 }
 
+bool BVToInt::childrenTypesChanged(Node n) {
+  bool result = false;
+  for (Node child : n) {
+    TypeNode originalType = child.getType();
+    TypeNode newType = d_bvToIntCache[child].getType();
+    if (! newType.isSubtypeOf(originalType)) {
+      result = true;
+      break;
+    }
+  }
+  return result;
+}
+
 BVToInt::BVToInt(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "bv-to-int"),
       d_binarizeCache(),

diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h
index dd02d98ec84899e5ef0695ec1f074dcd2a45c8a9..f0e0ea02e665006ba34a3892ec9b6b2d85053354 100644 (file)
--- a/src/preprocessing/passes/bv_to_int.h
+++ b/src/preprocessing/passes/bv_to_int.h
@@ -231,6 +231,8 @@ class BVToInt : public PreprocessingPass
    */
   Node modpow2(Node n, uint64_t exponent);
 
+  bool childrenTypesChanged(Node n);
+
   /**
    * Add the range assertions collected in d_rangeAssertions
    * (using mkRangeConstraint) to the assertion pipeline.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1d096e1fede614fd2777630716a05818de1ea305..d3ba34b6ceecde4f7de5afe6f5b5dc9ba3a8df06 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1206,7 +1206,6 @@ void SmtEngine::setDefaults() {
     if (d_logic.isTheoryEnabled(THEORY_BV))
     {
       d_logic = d_logic.getUnlockedCopy();
-      d_logic.disableTheory(THEORY_BV);
       d_logic.enableTheory(THEORY_ARITH);
       d_logic.arithNonLinear();
       d_logic.lock();

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 02eb158263a4e3e79f0dd8eba98797894a85f204..fd4f2aef092dad55727ca14f28aec421ffe0d2e0 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1976,6 +1976,8 @@ set(regress_2_tests
   regress2/bug765.smt2
   regress2/bug812.smt2
   regress2/bv_to_int_ashr.smt2
+  regress2/bv_to_int_mask_array_1.smt2
+  regress2/bv_to_int_mask_array_2.smt2
   regress2/bv_to_int_shifts.smt2
   regress2/error0.smt2
   regress2/error1.smtv1.smt2

diff --git a/test/regress/regress2/bv_to_int_mask_array_1.smt2 b/test/regress/regress2/bv_to_int_mask_array_1.smt2
new file mode 100644 (file)
index 0000000..c1f20a4
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_mask_array_1.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun A () (Array Int Int))
+(declare-fun f ((_ BitVec 3)) Int)
+(declare-fun x () (_ BitVec 3))
+(declare-fun y () (_ BitVec 3))
+(assert (distinct (select A (f (bvand x y))) (select A (f (bvor x y)))))
+(assert (= x y))
+(check-sat)

diff --git a/test/regress/regress2/bv_to_int_mask_array_2.smt2 b/test/regress/regress2/bv_to_int_mask_array_2.smt2
new file mode 100644 (file)
index 0000000..b88f710
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_mask_array_2.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun A () (Array Int Int))
+(declare-fun f ((_ BitVec 3)) Int)
+(declare-fun x () (_ BitVec 3))
+(declare-fun y () (_ BitVec 3))
+(assert (distinct (select A (f (bvand x y))) (select A (f (bvor x y)))))
+(check-sat)