n = makeBinary(n);
vector<Node> toVisit;
toVisit.push_back(n);
- uint64_t granularity = options::BVAndIntegerGranularity();
- Assert(0 <= granularity && granularity <= 8);
while (!toVisit.empty())
{
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
// 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<BitVector>());
- Integer c = constant.toInteger();
- d_bvToIntCache[current] = d_nm->mkConst<Rational>(c);
- }
- else
- {
- // Other constants stay the same.
- d_bvToIntCache[current] = current;
- }
- }
+ Node translation = translateNoChildren(current);
+ d_bvToIntCache[current] = translation;
}
else
{
* The current node has children.
* Since we are on the way back up,
* these children were already translated.
- * We save their translation for future use.
+ * 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<Node> 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<Node> 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>());
- 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<TypeNode> bvDomain = tn.getArgTypes();
- vector<TypeNode> 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<Node>& 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<Node> 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>());
+ 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<Expr> args;
+ Node intToBVOp = d_nm->mkConst<IntToBitVector>(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<BitVector>());
+ Integer c = constant.toInteger();
+ translation = d_nm->mkConst<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<TypeNode> bvDomain = tn.getArgTypes();
+ vector<TypeNode> 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<TypeNode> 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<Expr> args;
// children of the new symbolic application
* 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;
projects / cvc5.git / commitdiff