Make `--solve-int-as-bv=X` robust to rewriting (#6722)

After commit 327a24508ed1d02a3fa233e680ffd0b30aa685a9, the int-to-bv
preprocessing pass is getting rewritten terms. As a result, the terms
can contain negative constants (instead of `(- c)`, i.e., `UMINUS` of a
positive constant) and `NONLINEAR_MULT`. The commit adds support for
those cases, does some minor cleanup, and adds regressions. The
regressions should allow us to detect if/when the preprocessing pass
breaks in the future.

diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index 7f03b9459711462c4babfc2f3d329458a61c63f2..15a16888dff7e27c4055b8b3d5d7dfbb16686a19 100644 (file)
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -69,7 +69,8 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache)
     }
     else if (current.getNumChildren() > 2
              && (current.getKind() == kind::PLUS
-                 || current.getKind() == kind::MULT))
+                 || current.getKind() == kind::MULT
+                 || current.getKind() == kind::NONLINEAR_MULT))
     {
       Assert(cache.find(current[0]) != cache.end());
       result = cache[current[0]];
@@ -118,15 +119,15 @@ Node intToBV(TNode n, NodeMap& cache)
     {
       // Not a leaf
       vector<Node> children;
-      unsigned max = 0;
-      for (unsigned i = 0; i < current.getNumChildren(); ++i)
+      uint64_t max = 0;
+      for (const Node& nc : current)
       {
-        Assert(cache.find(current[i]) != cache.end());
-        TNode childRes = cache[current[i]];
+        Assert(cache.find(nc) != cache.end());
+        TNode childRes = cache[nc];
         TypeNode type = childRes.getType();
         if (type.isBitVector())
         {
-          unsigned bvsize = type.getBitVectorSize();
+          uint32_t bvsize = type.getBitVectorSize();
           if (bvsize > max)
           {
             max = bvsize;
@@ -146,6 +147,7 @@ Node intToBV(TNode n, NodeMap& cache)
             max = max + 1;
             break;
           case kind::MULT:
+          case kind::NONLINEAR_MULT:
             Assert(children.size() == 2);
             newKind = kind::BITVECTOR_MULT;
             max = max * 2;
@@ -174,14 +176,14 @@ Node intToBV(TNode n, NodeMap& cache)
             }
             break;
         }
-        for (unsigned i = 0; i < children.size(); ++i)
+        for (size_t i = 0, csize = children.size(); i < csize; ++i)
         {
           TypeNode type = children[i].getType();
           if (!type.isBitVector())
           {
             continue;
           }
-          unsigned bvsize = type.getBitVectorSize();
+          uint32_t bvsize = type.getBitVectorSize();
           if (bvsize < max)
           {
             // sign extend
@@ -195,10 +197,7 @@ Node intToBV(TNode n, NodeMap& cache)
       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
         builder << current.getOperator();
       }
-      for (unsigned i = 0; i < children.size(); ++i)
-      {
-        builder << children[i];
-      }
+      builder.append(children);
       // Mark the substitution and continue
       Node result = builder;
 
@@ -226,7 +225,6 @@ Node intToBV(TNode n, NodeMap& cache)
           {
             Rational constant = current.getConst<Rational>();
             if (constant.isIntegral()) {
-              AlwaysAssert(constant >= 0);
               BitVector bv(size, constant.getNumerator());
               if (bv.toSignedInteger() != constant.getNumerator())
               {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 19c689b873c4a4e82fe9c4a497d6ffaddda22e6e..b94e06e47ee298c4c62661622b15e063f1d93a11 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -645,6 +645,10 @@ set(regress_0_tests
   regress0/incorrect1.smtv1.smt2
   regress0/ineq_basic.smtv1.smt2
   regress0/ineq_slack.smtv1.smt2
+  regress0/int-to-bv/basic.smt2
+  regress0/int-to-bv/neg-consts.smt2
+  regress0/int-to-bv/not-enough-bits.smt2
+  regress0/int-to-bv/overflow.smt2
   regress0/issue1063-overloading-dt-cons.smt2
   regress0/issue1063-overloading-dt-fun.smt2
   regress0/issue1063-overloading-dt-sel.smt2

diff --git a/test/regress/regress0/int-to-bv/basic.smt2 b/test/regress/regress0/int-to-bv/basic.smt2
new file mode 100644 (file)
index 0000000..1e30a7e
--- /dev/null
+++ b/test/regress/regress0/int-to-bv/basic.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --solve-int-as-bv=5 --no-check-models
+(set-logic QF_NIA)
+(declare-const x Int)
+(declare-const y Int)
+; Tests the conversion of negative constants and non-linear multiplication
+(assert (= (- 2) (* x y)))
+; Operators with more than two children
+(assert (= 8 (* x x x)))
+(set-info :status sat)
+(check-sat)

diff --git a/test/regress/regress0/int-to-bv/neg-consts.smt2 b/test/regress/regress0/int-to-bv/neg-consts.smt2
new file mode 100644 (file)
index 0000000..46c08da
--- /dev/null
+++ b/test/regress/regress0/int-to-bv/neg-consts.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --solve-int-as-bv=4 --no-check-models
+(set-logic QF_NIA)
+(declare-const x Int)
+(declare-const y Int)
+(assert (> (- 1) x))
+(assert (>= y x))
+(assert (< 0 y))
+(set-info :status sat)
+(check-sat)

diff --git a/test/regress/regress0/int-to-bv/not-enough-bits.smt2 b/test/regress/regress0/int-to-bv/not-enough-bits.smt2
new file mode 100644 (file)
index 0000000..49711ec
--- /dev/null
+++ b/test/regress/regress0/int-to-bv/not-enough-bits.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --solve-int-as-bv=3
+; SCRUBBER: sed -n "s/.*\(Not enough bits\).*: 4.*/\1/p"
+; EXPECT: Not enough bits
+; EXIT: 1
+(set-logic QF_NIA)
+(declare-const x Int)
+(declare-const y Int)
+; The negative constant fits, the positive does not
+(assert (= (- 4) (* x y)))
+(assert (= 4 (* x y)))
+(check-sat)

diff --git a/test/regress/regress0/int-to-bv/overflow.smt2 b/test/regress/regress0/int-to-bv/overflow.smt2
new file mode 100644 (file)
index 0000000..30e47ad
--- /dev/null
+++ b/test/regress/regress0/int-to-bv/overflow.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --solve-int-as-bv=4
+; EXPECT: unknown
+(set-logic QF_NIA)
+(declare-const x Int)
+(declare-const y Int)
+(assert (= (- 1) (+ x y)))
+(assert (> x 0))
+(assert (> y 0))
+(check-sat)