From 6e17dd6d5e3ec043e5edd097ac6a736f6a41c753 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Mon, 24 Feb 2020 19:58:01 -0800 Subject: [PATCH] bv_to_int preprocessing pass Introduces a preprocessing pass that translates bv problems to integer problems. --- src/CMakeLists.txt | 2 + src/options/smt_options.toml | 9 + src/preprocessing/passes/bv_to_int.cpp | 977 ++++++++++++++++++ src/preprocessing/passes/bv_to_int.h | 273 +++++ .../preprocessing_pass_registry.cpp | 2 + src/smt/smt_engine.cpp | 53 +- test/regress/CMakeLists.txt | 12 + test/regress/regress0/bv/bv_to_int1.smt2 | 13 + test/regress/regress0/bv/bv_to_int2.smt2 | 10 + .../regress0/bv/bv_to_int_bitwise.smt2 | 9 + .../regress/regress0/bv/bv_to_int_bvmul1.smt2 | 10 + .../regress/regress0/bv/bv_to_int_bvmul2.smt2 | 10 + test/regress/regress0/bv/bv_to_int_zext.smt2 | 7 + test/regress/regress0/bv/bvuf_to_intuf.smt2 | 8 + .../regress0/bv/bvuf_to_intuf_smtlib.smt2 | 81 ++ .../regress0/bv/bvuf_to_intuf_sorts.smt2 | 14 + test/regress/regress2/bv_to_int_ashr.smt2 | 9 + test/regress/regress2/bv_to_int_shifts.smt2 | 17 + test/regress/regress3/bv_to_int_and_or.smt2 | 8 + 19 files changed, 1521 insertions(+), 3 deletions(-) create mode 100644 src/preprocessing/passes/bv_to_int.cpp create mode 100644 src/preprocessing/passes/bv_to_int.h create mode 100644 test/regress/regress0/bv/bv_to_int1.smt2 create mode 100644 test/regress/regress0/bv/bv_to_int2.smt2 create mode 100644 test/regress/regress0/bv/bv_to_int_bitwise.smt2 create mode 100644 test/regress/regress0/bv/bv_to_int_bvmul1.smt2 create mode 100644 test/regress/regress0/bv/bv_to_int_bvmul2.smt2 create mode 100644 test/regress/regress0/bv/bv_to_int_zext.smt2 create mode 100644 test/regress/regress0/bv/bvuf_to_intuf.smt2 create mode 100644 test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 create mode 100644 test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 create mode 100644 test/regress/regress2/bv_to_int_ashr.smt2 create mode 100644 test/regress/regress2/bv_to_int_shifts.smt2 create mode 100644 test/regress/regress3/bv_to_int_and_or.smt2 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9a81ccc63..4567f45be 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -56,6 +56,8 @@ libcvc4_add_sources( preprocessing/passes/bv_intro_pow2.h preprocessing/passes/bv_to_bool.cpp preprocessing/passes/bv_to_bool.h + preprocessing/passes/bv_to_int.cpp + preprocessing/passes/bv_to_int.h preprocessing/passes/extended_rewriter_pass.cpp preprocessing/passes/extended_rewriter_pass.h preprocessing/passes/global_negate.cpp diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index f78dbb3b8..024530224 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -664,6 +664,15 @@ header = "options/smt_options.h" read_only = true help = "Force no CPU limit when dumping models and proofs" +[[option]] + name = "solveBVAsInt" + category = "undocumented" + long = "solve-bv-as-int=N" + type = "uint32_t" + default = "0" + read_only = true + help = "attempt to solve BV formulas by translation to integer arithmetic (experimental)" + [[option]] name = "solveIntAsBV" category = "undocumented" diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp new file mode 100644 index 000000000..75136913c --- /dev/null +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -0,0 +1,977 @@ +/********************* */ +/*! \file bv_to_int.cpp + ** \verbatim + ** Top contributors (to current version): + ** Yoni Zohar and Ahmed Irfan + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The BVToInt preprocessing pass + ** + ** Converts bit-vector operations into integer operations. + ** + **/ + +#include "preprocessing/passes/bv_to_int.h" + +#include +#include +#include +#include + +#include "expr/node.h" +#include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h" +#include "theory/bv/theory_bv_rewrite_rules_simplification.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using namespace CVC4::theory; +using namespace CVC4::theory::bv; + +namespace { + +Rational intpow2(uint64_t b) +{ + return Rational(Integer(2).pow(b), Integer(1)); +} + +/** + * Helper functions for createBitwiseNode + */ +bool oneBitAnd(bool a, bool b) { return (a && b); } + +bool oneBitOr(bool a, bool b) { return (a || b); } + +bool oneBitXor(bool a, bool b) { return a != b; } + +bool oneBitXnor(bool a, bool b) { return a == b; } + +bool oneBitNand(bool a, bool b) { return !(a && b); } + +bool oneBitNor(bool a, bool b) { return !(a || b); } + +} //end empty namespace + +Node BVToInt::mkRangeConstraint(Node newVar, uint64_t k) +{ + Node lower = d_nm->mkNode(kind::LEQ, d_zero, newVar); + Node upper = d_nm->mkNode(kind::LT, newVar, pow2(k)); + Node result = d_nm->mkNode(kind::AND, lower, upper); + return Rewriter::rewrite(result); +} + +Node BVToInt::maxInt(uint64_t k) +{ + Assert(k > 0); + Rational max_value = intpow2(k) - 1; + return d_nm->mkConst(max_value); +} + +Node BVToInt::pow2(uint64_t k) +{ + Assert(k >= 0); + return d_nm->mkConst(intpow2(k)); +} + +Node BVToInt::modpow2(Node n, uint64_t exponent) +{ + Node p2 = d_nm->mkConst(intpow2(exponent)); + return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, n, p2); +} + +/** + * Binarizing n via post-order traversal. + */ +Node BVToInt::makeBinary(Node n) +{ + vector toVisit; + toVisit.push_back(n); + while (!toVisit.empty()) + { + Node current = toVisit.back(); + uint64_t numChildren = current.getNumChildren(); + if (d_binarizeCache.find(current) == d_binarizeCache.end()) + { + /** + * We still haven't visited the sub-dag rooted at the current node. + * In this case, we: + * mark that we have visited this node by assigning a null node to it in + * the cache, and add its children to toVisit. + */ + d_binarizeCache[current] = Node(); + toVisit.insert(toVisit.end(), current.begin(), current.end()); + } + else if (d_binarizeCache[current].isNull()) + { + /* + * We already visited the sub-dag rooted at the current node, + * and binarized all its children. + * Now we binarize the current node itself. + */ + toVisit.pop_back(); + kind::Kind_t k = current.getKind(); + if ((numChildren > 2) + && (k == kind::BITVECTOR_PLUS || k == kind::BITVECTOR_MULT + || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR + || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT)) + { + // We only binarize bvadd, bvmul, bvand, bvor, bvxor, bvconcat + Assert(d_binarizeCache.find(current[0]) != d_binarizeCache.end()); + Node result = d_binarizeCache[current[0]]; + for (uint64_t i = 1; i < numChildren; i++) + { + Assert(d_binarizeCache.find(current[i]) != d_binarizeCache.end()); + Node child = d_binarizeCache[current[i]]; + result = d_nm->mkNode(current.getKind(), result, child); + } + d_binarizeCache[current] = result; + } + else if (numChildren > 0) + { + // current has children, but we do not binarize it + NodeBuilder<> builder(k); + if (current.getKind() == kind::BITVECTOR_EXTRACT + || current.getKind() == kind::APPLY_UF) + { + builder << current.getOperator(); + } + for (Node child : current) + { + builder << d_binarizeCache[child]; + } + d_binarizeCache[current] = builder.constructNode(); + } + else + { + // current has no children + d_binarizeCache[current] = current; + } + } + else + { + // We already binarized current and it is in the cache. + toVisit.pop_back(); + } + } + return d_binarizeCache[n]; +} + +/** + * We traverse n and perform rewrites both on the way down and on the way up. + * On the way down we rewrite the node but not it's children. + * On the way up, we update the node's children to the rewritten ones. + * For each sub-node, we perform rewrites to eliminate operators. + * Then, the original children are added to toVisit stack so that we rewrite + * them as well. + */ +Node BVToInt::eliminationPass(Node n) +{ + std::vector toVisit; + toVisit.push_back(n); + Node current; + while (!toVisit.empty()) + { + current = toVisit.back(); + toVisit.pop_back(); + bool inEliminationCache = + (d_eliminationCache.find(current) != d_eliminationCache.end()); + bool inRebuildCache = + (d_rebuildCache.find(current) != d_rebuildCache.end()); + if (!inRebuildCache) + { + // current is not the elimination of any previously-visited node + if (!inEliminationCache) + { + // current hasn't been eliminated yet. + // eliminate operators from it + Node currentEliminated = + FixpointRewriteStrategy, + RewriteRule, + RewriteRule, + RewriteRule, + RewriteRule, + RewriteRule, + RewriteRule, + RewriteRule, + RewriteRule, + RewriteRule, + RewriteRule, + RewriteRule, + RewriteRule, + RewriteRule, + RewriteRule, + RewriteRule >::apply(current); + // save in the cache + d_eliminationCache[current] = currentEliminated; + // put the eliminated node in the rebuild cache, but mark that it hasn't + // yet been rebuilt by assigning null. + d_rebuildCache[currentEliminated] = Node(); + // Push the eliminated node to the stack + toVisit.push_back(currentEliminated); + // Add the children to the stack for future processing. + toVisit.insert( + toVisit.end(), currentEliminated.begin(), currentEliminated.end()); + } + } + else + { + // current was already added to the rebuild cache. + if (d_rebuildCache[current].isNull()) + { + // current wasn't rebuilt yet. + uint64_t numChildren = current.getNumChildren(); + if (numChildren == 0) + { + // We only eliminate operators that are not nullary. + d_rebuildCache[current] = current; + } + else + { + // The main operator is replaced, and the children + // are replaced with their eliminated counterparts. + NodeBuilder<> builder(current.getKind()); + if (current.getKind() == kind::BITVECTOR_EXTRACT + || current.getKind() == kind::APPLY_UF) + { + builder << current.getOperator(); + } + for (Node child : current) + { + Assert(d_eliminationCache.find(child) != d_eliminationCache.end()); + Node eliminatedChild = d_eliminationCache[child]; + Assert(d_rebuildCache.find(eliminatedChild) != d_eliminationCache.end()); + Assert(!d_rebuildCache[eliminatedChild].isNull()); + builder << d_rebuildCache[eliminatedChild]; + } + d_rebuildCache[current] = builder.constructNode(); + } + } + } + } + Assert(d_eliminationCache.find(n) != d_eliminationCache.end()); + Node eliminated = d_eliminationCache[n]; + Assert(d_rebuildCache.find(eliminated) != d_rebuildCache.end()); + Assert(!d_rebuildCache[eliminated].isNull()); + return d_rebuildCache[eliminated]; +} + +/** + * Translate n to Integers via post-order traversal. + */ +Node BVToInt::bvToInt(Node n) +{ + n = eliminationPass(n); + n = makeBinary(n); + vector toVisit; + toVisit.push_back(n); + uint64_t granularity = options::solveBVAsInt(); + + while (!toVisit.empty()) + { + Node current = toVisit.back(); + uint64_t currentNumChildren = current.getNumChildren(); + if (d_bvToIntCache.find(current) == d_bvToIntCache.end()) + { + // This is the first time we visit this node and it is not in the cache. + d_bvToIntCache[current] = Node(); + toVisit.insert(toVisit.end(), current.begin(), current.end()); + } + else + { + // We already visited this node + if (!d_bvToIntCache[current].isNull()) + { + // We are done computing the translation for current + toVisit.pop_back(); + } + else + { + // We are now visiting current on the way back up. + // This is when we do the actual translation. + if (currentNumChildren == 0) + { + Assert(current.isVar() || current.isConst()); + if (current.isVar()) + { + if (current.getType().isBitVector()) + { + // For bit-vector variables, we create integer variables and add a + // range constraint. + Node newVar = d_nm->mkSkolem("__bvToInt_var", + d_nm->integerType(), + "Variable introduced in bvToInt " + "pass instead of original variable " + + current.toString()); + + d_bvToIntCache[current] = newVar; + d_rangeAssertions.insert(mkRangeConstraint( + newVar, current.getType().getBitVectorSize())); + } + else + { + // Boolean variables are left unchanged. + AlwaysAssert(current.getType() == d_nm->booleanType() + || current.getType().isSort()); + d_bvToIntCache[current] = current; + } + } + else + { + // current is a const + if (current.getKind() == kind::CONST_BITVECTOR) + { + // Bit-vector constants are transformed into their integer value. + BitVector constant(current.getConst()); + Integer c = constant.toInteger(); + d_bvToIntCache[current] = d_nm->mkConst(c); + } + else + { + // Other constants stay the same. + d_bvToIntCache[current] = current; + } + } + } + else + { + /** + * The current node has children. + * Since we are on the way back up, + * these children were already translated. + * We save their translation for future use. + */ + vector translated_children; + for (uint64_t i = 0; i < currentNumChildren; i++) + { + translated_children.push_back(d_bvToIntCache[current[i]]); + } + // The translation of the current node is determined by the kind of + // the node. + kind::Kind_t oldKind = current.getKind(); + //ultbv and sltbv were supposed to be eliminated before this point. + Assert(oldKind != kind::BITVECTOR_ULTBV); + Assert(oldKind != kind::BITVECTOR_SLTBV); + switch (oldKind) + { + case kind::BITVECTOR_PLUS: + { + uint64_t bvsize = current[0].getType().getBitVectorSize(); + /** + * we avoid modular arithmetics by the addition of an + * indicator variable sigma. + * Tr(a+b) is Tr(a)+Tr(b)-(sigma*2^k), + * with k being the bit width, + * and sigma being either 0 or 1. + */ + Node sigma = d_nm->mkSkolem( + "__bvToInt_sigma_var", + d_nm->integerType(), + "Variable introduced in bvToInt pass to avoid integer mod"); + Node plus = d_nm->mkNode(kind::PLUS, translated_children); + Node multSig = d_nm->mkNode(kind::MULT, sigma, pow2(bvsize)); + d_bvToIntCache[current] = + d_nm->mkNode(kind::MINUS, plus, multSig); + d_rangeAssertions.insert(d_nm->mkNode(kind::LEQ, d_zero, sigma)); + d_rangeAssertions.insert(d_nm->mkNode(kind::LEQ, sigma, d_one)); + d_rangeAssertions.insert( + mkRangeConstraint(d_bvToIntCache[current], bvsize)); + break; + } + case kind::BITVECTOR_MULT: + { + uint64_t bvsize = current[0].getType().getBitVectorSize(); + /** + * we use a similar trick to the one used for addition. + * Tr(a*b) is Tr(a)*Tr(b)-(sigma*2^k), + * with k being the bit width, + * and sigma is between [0, 2^k - 1). + */ + Node sigma = d_nm->mkSkolem( + "__bvToInt_sigma_var", + d_nm->integerType(), + "Variable introduced in bvToInt pass to avoid integer mod"); + Node mult = d_nm->mkNode(kind::MULT, translated_children); + Node multSig = d_nm->mkNode(kind::MULT, sigma, pow2(bvsize)); + d_bvToIntCache[current] = + d_nm->mkNode(kind::MINUS, mult, multSig); + d_rangeAssertions.insert( + mkRangeConstraint(d_bvToIntCache[current], bvsize)); + d_rangeAssertions.insert(mkRangeConstraint(sigma, bvsize)); + break; + } + case kind::BITVECTOR_UDIV_TOTAL: + { + uint64_t bvsize = current[0].getType().getBitVectorSize(); + // we use an ITE for the case where the second operand is 0. + Node pow2BvSize = pow2(bvsize); + Node divNode = + d_nm->mkNode(kind::INTS_DIVISION_TOTAL, translated_children); + Node ite = d_nm->mkNode( + kind::ITE, + d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero), + d_nm->mkNode(kind::MINUS, pow2BvSize, d_one), + divNode); + d_bvToIntCache[current] = ite; + break; + } + case kind::BITVECTOR_UREM_TOTAL: + { + // we use an ITE for the case where the second operand is 0. + Node modNode = + d_nm->mkNode(kind::INTS_MODULUS_TOTAL, translated_children); + Node ite = d_nm->mkNode( + kind::ITE, + d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero), + translated_children[0], + modNode); + d_bvToIntCache[current] = ite; + break; + } + case kind::BITVECTOR_NEG: + { + // (bvneg x) is 2^k-x, unless x is 0, + // in which case the result should be 0. + // This can be expressed by (2^k-x) mod 2^k + // However, since mod is an expensive arithmetic operation, + // we represent `bvneg` using an ITE. + uint64_t bvsize = current[0].getType().getBitVectorSize(); + Node pow2BvSize = pow2(bvsize); + Node neg = + d_nm->mkNode(kind::MINUS, pow2BvSize, translated_children[0]); + Node isZero = + d_nm->mkNode(kind::EQUAL, translated_children[0], d_zero); + d_bvToIntCache[current] = + d_nm->mkNode(kind::ITE, isZero, d_zero, neg); + break; + } + case kind::BITVECTOR_NOT: + { + uint64_t bvsize = current[0].getType().getBitVectorSize(); + // we use a specified function to generate the node. + d_bvToIntCache[current] = + createBVNotNode(translated_children[0], bvsize); + break; + } + case kind::BITVECTOR_TO_NAT: + { + // In this case, we already translated the child to integer. + // So the result is the translated child. + d_bvToIntCache[current] = translated_children[0]; + break; + } + case kind::BITVECTOR_AND: + { + // Construct an ite, based on granularity. + uint64_t bvsize = current[0].getType().getBitVectorSize(); + Assert(translated_children.size() == 2); + Node newNode = createBitwiseNode(translated_children[0], + translated_children[1], + bvsize, + granularity, + &oneBitAnd); + d_bvToIntCache[current] = newNode; + break; + } + case kind::BITVECTOR_OR: + { + // Construct an ite, based on granularity. + uint64_t bvsize = current[0].getType().getBitVectorSize(); + Node newNode = createBitwiseNode(translated_children[0], + translated_children[1], + bvsize, + granularity, + &oneBitOr); + d_bvToIntCache[current] = newNode; + break; + } + case kind::BITVECTOR_XOR: + { + // Construct an ite, based on granularity. + uint64_t bvsize = current[0].getType().getBitVectorSize(); + Node newNode = createBitwiseNode(translated_children[0], + translated_children[1], + bvsize, + granularity, + &oneBitXor); + d_bvToIntCache[current] = newNode; + break; + } + case kind::BITVECTOR_XNOR: + { + // Construct an ite, based on granularity. + uint64_t bvsize = current[0].getType().getBitVectorSize(); + Node newNode = createBitwiseNode(translated_children[0], + translated_children[1], + bvsize, + granularity, + &oneBitXnor); + d_bvToIntCache[current] = newNode; + break; + } + case kind::BITVECTOR_NAND: + { + // Construct an ite, based on granularity. + uint64_t bvsize = current[0].getType().getBitVectorSize(); + Node newNode = createBitwiseNode(translated_children[0], + translated_children[1], + bvsize, + granularity, + &oneBitNand); + d_bvToIntCache[current] = newNode; + break; + } + case kind::BITVECTOR_NOR: + { + // Construct an ite, based on granularity. + uint64_t bvsize = current[0].getType().getBitVectorSize(); + Node newNode = createBitwiseNode(translated_children[0], + translated_children[1], + bvsize, + granularity, + &oneBitNor); + d_bvToIntCache[current] = newNode; + break; + } + case kind::BITVECTOR_SHL: + { + /** + * a << b is a*2^b. + * The exponentiation is simulated by an ite. + * Only cases where b <= bit width are considered. + * Otherwise, the result is 0. + */ + uint64_t bvsize = current[0].getType().getBitVectorSize(); + Node newNode = createShiftNode(translated_children, bvsize, true); + d_bvToIntCache[current] = newNode; + break; + } + case kind::BITVECTOR_LSHR: + { + /** + * a >> b is a div 2^b. + * The exponentiation is simulated by an ite. + * Only cases where b <= bit width are considered. + * Otherwise, the result is 0. + */ + uint64_t bvsize = current[0].getType().getBitVectorSize(); + Node newNode = createShiftNode(translated_children, bvsize, false); + d_bvToIntCache[current] = newNode; + break; + } + case kind::BITVECTOR_ASHR: + { + /* From SMT-LIB2: + * (bvashr s t) abbreviates + * (ite (= ((_ extract |m-1| |m-1|) s) #b0) + * (bvlshr s t) + * (bvnot (bvlshr (bvnot s) t))) + * + * Equivalently: + * (bvashr s t) abbreviates + * (ite (bvult s 100000...) + * (bvlshr s t) + * (bvnot (bvlshr (bvnot s) t))) + * + */ + uint64_t bvsize = current[0].getType().getBitVectorSize(); + // signed_min is 100000... + Node signed_min = pow2(bvsize - 1); + Node condition = + d_nm->mkNode(kind::LT, translated_children[0], signed_min); + Node thenNode = createShiftNode(translated_children, bvsize, false); + vector children = { + createBVNotNode(translated_children[0], bvsize), + translated_children[1]}; + Node elseNode = createBVNotNode( + createShiftNode(children, bvsize, false), bvsize); + Node ite = d_nm->mkNode(kind::ITE, condition, thenNode, elseNode); + d_bvToIntCache[current] = ite; + break; + } + case kind::BITVECTOR_ITE: + { + // Lifted to a boolean ite. + Node cond = d_nm->mkNode(kind::EQUAL, translated_children[0], d_one); + Node ite = d_nm->mkNode( + kind::ITE, cond, translated_children[1], translated_children[2]); + d_bvToIntCache[current] = ite; + break; + } + case kind::BITVECTOR_CONCAT: + { + // (concat a b) translates to a*2^k+b, k being the bitwidth of b. + uint64_t bvsizeRight = current[1].getType().getBitVectorSize(); + Node pow2BvSizeRight = pow2(bvsizeRight); + Node a = d_nm->mkNode( + kind::MULT, translated_children[0], pow2BvSizeRight); + Node b = translated_children[1]; + Node sum = d_nm->mkNode(kind::PLUS, a, b); + d_bvToIntCache[current] = sum; + break; + } + case kind::BITVECTOR_EXTRACT: + { + // ((_ extract i j) a) is a / 2^j mod 2^{i-j+1} + // current = a[i:j] + Node a = current[0]; + uint64_t i = bv::utils::getExtractHigh(current); + uint64_t j = bv::utils::getExtractLow(current); + Assert(d_bvToIntCache.find(a) != d_bvToIntCache.end()); + Assert(i >= j); + Node div = d_nm->mkNode( + kind::INTS_DIVISION_TOTAL, d_bvToIntCache[a], pow2(j)); + d_bvToIntCache[current] = modpow2(div, i - j + 1); + break; + } + case kind::EQUAL: + { + d_bvToIntCache[current] = + d_nm->mkNode(kind::EQUAL, translated_children); + break; + } + case kind::BITVECTOR_ULT: + { + d_bvToIntCache[current] = + d_nm->mkNode(kind::LT, translated_children); + break; + } + case kind::BITVECTOR_ULE: + { + d_bvToIntCache[current] = + d_nm->mkNode(kind::LEQ, translated_children); + break; + } + case kind::BITVECTOR_UGT: + { + d_bvToIntCache[current] = + d_nm->mkNode(kind::GT, translated_children); + break; + } + case kind::BITVECTOR_UGE: + { + d_bvToIntCache[current] = + d_nm->mkNode(kind::GEQ, translated_children); + break; + } + case kind::LT: + { + d_bvToIntCache[current] = + d_nm->mkNode(kind::LT, translated_children); + break; + } + case kind::LEQ: + { + d_bvToIntCache[current] = + d_nm->mkNode(kind::LEQ, translated_children); + break; + } + case kind::GT: + { + d_bvToIntCache[current] = + d_nm->mkNode(kind::GT, translated_children); + break; + } + case kind::GEQ: + { + d_bvToIntCache[current] = + d_nm->mkNode(kind::GEQ, translated_children); + break; + } + case kind::ITE: + { + d_bvToIntCache[current] = d_nm->mkNode(oldKind, translated_children); + break; + } + case kind::APPLY_UF: + { + /* + * We replace all BV-sorts of the domain with INT + * If the range is a BV sort, we replace it with INT + * We cache both the term itself (e.g., f(a)) and the function + * symbol f. + */ + Node bvUF = current.getOperator(); + Node intUF; + TypeNode tn = current.getOperator().getType(); + TypeNode bvRange = tn.getRangeType(); + if (d_bvToIntCache.find(bvUF) != d_bvToIntCache.end()) + { + intUF = d_bvToIntCache[bvUF]; + } + else + { + vector bvDomain = tn.getArgTypes(); + vector intDomain; + /** + * if the original range is a bit-vector sort, + * the new range should be an integer sort. + * Otherwise, we keep the original range. + */ + TypeNode intRange = + bvRange.isBitVector() ? d_nm->integerType() : bvRange; + for (TypeNode d : bvDomain) + { + intDomain.push_back(d.isBitVector() ? d_nm->integerType() + : d); + } + ostringstream os; + os << "__bvToInt_fun_" << bvUF << "_int"; + intUF = + d_nm->mkSkolem(os.str(), + d_nm->mkFunctionType(intDomain, intRange), + "bv2int function"); + // 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); + /** + * 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. + */ + if (bvRange.isBitVector()) + { + d_rangeAssertions.insert( + mkRangeConstraint(d_bvToIntCache[current], + current.getType().getBitVectorSize())); + } + break; + } + default: + { + if (Theory::theoryOf(current) == THEORY_BOOL) + { + 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(); + } + } + } + } + toVisit.pop_back(); + } + } + } + return d_bvToIntCache[n]; +} + +BVToInt::BVToInt(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "bv-to-int"), + d_binarizeCache(), + d_eliminationCache(), + d_bvToIntCache(), + d_rangeAssertions() +{ + d_nm = NodeManager::currentNM(); + d_zero = d_nm->mkConst(0); + d_one = d_nm->mkConst(1); +}; + +PreprocessingPassResult BVToInt::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + AlwaysAssert(!options::incrementalSolving()); + for (uint64_t i = 0; i < assertionsToPreprocess->size(); ++i) + { + Node bvNode = (*assertionsToPreprocess)[i]; + Node intNode = bvToInt(bvNode); + Node rwNode = Rewriter::rewrite(intNode); + Trace("bv-to-int-debug") << "bv node: " << bvNode << std::endl; + Trace("bv-to-int-debug") << "int node: " << intNode << std::endl; + Trace("bv-to-int-debug") << "rw node: " << rwNode << std::endl; + assertionsToPreprocess->replace(i, rwNode); + } + addFinalizeRangeAssertions(assertionsToPreprocess); + return PreprocessingPassResult::NO_CONFLICT; +} + +void BVToInt::addFinalizeRangeAssertions( + AssertionPipeline* assertionsToPreprocess) +{ + vector vec_range; + vec_range.assign(d_rangeAssertions.begin(), d_rangeAssertions.end()); + if (vec_range.size() == 1) + { + assertionsToPreprocess->push_back(vec_range[0]); + Trace("bv-to-int-debug") + << "range constraints: " << vec_range[0].toString() << std::endl; + } + else if (vec_range.size() >= 2) + { + Node rangeAssertions = + Rewriter::rewrite(d_nm->mkNode(kind::AND, vec_range)); + assertionsToPreprocess->push_back(rangeAssertions); + Trace("bv-to-int-debug") + << "range constraints: " << rangeAssertions.toString() << std::endl; + } +} + +Node BVToInt::createShiftNode(vector children, + uint64_t bvsize, + bool isLeftShift) +{ + Node x = children[0]; + Node y = children[1]; + Assert(!y.isConst()); + // ite represents 2^x for every integer x from 0 to bvsize-1. + Node ite = pow2(0); + for (uint64_t i = 1; i < bvsize; i++) + { + ite = d_nm->mkNode(kind::ITE, + d_nm->mkNode(kind::EQUAL, y, d_nm->mkConst(i)), + pow2(i), + ite); + } + /** + * from SMT-LIB: + * [[(bvshl s t)]] := nat2bv[m](bv2nat([[s]]) * 2^(bv2nat([[t]]))) + * [[(bvlshr s t)]] := nat2bv[m](bv2nat([[s]]) div 2^(bv2nat([[t]]))) + * Since we don't have exponentiation, we use the ite declared above. + */ + kind::Kind_t then_kind = isLeftShift ? kind::MULT : kind::INTS_DIVISION_TOTAL; + return d_nm->mkNode(kind::ITE, + d_nm->mkNode(kind::LT, y, d_nm->mkConst(bvsize)), + d_nm->mkNode(kind::INTS_MODULUS_TOTAL, + d_nm->mkNode(then_kind, x, ite), + pow2(bvsize)), + d_zero); +} + +Node BVToInt::createITEFromTable( + Node x, + Node y, + uint64_t granularity, + std::map, uint64_t> table) +{ + Assert(granularity <= 8); + uint64_t max_value = ((uint64_t)pow(2, granularity)); + // The table represents a function from pairs of integers to integers, where + // all integers are between 0 (inclusive) and max_value (exclusive). + Assert(table.size() == max_value * max_value); + Node ite = d_nm->mkConst(table[std::make_pair(0, 0)]); + for (uint64_t i = 0; i < max_value; i++) + { + for (uint64_t j = 0; j < max_value; j++) + { + if ((i == 0) && (j == 0)) + { + continue; + } + ite = d_nm->mkNode( + kind::ITE, + d_nm->mkNode( + kind::AND, + d_nm->mkNode(kind::EQUAL, x, d_nm->mkConst(i)), + d_nm->mkNode(kind::EQUAL, y, d_nm->mkConst(j))), + d_nm->mkConst(table[std::make_pair(i, j)]), + ite); + } + } + return ite; +} + +Node BVToInt::createBitwiseNode(Node x, + Node y, + uint64_t bvsize, + uint64_t granularity, + bool (*f)(bool, bool)) +{ + /** + * Standardize granularity. + * If it is greater than bvsize, it is set to bvsize. + * Otherwise, it is set to the closest (going down) divider of bvsize. + */ + Assert(granularity > 0); + if (granularity > bvsize) + { + granularity = bvsize; + } + else + { + while (bvsize % granularity != 0) + { + granularity = granularity - 1; + } + } + // transform f into a table + // f is defined over 1 bit, while the table is defined over `granularity` bits + std::map, uint64_t> table; + uint64_t max_value = ((uint64_t)pow(2, granularity)); + for (uint64_t i = 0; i < max_value; i++) + { + for (uint64_t j = 0; j < max_value; j++) + { + uint64_t sum = 0; + for (uint64_t n = 0; n < granularity; n++) + { + // b is the result of f on the current bit + bool b = f((((i >> n) & 1) == 1), (((j >> n) & 1) == 1)); + // add the corresponding power of 2 only if the result is 1 + if (b) + { + sum += 1 << n; + } + } + table[std::make_pair(i, j)] = sum; + } + } + Assert(table.size() == max_value * max_value); + + /* + * Create the sum. + * For granularity 1, the sum has bvsize elements. + * In contrast, if bvsize = granularity, sum has one element. + * Each element in the sum is an ite that corresponds to the generated table, + * multiplied by the appropriate power of two. + * More details are in bv_to_int.h . + */ + uint64_t sumSize = bvsize / granularity; + Node sumNode = d_zero; + /** + * extract definition in integers is: + * (define-fun intextract ((k Int) (i Int) (j Int) (a Int)) Int + * (mod (div a (two_to_the j)) (two_to_the (+ (- i j) 1)))) + */ + for (uint64_t i = 0; i < sumSize; i++) + { + Node xExtract = d_nm->mkNode( + kind::INTS_MODULUS_TOTAL, + d_nm->mkNode(kind::INTS_DIVISION_TOTAL, x, pow2(i * granularity)), + pow2(granularity)); + Node yExtract = d_nm->mkNode( + kind::INTS_MODULUS_TOTAL, + d_nm->mkNode(kind::INTS_DIVISION_TOTAL, y, pow2(i * granularity)), + pow2(granularity)); + Node ite = createITEFromTable(xExtract, yExtract, granularity, table); + sumNode = + d_nm->mkNode(kind::PLUS, + sumNode, + d_nm->mkNode(kind::MULT, pow2(i * granularity), ite)); + } + return sumNode; +} + +Node BVToInt::createBVNotNode(Node n, uint64_t bvsize) +{ + return d_nm->mkNode(kind::MINUS, maxInt(bvsize), n); +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h new file mode 100644 index 000000000..dd02d98ec --- /dev/null +++ b/src/preprocessing/passes/bv_to_int.h @@ -0,0 +1,273 @@ +/********************* */ +/*! \file bv_to_int.h + ** \verbatim + ** Top contributors (to current version): + ** Yoni Zohar and Ahmed Irfan + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The BVToInt preprocessing pass + ** + ** Converts bit-vector formulas to integer formulas. + ** The conversion is implemented using a translation function Tr, + ** roughly described as follows: + ** + ** Tr(x) = fresh_x for every bit-vector variable x, where fresh_x is a fresh + ** integer variable. + ** Tr(c) = the integer value of c, for any bit-vector constant c. + ** Tr((bvadd s t)) = Tr(s) + Tr(t) mod 2^k, where k is the bit width of + ** s and t. + ** Similar transformations are done for bvmul, bvsub, bvudiv, bvurem, bvneg, + ** bvnot, bvconcat, bvextract + ** + ** Tr((bvand s t)) depends on the granularity, which is provided by the user + ** when enabling this preprocessing pass. + ** We divide s and t to blocks. + ** The size of each block is the granularity, and so the number of + ** blocks is: + ** bit width/granularity (rounded down). + ** We create an ITE that represents an arbitrary block, + ** and then create a sum by mutiplying each block by the + ** appropriate power of two. + ** More formally: + ** Let g denote the granularity. + ** Let k denote the bit width of s and t. + ** Let b denote floor(k/g) if k >= g, or just k otherwise. + ** Tr((bvand s t)) = + ** Sigma_{i=0}^{b-1}(bvand s[(i+1)*g, i*g] t[(i+1)*g, i*g])*2^(i*g) + ** + ** More details and examples for this case are described next to + ** the function createBitwiseNode. + ** Similar transformations are done for bvor, bvxor, bvxnor, bvnand, bvnor. + ** + ** Tr((bvshl a b)) = ite(Tr(b) >= k, 0, Tr(a)*ITE), where k is the bit width of + ** a and b, and ITE represents exponentiation up to k, that is: + ** ITE = ite(Tr(b)=0, 1, ite(Tr(b)=1), 2, ite(Tr(b)=2, 4, ...)) + ** Similar transformations are done for bvlshr. + ** + ** Tr(a=b) = Tr(a)=Tr(b) + ** Tr((bvult a b)) = Tr(a) < Tr(b) + ** Similar transformations are done for bvule, bvugt, and bvuge. + ** + ** Bit-vector operators that are not listed above are either eliminated using + ** the function eliminationPass, or are not supported. + ** + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H +#define __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using NodeMap = std::unordered_map; + +class BVToInt : public PreprocessingPass +{ + public: + BVToInt(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + /** + * A generic function that creates a node that represents a bitwise + * operation. + * + * For example: Suppose bvsize is 4, granularity is 1, and f(x,y) = x && y. + * Denote by ITE(a,b) the term: ite(a==0, 0, ite(b==1, 1, 0)). + * The result of this function would be: + * ITE(x[0], y[0])*2^0 + ... + ITE(x[3], y[3])*2^3 + * + * For another example: Suppose bvsize is 4, granularity is 2, + * and f(x,y) = x && y. + * Denote by ITE(a,b) the term that corresponds to the following table: + * a | b | ITE(a,b) + * ---------------- + * 0 | 0 | 0 + * 0 | 1 | 0 + * 0 | 2 | 0 + * 0 | 3 | 0 + * 1 | 0 | 0 + * 1 | 1 | 1 + * 1 | 2 | 0 + * 1 | 3 | 1 + * 2 | 0 | 0 + * 2 | 1 | 0 + * 2 | 2 | 2 + * 2 | 3 | 2 + * 3 | 0 | 0 + * 3 | 1 | 1 + * 3 | 2 | 2 + * 3 | 3 | 3 + * + * For example, 2 in binary is 10 and 1 in binary is 01, and so doing + * "bitwise f" on them gives 00. + * The result of this function would be: + * ITE(x[1:0], y[1:0])*2^0 + ITE(x[3:2], y[3:2])*2^2 + * + * + * @param x is an integer operand that correspond to the first original + * bit-vector operand. + * @param y is an integer operand that correspond to the second original + * bit-vector operand. + * @param bvsize is the bit width of the original bit-vector variables. + * @param granularity is specified in the options for this preprocessing + * pass. + * @param f is a pointer to a boolean function that corresponds + * to the original bitwise operation. + * @return A node that represents the operation, as described above. + */ + Node createBitwiseNode(Node x, + Node y, + uint64_t bvsize, + uint64_t granularity, + bool (*f)(bool, bool)); + + /** + * A helper function for createBitwiseNode + * @param x integer node corresponding to the original first bit-vector + * argument + * @param y integer node corresponding to the original second bit-vector + * argument nodes. + * @param granularity the bitwidth of the original bit-vector nodes. + * @param table a function from pairs of integers to integers. + * The domain of this function consists of pairs of + * integers between 0 (inclusive) and 2^{bitwidth} (exclusive). + * @return An ite term that represents this table. + */ + Node createITEFromTable( + Node x, + Node y, + uint64_t granularity, + std::map, uint64_t> table); + + /** + * A generic function that creates a logical shift node (either left or + * right). a << b gets translated to a * 2^b mod 2^k, where k is the bit + * width. a >> b gets translated to a div 2^b mod 2^k, where k is the bit + * width. The exponentiation operation is translated to an ite for possible + * values of the exponent, from 0 to k-1. + * If the right operand of the shift is greater than k-1, + * the result is 0. + * @param children the two operands for the shift + * @param bvsize the original bit widths of the operands + * (before translation to integers) + * @param isLeftShift true iff the desired operation is a left shift. + * @return a node representing the shift. + * + */ + Node createShiftNode(vector children, + uint64_t bvsize, + bool isLeftShift); + + /** + * Returns a node that represents the bitwise negation of n. + */ + Node createBVNotNode(Node n, uint64_t bvsize); + + /** + * The result is an integer term and is computed + * according to the translation specified above. + * @param n is a bit-vector term or formula to be translated. + * @return integer node that corresponds to n. + */ + Node bvToInt(Node n); + + /** + * Whenever we introduce an integer variable that represents a bit-vector + * variable, we need to guard the range of the newly introduced variable. + * For bit width k, the constraint is 0 <= newVar < 2^k. + * @param newVar the newly introduced integer variable + * @param k the bit width of the original bit-vector variable. + * @return a node representing the range constraint. + */ + Node mkRangeConstraint(Node newVar, uint64_t k); + + /** + * In the translation to integers, it is convenient to assume that certain + * bit-vector operators do not occur in the original formula (e.g., repeat). + * This function eliminates all these operators. + */ + Node eliminationPass(Node n); + + /** + * Some bit-vector operators (e.g., bvadd, bvand) are binary, but allow more + * than two arguments as a syntactic sugar. + * For example, we can have a node for (bvand x y z), + * that represents (bvand (x (bvand y z))). + * This function makes all such operators strictly binary. + */ + Node makeBinary(Node n); + + /** + * @param k A non-negative integer + * @return A node that represents the constant 2^k + */ + Node pow2(uint64_t k); + + /** + * @param k A positive integer k + * @return A node that represent the constant 2^k-1 + * For example, if k is 4, the result is a node representing the + * constant 15. + */ + Node maxInt(uint64_t k); + + /** + * @param n A node representing an integer term + * @param exponent A non-negative integer + * @return A node representing (n mod (2^exponent)) + */ + Node modpow2(Node n, uint64_t exponent); + + /** + * Add the range assertions collected in d_rangeAssertions + * (using mkRangeConstraint) to the assertion pipeline. + * If there are no range constraints, do nothing. + * If there is a single range constraint, add it to the pipeline. + * Otherwise, add all of them as a single conjunction + */ + void addFinalizeRangeAssertions(AssertionPipeline* assertionsToPreprocess); + + /** + * Caches for the different functions + */ + NodeMap d_binarizeCache; + NodeMap d_eliminationCache; + NodeMap d_rebuildCache; + NodeMap d_bvToIntCache; + + /** + * Node manager that is used throughout the pass + */ + NodeManager* d_nm; + + /** + * A set of constraints of the form 0 <= x < 2^k + * These are added for every new integer variable that we introduce. + */ + unordered_set d_rangeAssertions; + + /** + * Useful constants + */ + Node d_zero; + Node d_one; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H */ diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index 5df449237..154ed9086 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -32,6 +32,7 @@ #include "preprocessing/passes/bv_gauss.h" #include "preprocessing/passes/bv_intro_pow2.h" #include "preprocessing/passes/bv_to_bool.h" +#include "preprocessing/passes/bv_to_int.h" #include "preprocessing/passes/extended_rewriter_pass.h" #include "preprocessing/passes/global_negate.h" #include "preprocessing/passes/ho_elim.h" @@ -124,6 +125,7 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() registerPassInfo("apply-to-const", callCtor); registerPassInfo("global-negate", callCtor); registerPassInfo("int-to-bv", callCtor); + registerPassInfo("bv-to-int", callCtor); registerPassInfo("synth-rr", callCtor); registerPassInfo("real-to-int", callCtor); registerPassInfo("sygus-infer", callCtor); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6f40d815f..2bfb8353f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1215,9 +1215,17 @@ void SmtEngine::setDefaults() { } d_logic = LogicInfo("QF_BV"); } - else if (d_logic.getLogicString() == "QF_NRA" && options::solveRealAsInt()) + + if (options::solveBVAsInt() > 0) { - d_logic = LogicInfo("QF_NIA"); + 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(); + } } // set options about ackermannization @@ -1441,6 +1449,17 @@ void SmtEngine::setDefaults() { options::preSkolemQuant.set(false); } + if (options::solveBVAsInt() > 0) + { + /** + * Operations on 1 bits are better handled as Boolean operations + * than as integer operations. + * Therefore, we enable bv-to-bool, which runs before + * the translation to integers. + */ + options::bitvectorToBool.set(true); + } + if (options::bitvectorToBool()) { if (options::bitvectorToBool.wasSetByUser()) @@ -3297,7 +3316,7 @@ void SmtEnginePrivate::processAssertions() { if (options::solveRealAsInt()) { d_passes["real-to-int"]->apply(&d_assertions); } - + if (options::solveIntAsBV() > 0) { d_passes["int-to-bv"]->apply(&d_assertions); @@ -3358,6 +3377,34 @@ void SmtEnginePrivate::processAssertions() { { d_passes["bv-to-bool"]->apply(&d_assertions); } + if (options::solveBVAsInt() > 0) + { + if (options::incrementalSolving()) + { + throw ModalException( + "solving bitvectors as integers is currently not supported " + "when solving incrementally."); + } else if (options::boolToBitvector() != options::BoolToBVMode::OFF) { + throw ModalException( + "solving bitvectors as integers is incompatible with --bool-to-bv."); + } + else if (options::solveBVAsInt() > 8) + { + /** + * The granularity sets the size of the ITE in each element + * of the sum that is generated for bitwise operators. + * The size of the ITE is 2^{2*granularity}. + * Since we don't want to introduce ITEs with unbounded size, + * we bound the granularity. + */ + throw ModalException("solve-bv-as-int accepts values from 0 to 8."); + } + else + { + d_passes["bv-to-int"]->apply(&d_assertions); + } + } + // Convert non-top-level Booleans to bit-vectors of size 1 if (options::boolToBitvector() != options::BoolToBVMode::OFF) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 92a6200ee..b909817df 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -204,6 +204,15 @@ set(regress_0_tests regress0/bv/bv-options4.smt2 regress0/bv/bv-to-bool1.smtv1.smt2 regress0/bv/bv-to-bool2.smt2 + regress0/bv/bv_to_int1.smt2 + regress0/bv/bv_to_int2.smt2 + regress0/bv/bv_to_int_bvmul1.smt2 + regress0/bv/bv_to_int_bvmul2.smt2 + regress0/bv/bv_to_int_zext.smt2 + regress0/bv/bv_to_int_bitwise.smt2 + regress0/bv/bvuf_to_intuf.smt2 + regress0/bv/bvuf_to_intuf_smtlib.smt2 + regress0/bv/bvuf_to_intuf_sorts.smt2 regress0/bv/bv2nat-ground-c.smt2 regress0/bv/bv2nat-simp-range.smt2 regress0/bv/bvmul-pow2-only.smt2 @@ -1922,6 +1931,8 @@ set(regress_2_tests regress2/bug674.smt2 regress2/bug765.smt2 regress2/bug812.smt2 + regress2/bv_to_int_ashr.smt2 + regress2/bv_to_int_shifts.smt2 regress2/error0.smt2 regress2/error1.smtv1.smt2 regress2/friedman_n4_i5.smtv1.smt2 @@ -2007,6 +2018,7 @@ set(regress_3_tests regress3/bmc-ibm-2.smtv1.smt2 regress3/bmc-ibm-5.smtv1.smt2 regress3/bmc-ibm-7.smtv1.smt2 + regress3/bv_to_int_and_or.smt2 regress3/eq_diamond14.smtv1.smt2 regress3/friedman_n6_i4.smtv1.smt2 regress3/hole9.cvc diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2 new file mode 100644 index 000000000..1df9ec2d6 --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int1.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=2 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=3 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=4 --no-check-models --no-check-unsat-cores --no-check-proofs +; EXPECT: unsat +(set-logic QF_BV) +(declare-fun x () (_ BitVec 4)) +(declare-fun y () (_ BitVec 4)) +(assert (= x (_ bv3 4))) +(assert (= y (_ bv3 4))) +(assert (not (bvsle (bvadd x y) (_ bv6 4)))) +(assert (= (bvadd x y) (_ bv6 4))) +(check-sat) diff --git a/test/regress/regress0/bv/bv_to_int2.smt2 b/test/regress/regress0/bv/bv_to_int2.smt2 new file mode 100644 index 000000000..ab1bf10f3 --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int2.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=5 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=8 --no-check-models --no-check-unsat-cores +; EXPECT: sat +(set-logic QF_BV) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) +(assert (bvult (bvshl a b) (bvlshr a b))) + +(check-sat) diff --git a/test/regress/regress0/bv/bv_to_int_bitwise.smt2 b/test/regress/regress0/bv/bv_to_int_bitwise.smt2 new file mode 100644 index 000000000..52eb78830 --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int_bitwise.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=5 --no-check-models --no-check-unsat-cores --no-check-proofs +; EXPECT: unsat +(set-logic QF_BV) +(declare-fun s () (_ BitVec 4)) +(declare-fun t () (_ BitVec 4)) +(assert (not (= (bvlshr s (bvor (bvand t #b0000) s)) #b0000))) +(check-sat) +(exit) diff --git a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 new file mode 100644 index 000000000..d0d699b4d --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=4 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=8 --no-check-models --no-check-unsat-cores +; EXPECT: sat +(set-logic QF_BV) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) +(assert (bvult (bvmul a b) (bvudiv a b))) + +(check-sat) diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 new file mode 100644 index 000000000..541229813 --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int_bvmul2.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 QF_BV) +(declare-fun T4_180 () (_ BitVec 32)) +(assert (and +(= (bvmul T4_180 (_ bv1056 32)) (_ bv0 32)) +(not (= (bvmul T4_180 (_ bv1408 32)) (_ bv0 32))) +) +) +(check-sat) diff --git a/test/regress/regress0/bv/bv_to_int_zext.smt2 b/test/regress/regress0/bv/bv_to_int_zext.smt2 new file mode 100644 index 000000000..3525cebb6 --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int_zext.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores --no-check-proofs +; EXPECT: unsat +(set-logic QF_BV) +(declare-fun T1_31078 () (_ BitVec 8)) +(assert (let ((?v_0 ((_ zero_extend 8) T1_31078))) (and true (= ?v_0 (_ bv123 16)) (not (= (_ bv123 16) ?v_0))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/bv/bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bvuf_to_intuf.smt2 new file mode 100644 index 000000000..7176f4012 --- /dev/null +++ b/test/regress/regress0/bv/bvuf_to_intuf.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores +; EXPECT: sat +(set-logic QF_UFBV) +(declare-fun a () (_ BitVec 4)) +(declare-fun b () (_ BitVec 4)) +(declare-fun f ((_ BitVec 4)) (_ BitVec 4) ) +(assert (distinct (bvadd a b) (f a))) +(check-sat) diff --git a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 b/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 new file mode 100644 index 000000000..297bb2422 --- /dev/null +++ b/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 @@ -0,0 +1,81 @@ +;COMMAND-LINE: --solve-bv-as-int=1 --no-produce-models --no-produce-unsat-cores --no-check-proofs +;EXPECT: unsat + +(set-logic QF_UFBV) +(declare-fun z$n0s32 () (_ BitVec 32)) +(declare-fun dataOut () (_ BitVec 32)) +(declare-fun z$2 () (_ BitVec 1)) +(declare-fun stageOne () (_ BitVec 32)) +(declare-fun z$4 () (_ BitVec 1)) +(declare-fun stageTwo () (_ BitVec 32)) +(declare-fun z$6 () (_ BitVec 1)) +(declare-fun tmp_stageOne () (_ BitVec 32)) +(declare-fun z$8 () (_ BitVec 1)) +(declare-fun tmp_stageTwo () (_ BitVec 32)) +(declare-fun z$10 () (_ BitVec 1)) +(declare-fun reset_ () (_ BitVec 1)) +(declare-fun z$14 () (_ BitVec 1)) +(declare-fun Add_32_32_32 ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32)) +(declare-fun z$15 () (_ BitVec 32)) +(declare-fun z$17 () (_ BitVec 32)) +(declare-fun dataOut$next () (_ BitVec 32)) +(declare-fun z$19 () (_ BitVec 1)) +(declare-fun c1 () (_ BitVec 32)) +(declare-fun dataIn () (_ BitVec 32)) +(declare-fun z$23 () (_ BitVec 32)) +(declare-fun stageOne$next () (_ BitVec 32)) +(declare-fun z$25 () (_ BitVec 1)) +(declare-fun c2 () (_ BitVec 32)) +(declare-fun z$28 () (_ BitVec 32)) +(declare-fun stageTwo$next () (_ BitVec 32)) +(declare-fun z$30 () (_ BitVec 1)) +(declare-fun tmp_stageOne$next () (_ BitVec 32)) +(declare-fun z$32 () (_ BitVec 1)) +(declare-fun tmp_stageTwo$next () (_ BitVec 32)) +(declare-fun z$34 () (_ BitVec 1)) +(declare-fun z$35 () (_ BitVec 1)) +(declare-fun z$55 () (_ BitVec 32)) +(declare-fun z$57 () (_ BitVec 1)) +(declare-fun z$58 () (_ BitVec 1)) +(declare-fun z$59 () (_ BitVec 1)) +(declare-fun prop$next () (_ BitVec 1)) +(declare-fun z$61 () (_ BitVec 1)) +(declare-fun z$54 () (_ BitVec 1)) +(declare-fun z$63 () (_ BitVec 1)) +(assert + (= z$15 (Add_32_32_32 stageTwo stageOne))) +(assert + (= z$17 (ite (= z$14 (_ bv1 1)) z$15 z$n0s32))) +(assert + (= z$19 (ite (= dataOut$next z$17) (_ bv1 1) (_ bv0 1)))) +(assert + (= z$25 (ite (= stageOne$next z$23) (_ bv1 1) (_ bv0 1)))) + + +(assert + (= z$32 (ite (= tmp_stageOne$next stageOne) (_ bv1 1) (_ bv0 1)))) +(assert + (= z$34 (ite (= tmp_stageTwo$next stageTwo) (_ bv1 1) (_ bv0 1)))) +(assert + (let (($x130 (and (= z$19 (_ bv1 1)) (= z$25 (_ bv1 1)) (= z$30 (_ bv1 1)) (= z$32 (_ bv1 1)) (= z$34 (_ bv1 1))))) + (= z$35 (ite $x130 (_ bv1 1) (_ bv0 1))))) +(assert + (= z$55 (Add_32_32_32 tmp_stageTwo$next tmp_stageOne$next))) +(assert + (= z$57 (ite (= dataOut$next z$55) (_ bv1 1) (_ bv0 1)))) +(assert + (= z$58 (ite (= dataOut$next z$n0s32) (_ bv1 1) (_ bv0 1)))) +(assert + (= z$59 (ite (or (= z$57 (_ bv1 1)) (= z$58 (_ bv1 1))) (_ bv1 1) (_ bv0 1)))) +(assert + (= z$61 (ite (= prop$next z$59) (_ bv1 1) (_ bv0 1)))) +(assert + (= z$54 (ite (= prop$next (_ bv0 1)) (_ bv1 1) (_ bv0 1)))) +(assert + (let (($x52 (= z$2 (_ bv1 1)))) + (let (($x165 (and $x52 (= z$4 (_ bv1 1)) (= z$6 (_ bv1 1)) (= z$8 (_ bv1 1)) (= z$10 (_ bv1 1)) (= z$35 (_ bv1 1)) (= z$61 (_ bv1 1)) (= z$54 (_ bv1 1))))) + (= z$63 (ite $x165 (_ bv1 1) (_ bv0 1)))))) +(assert + (= z$63 (_ bv1 1))) +(check-sat) +(exit) diff --git a/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 new file mode 100644 index 000000000..873acd6c4 --- /dev/null +++ b/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores +; EXPECT: sat +(set-logic QF_UFBV) +(declare-sort S 0) +(declare-fun s () S) +(declare-fun a () (_ BitVec 4)) +(declare-fun b () (_ BitVec 4)) +(declare-fun f ((_ BitVec 4)) (_ BitVec 4) ) +(declare-fun g (S) (_ BitVec 4)) +(declare-fun h ((_ BitVec 4)) S) +(assert (distinct (bvadd a b) (f a))) +(assert (distinct (f a) (g s))) +(assert (distinct (h a) s)) +(check-sat) diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2 new file mode 100644 index 000000000..e3fcb1790 --- /dev/null +++ b/test/regress/regress2/bv_to_int_ashr.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=8 --no-check-models --no-check-unsat-cores --no-check-proofs +; EXPECT: unsat +(set-logic QF_BV) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) +(assert (bvult (bvashr a b) (bvlshr a b))) + +(check-sat) diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2 new file mode 100644 index 000000000..39dace123 --- /dev/null +++ b/test/regress/regress2/bv_to_int_shifts.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores +; EXPECT: sat +(set-logic QF_BV) +(declare-fun s () (_ BitVec 64)) +(declare-fun t () (_ BitVec 64)) +(declare-fun splust () (_ BitVec 64)) +(declare-fun shift1 () (_ BitVec 64)) +(declare-fun shift2 () (_ BitVec 64)) +(declare-fun negshift1 () (_ BitVec 64)) + +(assert (= shift1 (bvlshr s splust))) +(assert (= shift2 (bvlshr t splust))) +(assert (= negshift1 (bvneg shift1))) +(assert (= splust (bvadd s t))) +(assert (distinct negshift1 shift2)) + +(check-sat) diff --git a/test/regress/regress3/bv_to_int_and_or.smt2 b/test/regress/regress3/bv_to_int_and_or.smt2 new file mode 100644 index 000000000..54a491093 --- /dev/null +++ b/test/regress/regress3/bv_to_int_and_or.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=2 --no-check-models --no-check-unsat-cores --no-check-proofs +; EXPECT: unsat +(set-logic QF_BV) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) +(assert (bvult (bvor a b) (bvand a b))) +(check-sat) -- 2.30.2