#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 {
d_introduceFreshIntVars(introduceFreshIntVars)
{
d_nm = NodeManager::currentNM();
- d_zero = d_nm->mkConst<Rational>(CONST_RATIONAL, 0);
- d_one = d_nm->mkConst<Rational>(CONST_RATIONAL, 1);
+ d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0));
+ d_one = d_nm->mkConst(CONST_RATIONAL, Rational(1));
};
IntBlaster::~IntBlaster() {}
uint64_t size,
std::vector<Node>& 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<Node>& 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<Rational>(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<Rational>(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<Rational>(CONST_RATIONAL, intpow2(exponent));
+ Node p2 = d_nm->mkConst(CONST_RATIONAL, intpow2(exponent));
return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, n, p2);
}
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())
{
translation =
translateWithChildren(current, translated_children, lemmas);
}
-
Assert(!translation.isNull());
// Map the current node to its translation in the cache.
d_intblastCache[current] = translation;
return d_intblastCache[n].get();
}
-Node IntBlaster::uts(Node n, uint64_t bw) { return Node(); }
-
Node IntBlaster::translateWithChildren(
Node original,
const std::vector<Node>& translated_children,
// 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_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()
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>());
+ 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,
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())
}
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<BitVector>());
Integer c = constant.toInteger();
- translation = d_nm->mkConst<Rational>(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;
}
}
{
// construct the new function symbol.
Node intUF;
-
// old and new types of domain and result
TypeNode tn = bvUF.getType();
TypeNode bvRange = tn.getRangeType();
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);
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)
{
Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize));
return d_nm->mkNode(intToBVOp, n);
}
-
// casting bit-vectors to ingers
Assert(n.getType().isBitVector());
Assert(tn.isInteger());
TypeNode resultType,
const std::vector<Node>& 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<Node> 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<Node> oldBoundVars;
+ std::vector<Node> newBoundVars;
+ std::vector<Node> 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,
uint64_t bvsize,
std::vector<Node>& 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>(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,
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);
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());
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<TypeNode> resultDomain = resultType.getArgTypes();
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);
result = intBlaster.translateWithChildren(original, {i1}, lemmas);
ASSERT_TRUE(result.getType().isInteger());
+ // sign extend
+ Node signExtOp =
+ d_nodeManager->mkConst<BitVectorSignExtend>(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);
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);
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
projects / cvc5.git / commitdiff