From: yoni206 Date: Thu, 10 Sep 2020 17:23:30 +0000 (-0700) Subject: bv2int: refactoring the main translation loop (#5051) X-Git-Tag: cvc5-1.0.0~2877 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a8939854b88a4d9ead58ef7191897f0e5f68cefb;p=cvc5.git bv2int: refactoring the main translation loop (#5051) This PR introduces a refactoring of the main translation loop in bv2int preprocessing pass. Many parts are wrapped by helper functions and so the main loop becomes smaller. remark: selecting "Hide whitespace changes" cuts the diff by ~50%. --- diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index e91e375c9..c219deefe 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -261,8 +261,6 @@ Node BVToInt::bvToInt(Node n) n = makeBinary(n); vector toVisit; toVisit.push_back(n); - uint64_t granularity = options::BVAndIntegerGranularity(); - Assert(0 <= granularity && granularity <= 8); while (!toVisit.empty()) { @@ -271,12 +269,22 @@ Node BVToInt::bvToInt(Node n) 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 this node + // We already visited and translated this node if (!d_bvToIntCache[current].get().isNull()) { // We are done computing the translation for current @@ -288,45 +296,8 @@ Node BVToInt::bvToInt(Node n) // 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 - { - // variables other than bit-vector variables are left intact - 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; - } - } + Node translation = translateNoChildren(current); + d_bvToIntCache[current] = translation; } else { @@ -334,485 +305,499 @@ Node BVToInt::bvToInt(Node n) * 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. + * 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; - for (uint64_t i = 0; i < currentNumChildren; i++) + if (current.getKind() == kind::APPLY_UF) { - translated_children.push_back(d_bvToIntCache[current[i]]); + translated_children.push_back( + d_bvToIntCache[current.getOperator()]); } - // 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) + for (uint64_t i = 0; i < currentNumChildren; i++) { - 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)); - if (translated_children[0].isConst() - || translated_children[1].isConst()) - { - /* - * based on equation (23), section 3.2.3 of: - * Bozzano et al. - * Encoding RTL Constructs for MathSAT: a Preliminary Report. - */ - // this is an optimization when one of the children is constant - Node c = translated_children[0].isConst() - ? translated_children[0] - : translated_children[1]; - d_rangeAssertions.insert( - d_nm->mkNode(kind::LEQ, d_zero, sigma)); - // the value of sigma is bounded by (c - 1) - // where c is the constant multiplicand - d_rangeAssertions.insert(d_nm->mkNode(kind::LT, sigma, c)); - } - else - { - 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_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_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_ZERO_EXTEND: - { - d_bvToIntCache[current] = translated_children[0]; - break; - } - case kind::BITVECTOR_SIGN_EXTEND: - { - uint64_t bvsize = current[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(current); - /* 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) - { - d_bvToIntCache[current] = 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; - Node result = d_nm->mkConst(sum); - d_bvToIntCache[current] = result; - } - } - else - { - uint64_t amount = bv::utils::getSignExtendAmount(current); - if (amount == 0) - { - d_bvToIntCache[current] = translated_children[0]; - } - else - { - Rational twoToKMinusOne(intpow2(bvsize - 1)); - Node minSigned = d_nm->mkConst(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); - 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].get(), 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 - */ - - // construct the new function symbol. - 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 - { - // 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); - } - 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; - - // introduce a `define-fun` in the smt-engine to keep - // the correspondence between the original - // function symbol and the new one. - defineBVUFAsIntUF(bvUF); - } - /** - * higher order logic allows comparing between functions - * The current translation does not support this, - * as the translated functions may be different outside - * of the bounds that were relevant for the original - * bit-vectors. - */ - if (childrenTypesChanged(current) && options::ufHo()) - { - throw TypeCheckingException( - current.toExpr(), - string("Cannot translate to Int: ") + current.toString()); - } - - // Now that the translated function symbol was - // created, we translate the applicatio and add to the cache. - // Additionally, we add - // range constraints induced by the original BV width of the - // the functions range (codomain).. - translated_children.insert(translated_children.begin(), intUF); - // Insert the translated application term to the cache - d_bvToIntCache[current] = - d_nm->mkNode(kind::APPLY_UF, translated_children); - // Add range constraints if necessary. - // If the original range was a BV sort, the current application of - // the function Must be within the range determined by the - // bitwidth. - if (bvRange.isBitVector()) - { - Node m = d_bvToIntCache[current]; - d_rangeAssertions.insert( - mkRangeConstraint(d_bvToIntCache[current], - current.getType().getBitVectorSize())); - } - break; - } - default: - { - // 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 (current.getType().isBitVector()) - { - resultingType = d_nm->integerType(); - } - else - { - resultingType = current.getType(); - } - Node reconstruction = - reconstructNode(current, resultingType, translated_children); - d_bvToIntCache[current] = reconstruction; - break; - } + translated_children.push_back(d_bvToIntCache[current[i]]); } + Node translation = + translateWithChildren(current, translated_children); + d_bvToIntCache[current] = translation; } toVisit.pop_back(); } } } - return d_bvToIntCache[n]; + return d_bvToIntCache[n].get(); } -void BVToInt::defineBVUFAsIntUF(Node bvUF) +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); + Node returnNode; + switch (oldKind) + { + case kind::BITVECTOR_PLUS: + { + uint64_t bvsize = original[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)); + returnNode = 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(returnNode, bvsize)); + break; + } + case kind::BITVECTOR_MULT: + { + uint64_t bvsize = original[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)); + returnNode = d_nm->mkNode(kind::MINUS, mult, multSig); + d_rangeAssertions.insert( + mkRangeConstraint(returnNode, bvsize)); + if (translated_children[0].isConst() || translated_children[1].isConst()) + { + /* + * based on equation (23), section 3.2.3 of: + * Bozzano et al. + * Encoding RTL Constructs for MathSAT: a Preliminary Report. + */ + // this is an optimization when one of the children is constant + Node c = translated_children[0].isConst() ? translated_children[0] + : translated_children[1]; + d_rangeAssertions.insert(d_nm->mkNode(kind::LEQ, d_zero, sigma)); + // the value of sigma is bounded by (c - 1) + // where c is the constant multiplicand + d_rangeAssertions.insert(d_nm->mkNode(kind::LT, sigma, c)); + } + else + { + d_rangeAssertions.insert(mkRangeConstraint(sigma, bvsize)); + } + break; + } + case kind::BITVECTOR_UDIV_TOTAL: + { + 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_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); + 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::BITVECTOR_AND: + { + // Construct an ite, based on granularity. + uint64_t bvsize = original[0].getType().getBitVectorSize(); + Assert(translated_children.size() == 2); + Node newNode = createBitwiseNode(translated_children[0], + translated_children[1], + bvsize, + options::BVAndIntegerGranularity(), + &oneBitAnd); + returnNode = 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 = 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(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(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 current translation does not support this, + * as the translated functions may be different outside + * of the bounds that were relevant for the original + * bit-vectors. + */ + if (childrenTypesChanged(original) && options::ufHo()) + { + throw TypeCheckingException( + original.toExpr(), + 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; + } + default: + { + // 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) +{ + Node translation; + Assert(original.isVar() || original.isConst()); + if (original.isVar()) + { + if (original.getType().isBitVector()) + { + Node newVar = d_nm->mkSkolem("__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)); + std::vector args; + Node intToBVOp = d_nm->mkConst(IntToBitVector(bvsize)); + Node newNode = d_nm->mkNode(intToBVOp, newVar); + smt::currentSmtEngine()->defineFunction( + original.toExpr(), args, newNode.toExpr(), true); + } + 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(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); + } + ostringstream os; + os << "__bvToInt_fun_" << bvUF << "_int"; + intUF = d_nm->mkSkolem( + 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) { // This function should only be called after translating // the function symbol to a new function symbol // with the right domain and range. - Assert(d_bvToIntCache.find(bvUF) != d_bvToIntCache.end()); // get domain and range of the original function TypeNode tn = bvUF.getType(); vector bvDomain = tn.getArgTypes(); TypeNode bvRange = tn.getRangeType(); - // get the translated function symbol - Node intUF = d_bvToIntCache[bvUF]; - - // create a symbolic application to be used in define-fun - // symbolic arguments of original function vector args; // children of the new symbolic application @@ -1042,7 +1027,7 @@ Node BVToInt::createBitwiseNode(Node x, * 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); + Assert(0 < granularity && granularity <= 8); if (granularity > bvsize) { granularity = bvsize; diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h index bec8a9a21..db2d08b7d 100644 --- a/src/preprocessing/passes/bv_to_int.h +++ b/src/preprocessing/passes/bv_to_int.h @@ -292,8 +292,33 @@ class BVToInt : public PreprocessingPass * 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 + * @param intUF the translated function */ - void defineBVUFAsIntUF(Node bvUF); + 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 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 */