From: yoni206 Date: Sat, 20 Nov 2021 00:05:03 +0000 (+0200) Subject: bv2int module: translation of more cases (#7653) X-Git-Tag: cvc5-1.0.0~792 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b984eae6a8608993b8ec13fa8b56ca1d67332e9a;p=cvc5.git bv2int module: translation of more cases (#7653) This commit adds the implementation of the translation from BV to Int for the remaining operators. Some cases are left for the next PR. Corresponding unit tests are added. Notice that in the new module, the following issues do not occur. They will be added as tests in the following PRs: https://github.com/cvc5/cvc5-projects/issues/345 https://github.com/cvc5/cvc5-projects/issues/344 https://github.com/cvc5/cvc5-projects/issues/343 --- diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp index eff5ec611..649be5aab 100644 --- a/src/theory/bv/int_blaster.cpp +++ b/src/theory/bv/int_blaster.cpp @@ -28,12 +28,14 @@ #include "options/uf_options.h" #include "theory/bv/theory_bv_utils.h" #include "theory/logic_info.h" +#include "theory/rewriter.h" #include "util/bitvector.h" #include "util/iand.h" #include "util/rational.h" using namespace cvc5::kind; using namespace cvc5::theory; +using namespace cvc5::theory::bv; namespace cvc5 { @@ -59,8 +61,8 @@ IntBlaster::IntBlaster(Env& env, d_introduceFreshIntVars(introduceFreshIntVars) { d_nm = NodeManager::currentNM(); - d_zero = d_nm->mkConst(CONST_RATIONAL, 0); - d_one = d_nm->mkConst(CONST_RATIONAL, 1); + d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0)); + d_one = d_nm->mkConst(CONST_RATIONAL, Rational(1)); }; IntBlaster::~IntBlaster() {} @@ -69,31 +71,55 @@ void IntBlaster::addRangeConstraint(Node node, uint64_t size, std::vector& lemmas) { + Node rangeConstraint = mkRangeConstraint(node, size); + Trace("int-blaster-debug") + << "range constraint computed: " << rangeConstraint << std::endl; + if (d_rangeAssertions.find(rangeConstraint) == d_rangeAssertions.end()) + { + Trace("int-blaster-debug") + << "range constraint added to cache and lemmas " << std::endl; + d_rangeAssertions.insert(rangeConstraint); + lemmas.push_back(rangeConstraint); + } } void IntBlaster::addBitwiseConstraint(Node bitwiseConstraint, std::vector& lemmas) { + if (d_bitwiseAssertions.find(bitwiseConstraint) == d_bitwiseAssertions.end()) + { + Trace("int-blaster-debug") + << "bitwise constraint added to cache and lemmas: " << bitwiseConstraint + << std::endl; + d_bitwiseAssertions.insert(bitwiseConstraint); + lemmas.push_back(bitwiseConstraint); + } } -Node IntBlaster::mkRangeConstraint(Node newVar, uint64_t k) { return Node(); } +Node IntBlaster::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 IntBlaster::maxInt(uint64_t k) { Assert(k > 0); Rational max_value = intpow2(k) - 1; - return d_nm->mkConst(CONST_RATIONAL, max_value); + return d_nm->mkConst(CONST_RATIONAL, max_value); } Node IntBlaster::pow2(uint64_t k) { Assert(k >= 0); - return d_nm->mkConst(CONST_RATIONAL, intpow2(k)); + return d_nm->mkConst(CONST_RATIONAL, intpow2(k)); } Node IntBlaster::modpow2(Node n, uint64_t exponent) { - Node p2 = d_nm->mkConst(CONST_RATIONAL, intpow2(exponent)); + Node p2 = d_nm->mkConst(CONST_RATIONAL, intpow2(exponent)); return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, n, p2); } @@ -139,6 +165,7 @@ Node IntBlaster::intBlast(Node n, while (!toVisit.empty()) { Node current = toVisit.back(); + Trace("int-blaster-debug") << "current: " << current << std::endl; uint64_t currentNumChildren = current.getNumChildren(); if (d_intblastCache.find(current) == d_intblastCache.end()) { @@ -200,7 +227,6 @@ Node IntBlaster::intBlast(Node n, translation = translateWithChildren(current, translated_children, lemmas); } - Assert(!translation.isNull()); // Map the current node to its translation in the cache. d_intblastCache[current] = translation; @@ -213,8 +239,6 @@ Node IntBlaster::intBlast(Node n, return d_intblastCache[n].get(); } -Node IntBlaster::uts(Node n, uint64_t bw) { return Node(); } - Node IntBlaster::translateWithChildren( Node original, const std::vector& translated_children, @@ -223,7 +247,6 @@ Node IntBlaster::translateWithChildren( // 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); @@ -239,7 +262,6 @@ Node IntBlaster::translateWithChildren( 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() @@ -562,9 +584,65 @@ Node IntBlaster::translateWithChildren( return returnNode; } +Node IntBlaster::uts(Node x, uint64_t bvsize) +{ + Node powNode = pow2(bvsize - 1); + Node modNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, x, powNode); + Node two = d_nm->mkConst(CONST_RATIONAL, Rational(2)); + Node twoTimesNode = d_nm->mkNode(kind::MULT, two, modNode); + return d_nm->mkNode(kind::MINUS, twoTimesNode, x); +} + Node IntBlaster::createSignExtendNode(Node x, uint64_t bvsize, uint64_t amount) { - return Node(); + Node returnNode; + if (x.isConst()) + { + Rational c(x.getConst()); + Rational twoToKMinusOne(intpow2(bvsize - 1)); + /* 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 = x; + } + 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 + { + if (amount == 0) + { + returnNode = x; + } + 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, x, minSigned); + Node thenResult = x; + Node left = maxInt(amount); + Node mul = d_nm->mkNode(kind::MULT, left, pow2(bvsize)); + Node sum = d_nm->mkNode(kind::PLUS, mul, x); + Node elseResult = sum; + Node ite = d_nm->mkNode(kind::ITE, condition, thenResult, elseResult); + returnNode = ite; + } + } + return returnNode; } Node IntBlaster::translateNoChildren(Node original, @@ -574,13 +652,12 @@ Node IntBlaster::translateNoChildren(Node original, Trace("int-blaster-debug") << "translating leaf: " << original << "; of type: " << original.getType() << std::endl; - // The result of the translation Node translation; // The translation is done differently for variables (bound or free) and // constants (values) - Assert(original.isVar() || original.isConst()); + Assert(original.isVar() || original.isConst() || original.isNullaryOp()); if (original.isVar()) { if (original.getType().isBitVector()) @@ -653,17 +730,18 @@ Node IntBlaster::translateNoChildren(Node original, } else { - // original is a constant (value) + // original is a constant (value) or a nullary op (e.g., PI) 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, c); + Rational r = Rational(c, Integer(1)); + translation = d_nm->mkConst(CONST_RATIONAL, r); } else { - // Other constants stay the same. + // Other constants or nullary ops stay the same. translation = original; } } @@ -675,7 +753,6 @@ Node IntBlaster::translateFunctionSymbol(Node bvUF, { // construct the new function symbol. Node intUF; - // old and new types of domain and result TypeNode tn = bvUF.getType(); TypeNode bvRange = tn.getRangeType(); @@ -724,7 +801,6 @@ Node IntBlaster::translateFunctionSymbol(Node bvUF, achildren.push_back(castedArg); i++; } - // create the lambda expression, and add it to skolems Node app = d_nm->mkNode(kind::APPLY_UF, achildren); Node body = castToType(app, bvRange); @@ -737,7 +813,22 @@ Node IntBlaster::translateFunctionSymbol(Node bvUF, return intUF; } -bool IntBlaster::childrenTypesChanged(Node n) { return true; } +bool IntBlaster::childrenTypesChanged(Node n) +{ + bool result = false; + for (const Node& child : n) + { + TypeNode originalType = child.getType(); + Assert(d_intblastCache.find(child) != d_intblastCache.end()); + TypeNode newType = d_intblastCache[child].get().getType(); + if (!newType.isSubtypeOf(originalType)) + { + result = true; + break; + } + } + return result; +} Node IntBlaster::castToType(Node n, TypeNode tn) { @@ -761,7 +852,6 @@ Node IntBlaster::castToType(Node n, TypeNode tn) Node intToBVOp = d_nm->mkConst(IntToBitVector(bvsize)); return d_nm->mkNode(intToBVOp, n); } - // casting bit-vectors to ingers Assert(n.getType().isBitVector()); Assert(tn.isInteger()); @@ -772,19 +862,118 @@ Node IntBlaster::reconstructNode(Node originalNode, TypeNode resultType, const std::vector& translated_children) { - return Node(); + // 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; } Node IntBlaster::createShiftNode(std::vector children, uint64_t bvsize, bool isLeftShift) { - return Node(); + /** + * 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(Integer(i), Integer(1)))), + body, + ite); + } + return ite; } Node IntBlaster::translateQuantifiedFormula(Node quantifiedNode) { - return Node(); + 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. + std::vector oldBoundVars; + std::vector newBoundVars; + std::vector rangeConstraints; + for (Node bv : quantifiedNode[0]) + { + oldBoundVars.push_back(bv); + if (bv.getType().isBitVector()) + { + // bit-vector variables are replaced by integer ones. + // the new variables induce range constraints based on the + // original bit-width. + Node newBoundVar = d_intblastCache[bv]; + newBoundVars.push_back(newBoundVar); + rangeConstraints.push_back( + mkRangeConstraint(newBoundVar, bv.getType().getBitVectorSize())); + } + else + { + // variables that are not bit-vectors are not changed + newBoundVars.push_back(bv); + } + } + + // the body of the quantifier + Node matrix = d_intblastCache[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 IntBlaster::createBVAndNode(Node x, @@ -792,7 +981,34 @@ Node IntBlaster::createBVAndNode(Node x, uint64_t bvsize, std::vector& lemmas) { - return Node(); + // 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 + Node returnNode; + if (d_mode == options::SolveBVAsIntMode::IAND) + { + Node iAndOp = d_nm->mkConst(IntAnd(bvsize)); + returnNode = d_nm->mkNode(kind::IAND, iAndOp, x, y); + } + else if (d_mode == options::SolveBVAsIntMode::BV) + { + // translate the children back to BV + Node intToBVOp = d_nm->mkConst(IntToBitVector(bvsize)); + 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 if (d_mode == options::SolveBVAsIntMode::SUM) + { + // Construct a sum of ites, based on granularity. + returnNode = d_iandUtils.createSumNode(x, y, bvsize, d_granularity); + } + return returnNode; } Node IntBlaster::createBVOrNode(Node x, diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp index 106a0a39e..2ad8695de 100644 --- a/test/unit/theory/theory_bv_int_blaster_white.cpp +++ b/test/unit/theory/theory_bv_int_blaster_white.cpp @@ -61,8 +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, false); Node result = intBlaster.translateNoChildren(bv7_4, lemmas, skolems); Node seven = d_nodeManager->mkConst(CONST_RATIONAL, Rational(7)); ASSERT_EQ(seven, result); @@ -87,8 +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, true); Node result = intBlaster.translateNoChildren(bv, lemmas, skolems); ASSERT_TRUE(result.isVar() && result.getType().isInteger()); @@ -118,8 +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, true); Node result = intBlaster.translateNoChildren(f, lemmas, skolems); TypeNode resultType = result.getType(); std::vector resultDomain = resultType.getArgTypes(); @@ -146,8 +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, true); // bit-vector variables TypeNode bvType = d_nodeManager->mkBitVectorType(4); @@ -211,6 +207,13 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_with_children) result = intBlaster.translateWithChildren(original, {i1}, lemmas); ASSERT_TRUE(result.getType().isInteger()); + // sign extend + Node signExtOp = + d_nodeManager->mkConst(BitVectorSignExtend(4)); + original = d_nodeManager->mkNode(signExtOp, 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); @@ -220,6 +223,31 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_with_children) ASSERT_TRUE(result.getType().isInteger()); ASSERT_TRUE(intExtract.getType().isInteger()); + // left shift + original = d_nodeManager->mkNode(BITVECTOR_SHL, v1, v2); + result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); + ASSERT_TRUE(result.getType().isInteger()); + + // logical right shift + original = d_nodeManager->mkNode(BITVECTOR_LSHR, v1, v2); + result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); + ASSERT_TRUE(result.getType().isInteger()); + + // arithmetic right shift + original = d_nodeManager->mkNode(BITVECTOR_ASHR, v1, v2); + result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); + ASSERT_TRUE(result.getType().isInteger()); + + // bvand + original = d_nodeManager->mkNode(BITVECTOR_AND, v1, v2); + result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); + ASSERT_TRUE(result.getType().isInteger()); + + // bvor + original = d_nodeManager->mkNode(BITVECTOR_OR, v1, v2); + result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); + ASSERT_TRUE(result.getType().isInteger()); + // concat original = d_nodeManager->mkNode(BITVECTOR_CONCAT, v1, v2); result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); @@ -250,14 +278,6 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_with_children) 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