#include "expr/skolem_manager.h"
#include "options/option_exception.h"
#include "options/uf_options.h"
+#include "theory/bv/theory_bv_utils.h"
#include "theory/rewriter.h"
#include "util/bitvector.h"
#include "util/iand.h"
namespace cvc5 {
using namespace cvc5::theory;
+namespace {
+
+// A helper function to compute 2^b as a Rational
+Rational intpow2(uint64_t b) { return Rational(Integer(2).pow(b), Integer(1)); }
+
+} // namespace
+
IntBlaster::IntBlaster(context::Context* c,
options::SolveBVAsIntMode mode,
uint64_t granularity,
Node IntBlaster::mkRangeConstraint(Node newVar, uint64_t k) { return Node(); }
-Node IntBlaster::maxInt(uint64_t k) { return Node(); }
+Node IntBlaster::maxInt(uint64_t k)
+{
+ Assert(k > 0);
+ Rational max_value = intpow2(k) - 1;
+ return d_nm->mkConst<Rational>(max_value);
+}
-Node IntBlaster::pow2(uint64_t k) { return Node(); }
+Node IntBlaster::pow2(uint64_t k)
+{
+ Assert(k >= 0);
+ return d_nm->mkConst<Rational>(intpow2(k));
+}
-Node IntBlaster::modpow2(Node n, uint64_t exponent) { return Node(); }
+Node IntBlaster::modpow2(Node n, uint64_t exponent)
+{
+ Node p2 = d_nm->mkConst<Rational>(intpow2(exponent));
+ return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, n, p2);
+}
Node IntBlaster::makeBinary(Node n)
{
const std::vector<Node>& translated_children,
std::vector<Node>& lemmas)
{
- Node binarized = makeBinary(original);
- // continue to process the binarized version
+ // The translation of the original node is determined by the kind of
+ // the node.
+ kind::Kind_t oldKind = original.getKind();
+
+ // Some BV operators were eliminated before this point.
+ Assert(oldKind != kind::BITVECTOR_SDIV);
+ Assert(oldKind != kind::BITVECTOR_SREM);
+ Assert(oldKind != kind::BITVECTOR_SMOD);
+ Assert(oldKind != kind::BITVECTOR_XNOR);
+ Assert(oldKind != kind::BITVECTOR_NAND);
+ Assert(oldKind != kind::BITVECTOR_SUB);
+ Assert(oldKind != kind::BITVECTOR_REPEAT);
+ Assert(oldKind != kind::BITVECTOR_ROTATE_RIGHT);
+ Assert(oldKind != kind::BITVECTOR_ROTATE_LEFT);
+ Assert(oldKind != kind::BITVECTOR_COMP);
+ Assert(oldKind != kind::BITVECTOR_SGT);
+ Assert(oldKind != kind::BITVECTOR_SLE);
+ Assert(oldKind != kind::BITVECTOR_SGE);
+ Assert(oldKind != kind::EXISTS);
+
+ // BV division by zero was eliminated before this point.
+ Assert(oldKind != kind::BITVECTOR_UDIV
+ || !(original[1].isConst()
+ && original[1].getConst<BitVector>().getValue().isZero()));
+
+ // Store the translated node
+ Node returnNode;
+
+ // Translate according to the kind of the original node.
+ switch (oldKind)
+ {
+ case kind::BITVECTOR_ADD:
+ {
+ Assert(original.getNumChildren() == 2);
+ uint64_t bvsize = original[0].getType().getBitVectorSize();
+ returnNode = createBVAddNode(
+ translated_children[0], translated_children[1], bvsize);
+ break;
+ }
+ case kind::BITVECTOR_MULT:
+ {
+ Assert(original.getNumChildren() == 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:
+ {
+ // we use an ITE for the case where the second operand is 0.
+ uint64_t bvsize = original[0].getType().getBitVectorSize();
+ 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();
+ returnNode = createBVNotNode(translated_children[0], bvsize);
+ break;
+ }
+ case kind::BITVECTOR_NEG:
+ {
+ uint64_t bvsize = original[0].getType().getBitVectorSize();
+ returnNode = createBVNegNode(translated_children[0], bvsize);
+ break;
+ }
+ case kind::BITVECTOR_TO_NAT:
+ {
+ // In this case, we already translated the child to integer.
+ // The result is simply the translated child.
+ returnNode = translated_children[0];
+ break;
+ }
+ case kind::INT_TO_BITVECTOR:
+ {
+ // In this case we take the original integer,
+ // modulo 2 to the power of the bit-width
+ returnNode =
+ modpow2(translated_children[0],
+ original.getOperator().getConst<IntToBitVector>().d_size);
+ break;
+ }
+ case kind::BITVECTOR_OR:
+ {
+ Assert(translated_children.size() == 2);
+ uint64_t bvsize = original[0].getType().getBitVectorSize();
+ returnNode = createBVOrNode(
+ translated_children[0], translated_children[1], bvsize, lemmas);
+ break;
+ }
+ case kind::BITVECTOR_XOR:
+ {
+ Assert(translated_children.size() == 2);
+ uint64_t bvsize = original[0].getType().getBitVectorSize();
+ // Based on Hacker's Delight section 2-2 equation n:
+ // x xor y = x|y - x&y
+ Node bvor = createBVOrNode(
+ translated_children[0], translated_children[1], bvsize, lemmas);
+ Node bvand = createBVAndNode(
+ translated_children[0], translated_children[1], bvsize, lemmas);
+ returnNode = createBVSubNode(bvor, bvand, bvsize);
+ break;
+ }
+ case kind::BITVECTOR_AND:
+ {
+ Assert(translated_children.size() == 2);
+ uint64_t bvsize = original[0].getType().getBitVectorSize();
+ returnNode = createBVAndNode(
+ translated_children[0], translated_children[1], bvsize, lemmas);
+ break;
+ }
+ case kind::BITVECTOR_SHL:
+ {
+ uint64_t bvsize = original[0].getType().getBitVectorSize();
+ returnNode = createShiftNode(translated_children, bvsize, true);
+ break;
+ }
+ case kind::BITVECTOR_LSHR:
+ {
+ 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)))
+ *
+ */
+ // signed_min is 100000...
+ uint64_t bvsize = original[0].getType().getBitVectorSize();
+ 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);
+ std::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:
+ {
+ // zero extension does not change the integer translation.
+ returnNode = translated_children[0];
+ break;
+ }
+ case kind::BITVECTOR_SIGN_EXTEND:
+ {
+ uint64_t bvsize = original[0].getType().getBitVectorSize();
+ returnNode =
+ createSignExtendNode(translated_children[0],
+ bvsize,
+ bv::utils::getSignExtendAmount(original));
+ 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_SLT:
+ {
+ uint64_t bvsize = original[0].getType().getBitVectorSize();
+ returnNode = d_nm->mkNode(kind::LT,
+ uts(translated_children[0], bvsize),
+ uts(translated_children[1], bvsize));
+ 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::BITVECTOR_ULTBV:
+ {
+ returnNode = d_nm->mkNode(kind::ITE,
+ d_nm->mkNode(kind::LT, translated_children),
+ d_one,
+ d_zero);
+ break;
+ }
+ case kind::BITVECTOR_SLTBV:
+ {
+ uint64_t bvsize = original[0].getType().getBitVectorSize();
+ returnNode =
+ d_nm->mkNode(kind::ITE,
+ d_nm->mkNode(kind::LT,
+ uts(translated_children[0], bvsize),
+ uts(translated_children[1], bvsize)),
+ d_one,
+ d_zero);
+ 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) && options::ufHo())
+ {
+ throw OptionException("bv-to-int does not support higher order logic ");
+ }
+ // 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())
+ {
+ addRangeConstraint(
+ returnNode, original.getType().getBitVectorSize(), lemmas);
+ }
+ break;
+ }
+ case kind::BOUND_VAR_LIST:
+ {
+ returnNode = d_nm->mkNode(oldKind, translated_children);
+ break;
+ }
+ case kind::FORALL:
+ {
+ returnNode = translateQuantifiedFormula(original);
+ break;
+ }
+ default:
+ {
+ // first, verify that we haven't missed
+ // any bv operator
+ Assert(theory::kindToTheoryId(oldKind) != THEORY_BV);
+
+ // 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("int-blaster-debug") << "original: " << original << std::endl;
+ Trace("int-blaster-debug") << "returnNode: " << returnNode << std::endl;
+ return returnNode;
+}
+
+Node IntBlaster::createSignExtendNode(Node x, uint64_t bvsize, uint64_t amount)
+{
return Node();
}
return Node();
}
+Node IntBlaster::createBVAndNode(Node x,
+ Node y,
+ uint64_t bvsize,
+ std::vector<Node>& lemmas)
+{
+ return Node();
+}
+
+Node IntBlaster::createBVOrNode(Node x,
+ Node y,
+ uint64_t bvsize,
+ std::vector<Node>& lemmas)
+{
+ // Based on Hacker's Delight section 2-2 equation h:
+ // x+y = x|y + x&y
+ // from which we deduce:
+ // x|y = x+y - x&y
+ Node plus = createBVAddNode(x, y, bvsize);
+ Node bvand = createBVAndNode(x, y, bvsize, lemmas);
+ return createBVSubNode(plus, bvand, bvsize);
+}
+
+Node IntBlaster::createBVSubNode(Node x, Node y, uint64_t bvsize)
+{
+ Node minus = d_nm->mkNode(kind::MINUS, x, y);
+ Node p2 = pow2(bvsize);
+ return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, minus, p2);
+}
+
+Node IntBlaster::createBVAddNode(Node x, Node y, uint64_t bvsize)
+{
+ Node plus = d_nm->mkNode(kind::PLUS, x, y);
+ Node p2 = pow2(bvsize);
+ return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, plus, p2);
+}
+
+Node IntBlaster::createBVNegNode(Node n, uint64_t bvsize)
+{
+ // Based on Hacker's Delight section 2-2 equation a:
+ // -x = ~x+1
+ Node p2 = pow2(bvsize);
+ return d_nm->mkNode(kind::MINUS, p2, n);
+}
+
+Node IntBlaster::createBVNotNode(Node n, uint64_t bvsize)
+{
+ return d_nm->mkNode(kind::MINUS, maxInt(bvsize), n);
+}
+
} // namespace cvc5
#include "options/options.h"
#include "test_smt.h"
#include "theory/bv/int_blaster.h"
+#include "theory/bv/theory_bv_utils.h"
#include "util/bitvector.h"
#include "util/rational.h"
namespace cvc5 {
Node d_one;
};
-TEST_F(TestTheoryWhiteBvIntblaster, bitblaster_constants)
+TEST_F(TestTheoryWhiteBvIntblaster, intblaster_constants)
{
// place holders for lemmas and skolem
std::vector<Node> lemmas;
ASSERT_EQ(seven, result);
}
-TEST_F(TestTheoryWhiteBvIntblaster, bitblaster_symbolic_constant)
+TEST_F(TestTheoryWhiteBvIntblaster, intblaster_symbolic_constant)
{
// place holders for lemmas and skolem
std::vector<Node> lemmas;
ASSERT_EQ(resultSquared, result);
}
-TEST_F(TestTheoryWhiteBvIntblaster, bitblaster_uf)
+TEST_F(TestTheoryWhiteBvIntblaster, intblaster_uf)
{
// place holders for lemmas and skolem
std::vector<Node> lemmas;
ASSERT_TRUE(resultRange.isBoolean());
}
+/** Check all cases of the translation.
+ * This is a sanity check, that noly verifies
+ * the expected type, and that there were no
+ * failures.
+ */
+TEST_F(TestTheoryWhiteBvIntblaster, intblaster_with_children)
+{
+ // place holders for lemmas and skolem
+ std::vector<Node> lemmas;
+ std::map<Node, Node> skolems;
+ IntBlaster intBlaster(
+ d_smtEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true);
+
+ // bit-vector variables
+ TypeNode bvType = d_nodeManager->mkBitVectorType(4);
+ Node v1 = d_nodeManager->mkVar("v1", bvType);
+ Node v2 = d_nodeManager->mkVar("v2", bvType);
+
+ // translated integer variables
+ Node i1 = intBlaster.translateNoChildren(v1, lemmas, skolems);
+ Node i2 = intBlaster.translateNoChildren(v2, lemmas, skolems);
+
+ // if original is BV, result should be Int.
+ // Otherwise, they should have the same type.
+ Node original;
+ Node result;
+
+ // sum
+ original = d_nodeManager->mkNode(BITVECTOR_ADD, v1, v2);
+ result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+ ASSERT_TRUE(result.getType().isInteger());
+
+ // multiplication
+ original = d_nodeManager->mkNode(BITVECTOR_MULT, v1, v2);
+ result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+ ASSERT_TRUE(result.getType().isInteger());
+
+ // division 1
+ original = d_nodeManager->mkNode(BITVECTOR_UDIV, v1, v2);
+ result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+ ASSERT_TRUE(result.getType().isInteger());
+
+ // division 2
+ original = d_nodeManager->mkNode(BITVECTOR_UREM, v1, v2);
+ result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+ ASSERT_TRUE(result.getType().isInteger());
+
+ // bit-wise negation
+ original = d_nodeManager->mkNode(BITVECTOR_NOT, v1);
+ result = intBlaster.translateWithChildren(original, {i1}, lemmas);
+ ASSERT_TRUE(result.getType().isInteger());
+
+ // arithmetic negation
+ original = d_nodeManager->mkNode(BITVECTOR_NEG, v1);
+ result = intBlaster.translateWithChildren(original, {i1}, lemmas);
+ ASSERT_TRUE(result.getType().isInteger());
+
+ // bv2nat
+ original = d_nodeManager->mkNode(BITVECTOR_TO_NAT, v1);
+ result = intBlaster.translateWithChildren(original, {i1}, lemmas);
+ ASSERT_TRUE(result.getType().isInteger());
+
+ // int2bv
+ Node intToBVOp = d_nodeManager->mkConst<IntToBitVector>(IntToBitVector(4));
+ original = d_nodeManager->mkNode(intToBVOp, i1);
+ result = intBlaster.translateWithChildren(original, {i1}, lemmas);
+ ASSERT_TRUE(result.getType().isInteger());
+
+ // zero extend
+ Node zeroExtOp =
+ d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(4));
+ original = d_nodeManager->mkNode(zeroExtOp, v1);
+ result = intBlaster.translateWithChildren(original, {i1}, lemmas);
+ ASSERT_TRUE(result.getType().isInteger());
+
+ // extract + BV ITE
+ Node extract = theory::bv::utils::mkExtract(v1, 0, 0);
+ original = d_nodeManager->mkNode(BITVECTOR_ITE, extract, v2, v1);
+ Node intExtract = intBlaster.translateWithChildren(extract, {i1}, lemmas);
+ result =
+ intBlaster.translateWithChildren(original, {intExtract, i1, i2}, lemmas);
+ ASSERT_TRUE(result.getType().isInteger());
+ ASSERT_TRUE(intExtract.getType().isInteger());
+
+ // concat
+ original = d_nodeManager->mkNode(BITVECTOR_CONCAT, v1, v2);
+ result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+ ASSERT_TRUE(result.getType().isInteger());
+
+ // predicates
+ original = d_nodeManager->mkNode(EQUAL, v1, v2);
+ result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+ ASSERT_TRUE(result.getType().isBoolean());
+
+ original = d_nodeManager->mkNode(BITVECTOR_ULT, v1, v2);
+ result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+ ASSERT_TRUE(result.getType().isBoolean());
+
+ original = d_nodeManager->mkNode(BITVECTOR_ULE, v1, v2);
+ result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+ ASSERT_TRUE(result.getType().isBoolean());
+
+ original = d_nodeManager->mkNode(BITVECTOR_UGT, v1, v2);
+ result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+ ASSERT_TRUE(result.getType().isBoolean());
+
+ original = d_nodeManager->mkNode(BITVECTOR_UGE, v1, v2);
+ result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+ ASSERT_TRUE(result.getType().isBoolean());
+
+ // BVULT with a BV result
+ original = d_nodeManager->mkNode(BITVECTOR_ULTBV, v1, v2);
+ result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+ ASSERT_TRUE(result.getType().isInteger());
+
+ // function application
+ TypeNode funType = d_nodeManager->mkFunctionType({bvType}, bvType);
+ Node f = d_nodeManager->mkVar("f", funType);
+ Node g = intBlaster.translateNoChildren(f, lemmas, skolems);
+ original = d_nodeManager->mkNode(APPLY_UF, f, v1);
+ result = intBlaster.translateWithChildren(original, {g, i1}, lemmas);
+ ASSERT_TRUE(result.getType().isInteger());
+}
+
} // namespace test
} // namespace cvc5
projects / cvc5.git / commitdiff