From: yoni206 Date: Mon, 29 Mar 2021 13:38:19 +0000 (-0700) Subject: Modular bv2int part 1 (#6212) X-Git-Tag: cvc5-1.0.0~2020 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ba91b0ea10021ad299f30d23de4864940bb78100;p=cvc5.git Modular bv2int part 1 (#6212) This PR introduces the header file for a more modular bv-to-int module, that will be called from the preprocessing pass bv-to-int, and possibly from the bit-vector solver after preprocessing. The header file is basically a copy of the bv_to_int.h header file from preprocessing, with some adjustments to increase modularity. In addition to the header file we also introduce an empty unit test that #includes the header, in order to identify compilation errors. The unit test will be populated in subsequent PRs, that will also include implementations. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index febb34281..41a6a0df5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -549,6 +549,7 @@ libcvc4_add_sources( theory/bv/bv_subtheory_core.h theory/bv/bv_subtheory_inequality.cpp theory/bv/bv_subtheory_inequality.h + theory/bv/int_blaster.h theory/bv/proof_checker.cpp theory/bv/proof_checker.h theory/bv/slicer.cpp diff --git a/src/theory/bv/int_blaster.h b/src/theory/bv/int_blaster.h new file mode 100644 index 000000000..80f47509e --- /dev/null +++ b/src/theory/bv/int_blaster.h @@ -0,0 +1,354 @@ +/********************* */ +/*! \file int_blaster.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 A translation utility from bit-vectors to integers. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BV__INT_BLASTER__H +#define __CVC4__THEORY__BV__INT_BLASTER__H + +#include "context/cdhashmap.h" +#include "context/cdhashset.h" +#include "context/cdo.h" +#include "context/context.h" +#include "options/smt_options.h" +#include "theory/arith/nl/iand_utils.h" + +namespace CVC4 { + +/* +** Converts bit-vector formulas to integer formulas. +** The conversion is implemented using a translation function Tr, +** roughly described as follows: +** +** Tr(x) = fresh_x for every bit-vector variable x, where fresh_x is a fresh +** integer variable. +** Tr(c) = the integer value of c, for any bit-vector constant c. +** Tr((bvadd s t)) = Tr(s) + Tr(t) mod 2^k, where k is the bit width of +** s and t. +** Similar transformations are done for bvmul, bvsub, bvudiv, bvurem, bvneg, +** bvnot, bvconcat, bvextract +** Tr((_ zero_extend m) x) = Tr(x) +** Tr((_ sign_extend m) x) = ite(msb(x)=0, x, 2^k*(2^m-1) + x)) +** explanation: if the msb is 0, this is the same as zero_extend, +** which does not change the integer value. +** If the msb is 1, then the result should correspond to +** concat(1...1, x), with m 1's. +** m 1's is 2^m-1, and multiplying it by x's width (k) moves it +** to the front. +** +** Tr((bvand s t)) depends on the granularity, which is provided via an option. +** We divide s and t to blocks. +** The size of each block is the granularity, and so the number of +** blocks is: +** bit width/granularity (rounded down). +** We create an ITE that represents an arbitrary block, +** and then create a sum by mutiplying each block by the +** appropriate power of two. +** More formally: +** Let g denote the granularity. +** Let k denote the bit width of s and t. +** Let b denote floor(k/g) if k >= g, or just k otherwise. +** Tr((bvand s t)) = +** Sigma_{i=0}^{b-1}(bvand s[(i+1)*g, i*g] t[(i+1)*g, i*g])*2^(i*g) +** +** bvor, bvxor, bvxnor, bvnand, bvnor -- are eliminated and so bvand is the +*only bit-wise operator that is directly handled. +** +** Tr((bvshl a b)) = ite(Tr(b) >= k, 0, Tr(a)*ITE), where k is the bit width of +** a and b, and ITE represents exponentiation up to k, that is: +** ITE = ite(Tr(b)=0, 1, ite(Tr(b)=1), 2, ite(Tr(b)=2, 4, ...)) +** Similar transformations are done for bvlshr. +** +** Tr(a=b) = Tr(a)=Tr(b) +** Tr((bvult a b)) = Tr(a) < Tr(b) +** Similar transformations are done for bvule, bvugt, and bvuge. +** +** Bit-vector operators that are not listed above are either eliminated using +** the function eliminationPass, or go through the following default +*translation, that also works for non-bit-vector operators +** with result type BV: +** Tr((op t1 ... tn)) = (bv2nat (op (cast t1) ... (cast tn))) +** where (cast x) is ((_ nat2bv k) x) or just x, +** depending on the type of the corresponding argument of +** op. +** +**/ +class IntBlaster +{ + using CDNodeMap = context::CDHashMap; + + public: + /** + * Constructor. + * @param context user context + * @param mode bv-to-int translation mode + * @param granularity bv-to-int translation granularity + * @param introduceFreshIntVars determines whether bit-vector variables are + * translated to integer variables, or are directly casted using `bv2nat` + * operator. not purely bit-vector nodes. + */ + IntBlaster(context::Context* context, + options::SolveBVAsIntMode mode, + uint64_t granluarity = 1, + bool introduceFreshIntVars = true); + + /** + * The result is an integer term and is computed + * according to the translation specified above. + * @param n is a bit-vector term or formula to be translated. + * @param lemmas additional lemmas that are needed for the translation + * to be sound. These are range constraints on introduced variables. + * @param skolems a map in which the following information will be stored + * during the run of intBlast: for each BV variable n, skolems[n] is its new + * definition: ((_ nat2bv k) nn), where k is the bit-width of n, and nn is the + * integer variable that corresponds to n. + * For each UF f from BV to BV, skolems[f] is lambda x : BV[k] . ((_ nat2bv i) + * ff((bv2nat x))), where k is the bit-width of the domain of f, i is the + * bit-width of its range, and ff is a Int->Int function that corresponds to + * f. For functions with other signatures this is similar + * @return integer node that corresponds to n, or a null node if d_supportNoBV + * is set to false and n is note purely BV. + */ + Node intBlast(Node n, + std::vector& lemmas, + std::map& skolems); + + protected: + /** + * 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 + * width. a >> b gets translated to a div 2^b mod 2^k, where k is the bit + * width. The exponentiation operation is translated to an ite for possible + * values of the exponent, from 0 to k-1. + * If the right operand of the shift is greater than k-1, + * the result is 0. + * @param children the two operands for the shift + * @param bvsize the original bit widths of the operands + * (before translation to integers) + * @param isLeftShift true iff the desired operation is a left shift. + * @return a node representing the shift. + * + */ + Node createShiftNode(std::vector children, + uint64_t bvsize, + bool isLeftShift); + + /** Adds the constraint 0 <= node < 2^size to lemmas */ + void addRangeConstraint(Node node, uint64_t size, std::vector& lemmas); + + /** Adds a constraint that encodes bitwise and */ + void addBitwiseConstraint(Node bitwiseConstraint, std::vector& lemmas); + + /** Returns a node that represents the bitwise negation of n. */ + Node createBVNotNode(Node n, uint64_t bvsize); + + /** + * Whenever we introduce an integer variable that represents a bit-vector + * variable, we need to guard the range of the newly introduced variable. + * For bit width k, the constraint is 0 <= newVar < 2^k. + * @param newVar the newly introduced integer variable + * @param k the bit width of the original bit-vector variable. + * @return a node representing the range constraint. + */ + Node mkRangeConstraint(Node newVar, uint64_t k); + + /** + * In the translation to integers, it is convenient to assume that certain + * bit-vector operators do not occur in the original formula (e.g., repeat). + * This function eliminates all these operators. + */ + Node eliminationPass(Node n); + + /** + * Some bit-vector operators (e.g., bvadd, bvand) are binary, but allow more + * than two arguments as a syntactic sugar. + * For example, we can have a node for (bvand x y z), + * that represents (bvand (x (bvand y z))). + * This function makes all such operators strictly binary. + */ + Node makeBinary(Node n); + + /** + * @param k A non-negative integer + * @return A node that represents the constant 2^k + */ + Node pow2(uint64_t k); + + /** + * @param k A positive integer k + * @return A node that represent the constant 2^k-1 + * For example, if k is 4, the result is a node representing the + * constant 15. + */ + Node maxInt(uint64_t k); + + /** + * @param n A node representing an integer term + * @param exponent A non-negative integer + * @return A node representing (n mod (2^exponent)) + */ + Node modpow2(Node n, uint64_t exponent); + + /** + * Returns true iff the type of at least + * one child of n was changed by the translation. + */ + bool childrenTypesChanged(Node n); + + /** + * @param quantifiedNode a node whose main operator is forall/exists. + * @return a node opbtained from quantifiedNode by: + * 1. Replacing all bound BV variables by new bound integer variables. + * 2. Add range constraints for the new variables, induced by the original + * bit-width. These range constraints are added with "AND" in case of exists + * and with "IMPLIES" in case of forall. + */ + Node translateQuantifiedFormula(Node quantifiedNode); + + /** + * Reconstructs a node whose main operator cannot be + * translated to integers. + * Reconstruction is done by casting to integers/bit-vectors + * as needed. + * For example, if node is (select A x) where A + * is a bit-vector array, we do not change A to be + * an integer array, even though x was translated + * to integers. + * In this case we cast x to (bv2nat x) during + * the reconstruction. + * + * @param originalNode the node that we are reconstructing + * @param resultType the desired type for the reconstruction + * @param translated_children the children of originalNode + * after their translation to integers. + * @return A node with originalNode's operator that has type resultType. + */ + Node reconstructNode(Node originalNode, + TypeNode resultType, + const std::vector& translated_children); + + /** + * A useful utility function. + * if n is an integer and tn is bit-vector, + * applies the IntToBitVector operator on n. + * if n is a vit-vector and tn is integer, + * applies BitVector_TO_NAT operator. + * Otherwise, keeps n intact. + */ + Node castToType(Node n, TypeNode tn); + + /** + * When a UF f is translated to a UF g, + * we compute a definition + * to relate between f and g. + * We do the same when f and g are just variables. + * This is useful, for example, when asking + * for a model-value of a term that includes the + * original UF f. + * + * For example: if bvUF is a BV variable x and + * intUF is an integer variable xx, + * the return value is ((_ nat2bv k) xx), + * where k is the width of k. + * + * For another example: if bvUF is a BV to BV function + * f and intUF is an integer to integer function ff, + * the return value is: + * lambda x : BV[k]. ((_ nat2bv k) (ff (bv2nat x))), + * where k is the bit-width of the co-domain of f. + * + * @param bvUF the original function or variable + * @param intUF the translated function or variable + */ + Node defineBVUFAsIntUF(Node bvUF, Node intUF); + + /** + * @param bvUF is an uninterpreted function symbol from the original formula + * @return a fresh uninterpreted function symbol, obtained from bvUF + by replacing every argument of type BV to an argument of type Integer, + and the return type becomes integer in case it was BV. + */ + Node translateFunctionSymbol(Node bvUF, std::map& skolems); + + /** + * returns an integer m such that the unsigned + * binary representation of n is the same as the + * signed binary representation of m. + */ + Node unsignedTosigned(Node n, uint64_t bvsize); + + /** + * Performs the actual translation to integers for nodes + * that have children. + */ + Node translateWithChildren(Node original, + const std::vector& translated_children, + std::vector& lemmas); + + /** + * Performs the actual translation to integers for nodes + * that don't have children (variables, constants, uninterpreted function + * symbols). + */ + Node translateNoChildren(Node original, + std::vector& lemmas, + std::map& skolems); + + /** Caches for the different functions */ + CDNodeMap d_binarizeCache; + CDNodeMap d_eliminationCache; + CDNodeMap d_rebuildCache; + CDNodeMap d_intblastCache; + + /** Node manager that is used throughout the pass */ + NodeManager* d_nm; + + /** + * Range constraints of the form 0 <= x < 2^k + * These are added for every new integer variable that we introduce. + */ + context::CDHashSet d_rangeAssertions; + + /** + * A set of "bitwise" equalities over integers for BITVECTOR_AND + * used in for options::SolveBVAsIntMode::BITWISE + */ + context::CDHashSet d_bitwiseAssertions; + + /** Useful constants */ + Node d_zero; + Node d_one; + + /** helper class for handeling bvand translation */ + theory::arith::nl::IAndUtils d_iandUtils; + + /** the mode for translation to integers */ + options::SolveBVAsIntMode d_mode; + + /** the granularity to use in the translation */ + uint64_t d_granularity; + + /** an SmtEngine for context */ + context::Context* d_context; + + /** true iff the translator should introduce + * fresh integer variables for bit-vector variables. + * Otherwise, we introduce a nat2bv term. + */ + bool d_introduceFreshIntVars; +}; + +} // namespace CVC4 + +#endif /* __CVC4__THEORY__BV__INT_BLASTER_H */ diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index dd312498f..723369200 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -20,6 +20,7 @@ cvc4_add_unit_test_white(theory_bags_rewriter_white theory) cvc4_add_unit_test_white(theory_bags_type_rules_white theory) cvc4_add_unit_test_white(theory_bv_rewriter_white theory) cvc4_add_unit_test_white(theory_bv_white theory) +cvc4_add_unit_test_white(theory_bv_int_blaster_white theory) cvc4_add_unit_test_white(theory_engine_white theory) cvc4_add_unit_test_white(theory_int_opt_white theory) cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory) diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp new file mode 100644 index 000000000..7888ba52b --- /dev/null +++ b/test/unit/theory/theory_bv_int_blaster_white.cpp @@ -0,0 +1,47 @@ +/********************* */ +/*! \file theory_bv_rewriter_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Yoni Zohar + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 Unit tests for bit-vector solving via integers + ** + ** Unit tests for bit-vector solving via integers. + **/ + +#include +#include +#include + +#include "test_smt.h" +#include "theory/bv/int_blaster.h" +#include "util/bitvector.h" + +namespace CVC4 { + +using namespace kind; +using namespace theory; + +namespace test { + +class TestTheoryWhiteBvIntblaster : public TestSmtNoFinishInit +{ + protected: + void SetUp() override + { + TestSmtNoFinishInit::SetUp(); + d_smtEngine->setOption("produce-models", "true"); + d_smtEngine->finishInit(); + d_true = d_nodeManager->mkConst(true); + d_one = d_nodeManager->mkConst(Rational(1)); + } + Node d_true; + Node d_one; +}; +} // namespace test +} // namespace CVC4