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.

4 files changed, 403 insertions, 0 deletions

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<Node, Node, NodeHashFunction>;
+
+ 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<Node>& lemmas,
+                std::map<Node, Node>& 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<Node> children,
+                       uint64_t bvsize,
+                       bool isLeftShift);
+
+  /** Adds the constraint 0 <= node < 2^size to lemmas */
+  void addRangeConstraint(Node node, uint64_t size, std::vector<Node>& lemmas);
+
+  /** Adds a constraint that encodes bitwise and */
+  void addBitwiseConstraint(Node bitwiseConstraint, std::vector<Node>& 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<Node>& 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<Node, Node>& 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<Node>& translated_children,
+                             std::vector<Node>& 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<Node>& lemmas,
+                           std::map<Node, Node>& 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<Node, NodeHashFunction> d_rangeAssertions;
+
+  /**
+   * A set of "bitwise" equalities over integers for BITVECTOR_AND
+   *   used in for options::SolveBVAsIntMode::BITWISE
+   */
+  context::CDHashSet<Node, NodeHashFunction> 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 <iostream>
+#include <memory>
+#include <vector>
+
+#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<bool>(true);
+    d_one = d_nodeManager->mkConst<Rational>(Rational(1));
+  }
+  Node d_true;
+  Node d_one;
+};
+}  // namespace test
+}  // namespace CVC4