From ad885db118e388687be7f657ddc943e74a0a9601 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Mon, 13 Dec 2021 18:16:08 +0200 Subject: [PATCH] Integrate new int-blaster (#7781) This PR removes the code that translates from bit-vectors to integers from the bv_to_int preprocessing pass, and replaces it with a call to the IntBlaster module. Tests are updated and added, as well as other minor changes. Solves the following issues (and contains corresponding tests): cvc5/cvc5-projects#345 cvc5/cvc5-projects#344 cvc5/cvc5-projects#343 @mpreiner FYI --- src/preprocessing/passes/bv_to_int.cpp | 1040 +---------------- src/preprocessing/passes/bv_to_int.h | 261 +---- src/theory/arith/arith_rewriter.cpp | 7 +- src/theory/arith/nl/iand_solver.cpp | 4 +- src/theory/bv/int_blaster.cpp | 46 +- src/theory/bv/int_blaster.h | 9 +- ...ry_bv_rewrite_rules_operator_elimination.h | 78 -- test/api/cpp/CMakeLists.txt | 2 + test/api/cpp/proj-issue344.cpp | 33 + test/api/cpp/proj-issue345.cpp | 34 + test/regress/CMakeLists.txt | 3 + test/regress/regress0/bv/bv_to_int1.smt2 | 1 + .../regress/regress0/bv/bv_to_int_bvmul2.smt2 | 1 + .../regress0/bv/bv_to_int_bvuf_to_intuf.smt2 | 1 + .../bv/bv_to_int_bvuf_to_intuf_sorts.smt2 | 1 + .../regress0/bv/bv_to_int_elim_err.smt2 | 3 +- test/regress/regress0/bv/bv_to_int_int1.smt2 | 11 + test/regress/regress0/bv/bv_to_int_zext.smt2 | 1 + test/regress/regress0/bv/proj-issue343.smt2 | 7 + test/regress/regress2/bv_to_int2.smt2 | 1 + test/regress/regress2/bv_to_int_ashr.smt2 | 1 + test/regress/regress2/bv_to_int_bitwise.smt2 | 12 +- test/regress/regress2/bv_to_int_bvmul1.smt2 | 1 + .../bv_to_int_bvuf_to_intuf_smtlib.smt2 | 3 +- test/regress/regress2/bv_to_int_inc1.smt2 | 1 + .../regress2/bv_to_int_mask_array_1.smt2 | 5 +- .../regress2/bv_to_int_mask_array_2.smt2 | 1 + .../regress2/bv_to_int_mask_array_3.smt2 | 1 + .../regress2/bv_to_int_quantifiers_bvand.smt2 | 9 + test/regress/regress2/bv_to_int_shifts.smt2 | 1 + test/regress/regress3/bv_to_int_and_or.smt2 | 6 +- .../bv_to_int_bench_9839.smt2.minimized.smt2 | 5 +- ...eck_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 | 6 +- ..._input_mouser_detect.c.smt2.minimized.smt2 | 2 +- .../theory/theory_bv_int_blaster_white.cpp | 10 +- 35 files changed, 210 insertions(+), 1398 deletions(-) create mode 100644 test/api/cpp/proj-issue344.cpp create mode 100644 test/api/cpp/proj-issue345.cpp create mode 100644 test/regress/regress0/bv/bv_to_int_int1.smt2 create mode 100644 test/regress/regress0/bv/proj-issue343.smt2 create mode 100644 test/regress/regress2/bv_to_int_quantifiers_bvand.smt2 diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index f106f1ccf..ac1edeb96 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -19,1060 +19,90 @@ #include "preprocessing/passes/bv_to_int.h" #include -#include #include #include #include #include "expr/node.h" #include "expr/node_traversal.h" -#include "expr/skolem_manager.h" -#include "options/option_exception.h" #include "options/smt_options.h" #include "options/uf_options.h" -#include "preprocessing/assertion_pipeline.h" -#include "preprocessing/preprocessing_pass_context.h" #include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h" +#include "preprocessing/assertion_pipeline.h" #include "theory/bv/theory_bv_rewrite_rules_simplification.h" #include "theory/rewriter.h" -#include "util/bitvector.h" -#include "util/iand.h" -#include "util/rational.h" namespace cvc5 { namespace preprocessing { namespace passes { using namespace std; -using namespace cvc5::kind; using namespace cvc5::theory; using namespace cvc5::theory::bv; -namespace { - -Rational intpow2(uint64_t b) -{ - return Rational(Integer(2).pow(b), Integer(1)); -} - -} //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 rewrite(result); -} - -Node BVToInt::maxInt(uint64_t k) -{ - Assert(k > 0); - Rational max_value = intpow2(k) - 1; - return d_nm->mkConst(CONST_RATIONAL, max_value); -} - -Node BVToInt::pow2(uint64_t k) -{ - Assert(k >= 0); - return d_nm->mkConst(CONST_RATIONAL, Rational(intpow2(k))); -} - -Node BVToInt::modpow2(Node n, uint64_t exponent) -{ - Node p2 = d_nm->mkConst(CONST_RATIONAL, Rational(intpow2(exponent))); - return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, n, p2); -} - -/** - * Binarizing n via post-order traversal. - */ -Node BVToInt::makeBinary(Node n) -{ - for (TNode current : NodeDfsIterable(n, - VisitOrder::POSTORDER, - // skip visited nodes - [this](TNode tn) { - return d_binarizeCache.find(tn) - != d_binarizeCache.end(); - })) - { - uint64_t numChildren = current.getNumChildren(); - /* - * We already visited the sub-dag rooted at the current node, - * and binarized all its children. - * Now we binarize the current node itself. - */ - kind::Kind_t k = current.getKind(); - if ((numChildren > 2) - && (k == kind::BITVECTOR_ADD || 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.getMetaKind() == kind::metakind::PARAMETERIZED) - { - builder << current.getOperator(); - } - for (Node child : current) - { - builder << d_binarizeCache[child].get(); - } - d_binarizeCache[current] = builder.constructNode(); - } - else - { - // current has no children - d_binarizeCache[current] = current; - } - } - 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(); - // assert that the node is binarized - // The following variable is only used in assertions - CVC5_UNUSED kind::Kind_t k = current.getKind(); - uint64_t numChildren = current.getNumChildren(); - Assert((numChildren == 2) - || !(k == kind::BITVECTOR_ADD || k == kind::BITVECTOR_MULT - || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR - || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT)); - toVisit.pop_back(); - bool inEliminationCache = - (d_eliminationCache.find(current) != d_eliminationCache.end()); - bool inRebuildCache = - (d_rebuildCache.find(current) != d_rebuildCache.end()); - if (!inEliminationCache) - { - // current is not the elimination of any previously-visited node - // current hasn't been eliminated yet. - // eliminate operators from it using rewrite rules - Node currentEliminated = - FixpointRewriteStrategy, - RewriteRule, - RewriteRule, - RewriteRule, - 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; - // also assign the eliminated now to itself to avoid revisiting. - d_eliminationCache[currentEliminated] = 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()); - } - if (inRebuildCache) - { - // current was already added to the rebuild cache. - if (d_rebuildCache[current].get().isNull()) - { - // current wasn't rebuilt yet. - 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.getMetaKind() == kind::metakind::PARAMETERIZED) - { - 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].get().isNull()); - builder << d_rebuildCache[eliminatedChild].get(); - } - 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].get().isNull()); - return d_rebuildCache[eliminated]; -} - -/** - * Translate n to Integers via post-order traversal. - */ -Node BVToInt::bvToInt(Node n) -{ - // make sure the node is re-written before processing it. - n = rewrite(n); - n = makeBinary(n); - n = eliminationPass(n); - // binarize again, in case the elimination pass introduced - // non-binary terms (as can happen by RepeatEliminate, for example). - n = makeBinary(n); - vector toVisit; - toVisit.push_back(n); - - 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. - // We mark this node as visited but not translated by assiging - // a null node to it. - d_bvToIntCache[current] = Node(); - // all the node's children are added to the stack to be visited - // before visiting this node again. - toVisit.insert(toVisit.end(), current.begin(), current.end()); - // If this is a UF applicatinon, we also add the function to - // toVisit. - if (current.getKind() == kind::APPLY_UF) - { - toVisit.push_back(current.getOperator()); - } - } - else - { - // We already visited and translated this node - if (!d_bvToIntCache[current].get().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. - Node translation; - if (currentNumChildren == 0) - { - translation = translateNoChildren(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 easy access. - * If the node's kind is APPLY_UF, - * we also need to include the translated uninterpreted function in - * this list. - */ - vector translated_children; - if (current.getKind() == kind::APPLY_UF) - { - translated_children.push_back( - d_bvToIntCache[current.getOperator()]); - } - for (uint64_t i = 0; i < currentNumChildren; i++) - { - translated_children.push_back(d_bvToIntCache[current[i]]); - } - translation = translateWithChildren(current, translated_children); - } - // Map the current node to its translation in the cache. - d_bvToIntCache[current] = translation; - // Also map the translation to itself. - d_bvToIntCache[translation] = translation; - toVisit.pop_back(); - } - } - } - return d_bvToIntCache[n].get(); -} - -Node BVToInt::translateWithChildren(Node original, - const vector& translated_children) -{ - // The translation of the original node is determined by the kind of - // the node. - kind::Kind_t oldKind = original.getKind(); - // ultbv and sltbv were supposed to be eliminated before this point. - Assert(oldKind != kind::BITVECTOR_ULTBV); - Assert(oldKind != kind::BITVECTOR_SLTBV); - // The following variable will only be used in assertions. - CVC5_UNUSED uint64_t originalNumChildren = original.getNumChildren(); - Node returnNode; - switch (oldKind) - { - case kind::BITVECTOR_ADD: - { - Assert(originalNumChildren == 2); - uint64_t bvsize = original[0].getType().getBitVectorSize(); - Node plus = d_nm->mkNode(kind::PLUS, translated_children); - Node p2 = pow2(bvsize); - returnNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, plus, p2); - break; - } - case kind::BITVECTOR_MULT: - { - Assert(originalNumChildren == 2); - uint64_t bvsize = original[0].getType().getBitVectorSize(); - Node mult = d_nm->mkNode(kind::MULT, translated_children); - Node p2 = pow2(bvsize); - returnNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, mult, p2); - break; - } - case kind::BITVECTOR_UDIV: - { - uint64_t bvsize = original[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); - returnNode = d_nm->mkNode( - kind::ITE, - d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero), - d_nm->mkNode(kind::MINUS, pow2BvSize, d_one), - divNode); - break; - } - case kind::BITVECTOR_UREM: - { - // we use an ITE for the case where the second operand is 0. - Node modNode = - d_nm->mkNode(kind::INTS_MODULUS_TOTAL, translated_children); - returnNode = d_nm->mkNode( - kind::ITE, - d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero), - translated_children[0], - modNode); - break; - } - case kind::BITVECTOR_NOT: - { - uint64_t bvsize = original[0].getType().getBitVectorSize(); - // we use a specified function to generate the node. - returnNode = 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. - returnNode = translated_children[0]; - break; - } - case kind::INT_TO_BITVECTOR: - { - // ((_ int2bv n) t) ---> (mod t 2^n) - size_t sz = original.getOperator().getConst().d_size; - returnNode = d_nm->mkNode( - kind::INTS_MODULUS_TOTAL, translated_children[0], pow2(sz)); - } - break; - case kind::BITVECTOR_AND: - { - // We support three configurations: - // 1. translating to IAND - // 2. translating back to BV (using BITVECTOR_TO_NAT and INT_TO_BV - // operators) - // 3. translating into a sum - uint64_t bvsize = original[0].getType().getBitVectorSize(); - if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::IAND) - { - Node iAndOp = d_nm->mkConst(IntAnd(bvsize)); - returnNode = d_nm->mkNode( - kind::IAND, iAndOp, translated_children[0], translated_children[1]); - } - else if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::BV) - { - // translate the children back to BV - Node intToBVOp = d_nm->mkConst(IntToBitVector(bvsize)); - Node x = translated_children[0]; - Node y = translated_children[1]; - Node bvx = d_nm->mkNode(intToBVOp, x); - Node bvy = d_nm->mkNode(intToBVOp, y); - // perform bvand on the bit-vectors - Node bvand = d_nm->mkNode(kind::BITVECTOR_AND, bvx, bvy); - // translate the result to integers - returnNode = d_nm->mkNode(kind::BITVECTOR_TO_NAT, bvand); - } - else - { - Assert(options().smt.solveBVAsInt == options::SolveBVAsIntMode::SUM); - // Construct a sum of ites, based on granularity. - Assert(translated_children.size() == 2); - returnNode = - d_iandUtils.createSumNode(translated_children[0], - translated_children[1], - bvsize, - options().smt.BVAndIntegerGranularity); - } - 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 = original[0].getType().getBitVectorSize(); - returnNode = createShiftNode(translated_children, bvsize, true); - 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 = original[0].getType().getBitVectorSize(); - returnNode = createShiftNode(translated_children, bvsize, false); - 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 = original[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); - returnNode = d_nm->mkNode(kind::ITE, condition, thenNode, elseNode); - break; - } - case kind::BITVECTOR_ITE: - { - // Lifted to a boolean ite. - Node cond = d_nm->mkNode(kind::EQUAL, translated_children[0], d_one); - returnNode = d_nm->mkNode( - kind::ITE, cond, translated_children[1], translated_children[2]); - break; - } - case kind::BITVECTOR_ZERO_EXTEND: - { - returnNode = translated_children[0]; - break; - } - case kind::BITVECTOR_SIGN_EXTEND: - { - uint64_t bvsize = original[0].getType().getBitVectorSize(); - Node arg = translated_children[0]; - if (arg.isConst()) - { - Rational c(arg.getConst()); - Rational twoToKMinusOne(intpow2(bvsize - 1)); - uint64_t amount = bv::utils::getSignExtendAmount(original); - /* if the msb is 0, this is like zero_extend. - * msb is 0 <-> the value is less than 2^{bvsize-1} - */ - if (c < twoToKMinusOne || amount == 0) - { - returnNode = arg; - } - else - { - /* otherwise, we add the integer equivalent of - * 11....1 `amount` times - */ - Rational max_of_amount = intpow2(amount) - 1; - Rational mul = max_of_amount * intpow2(bvsize); - Rational sum = mul + c; - returnNode = d_nm->mkConst(CONST_RATIONAL, sum); - } - } - else - { - uint64_t amount = bv::utils::getSignExtendAmount(original); - if (amount == 0) - { - returnNode = translated_children[0]; - } - else - { - Rational twoToKMinusOne(intpow2(bvsize - 1)); - Node minSigned = d_nm->mkConst(CONST_RATIONAL, twoToKMinusOne); - /* condition checks whether the msb is 1. - * This holds when the integer value is smaller than - * 100...0, which is 2^{bvsize-1}. - */ - Node condition = d_nm->mkNode(kind::LT, arg, minSigned); - Node thenResult = arg; - Node left = maxInt(amount); - Node mul = d_nm->mkNode(kind::MULT, left, pow2(bvsize)); - Node sum = d_nm->mkNode(kind::PLUS, mul, arg); - Node elseResult = sum; - Node ite = d_nm->mkNode(kind::ITE, condition, thenResult, elseResult); - returnNode = ite; - } - } - break; - } - case kind::BITVECTOR_CONCAT: - { - // (concat a b) translates to a*2^k+b, k being the bitwidth of b. - uint64_t bvsizeRight = original[1].getType().getBitVectorSize(); - Node pow2BvSizeRight = pow2(bvsizeRight); - Node a = - d_nm->mkNode(kind::MULT, translated_children[0], pow2BvSizeRight); - Node b = translated_children[1]; - returnNode = d_nm->mkNode(kind::PLUS, a, b); - break; - } - case kind::BITVECTOR_EXTRACT: - { - // ((_ extract i j) a) is a / 2^j mod 2^{i-j+1} - // original = a[i:j] - uint64_t i = bv::utils::getExtractHigh(original); - uint64_t j = bv::utils::getExtractLow(original); - Assert(i >= j); - Node div = d_nm->mkNode( - kind::INTS_DIVISION_TOTAL, translated_children[0], pow2(j)); - returnNode = modpow2(div, i - j + 1); - break; - } - case kind::EQUAL: - { - returnNode = d_nm->mkNode(kind::EQUAL, translated_children); - break; - } - case kind::BITVECTOR_ULT: - { - returnNode = d_nm->mkNode(kind::LT, translated_children); - break; - } - case kind::BITVECTOR_ULE: - { - returnNode = d_nm->mkNode(kind::LEQ, translated_children); - break; - } - case kind::BITVECTOR_UGT: - { - returnNode = d_nm->mkNode(kind::GT, translated_children); - break; - } - case kind::BITVECTOR_UGE: - { - returnNode = d_nm->mkNode(kind::GEQ, translated_children); - break; - } - case kind::LT: - { - returnNode = d_nm->mkNode(kind::LT, translated_children); - break; - } - case kind::LEQ: - { - returnNode = d_nm->mkNode(kind::LEQ, translated_children); - break; - } - case kind::GT: - { - returnNode = d_nm->mkNode(kind::GT, translated_children); - break; - } - case kind::GEQ: - { - returnNode = d_nm->mkNode(kind::GEQ, translated_children); - break; - } - case kind::ITE: - { - returnNode = d_nm->mkNode(oldKind, translated_children); - break; - } - case kind::APPLY_UF: - { - /** - * higher order logic allows comparing between functions - * The 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 (childrenTypesChanged(original) && logicInfo().isHigherOrder()) - { - throw TypeCheckingExceptionPrivate( - original, - string("Cannot translate to Int: ") + original.toString()); - } - // Insert the translated application term to the cache - returnNode = d_nm->mkNode(kind::APPLY_UF, translated_children); - // Add range constraints if necessary. - // If the original range was a BV sort, the original application of - // the function Must be within the range determined by the - // bitwidth. - if (original.getType().isBitVector()) - { - d_rangeAssertions.insert(mkRangeConstraint( - returnNode, original.getType().getBitVectorSize())); - } - break; - } - case kind::BOUND_VAR_LIST: - { - returnNode = d_nm->mkNode(oldKind, translated_children); - break; - } - case kind::FORALL: - { - returnNode = translateQuantifiedFormula(original); - break; - } - default: - { - Assert(oldKind != kind::EXISTS); // Exists is eliminated by the rewriter. - // In the default case, we have reached an operator that we do not - // translate directly to integers. The children whose types have - // changed from bv to int should be adjusted back to bv and then - // this term is reconstructed. - TypeNode resultingType; - if (original.getType().isBitVector()) - { - resultingType = d_nm->integerType(); - } - else - { - resultingType = original.getType(); - } - Node reconstruction = - reconstructNode(original, resultingType, translated_children); - returnNode = reconstruction; - break; - } - } - Trace("bv-to-int-debug") << "original: " << original << endl; - Trace("bv-to-int-debug") << "returnNode: " << returnNode << endl; - return returnNode; -} - -Node BVToInt::translateNoChildren(Node original) -{ - SkolemManager* sm = d_nm->getSkolemManager(); - Node translation; - Assert(original.isVar() || original.isConst()); - if (original.isVar()) - { - if (original.getType().isBitVector()) - { - // For bit-vector variables, we create fresh integer variables. - if (original.getKind() == kind::BOUND_VARIABLE) - { - // Range constraints for the bound integer variables are not added now. - // they will be added once the quantifier itself is handled. - std::stringstream ss; - ss << original; - translation = d_nm->mkBoundVar(ss.str() + "_int", d_nm->integerType()); - } - else - { - // New integer variables that are not bound (symbolic constants) - // are added together with range constraints induced by the - // bit-width of the original bit-vector variables. - Node newVar = sm->mkDummySkolem("__bvToInt_var", - d_nm->integerType(), - "Variable introduced in bvToInt " - "pass instead of original variable " - + original.toString()); - uint64_t bvsize = original.getType().getBitVectorSize(); - translation = newVar; - d_rangeAssertions.insert(mkRangeConstraint(newVar, bvsize)); - defineBVUFAsIntUF(original, newVar); - } - } - else if (original.getType().isFunction()) - { - translation = translateFunctionSymbol(original); - } - else - { - // variables other than bit-vector variables and function symbols - // are left intact - translation = original; - } - } - else - { - // original is a const - if (original.getKind() == kind::CONST_BITVECTOR) - { - // Bit-vector constants are transformed into their integer value. - BitVector constant(original.getConst()); - Integer c = constant.toInteger(); - translation = d_nm->mkConst(CONST_RATIONAL, Rational(c)); - } - else - { - // Other constants stay the same. - translation = original; - } - } - return translation; -} - -Node BVToInt::translateFunctionSymbol(Node bvUF) -{ - // construct the new function symbol. - Node intUF; - TypeNode tn = bvUF.getType(); - TypeNode bvRange = tn.getRangeType(); - // The function symbol has not been converted yet - 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. - * Similarly for the domains. - */ - TypeNode intRange = bvRange.isBitVector() ? d_nm->integerType() : bvRange; - for (TypeNode d : bvDomain) - { - intDomain.push_back(d.isBitVector() ? d_nm->integerType() : d); - } - SkolemManager* sm = d_nm->getSkolemManager(); - ostringstream os; - os << "__bvToInt_fun_" << bvUF << "_int"; - intUF = sm->mkDummySkolem( - os.str(), d_nm->mkFunctionType(intDomain, intRange), "bv2int function"); - // introduce a `define-fun` in the smt-engine to keep - // the correspondence between the original - // function symbol and the new one. - defineBVUFAsIntUF(bvUF, intUF); - return intUF; -} - -void BVToInt::defineBVUFAsIntUF(Node bvUF, Node intUF) -{ - // The resulting term - Node result; - // The type of the resulting term - TypeNode resultType; - // symbolic arguments of original function - vector args; - if (!bvUF.getType().isFunction()) { - // bvUF is a variable. - // in this case, the result is just the original term - // (it will be casted later if needed) - result = intUF; - resultType = bvUF.getType(); - } else { - // bvUF is a function with arguments - // The arguments need to be casted as well. - TypeNode tn = bvUF.getType(); - resultType = tn.getRangeType(); - vector bvDomain = tn.getArgTypes(); - // children of the new symbolic application - vector achildren; - achildren.push_back(intUF); - int i = 0; - for (const TypeNode& d : bvDomain) - { - // Each bit-vector argument is casted to a natural number - // Other arguments are left intact. - Node fresh_bound_var = d_nm->mkBoundVar(d); - args.push_back(fresh_bound_var); - Node castedArg = args[i]; - if (d.isBitVector()) - { - castedArg = castToType(castedArg, d_nm->integerType()); - } - achildren.push_back(castedArg); - i++; - } - result = d_nm->mkNode(kind::APPLY_UF, achildren); - } - // If the result is BV, it needs to be casted back. - result = castToType(result, resultType); - // add the substitution to the preprocessing context, which ensures the - // model for bvUF is correct, as well as substituting it in the input - // assertions when necessary. - if (!args.empty()) - { - result = d_nm->mkNode( - kind::LAMBDA, d_nm->mkNode(kind::BOUND_VAR_LIST, args), result); - } - d_preprocContext->addSubstitution(bvUF, result); -} - -bool BVToInt::childrenTypesChanged(Node n) -{ - bool result = false; - for (const Node& child : n) - { - TypeNode originalType = child.getType(); - TypeNode newType = d_bvToIntCache[child].get().getType(); - if (!newType.isSubtypeOf(originalType)) - { - result = true; - break; - } - } - return result; -} - -Node BVToInt::castToType(Node n, TypeNode tn) -{ - // If there is no reason to cast, return the - // original node. - if (n.getType().isSubtypeOf(tn)) - { - return n; - } - // We only case int to bv or vice verse. - Assert((n.getType().isBitVector() && tn.isInteger()) - || (n.getType().isInteger() && tn.isBitVector())); - if (n.getType().isInteger()) - { - Assert(tn.isBitVector()); - unsigned bvsize = tn.getBitVectorSize(); - Node intToBVOp = d_nm->mkConst(IntToBitVector(bvsize)); - return d_nm->mkNode(intToBVOp, n); - } - Assert(n.getType().isBitVector()); - Assert(tn.isInteger()); - return d_nm->mkNode(kind::BITVECTOR_TO_NAT, n); -} - -Node BVToInt::reconstructNode(Node originalNode, - TypeNode resultType, - const vector& translated_children) -{ - // first, we adjust the children of the node as needed. - // re-construct the term with the adjusted children. - kind::Kind_t oldKind = originalNode.getKind(); - NodeBuilder builder(oldKind); - if (originalNode.getMetaKind() == kind::metakind::PARAMETERIZED) - { - builder << originalNode.getOperator(); - } - for (size_t i = 0; i < originalNode.getNumChildren(); i++) - { - Node originalChild = originalNode[i]; - Node translatedChild = translated_children[i]; - Node adjustedChild = castToType(translatedChild, originalChild.getType()); - builder << adjustedChild; - } - Node reconstruction = builder.constructNode(); - // cast to tn in case the reconstruction is a bit-vector. - reconstruction = castToType(reconstruction, resultType); - return reconstruction; -} - BVToInt::BVToInt(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "bv-to-int"), - d_binarizeCache(userContext()), - d_eliminationCache(userContext()), - d_rebuildCache(userContext()), - d_bvToIntCache(userContext()), - d_rangeAssertions(userContext()) -{ - d_nm = NodeManager::currentNM(); - d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0)); - d_one = d_nm->mkConst(CONST_RATIONAL, Rational(1)); - - if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::BITWISE) - { - throw OptionException("bitwise option is not supported currently"); - } -}; + d_intBlaster(preprocContext->getEnv(), + options::solveBVAsInt(), + options::BVAndIntegerGranularity()) {} PreprocessingPassResult BVToInt::applyInternal( AssertionPipeline* assertionsToPreprocess) { + // vector of boolean nodes for additional constraints + // this will always contain range constraints + // and for options::SolveBVAsIntMode::BITWISE, it will + // also include bitwise assertion constraints + std::vector additionalConstraints; + std::map skolems; for (uint64_t i = 0; i < assertionsToPreprocess->size(); ++i) { Node bvNode = (*assertionsToPreprocess)[i]; - Node intNode = bvToInt(bvNode); + Node intNode = + d_intBlaster.intBlast(bvNode, additionalConstraints, skolems); Node rwNode = 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); + addFinalizeAssertions(assertionsToPreprocess, additionalConstraints); + addSkolemDefinitions(skolems); return PreprocessingPassResult::NO_CONFLICT; } -void BVToInt::addFinalizeRangeAssertions( - AssertionPipeline* assertionsToPreprocess) -{ - // collect the range assertions from d_rangeAssertions - // (which is a context-dependent set) - // into a vector. - vector vec_range; - vec_range.assign(d_rangeAssertions.key_begin(), d_rangeAssertions.key_end()); - // conjoin all range assertions and add the conjunction - // as a new assertion - Node rangeAssertions = rewrite(d_nm->mkAnd(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) -{ - /** - * 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 an ite. - * Important note: below we use INTS_DIVISION_TOTAL, which is safe here - * because we divide by 2^... which is never 0. - */ - Node x = children[0]; - Node y = children[1]; - // shifting by const is eliminated by the theory rewriter - Assert(!y.isConst()); - Node ite = d_zero; - Node body; - for (uint64_t i = 0; i < bvsize; i++) - { - if (isLeftShift) - { - body = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, - d_nm->mkNode(kind::MULT, x, pow2(i)), - pow2(bvsize)); - } - else - { - body = d_nm->mkNode(kind::INTS_DIVISION_TOTAL, x, pow2(i)); - } - ite = d_nm->mkNode( - kind::ITE, - d_nm->mkNode( - kind::EQUAL, y, d_nm->mkConst(CONST_RATIONAL, Rational(i))), - body, - ite); - } - return ite; -} - -Node BVToInt::translateQuantifiedFormula(Node quantifiedNode) +void BVToInt::addSkolemDefinitions(const std::map& skolems) { - kind::Kind_t k = quantifiedNode.getKind(); - Node boundVarList = quantifiedNode[0]; - Assert(boundVarList.getKind() == kind::BOUND_VAR_LIST); - // Since bit-vector variables are being translated to - // integer variables, we need to substitute the new ones - // for the old ones. - vector oldBoundVars; - vector newBoundVars; - vector rangeConstraints; - for (Node bv : quantifiedNode[0]) + map::const_iterator it; + for (it = skolems.begin(); it != skolems.end(); it++) { - oldBoundVars.push_back(bv); - if (bv.getType().isBitVector()) + Node originalSkolem = it->first; + Node definition = it->second; + std::vector args; + Node body; + if (definition.getType().isFunction()) { - // bit-vector variables are replaced by integer ones. - // the new variables induce range constraints based on the - // original bit-width. - Node newBoundVar = d_bvToIntCache[bv]; - newBoundVars.push_back(newBoundVar); - rangeConstraints.push_back( - mkRangeConstraint(newBoundVar, bv.getType().getBitVectorSize())); + args.insert(args.end(), definition[0].begin(), definition[0].end()); + body = definition[1]; } else { - // variables that are not bit-vectors are not changed - newBoundVars.push_back(bv); + body = definition; } + Trace("bv-to-int-debug") << "adding substitution: " << "[" << originalSkolem << "] ----> [" << definition << "]" << std::endl; + d_preprocContext->addSubstitution(originalSkolem, definition); } - - // the body of the quantifier - Node matrix = d_bvToIntCache[quantifiedNode[1]]; - // make the substitution - matrix = matrix.substitute(oldBoundVars.begin(), - oldBoundVars.end(), - newBoundVars.begin(), - newBoundVars.end()); - // A node to represent all the range constraints. - Node ranges = d_nm->mkAnd(rangeConstraints); - // Add the range constraints to the body of the quantifier. - // For "exists", this is added conjunctively - // For "forall", this is added to the left side of an implication. - matrix = d_nm->mkNode( - k == kind::FORALL ? kind::IMPLIES : kind::AND, ranges, matrix); - // create the new quantified formula and return it. - Node newBoundVarsList = d_nm->mkNode(kind::BOUND_VAR_LIST, newBoundVars); - Node result = d_nm->mkNode(kind::FORALL, newBoundVarsList, matrix); - return result; } -Node BVToInt::createBVNotNode(Node n, uint64_t bvsize) +void BVToInt::addFinalizeAssertions( + AssertionPipeline* assertionsToPreprocess, + const std::vector& additionalConstraints) { - return d_nm->mkNode(kind::MINUS, maxInt(bvsize), n); + NodeManager* nm = NodeManager::currentNM(); + Node lemmas = nm->mkAnd(additionalConstraints); + assertionsToPreprocess->push_back(lemmas); + Trace("bv-to-int-debug") << "range constraints: " << lemmas.toString() + << std::endl; } } // namespace passes diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h index d09f9e738..24fc185b5 100644 --- a/src/preprocessing/passes/bv_to_int.h +++ b/src/preprocessing/passes/bv_to_int.h @@ -1,6 +1,7 @@ + /****************************************************************************** * Top contributors (to current version): - * Yoni Zohar, Gereon Kremer, Makai Mann + * Yoni Zohar * * This file is part of the cvc5 project. * @@ -10,69 +11,18 @@ * directory for licensing information. * **************************************************************************** * - * 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((_ zero_extend m) x) = Tr(x) - * Tr((_ sign_extend m) x) = ite(msb(x)=0, x, 2^k*(2^m-1) + x)) - * explanation: if the msb is 0, this is the same as zero_extend, - * which does not change the integer value. - * If the msb is 1, then the result should correspond to - * concat(1...1, x), with m 1's. - * m 1's is 2^m-1, and multiplying it by x's width (k) moves it - * to the front. - * - * 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) - * - * 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. - * + * The bv-to-int preprocessing pass. */ -#include "cvc5_private.h" - #ifndef __CVC5__PREPROCESSING__PASSES__BV_TO_INT_H #define __CVC5__PREPROCESSING__PASSES__BV_TO_INT_H #include "context/cdhashmap.h" -#include "context/cdhashset.h" +#include "context/cdo.h" +#include "context/context.h" #include "preprocessing/preprocessing_pass.h" -#include "theory/arith/nl/iand_utils.h" +#include "preprocessing/preprocessing_pass_context.h" +#include "theory/bv/int_blaster.h" namespace cvc5 { namespace preprocessing { @@ -88,200 +38,15 @@ class BVToInt : public PreprocessingPass protected: PreprocessingPassResult applyInternal( AssertionPipeline* assertionsToPreprocess) override; - /** - * 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(std::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); - - bool childrenTypesChanged(Node n); - - /** - * 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); - - /** - * @param quantifiedNode a node whose main operator is forall/exists. - * @return a node opbtained from quantifiedNode by: - * 1. Replacing all bound BV variables by new bound integer variables. - * 2. Add range constraints for the new variables, induced by the original - * bit-width. These range constraints are added with "AND" in case of exists - * and with "IMPLIES" in case of forall. - */ - Node translateQuantifiedFormula(Node quantifiedNode); - - /** - * Reconstructs a node whose main operator cannot be - * translated to integers. - * Reconstruction is done by casting to integers/bit-vectors - * as needed. - * For example, if node is (select A x) where A - * is a bit-vector array, we do not change A to be - * an integer array, even though x was translated - * to integers. - * In this case we cast x to (bv2nat x) during - * the reconstruction. - * - * @param originalNode the node that we are reconstructing - * @param resultType the desired type for the reconstruction - * @param translated_children the children of originalNode - * after their translation to integers. - * @return A node with originalNode's operator that has type resultType. - */ - Node reconstructNode(Node originalNode, - TypeNode resultType, - const std::vector& translated_children); - - /** - * A useful utility function. - * if n is an integer and tn is bit-vector, - * applies the IntToBitVector operator on n. - * if n is a vit-vector and tn is integer, - * applies BitVector_TO_NAT operator. - * Otherwise, keeps n intact. - */ - Node castToType(Node n, TypeNode tn); - - /** - * When a UF f is translated to a UF g, - * we add a define-fun command to the smt-engine - * to relate between f and g. - * We do the same when f and g are just variables. - * This is useful, for example, when asking - * for a model-value of a term that includes the - * original UF f. - * @param bvUF the original function or variable - * @param intUF the translated function or variable - */ - void defineBVUFAsIntUF(Node bvUF, Node intUF); - - /** - * @param bvUF is an uninterpreted function symbol from the original formula - * @return a fresh uninterpreted function symbol, obtained from bvUF - by replacing every argument of type BV to an argument of type Integer, - and the return type becomes integer in case it was BV. - */ - Node translateFunctionSymbol(Node bvUF); - - /** - * Performs the actual translation to integers for nodes - * that have children. - */ - Node translateWithChildren(Node original, - const std::vector& translated_children); - - /** - * Performs the actual translation to integers for nodes - * that don't have children (variables, constants, uninterpreted function - * symbols). - */ - Node translateNoChildren(Node original); - - /** - * Caches for the different functions - */ - CDNodeMap d_binarizeCache; - CDNodeMap d_eliminationCache; - CDNodeMap d_rebuildCache; - CDNodeMap d_bvToIntCache; - /** - * Node manager that is used throughout the pass - */ - NodeManager* d_nm; + // Add the lemmas in `additionalConstraints` to the assertions pipeline. + void addFinalizeAssertions(AssertionPipeline* assertionsToPreprocess, + const std::vector& additionalConstraints); - /** - * A set of constraints of the form 0 <= x < 2^k - * These are added for every new integer variable that we introduce. - */ - context::CDHashSet d_rangeAssertions; + // include the skolem map as substitutions + void addSkolemDefinitions(const std::map& skolems); - /** - * Useful constants - */ - Node d_zero; - Node d_one; - - /** helper class for handeling bvand translation */ - theory::arith::nl::IAndUtils d_iandUtils; + IntBlaster d_intBlaster; }; } // namespace passes diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index f5e7b427e..4c01f25f3 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -402,11 +402,11 @@ RewriteResponse ArithRewriter::postRewritePow2(TNode t) RewriteResponse ArithRewriter::postRewriteIAnd(TNode t) { Assert(t.getKind() == kind::IAND); + size_t bsize = t.getOperator().getConst().d_size; NodeManager* nm = NodeManager::currentNM(); // if constant, we eliminate if (t[0].isConst() && t[1].isConst()) { - size_t bsize = t.getOperator().getConst().d_size; Node iToBvop = nm->mkConst(IntToBitVector(bsize)); Node arg1 = nm->mkNode(kind::INT_TO_BITVECTOR, iToBvop, t[0]); Node arg2 = nm->mkNode(kind::INT_TO_BITVECTOR, iToBvop, t[1]); @@ -437,6 +437,11 @@ RewriteResponse ArithRewriter::postRewriteIAnd(TNode t) // ((_ iand k) 0 y) ---> 0 return RewriteResponse(REWRITE_DONE, t[i]); } + if (t[i].getConst().getNumerator() == Integer(2).pow(bsize) - 1) + { + // ((_ iand k) 111...1 y) ---> y + return RewriteResponse(REWRITE_DONE, t[i == 0 ? 1 : 0]); + } } return RewriteResponse(REWRITE_DONE, t); } diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index 90a9c5f78..92ecaf4e8 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -280,8 +280,8 @@ Node IAndSolver::bitwiseLemma(Node i) // compare each bit to bvI Node cond; Node bitIAnd; - unsigned high_bit; - for (unsigned j = 0; j < bvsize; j += granularity) + uint64_t high_bit; + for (uint64_t j = 0; j < bvsize; j += granularity) { high_bit = j + granularity - 1; // don't let high_bit pass bvsize diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp index 692fdc1b3..60bb0a9bc 100644 --- a/src/theory/bv/int_blaster.cpp +++ b/src/theory/bv/int_blaster.cpp @@ -48,8 +48,7 @@ Rational intpow2(uint64_t b) { return Rational(Integer(2).pow(b), Integer(1)); } IntBlaster::IntBlaster(Env& env, options::SolveBVAsIntMode mode, - uint64_t granularity, - bool introduceFreshIntVars) + uint64_t granularity) : EnvObj(env), d_binarizeCache(userContext()), d_intblastCache(userContext()), @@ -57,8 +56,7 @@ IntBlaster::IntBlaster(Env& env, d_bitwiseAssertions(userContext()), d_mode(mode), d_granularity(granularity), - d_context(userContext()), - d_introduceFreshIntVars(introduceFreshIntVars) + d_context(userContext()) { d_nm = NodeManager::currentNM(); d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0)); @@ -678,38 +676,18 @@ Node IntBlaster::translateNoChildren(Node original, } else { - // original is a bit-vector variable (symbolic constant). - // Either we translate it to a fresh integer variable, - // or we translate it to (bv2nat original). - // In the former case, we must include range lemmas, while in the - // latter we don't. - // This is determined by the option bv-to-int-fresh-vars. - // The variables intCast and bvCast are used for models: - // even if we introduce a fresh variable, - // it is associated with intCast (which is (bv2nat original)). - // bvCast is either ( (_ nat2bv k) original) or just original. Node intCast = castToType(original, d_nm->integerType()); Node bvCast; - if (d_introduceFreshIntVars) - { - // we introduce a fresh variable, add range constraints, and save the - // connection between original and the new variable via intCast - translation = d_nm->getSkolemManager()->mkPurifySkolem( - intCast, - "__intblast__var", - "Variable introduced in intblasting for " + original.toString()); - uint64_t bvsize = original.getType().getBitVectorSize(); - addRangeConstraint(translation, bvsize, lemmas); - // put new definition of old variable in skolems - bvCast = castToType(translation, original.getType()); - } - else - { - // we just translate original to (bv2nat original) - translation = intCast; - // no need to do any casting back to bit-vector in this case. - bvCast = original; - } + // we introduce a fresh variable, add range constraints, and save the + // connection between original and the new variable via intCast + translation = d_nm->getSkolemManager()->mkPurifySkolem( + intCast, + "__intblast__var", + "Variable introduced in intblasting for " + original.toString()); + uint64_t bvsize = original.getType().getBitVectorSize(); + addRangeConstraint(translation, bvsize, lemmas); + // put new definition of old variable in skolems + bvCast = castToType(translation, original.getType()); // add bvCast to skolems if it is not already there. if (skolems.find(original) == skolems.end()) diff --git a/src/theory/bv/int_blaster.h b/src/theory/bv/int_blaster.h index ed8ed10c6..fb7291f6e 100644 --- a/src/theory/bv/int_blaster.h +++ b/src/theory/bv/int_blaster.h @@ -101,14 +101,12 @@ class IntBlaster : protected EnvObj * @param context user context * @param mode bv-to-int translation mode * @param granularity bv-to-int translation granularity - * @param introduceFreshIntVars determines whether bit-vector variables are * translated to integer variables, or are directly casted using `bv2nat` * operator. not purely bit-vector nodes. */ IntBlaster(Env& env, options::SolveBVAsIntMode mode, - uint64_t granluarity = 1, - bool introduceFreshIntVars = true); + uint64_t granluarity = 1); ~IntBlaster(); @@ -371,11 +369,6 @@ class IntBlaster : protected EnvObj /** an SolverEngine for context */ context::Context* d_context; - /** true iff the translator should introduce - * fresh integer variables for bit-vector variables. - * Otherwise, we introduce a nat2bv term. - */ - bool d_introduceFreshIntVars; }; } // namespace cvc5 diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 496a625ee..a8ac27a81 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -29,84 +29,6 @@ namespace cvc5 { namespace theory { namespace bv { -/* - * This rewrite is not meant to be used by the BV rewriter. - * It is specifically designed for the bv-to-int preprocessing pass. - * Based on Hacker's Delight section 2-2 equation a: - * -x = ~x+1 - */ -template <> -inline bool RewriteRule::applies(TNode node) -{ - return (node.getKind() == kind::BITVECTOR_NEG); -} - -template <> -inline Node RewriteRule::apply(TNode node) -{ - Debug("bv-rewrite") << "RewriteRule(" << node << ")" - << std::endl; - NodeManager* nm = NodeManager::currentNM(); - TNode a = node[0]; - unsigned size = utils::getSize(a); - Node one = utils::mkOne(size); - Node nota = nm->mkNode(kind::BITVECTOR_NOT, a); - Node bvadd = nm->mkNode(kind::BITVECTOR_ADD, nota, one); - return bvadd; -} - -/* - * This rewrite is not meant to be used by the BV rewriter. - * It is specifically designed for the bv-to-int preprocessing pass. - * Based on Hacker's Delight section 2-2 equation h: - * x+y = x|y + x&y - */ -template <> -inline bool RewriteRule::applies(TNode node) -{ - return (node.getKind() == kind::BITVECTOR_OR); -} - -template <> -inline Node RewriteRule::apply(TNode node) -{ - Debug("bv-rewrite") << "RewriteRule(" << node << ")" - << std::endl; - NodeManager* nm = NodeManager::currentNM(); - TNode a = node[0]; - TNode b = node[1]; - Node bvadd = nm->mkNode(kind::BITVECTOR_ADD, a, b); - Node bvand = nm->mkNode(kind::BITVECTOR_AND, a, b); - Node result = - nm->mkNode(kind::BITVECTOR_SUB, bvadd, bvand); - return result; -} - -/* - * This rewrite is not meant to be used by the BV rewriter. - * It is specifically designed for the bv-to-int preprocessing pass. - * Based on Hacker's Delight section 2-2 equation n: - * x xor y = x|y - x&y - */ -template <> -inline bool RewriteRule::applies(TNode node) -{ - return (node.getKind() == kind::BITVECTOR_XOR); -} - -template <> -inline Node RewriteRule::apply(TNode node) -{ - Debug("bv-rewrite") << "RewriteRule(" << node << ")" - << std::endl; - NodeManager* nm = NodeManager::currentNM(); - TNode a = node[0]; - TNode b = node[1]; - Node bvor = nm->mkNode(kind::BITVECTOR_OR, a, b); - Node bvand = nm->mkNode(kind::BITVECTOR_AND, a, b); - Node result = nm->mkNode(kind::BITVECTOR_SUB, bvor, bvand); - return result; -} template <> inline bool RewriteRule::applies(TNode node) diff --git a/test/api/cpp/CMakeLists.txt b/test/api/cpp/CMakeLists.txt index eae57f3b9..929c5bef2 100644 --- a/test/api/cpp/CMakeLists.txt +++ b/test/api/cpp/CMakeLists.txt @@ -54,3 +54,5 @@ cvc5_add_api_test(issue4889) cvc5_add_api_test(issue6111) cvc5_add_api_test(proj-issue306) cvc5_add_api_test(proj-issue334) +cvc5_add_api_test(proj-issue344) +cvc5_add_api_test(proj-issue345) diff --git a/test/api/cpp/proj-issue344.cpp b/test/api/cpp/proj-issue344.cpp new file mode 100644 index 000000000..5f486706c --- /dev/null +++ b/test/api/cpp/proj-issue344.cpp @@ -0,0 +1,33 @@ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Test for project issue #345 + * + */ + + +#include "api/cpp/cvc5.h" +#include + +using namespace cvc5::api; + +int main(void) +{ + Solver slv; + slv.setOption("solve-bv-as-int", "iand"); + Sort s12 = slv.getIntegerSort(); + Term t13 = slv.mkConst(s12, "_x11"); + Term t25 = slv.mkTerm(slv.mkOp(Kind::INT_TO_BITVECTOR, 4124876294), {t13}); + Term t66 = slv.mkTerm(Kind::BITVECTOR_ULTBV, {t25, t25}); + Term t154 = slv.mkTerm(Kind::BITVECTOR_SGT, {t66, t66}); + slv.checkEntailed({t154, t154, t154, t154}); +} diff --git a/test/api/cpp/proj-issue345.cpp b/test/api/cpp/proj-issue345.cpp new file mode 100644 index 000000000..c33e9e5b8 --- /dev/null +++ b/test/api/cpp/proj-issue345.cpp @@ -0,0 +1,34 @@ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Test for project issue #345 + * + */ + + +#include "api/cpp/cvc5.h" +#include + +using namespace cvc5::api; + +int main(void) +{ + Solver slv; + slv.setOption("solve-bv-as-int", "iand"); + Sort s12 = slv.getIntegerSort(); + Term t13 = slv.mkConst(s12, "_x11"); + Term t25 = slv.mkTerm(slv.mkOp(Kind::INT_TO_BITVECTOR, 4124876294), {t13}); + Term t66 = slv.mkTerm(Kind::BITVECTOR_SLTBV, {t25, t25}); + Term t154 = slv.mkTerm(Kind::BITVECTOR_SGT, {t66, t66}); + slv.checkEntailed({t154, t154, t154, t154}); +} + diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6b8debc88..3be63c46d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -257,6 +257,7 @@ set(regress_0_tests regress0/bv/bv_to_int_bvuf_to_intuf.smt2 regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 regress0/bv/bv_to_int_elim_err.smt2 + regress0/bv/bv_to_int_int1.smt2 regress0/bv/bv_to_int_zext.smt2 regress0/bv/bvcomp.cvc.smt2 regress0/bv/bvmul-pow2-only.smt2 @@ -434,6 +435,7 @@ set(regress_0_tests regress0/bv/mult-pow2-negative.smt2 regress0/bv/pr4993-bvugt-bvurem-a.smt2 regress0/bv/pr4993-bvugt-bvurem-b.smt2 + regress0/bv/proj-issue343.smt2 regress0/bv/reset-assertions-assert-input.smt2 regress0/bv/sizecheck.cvc.smt2 regress0/bv/smtcompbug.smtv1.smt2 @@ -2627,6 +2629,7 @@ set(regress_2_tests regress2/bv_to_int_mask_array_2.smt2 regress2/bv_to_int_mask_array_3.smt2 regress2/bv_to_int_shifts.smt2 + regress2/bv_to_int_quantifiers_bvand.smt2 regress2/error1.smtv1.smt2 regress2/fp/issue7056.smt2 regress2/fuzz_2.smtv1.smt2 diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2 index 3908cdb16..eb8e75803 100644 --- a/test/regress/regress0/bv/bv_to_int1.smt2 +++ b/test/regress/regress0/bv/bv_to_int1.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: unsat (set-logic QF_BV) (declare-fun x () (_ BitVec 4)) diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 index 91e0c45fd..eced6e0e9 100644 --- a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun T4_180 () (_ BitVec 32)) diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 index 3e545ef03..45d539f04 100644 --- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: sat (set-logic QF_UFBV) (declare-fun a () (_ BitVec 4)) diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 index 0a0ec7b20..ae77380dd 100644 --- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: sat (set-logic QF_UFBV) (declare-sort S 0) diff --git a/test/regress/regress0/bv/bv_to_int_elim_err.smt2 b/test/regress/regress0/bv/bv_to_int_elim_err.smt2 index 01ee5dad8..cb7eefbb2 100644 --- a/test/regress/regress0/bv/bv_to_int_elim_err.smt2 +++ b/test/regress/regress0/bv/bv_to_int_elim_err.smt2 @@ -1,4 +1,5 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: sat (set-logic QF_BV) (declare-fun _substvar_183_ () (_ BitVec 32)) diff --git a/test/regress/regress0/bv/bv_to_int_int1.smt2 b/test/regress/regress0/bv/bv_to_int_int1.smt2 new file mode 100644 index 000000000..3295d3481 --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int_int1.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; EXPECT: sat +(set-logic QF_ALL) +(declare-fun x () (_ BitVec 4)) +(declare-fun y () (_ BitVec 4)) +(declare-fun z () Int) +(declare-fun w () Int) +(assert (= x (_ bv3 4))) +(assert (= y (_ bv3 4))) +(assert (> z w)) +(check-sat) diff --git a/test/regress/regress0/bv/bv_to_int_zext.smt2 b/test/regress/regress0/bv/bv_to_int_zext.smt2 index 8bf4a825d..4fd6109f4 100644 --- a/test/regress/regress0/bv/bv_to_int_zext.smt2 +++ b/test/regress/regress0/bv/bv_to_int_zext.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: unsat (set-logic QF_BV) (declare-fun T1_31078 () (_ BitVec 8)) diff --git a/test/regress/regress0/bv/proj-issue343.smt2 b/test/regress/regress0/bv/proj-issue343.smt2 new file mode 100644 index 000000000..6d2971ad8 --- /dev/null +++ b/test/regress/regress0/bv/proj-issue343.smt2 @@ -0,0 +1,7 @@ +; EXPECT: sat +; COMMAND-LINE: --no-check-models +(set-logic ALL) +(set-option :solve-bv-as-int bv) +(declare-const _x8 Real) +(assert (distinct real.pi _x8)) +(check-sat) diff --git a/test/regress/regress2/bv_to_int2.smt2 b/test/regress/regress2/bv_to_int2.smt2 index 424e95b27..b9c27c6b8 100644 --- a/test/regress/regress2/bv_to_int2.smt2 +++ b/test/regress/regress2/bv_to_int2.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: sat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2 index 0c6768546..1f5df2c31 100644 --- a/test/regress/regress2/bv_to_int_ashr.smt2 +++ b/test/regress/regress2/bv_to_int_ashr.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: unsat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress2/bv_to_int_bitwise.smt2 b/test/regress/regress2/bv_to_int_bitwise.smt2 index 23624e12c..4dc37a94c 100644 --- a/test/regress/regress2/bv_to_int_bitwise.smt2 +++ b/test/regress/regress2/bv_to_int_bitwise.smt2 @@ -1,8 +1,10 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 -; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value -; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum -; COMMAND-LINE: --solve-bv-as-int=bv +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=5 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun s () (_ BitVec 4)) diff --git a/test/regress/regress2/bv_to_int_bvmul1.smt2 b/test/regress/regress2/bv_to_int_bvmul1.smt2 index 232959f33..bf6f2cfc4 100644 --- a/test/regress/regress2/bv_to_int_bvmul1.smt2 +++ b/test/regress/regress2/bv_to_int_bvmul1.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: sat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2 b/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2 index babf9af32..2ecd0fe6c 100644 --- a/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2 +++ b/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2 @@ -1,4 +1,5 @@ -;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-unsat-cores +;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +;COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores ;EXPECT: unsat (set-logic QF_UFBV) (declare-fun z$n0s32 () (_ BitVec 32)) diff --git a/test/regress/regress2/bv_to_int_inc1.smt2 b/test/regress/regress2/bv_to_int_inc1.smt2 index 4b22c8ed8..28fb86f76 100644 --- a/test/regress/regress2/bv_to_int_inc1.smt2 +++ b/test/regress/regress2/bv_to_int_inc1.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --incremental --solve-bv-as-int=sum +; COMMAND-LINE: --incremental --solve-bv-as-int=bitwise ; COMMAND-LINE: --incremental --solve-bv-as-int=iand ; COMMAND-LINE: --incremental --solve-bv-as-int=bv ; EXPECT sat diff --git a/test/regress/regress2/bv_to_int_mask_array_1.smt2 b/test/regress/regress2/bv_to_int_mask_array_1.smt2 index 3b55c035d..c12138091 100644 --- a/test/regress/regress2/bv_to_int_mask_array_1.smt2 +++ b/test/regress/regress2/bv_to_int_mask_array_1.smt2 @@ -1,5 +1,6 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 -; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value --no-check-unsat-cores ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum --no-check-unsat-cores ; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores ; EXPECT: unsat diff --git a/test/regress/regress2/bv_to_int_mask_array_2.smt2 b/test/regress/regress2/bv_to_int_mask_array_2.smt2 index edcc14149..17a113f85 100644 --- a/test/regress/regress2/bv_to_int_mask_array_2.smt2 +++ b/test/regress/regress2/bv_to_int_mask_array_2.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum ; COMMAND-LINE: --solve-bv-as-int=bv diff --git a/test/regress/regress2/bv_to_int_mask_array_3.smt2 b/test/regress/regress2/bv_to_int_mask_array_3.smt2 index 74e5ca95a..2b411209d 100644 --- a/test/regress/regress2/bv_to_int_mask_array_3.smt2 +++ b/test/regress/regress2/bv_to_int_mask_array_3.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: sat (set-logic ALL) (declare-fun A () (Array (_ BitVec 4) (_ BitVec 4))) diff --git a/test/regress/regress2/bv_to_int_quantifiers_bvand.smt2 b/test/regress/regress2/bv_to_int_quantifiers_bvand.smt2 new file mode 100644 index 000000000..d454ad630 --- /dev/null +++ b/test/regress/regress2/bv_to_int_quantifiers_bvand.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores +; EXPECT: (error "Error in option parsing: --solve-bv-as-int=bitwise does not support quantifiers") +; EXIT: 1 +(set-logic BV) +(declare-const x (_ BitVec 8)) +(assert (forall ((y (_ BitVec 8))) + (distinct #b00000000 + (bvand x y)))) +(check-sat) diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2 index bcc31c38c..173f1a552 100644 --- a/test/regress/regress2/bv_to_int_shifts.smt2 +++ b/test/regress/regress2/bv_to_int_shifts.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: sat (set-logic QF_BV) (declare-fun s () (_ BitVec 4)) diff --git a/test/regress/regress3/bv_to_int_and_or.smt2 b/test/regress/regress3/bv_to_int_and_or.smt2 index 2c728417d..8ae10a04f 100644 --- a/test/regress/regress3/bv_to_int_and_or.smt2 +++ b/test/regress/regress3/bv_to_int_and_or.smt2 @@ -1,5 +1,7 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=2 --no-check-unsat-cores --no-check-proofs ; EXPECT: unsat (set-logic QF_BV) (declare-fun a () (_ BitVec 4)) diff --git a/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2 index aeacda35e..3a0320119 100644 --- a/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2 +++ b/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2 @@ -1,5 +1,6 @@ -; COMMAND-LINE: --solve-bv-as-int=bv -; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=sum +; COMMAND-LINE: --solve-bv-as-int=bv +; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=sum +; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=bitwise ; EXPECT: sat (set-logic QF_BV) (declare-fun _substvar_1171_ () (_ BitVec 32)) diff --git a/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 index c4988e3c6..3c50acc1c 100644 --- a/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 +++ b/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --solve-bv-as-int=bv -; COMMAND-LINE: --solve-bv-as-int=sum -; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum +; COMMAND-LINE: --solve-bv-as-int=bv +; COMMAND-LINE: --solve-bv-as-int=sum +; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=bitwise ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value ; EXPECT: unsat diff --git a/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2 index dd7e11a50..b37dc371d 100644 --- a/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2 +++ b/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=bv --no-check-models -; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=sum --full-saturate-quant --cegqi-all --no-check-models +; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=sum --full-saturate-quant --cegqi-all --no-check-models ;EXPECT: sat (set-logic BV) (assert (exists ((c__detect__main__1__i_36_C (_ BitVec 32))) (bvslt ((_ sign_extend 32) c__detect__main__1__i_36_C) (_ bv0 64)))) diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp index 0412fdabb..e8238ecbb 100644 --- a/test/unit/theory/theory_bv_int_blaster_white.cpp +++ b/test/unit/theory/theory_bv_int_blaster_white.cpp @@ -61,7 +61,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_constants) Env env(d_nodeManager, &opts); env.d_logic.setLogicString("QF_UFBV"); env.d_logic.lock(); - IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1, false); + IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1); Node result = intBlaster.translateNoChildren(bv7_4, lemmas, skolems); Node seven = d_nodeManager->mkConst(CONST_RATIONAL, Rational(7)); ASSERT_EQ(seven, result); @@ -86,7 +86,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_symbolic_constant) Env env(d_nodeManager, &opts); env.d_logic.setLogicString("QF_UFBV"); env.d_logic.lock(); - IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1, true); + IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1); Node result = intBlaster.translateNoChildren(bv, lemmas, skolems); ASSERT_TRUE(result.isVar() && result.getType().isInteger()); @@ -116,7 +116,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_uf) Env env(d_nodeManager, &opts); env.d_logic.setLogicString("QF_UFBV"); env.d_logic.lock(); - IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1, true); + IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1); Node result = intBlaster.translateNoChildren(f, lemmas, skolems); TypeNode resultType = result.getType(); std::vector resultDomain = resultType.getArgTypes(); @@ -143,7 +143,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_with_children) Env env(d_nodeManager, &opts); env.d_logic.setLogicString("QF_UFBV"); env.d_logic.lock(); - IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1, true); + IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1); // bit-vector variables TypeNode bvType = d_nodeManager->mkBitVectorType(4); @@ -294,7 +294,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_bitwise) Env env(d_nodeManager, &opts); env.d_logic.setLogicString("QF_UFBV"); env.d_logic.lock(); - IntBlaster intBlaster(env, options::SolveBVAsIntMode::BITWISE, 1, true); + IntBlaster intBlaster(env, options::SolveBVAsIntMode::BITWISE, 1); // bit-vector variables TypeNode bvType = d_nodeManager->mkBitVectorType(4); -- 2.30.2