From: Andres Noetzli Date: Wed, 9 Jun 2021 20:31:45 +0000 (-0700) Subject: Make `--solve-int-as-bv=X` robust to rewriting (#6722) X-Git-Tag: cvc5-1.0.0~1613 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6017579ab78cbc1390274290736ef311208a251b;p=cvc5.git 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 7f03b9459..15a16888d 100644 --- 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 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(); 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 19c689b87..b94e06e47 100644 --- 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 index 000000000..1e30a7ee8 --- /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 index 000000000..46c08dad5 --- /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 index 000000000..49711ecc9 --- /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 index 000000000..30e47adb3 --- /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)