This PR is essentially a code move.
It moves the code that translates bvand from the bv_to_int preprocessing pass to a new class IAndHelper, in the new files nl_iand_utils.{h,cpp}. The goal is to have this code in a place which can be shared between the bv2int preprocessing pass and the iand solver.
Future PRs will:
Optimize this utility
Make use of it in the iand solver
The code in nl_iand_utils.{h,cpp} is almost completely a move from bv_to_int.{h,cpp}. The changes are all minor, and include, e.g., the following changes:
the node manager is no longer a member, and so is the constant 0.
using the oneBitAnd function directly, without a function pointer.
theory/arith/nl/icp/intersection.h
theory/arith/nl/nl_constraint.cpp
theory/arith/nl/nl_constraint.h
+ theory/arith/nl/iand_table.cpp
+ theory/arith/nl/iand_table.h
theory/arith/nl/nl_lemma_utils.cpp
theory/arith/nl/nl_lemma_utils.h
theory/arith/nl/nl_model.cpp
/**
* Helper functions for createBitwiseNode
*/
-bool oneBitAnd(bool a, bool b) { return (a && b); }
} //end empty namespace
Assert(options::solveBVAsInt() == options::SolveBVAsIntMode::SUM);
// Construct a sum of ites, based on granularity.
Assert(translated_children.size() == 2);
- Node newNode = createBitwiseNode(translated_children[0],
- translated_children[1],
- bvsize,
- options::BVAndIntegerGranularity(),
- &oneBitAnd);
- returnNode = newNode;
+ returnNode =
+ d_iandTable.createBitwiseNode(translated_children[0],
+ translated_children[1],
+ bvsize,
+ options::BVAndIntegerGranularity());
}
break;
}
return result;
}
-Node BVToInt::createITEFromTable(
- Node x,
- Node y,
- uint64_t granularity,
- std::map<std::pair<uint64_t, uint64_t>, uint64_t> table)
-{
- Assert(granularity <= 8);
- uint64_t max_value = ((uint64_t)pow(2, granularity));
- // The table represents a function from pairs of integers to integers, where
- // all integers are between 0 (inclusive) and max_value (exclusive).
- Assert(table.size() == max_value * max_value);
- Node ite = d_nm->mkConst<Rational>(table[std::make_pair(0, 0)]);
- for (uint64_t i = 0; i < max_value; i++)
- {
- for (uint64_t j = 0; j < max_value; j++)
- {
- if ((i == 0) && (j == 0))
- {
- continue;
- }
- ite = d_nm->mkNode(
- kind::ITE,
- d_nm->mkNode(
- kind::AND,
- d_nm->mkNode(kind::EQUAL, x, d_nm->mkConst<Rational>(i)),
- d_nm->mkNode(kind::EQUAL, y, d_nm->mkConst<Rational>(j))),
- d_nm->mkConst<Rational>(table[std::make_pair(i, j)]),
- ite);
- }
- }
- return ite;
-}
-
-Node BVToInt::createBitwiseNode(Node x,
- Node y,
- uint64_t bvsize,
- uint64_t granularity,
- bool (*f)(bool, bool))
-{
- /**
- * Standardize granularity.
- * If it is greater than bvsize, it is set to bvsize.
- * Otherwise, it is set to the closest (going down) divider of bvsize.
- */
- Assert(0 < granularity && granularity <= 8);
- if (granularity > bvsize)
- {
- granularity = bvsize;
- }
- else
- {
- while (bvsize % granularity != 0)
- {
- granularity = granularity - 1;
- }
- }
- // transform f into a table
- // f is defined over 1 bit, while the table is defined over `granularity` bits
- std::map<std::pair<uint64_t, uint64_t>, uint64_t> table;
- uint64_t max_value = ((uint64_t)pow(2, granularity));
- for (uint64_t i = 0; i < max_value; i++)
- {
- for (uint64_t j = 0; j < max_value; j++)
- {
- uint64_t sum = 0;
- for (uint64_t n = 0; n < granularity; n++)
- {
- // b is the result of f on the current bit
- bool b = f((((i >> n) & 1) == 1), (((j >> n) & 1) == 1));
- // add the corresponding power of 2 only if the result is 1
- if (b)
- {
- sum += 1 << n;
- }
- }
- table[std::make_pair(i, j)] = sum;
- }
- }
- Assert(table.size() == max_value * max_value);
-
- /*
- * Create the sum.
- * For granularity 1, the sum has bvsize elements.
- * In contrast, if bvsize = granularity, sum has one element.
- * Each element in the sum is an ite that corresponds to the generated table,
- * multiplied by the appropriate power of two.
- * More details are in bv_to_int.h .
- */
- uint64_t sumSize = bvsize / granularity;
- Node sumNode = d_zero;
- /**
- * extract definition in integers is:
- * (define-fun intextract ((k Int) (i Int) (j Int) (a Int)) Int
- * (mod (div a (two_to_the j)) (two_to_the (+ (- i j) 1))))
- */
- for (uint64_t i = 0; i < sumSize; i++)
- {
- Node xExtract = d_nm->mkNode(
- kind::INTS_MODULUS_TOTAL,
- d_nm->mkNode(kind::INTS_DIVISION_TOTAL, x, pow2(i * granularity)),
- pow2(granularity));
- Node yExtract = d_nm->mkNode(
- kind::INTS_MODULUS_TOTAL,
- d_nm->mkNode(kind::INTS_DIVISION_TOTAL, y, pow2(i * granularity)),
- pow2(granularity));
- Node ite = createITEFromTable(xExtract, yExtract, granularity, table);
- sumNode =
- d_nm->mkNode(kind::PLUS,
- sumNode,
- d_nm->mkNode(kind::MULT, pow2(i * granularity), ite));
- }
- return sumNode;
-}
-
Node BVToInt::createBVNotNode(Node n, uint64_t bvsize)
{
return d_nm->mkNode(kind::MINUS, maxInt(bvsize), n);
#include "context/context.h"
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
+#include "theory/arith/nl/iand_table.h"
namespace CVC4 {
namespace preprocessing {
protected:
PreprocessingPassResult applyInternal(
AssertionPipeline* assertionsToPreprocess) override;
-
- /**
- * A generic function that creates a node that represents a bitwise
- * operation.
- *
- * For example: Suppose bvsize is 4, granularity is 1, and f(x,y) = x && y.
- * Denote by ITE(a,b) the term: ite(a==0, 0, ite(b==1, 1, 0)).
- * The result of this function would be:
- * ITE(x[0], y[0])*2^0 + ... + ITE(x[3], y[3])*2^3
- *
- * For another example: Suppose bvsize is 4, granularity is 2,
- * and f(x,y) = x && y.
- * Denote by ITE(a,b) the term that corresponds to the following table:
- * a | b | ITE(a,b)
- * ----------------
- * 0 | 0 | 0
- * 0 | 1 | 0
- * 0 | 2 | 0
- * 0 | 3 | 0
- * 1 | 0 | 0
- * 1 | 1 | 1
- * 1 | 2 | 0
- * 1 | 3 | 1
- * 2 | 0 | 0
- * 2 | 1 | 0
- * 2 | 2 | 2
- * 2 | 3 | 2
- * 3 | 0 | 0
- * 3 | 1 | 1
- * 3 | 2 | 2
- * 3 | 3 | 3
- *
- * For example, 2 in binary is 10 and 1 in binary is 01, and so doing
- * "bitwise f" on them gives 00.
- * The result of this function would be:
- * ITE(x[1:0], y[1:0])*2^0 + ITE(x[3:2], y[3:2])*2^2
- *
- *
- * @param x is an integer operand that correspond to the first original
- * bit-vector operand.
- * @param y is an integer operand that correspond to the second original
- * bit-vector operand.
- * @param bvsize is the bit width of the original bit-vector variables.
- * @param granularity is specified in the options for this preprocessing
- * pass.
- * @param f is a pointer to a boolean function that corresponds
- * to the original bitwise operation.
- * @return A node that represents the operation, as described above.
- */
- Node createBitwiseNode(Node x,
- Node y,
- uint64_t bvsize,
- uint64_t granularity,
- bool (*f)(bool, bool));
-
- /**
- * A helper function for createBitwiseNode
- * @param x integer node corresponding to the original first bit-vector
- * argument
- * @param y integer node corresponding to the original second bit-vector
- * argument nodes.
- * @param granularity the bitwidth of the original bit-vector nodes.
- * @param table a function from pairs of integers to integers.
- * The domain of this function consists of pairs of
- * integers between 0 (inclusive) and 2^{bitwidth} (exclusive).
- * @return An ite term that represents this table.
- */
- Node createITEFromTable(
- Node x,
- Node y,
- uint64_t granularity,
- std::map<std::pair<uint64_t, uint64_t>, uint64_t> table);
-
/**
* A generic function that creates a logical shift node (either left or
* right). a << b gets translated to a * 2^b mod 2^k, where k is the bit
*/
Node d_zero;
Node d_one;
+
+ /** helper class for handeling bvand translation */
+ theory::arith::nl::IAndTable d_iandTable;
};
} // namespace passes
return lem;
}
-bool oneBitAnd(bool a, bool b) { return (a && b); }
} // namespace nl
} // namespace arith
--- /dev/null
+/********************* */
+/*! \file iand_table.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Yoni Zohar
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utilities to maintain finite tables that represent
+ ** the value of iand.
+ **/
+
+#include "theory/arith/nl/iand_table.h"
+
+#include <cmath>
+
+#include "cvc4_private.h"
+#include "theory/arith/nl/nl_model.h"
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+
+static Rational intpow2(uint64_t b)
+{
+ return Rational(Integer(2).pow(b), Integer(1));
+}
+
+Node pow2(uint64_t k)
+{
+ Assert(k >= 0);
+ NodeManager* nm = NodeManager::currentNM();
+ return nm->mkConst<Rational>(intpow2(k));
+}
+
+bool oneBitAnd(bool a, bool b) { return (a && b); }
+
+Node IAndTable::createITEFromTable(
+ Node x,
+ Node y,
+ uint64_t granularity,
+ const std::map<std::pair<uint64_t, uint64_t>, uint64_t>& table)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Assert(granularity <= 8);
+ uint64_t max_value = ((uint64_t)pow(2, granularity));
+ // The table represents a function from pairs of integers to integers, where
+ // all integers are between 0 (inclusive) and max_value (exclusive).
+ Assert(table.size() == max_value * max_value);
+ Node ite = nm->mkConst<Rational>(table.at(std::make_pair(0, 0)));
+ for (uint64_t i = 0; i < max_value; i++)
+ {
+ for (uint64_t j = 0; j < max_value; j++)
+ {
+ if ((i == 0) && (j == 0))
+ {
+ continue;
+ }
+ ite = nm->mkNode(
+ kind::ITE,
+ nm->mkNode(kind::AND,
+ nm->mkNode(kind::EQUAL, x, nm->mkConst<Rational>(i)),
+ nm->mkNode(kind::EQUAL, y, nm->mkConst<Rational>(j))),
+ nm->mkConst<Rational>(table.at(std::make_pair(i, j))),
+ ite);
+ }
+ }
+ return ite;
+}
+
+Node IAndTable::createBitwiseNode(Node x,
+ Node y,
+ uint64_t bvsize,
+ uint64_t granularity)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ /**
+ * Standardize granularity.
+ * If it is greater than bvsize, it is set to bvsize.
+ * Otherwise, it is set to the closest (going down) divider of bvsize.
+ */
+ Assert(0 < granularity && granularity <= 8);
+ if (granularity > bvsize)
+ {
+ granularity = bvsize;
+ }
+ else
+ {
+ while (bvsize % granularity != 0)
+ {
+ granularity = granularity - 1;
+ }
+ }
+ // transform f into a table
+ // f is defined over 1 bit, while the table is defined over `granularity` bits
+ std::map<std::pair<uint64_t, uint64_t>, uint64_t> table;
+ uint64_t max_value = ((uint64_t)pow(2, granularity));
+ for (uint64_t i = 0; i < max_value; i++)
+ {
+ for (uint64_t j = 0; j < max_value; j++)
+ {
+ uint64_t sum = 0;
+ for (uint64_t n = 0; n < granularity; n++)
+ {
+ // b is the result of f on the current bit
+ bool b = oneBitAnd((((i >> n) & 1) == 1), (((j >> n) & 1) == 1));
+ // add the corresponding power of 2 only if the result is 1
+ if (b)
+ {
+ sum += 1 << n;
+ }
+ }
+ table[std::make_pair(i, j)] = sum;
+ }
+ }
+ Assert(table.size() == max_value * max_value);
+
+ /*
+ * Create the sum.
+ * For granularity 1, the sum has bvsize elements.
+ * In contrast, if bvsize = granularity, sum has one element.
+ * Each element in the sum is an ite that corresponds to the generated table,
+ * multiplied by the appropriate power of two.
+ * More details are in bv_to_int.h .
+ */
+ uint64_t sumSize = bvsize / granularity;
+ Node sumNode = nm->mkConst<Rational>(0);
+ /**
+ * extract definition in integers is:
+ * (define-fun intextract ((k Int) (i Int) (j Int) (a Int)) Int
+ * (mod (div a (two_to_the j)) (two_to_the (+ (- i j) 1))))
+ */
+ for (uint64_t i = 0; i < sumSize; i++)
+ {
+ Node xExtract = nm->mkNode(
+ kind::INTS_MODULUS_TOTAL,
+ nm->mkNode(kind::INTS_DIVISION_TOTAL, x, pow2(i * granularity)),
+ pow2(granularity));
+ Node yExtract = nm->mkNode(
+ kind::INTS_MODULUS_TOTAL,
+ nm->mkNode(kind::INTS_DIVISION_TOTAL, y, pow2(i * granularity)),
+ pow2(granularity));
+ Node ite = createITEFromTable(xExtract, yExtract, granularity, table);
+ sumNode = nm->mkNode(kind::PLUS,
+ sumNode,
+ nm->mkNode(kind::MULT, pow2(i * granularity), ite));
+ }
+ return sumNode;
+}
+
+} // namespace nl
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file iand_table.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Yoni Zohar
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utilities to maintain finite tables that represent
+ ** the value of iand.
+ **/
+
+#ifndef CVC4__THEORY__ARITH__IAND_TABLE_H
+#define CVC4__THEORY__ARITH__IAND_TABLE_H
+
+#include <tuple>
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+
+/**
+ * A class that computes tables for iand values
+ * with various bit-widths
+ */
+class IAndTable
+{
+ public:
+ /**
+ * A generic function that creates a node that represents a bitwise
+ * operation.
+ *
+ * For example: Suppose bvsize is 4, granularity is 1, and f(x,y) = x && y.
+ * Denote by ITE(a,b) the term: ite(a==0, 0, ite(b==1, 1, 0)).
+ * The result of this function would be:
+ * ITE(x[0], y[0])*2^0 + ... + ITE(x[3], y[3])*2^3
+ *
+ * For another example: Suppose bvsize is 4, granularity is 2,
+ * and f(x,y) = x && y.
+ * Denote by ITE(a,b) the term that corresponds to the following table:
+ * a | b | ITE(a,b)
+ * ----------------
+ * 0 | 0 | 0
+ * 0 | 1 | 0
+ * 0 | 2 | 0
+ * 0 | 3 | 0
+ * 1 | 0 | 0
+ * 1 | 1 | 1
+ * 1 | 2 | 0
+ * 1 | 3 | 1
+ * 2 | 0 | 0
+ * 2 | 1 | 0
+ * 2 | 2 | 2
+ * 2 | 3 | 2
+ * 3 | 0 | 0
+ * 3 | 1 | 1
+ * 3 | 2 | 2
+ * 3 | 3 | 3
+ *
+ * For example, 2 in binary is 10 and 1 in binary is 01, and so doing
+ * "bitwise f" on them gives 00.
+ * The result of this function would be:
+ * ITE(x[1:0], y[1:0])*2^0 + ITE(x[3:2], y[3:2])*2^2
+ *
+ *
+ * @param x is an integer operand that correspond to the first original
+ * bit-vector operand.
+ * @param y is an integer operand that correspond to the second original
+ * bit-vector operand.
+ * @param bvsize is the bit width of the original bit-vector variables.
+ * @param granularity is specified in the options for this preprocessing
+ * pass.
+ * @param f is a pointer to a boolean function that corresponds
+ * to the original bitwise operation.
+ * @return A node that represents the operation, as described above.
+ */
+ Node createBitwiseNode(Node x, Node y, uint64_t bvsize, uint64_t granularity);
+
+ /**
+ * A helper function for createBitwiseNode
+ * @param x integer node corresponding to the original first bit-vector
+ * argument
+ * @param y integer node corresponding to the original second bit-vector
+ * argument nodes.
+ * @param granularity the bitwidth of the original bit-vector nodes.
+ * @param table a function from pairs of integers to integers.
+ * The domain of this function consists of pairs of
+ * integers between 0 (inclusive) and 2^{bitwidth} (exclusive).
+ * @return An ite term that represents this table.
+ */
+ Node createITEFromTable(
+ Node x,
+ Node y,
+ uint64_t granularity,
+ const std::map<std::pair<uint64_t, uint64_t>, uint64_t>& table);
+};
+
+} // namespace nl
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__ARITH__IAND_TABLE_H */
projects / cvc5.git / commitdiff