diff options
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 126 | ||||
| -rw-r--r-- | src/preprocessing/passes/bv_to_int.h | 77 | ||||
| -rw-r--r-- | src/theory/arith/nl/iand_solver.cpp | 1 | ||||
| -rw-r--r-- | src/theory/arith/nl/iand_table.cpp | 157 | ||||
| -rw-r--r-- | src/theory/arith/nl/iand_table.h | 110 |
6 files changed, 278 insertions, 195 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index f70bdde3e..3896d3111 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -357,6 +357,8 @@ libcvc4_add_sources( 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 diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 9ee4e2b7d..06a5714d3 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -45,7 +45,6 @@ Rational intpow2(uint64_t b) /** * Helper functions for createBitwiseNode */ -bool oneBitAnd(bool a, bool b) { return (a && b); } } //end empty namespace @@ -446,12 +445,11 @@ Node BVToInt::translateWithChildren(Node original, 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; } @@ -1077,120 +1075,6 @@ Node BVToInt::translateQuantifiedFormula(Node quantifiedNode) 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); diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h index d1562ad65..0f6a6a4bb 100644 --- a/src/preprocessing/passes/bv_to_int.h +++ b/src/preprocessing/passes/bv_to_int.h @@ -75,6 +75,7 @@ #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 { @@ -90,79 +91,6 @@ class BVToInt : public PreprocessingPass 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 @@ -354,6 +282,9 @@ class BVToInt : public PreprocessingPass */ Node d_zero; Node d_one; + + /** helper class for handeling bvand translation */ + theory::arith::nl::IAndTable d_iandTable; }; } // namespace passes diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index a72010bf4..954f921ce 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -245,7 +245,6 @@ Node IAndSolver::valueBasedLemma(Node i) return lem; } -bool oneBitAnd(bool a, bool b) { return (a && b); } } // namespace nl } // namespace arith diff --git a/src/theory/arith/nl/iand_table.cpp b/src/theory/arith/nl/iand_table.cpp new file mode 100644 index 000000000..1ae866ef1 --- /dev/null +++ b/src/theory/arith/nl/iand_table.cpp @@ -0,0 +1,157 @@ +/********************* */ +/*! \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 diff --git a/src/theory/arith/nl/iand_table.h b/src/theory/arith/nl/iand_table.h new file mode 100644 index 000000000..54c8b8de7 --- /dev/null +++ b/src/theory/arith/nl/iand_table.h @@ -0,0 +1,110 @@ +/********************* */ +/*! \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 */ |