bv2int: refactoring the main translation loop (#5051)

This PR introduces a refactoring of the main translation loop in bv2int preprocessing pass.
Many parts are wrapped by helper functions and so the main loop becomes smaller.

remark: selecting "Hide whitespace changes" cuts the diff by ~50%.

2 files changed, 510 insertions, 500 deletions

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index e91e375c9..c219deefe 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -261,8 +261,6 @@ Node BVToInt::bvToInt(Node n)
   n = makeBinary(n);
   vector<Node> toVisit;
   toVisit.push_back(n);
-  uint64_t granularity = options::BVAndIntegerGranularity();
-  Assert(0 <= granularity && granularity <= 8);
 
   while (!toVisit.empty())
   {
@@ -271,12 +269,22 @@ Node BVToInt::bvToInt(Node n)
     if (d_bvToIntCache.find(current) == d_bvToIntCache.end())
     {
       // This is the first time we visit this node and it is not in the cache.
+      // We mark this node as visited but not translated by assiging
+      // a null node to it.
       d_bvToIntCache[current] = Node();
+      // all the node's children are added to the stack to be visited
+      // before visiting this node again.
       toVisit.insert(toVisit.end(), current.begin(), current.end());
+      // If this is a UF applicatinon, we also add the function to
+      // toVisit.
+      if (current.getKind() == kind::APPLY_UF)
+      {
+        toVisit.push_back(current.getOperator());
+      }
     }
     else
     {
-      // We already visited this node
+      // We already visited and translated this node
       if (!d_bvToIntCache[current].get().isNull())
       {
         // We are done computing the translation for current
@@ -288,45 +296,8 @@ Node BVToInt::bvToInt(Node n)
         // This is when we do the actual translation.
         if (currentNumChildren == 0)
         {
-          Assert(current.isVar() || current.isConst());
-          if (current.isVar())
-          {
-            if (current.getType().isBitVector())
-            {
-              // For bit-vector variables, we create integer variables and add a
-              // range constraint.
-              Node newVar = d_nm->mkSkolem("__bvToInt_var",
-                                           d_nm->integerType(),
-                                           "Variable introduced in bvToInt "
-                                           "pass instead of original variable "
-                                               + current.toString());
-
-              d_bvToIntCache[current] = newVar;
-              d_rangeAssertions.insert(mkRangeConstraint(
-                  newVar, current.getType().getBitVectorSize()));
-            }
-            else
-            {
-              // variables other than bit-vector variables are left intact
-              d_bvToIntCache[current] = current;
-            }
-          }
-          else
-          {
-            // current is a const
-            if (current.getKind() == kind::CONST_BITVECTOR)
-            {
-              // Bit-vector constants are transformed into their integer value.
-              BitVector constant(current.getConst<BitVector>());
-              Integer c = constant.toInteger();
-              d_bvToIntCache[current] = d_nm->mkConst<Rational>(c);
-            }
-            else
-            {
-              // Other constants stay the same.
-              d_bvToIntCache[current] = current;
-            }
-          }
+          Node translation = translateNoChildren(current);
+          d_bvToIntCache[current] = translation;
         }
         else
         {
@@ -334,485 +305,499 @@ Node BVToInt::bvToInt(Node n)
            * The current node has children.
            * Since we are on the way back up,
            * these children were already translated.
-           * We save their translation for future use.
+           * We save their translation for easy access.
+           * If the node's kind is APPLY_UF,
+           * we also need to include the translated uninterpreted function in
+           * this list.
            */
           vector<Node> translated_children;
-          for (uint64_t i = 0; i < currentNumChildren; i++)
+          if (current.getKind() == kind::APPLY_UF)
           {
-            translated_children.push_back(d_bvToIntCache[current[i]]);
+            translated_children.push_back(
+                d_bvToIntCache[current.getOperator()]);
           }
-          // The translation of the current node is determined by the kind of
-          // the node.
-          kind::Kind_t oldKind = current.getKind();
-          //ultbv and sltbv were supposed to be eliminated before this point.
-          Assert(oldKind != kind::BITVECTOR_ULTBV);
-          Assert(oldKind != kind::BITVECTOR_SLTBV);
-          switch (oldKind)
+          for (uint64_t i = 0; i < currentNumChildren; i++)
           {
-            case kind::BITVECTOR_PLUS:
-            {
-              uint64_t bvsize = current[0].getType().getBitVectorSize();
-              /**
-               * we avoid modular arithmetics by the addition of an
-               * indicator variable sigma.
-               * Tr(a+b) is Tr(a)+Tr(b)-(sigma*2^k),
-               * with k being the bit width,
-               * and sigma being either 0 or 1.
-               */
-              Node sigma = d_nm->mkSkolem(
-                  "__bvToInt_sigma_var",
-                  d_nm->integerType(),
-                  "Variable introduced in bvToInt pass to avoid integer mod");
-              Node plus = d_nm->mkNode(kind::PLUS, translated_children);
-              Node multSig = d_nm->mkNode(kind::MULT, sigma, pow2(bvsize));
-              d_bvToIntCache[current] =
-                  d_nm->mkNode(kind::MINUS, plus, multSig);
-              d_rangeAssertions.insert(d_nm->mkNode(kind::LEQ, d_zero, sigma));
-              d_rangeAssertions.insert(d_nm->mkNode(kind::LEQ, sigma, d_one));
-              d_rangeAssertions.insert(
-                  mkRangeConstraint(d_bvToIntCache[current], bvsize));
-              break;
-            }
-            case kind::BITVECTOR_MULT:
-            {
-              uint64_t bvsize = current[0].getType().getBitVectorSize();
-              /**
-               * we use a similar trick to the one used for addition.
-               * Tr(a*b) is Tr(a)*Tr(b)-(sigma*2^k),
-               * with k being the bit width,
-               * and sigma is between [0, 2^k - 1).
-               */
-              Node sigma = d_nm->mkSkolem(
-                  "__bvToInt_sigma_var",
-                  d_nm->integerType(),
-                  "Variable introduced in bvToInt pass to avoid integer mod");
-              Node mult = d_nm->mkNode(kind::MULT, translated_children);
-              Node multSig = d_nm->mkNode(kind::MULT, sigma, pow2(bvsize));
-              d_bvToIntCache[current] =
-                  d_nm->mkNode(kind::MINUS, mult, multSig);
-              d_rangeAssertions.insert(
-                  mkRangeConstraint(d_bvToIntCache[current], bvsize));
-              if (translated_children[0].isConst()
-                  || translated_children[1].isConst())
-              {
-                /*
-                 * based on equation (23), section 3.2.3 of:
-                 * Bozzano et al.
-                 * Encoding RTL Constructs for MathSAT: a Preliminary Report.
-                 */
-                // this is an optimization when one of the children is constant
-                Node c = translated_children[0].isConst()
-                             ? translated_children[0]
-                             : translated_children[1];
-                d_rangeAssertions.insert(
-                    d_nm->mkNode(kind::LEQ, d_zero, sigma));
-                // the value of sigma is bounded by (c - 1)
-                // where c is the constant multiplicand
-                d_rangeAssertions.insert(d_nm->mkNode(kind::LT, sigma, c));
-              }
-              else
-              {
-                d_rangeAssertions.insert(mkRangeConstraint(sigma, bvsize));
-              }
-              break;
-            }
-            case kind::BITVECTOR_UDIV_TOTAL:
-            {
-              uint64_t bvsize = current[0].getType().getBitVectorSize();
-              // we use an ITE for the case where the second operand is 0.
-              Node pow2BvSize = pow2(bvsize);
-              Node divNode =
-                  d_nm->mkNode(kind::INTS_DIVISION_TOTAL, translated_children);
-              Node ite = d_nm->mkNode(
-                  kind::ITE,
-                  d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero),
-                  d_nm->mkNode(kind::MINUS, pow2BvSize, d_one),
-                  divNode);
-              d_bvToIntCache[current] = ite;
-              break;
-            }
-            case kind::BITVECTOR_UREM_TOTAL:
-            {
-              // we use an ITE for the case where the second operand is 0.
-              Node modNode =
-                  d_nm->mkNode(kind::INTS_MODULUS_TOTAL, translated_children);
-              Node ite = d_nm->mkNode(
-                  kind::ITE,
-                  d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero),
-                  translated_children[0],
-                  modNode);
-              d_bvToIntCache[current] = ite;
-              break;
-            }
-            case kind::BITVECTOR_NOT:
-            {
-              uint64_t bvsize = current[0].getType().getBitVectorSize();
-              // we use a specified function to generate the node.
-              d_bvToIntCache[current] =
-                  createBVNotNode(translated_children[0], bvsize);
-              break;
-            }
-            case kind::BITVECTOR_TO_NAT:
-            {
-              // In this case, we already translated the child to integer.
-              // So the result is the translated child.
-              d_bvToIntCache[current] = translated_children[0];
-              break;
-            }
-            case kind::BITVECTOR_AND:
-            {
-              // Construct an ite, based on granularity.
-              uint64_t bvsize = current[0].getType().getBitVectorSize();
-              Assert(translated_children.size() == 2);
-              Node newNode = createBitwiseNode(translated_children[0],
-                                               translated_children[1],
-                                               bvsize,
-                                               granularity,
-                                               &oneBitAnd);
-              d_bvToIntCache[current] = newNode;
-              break;
-            }
-            case kind::BITVECTOR_SHL:
-            {
-              /**
-               * a << b is a*2^b.
-               * The exponentiation is simulated by an ite.
-               * Only cases where b <= bit width are considered.
-               * Otherwise, the result is 0.
-               */
-              uint64_t bvsize = current[0].getType().getBitVectorSize();
-              Node newNode = createShiftNode(translated_children, bvsize, true);
-              d_bvToIntCache[current] = newNode;
-              break;
-            }
-            case kind::BITVECTOR_LSHR:
-            {
-              /**
-               * a >> b is a div 2^b.
-               * The exponentiation is simulated by an ite.
-               * Only cases where b <= bit width are considered.
-               * Otherwise, the result is 0.
-               */
-              uint64_t bvsize = current[0].getType().getBitVectorSize();
-              Node newNode = createShiftNode(translated_children, bvsize, false);
-              d_bvToIntCache[current] = newNode;
-              break;
-            }
-            case kind::BITVECTOR_ASHR:
-            {
-              /*  From SMT-LIB2:
-               *  (bvashr s t) abbreviates
-               *     (ite (= ((_ extract |m-1| |m-1|) s) #b0)
-               *          (bvlshr s t)
-               *          (bvnot (bvlshr (bvnot s) t)))
-               *
-               *  Equivalently:
-               *  (bvashr s t) abbreviates
-               *      (ite (bvult s 100000...)
-               *           (bvlshr s t)
-               *           (bvnot (bvlshr (bvnot s) t)))
-               *
-               */
-              uint64_t bvsize = current[0].getType().getBitVectorSize();
-              // signed_min is 100000...
-              Node signed_min = pow2(bvsize - 1);
-              Node condition =
-                  d_nm->mkNode(kind::LT, translated_children[0], signed_min);
-              Node thenNode = createShiftNode(translated_children, bvsize, false);
-              vector<Node> children = {
-                  createBVNotNode(translated_children[0], bvsize),
-                  translated_children[1]};
-              Node elseNode = createBVNotNode(
-                  createShiftNode(children, bvsize, false), bvsize);
-              Node ite = d_nm->mkNode(kind::ITE, condition, thenNode, elseNode);
-              d_bvToIntCache[current] = ite;
-              break;
-            }
-            case kind::BITVECTOR_ITE:
-            {
-              // Lifted to a boolean ite.
-              Node cond = d_nm->mkNode(kind::EQUAL, translated_children[0], d_one);
-              Node ite = d_nm->mkNode(
-                  kind::ITE, cond, translated_children[1], translated_children[2]);
-              d_bvToIntCache[current] = ite;
-              break;
-            }
-            case kind::BITVECTOR_ZERO_EXTEND:
-            {
-              d_bvToIntCache[current] = translated_children[0];
-              break;
-            }
-            case kind::BITVECTOR_SIGN_EXTEND:
-            {
-              uint64_t bvsize = current[0].getType().getBitVectorSize();
-              Node arg = translated_children[0];
-              if (arg.isConst())
-              {
-                Rational c(arg.getConst<Rational>());
-                Rational twoToKMinusOne(intpow2(bvsize - 1));
-                uint64_t amount = bv::utils::getSignExtendAmount(current);
-                /* 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)
-                {
-                  d_bvToIntCache[current] = arg;
-                }
-                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;
-                  Node result = d_nm->mkConst(sum);
-                  d_bvToIntCache[current] = result;
-                }
-              }
-              else
-              {
-                uint64_t amount = bv::utils::getSignExtendAmount(current);
-                if (amount == 0)
-                {
-                  d_bvToIntCache[current] = translated_children[0];
-                }
-                else
-                {
-                  Rational twoToKMinusOne(intpow2(bvsize - 1));
-                  Node minSigned = d_nm->mkConst(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, arg, minSigned);
-                  Node thenResult = arg;
-                  Node left = maxInt(amount);
-                  Node mul = d_nm->mkNode(kind::MULT, left, pow2(bvsize));
-                  Node sum = d_nm->mkNode(kind::PLUS, mul, arg);
-                  Node elseResult = sum;
-                  Node ite = d_nm->mkNode(
-                      kind::ITE, condition, thenResult, elseResult);
-                  d_bvToIntCache[current] = ite;
-                }
-              }
-              break;
-            }
-            case kind::BITVECTOR_CONCAT:
-            {
-              // (concat a b) translates to a*2^k+b, k being the bitwidth of b.
-              uint64_t bvsizeRight = current[1].getType().getBitVectorSize();
-              Node pow2BvSizeRight = pow2(bvsizeRight);
-              Node a = d_nm->mkNode(
-                  kind::MULT, translated_children[0], pow2BvSizeRight);
-              Node b = translated_children[1];
-              Node sum = d_nm->mkNode(kind::PLUS, a, b);
-              d_bvToIntCache[current] = sum;
-              break;
-            }
-            case kind::BITVECTOR_EXTRACT:
-            {
-              // ((_ extract i j) a) is a / 2^j mod 2^{i-j+1}
-              // current = a[i:j]
-              Node a = current[0];
-              uint64_t i = bv::utils::getExtractHigh(current);
-              uint64_t j = bv::utils::getExtractLow(current);
-              Assert(d_bvToIntCache.find(a) != d_bvToIntCache.end());
-              Assert(i >= j);
-              Node div = d_nm->mkNode(
-                  kind::INTS_DIVISION_TOTAL, d_bvToIntCache[a].get(), pow2(j));
-              d_bvToIntCache[current] = modpow2(div, i - j + 1);
-              break;
-            }
-            case kind::EQUAL:
-            {
-              d_bvToIntCache[current] =
-                  d_nm->mkNode(kind::EQUAL, translated_children);
-              break;
-            }
-            case kind::BITVECTOR_ULT:
-            {
-              d_bvToIntCache[current] =
-                  d_nm->mkNode(kind::LT, translated_children);
-              break;
-            }
-            case kind::BITVECTOR_ULE:
-            {
-              d_bvToIntCache[current] =
-                  d_nm->mkNode(kind::LEQ, translated_children);
-              break;
-            }
-            case kind::BITVECTOR_UGT:
-            {
-              d_bvToIntCache[current] =
-                  d_nm->mkNode(kind::GT, translated_children);
-              break;
-            }
-            case kind::BITVECTOR_UGE:
-            {
-              d_bvToIntCache[current] =
-                  d_nm->mkNode(kind::GEQ, translated_children);
-              break;
-            }
-            case kind::LT:
-            {
-              d_bvToIntCache[current] =
-                  d_nm->mkNode(kind::LT, translated_children);
-              break;
-            }
-            case kind::LEQ:
-            {
-              d_bvToIntCache[current] =
-                  d_nm->mkNode(kind::LEQ, translated_children);
-              break;
-            }
-            case kind::GT:
-            {
-              d_bvToIntCache[current] =
-                  d_nm->mkNode(kind::GT, translated_children);
-              break;
-            }
-            case kind::GEQ:
-            {
-              d_bvToIntCache[current] =
-                  d_nm->mkNode(kind::GEQ, translated_children);
-              break;
-            }
-            case kind::ITE:
-            {
-              d_bvToIntCache[current] = d_nm->mkNode(oldKind, translated_children);
-              break;
-            }
-            case kind::APPLY_UF:
-            {
-              /*
-               * We replace all BV-sorts of the domain with INT
-               * If the range is a BV sort, we replace it with INT
-               */
-
-              // construct the new function symbol.
-              Node bvUF = current.getOperator();
-              Node intUF;
-              TypeNode tn = current.getOperator().getType();
-              TypeNode bvRange = tn.getRangeType();
-              if (d_bvToIntCache.find(bvUF) != d_bvToIntCache.end())
-              {
-                intUF = d_bvToIntCache[bvUF];
-              }
-              else
-              {
-                // The function symbol has not been converted yet
-                vector<TypeNode> bvDomain = tn.getArgTypes();
-                vector<TypeNode> intDomain;
-                /**
-                 * if the original range is a bit-vector sort,
-                 * the new range should be an integer sort.
-                 * Otherwise, we keep the original range.
-                 * Similarly for the domains.
-                 */
-                TypeNode intRange =
-                    bvRange.isBitVector() ? d_nm->integerType() : bvRange;
-                for (TypeNode d : bvDomain)
-                {
-                  intDomain.push_back(d.isBitVector() ? d_nm->integerType()
-                                                      : d);
-                }
-                ostringstream os;
-                os << "__bvToInt_fun_" << bvUF << "_int";
-                intUF =
-                    d_nm->mkSkolem(os.str(),
-                                   d_nm->mkFunctionType(intDomain, intRange),
-                                   "bv2int function");
-                // Insert the function symbol itself to the cache
-                d_bvToIntCache[bvUF] = intUF;
-
-                // introduce a `define-fun` in the smt-engine to keep
-                // the correspondence between the original
-                // function symbol and the new one.
-                defineBVUFAsIntUF(bvUF);
-              }
-              /**
-               * higher order logic allows comparing between functions
-               * The current translation does not support this,
-               * as the translated functions may be different outside
-               * of the bounds that were relevant for the original
-               * bit-vectors.
-               */
-              if (childrenTypesChanged(current) && options::ufHo())
-              {
-                throw TypeCheckingException(
-                    current.toExpr(),
-                    string("Cannot translate to Int: ") + current.toString());
-              }
-
-              // Now that the translated function symbol was
-              // created, we translate the applicatio and add to the cache.
-              // Additionally, we add
-              // range constraints induced by the original BV width of the
-              // the functions range (codomain)..
-              translated_children.insert(translated_children.begin(), intUF);
-              // Insert the translated application term to the cache
-              d_bvToIntCache[current] =
-                  d_nm->mkNode(kind::APPLY_UF, translated_children);
-              // Add range constraints if necessary.
-              // If the original range was a BV sort, the current application of
-              // the function Must be within the range determined by the
-              // bitwidth.
-              if (bvRange.isBitVector())
-              {
-                Node m = d_bvToIntCache[current];
-                d_rangeAssertions.insert(
-                    mkRangeConstraint(d_bvToIntCache[current],
-                                      current.getType().getBitVectorSize()));
-              }
-              break;
-            }
-            default:
-            {
-              // In the default case, we have reached an operator that we do not
-              // translate directly to integers. The children whose types have
-              // changed from bv to int should be adjusted back to bv and then
-              // this term is reconstructed.
-              TypeNode resultingType;
-              if (current.getType().isBitVector())
-              {
-                resultingType = d_nm->integerType();
-              }
-              else
-              {
-                resultingType = current.getType();
-              }
-              Node reconstruction =
-                  reconstructNode(current, resultingType, translated_children);
-              d_bvToIntCache[current] = reconstruction;
-              break;
-            }
+            translated_children.push_back(d_bvToIntCache[current[i]]);
           }
+          Node translation =
+              translateWithChildren(current, translated_children);
+          d_bvToIntCache[current] = translation;
         }
         toVisit.pop_back();
       }
     }
   }
-  return d_bvToIntCache[n];
+  return d_bvToIntCache[n].get();
 }
 
-void BVToInt::defineBVUFAsIntUF(Node bvUF)
+Node BVToInt::translateWithChildren(Node original,
+                                    const vector<Node>& translated_children)
+{
+  // The translation of the original node is determined by the kind of
+  // the node.
+  kind::Kind_t oldKind = original.getKind();
+  // ultbv and sltbv were supposed to be eliminated before this point.
+  Assert(oldKind != kind::BITVECTOR_ULTBV);
+  Assert(oldKind != kind::BITVECTOR_SLTBV);
+  Node returnNode;
+  switch (oldKind)
+  {
+    case kind::BITVECTOR_PLUS:
+    {
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      /**
+       * we avoid modular arithmetics by the addition of an
+       * indicator variable sigma.
+       * Tr(a+b) is Tr(a)+Tr(b)-(sigma*2^k),
+       * with k being the bit width,
+       * and sigma being either 0 or 1.
+       */
+      Node sigma = d_nm->mkSkolem(
+          "__bvToInt_sigma_var",
+          d_nm->integerType(),
+          "Variable introduced in bvToInt pass to avoid integer mod");
+      Node plus = d_nm->mkNode(kind::PLUS, translated_children);
+      Node multSig = d_nm->mkNode(kind::MULT, sigma, pow2(bvsize));
+      returnNode = d_nm->mkNode(kind::MINUS, plus, multSig);
+      d_rangeAssertions.insert(d_nm->mkNode(kind::LEQ, d_zero, sigma));
+      d_rangeAssertions.insert(d_nm->mkNode(kind::LEQ, sigma, d_one));
+      d_rangeAssertions.insert(
+          mkRangeConstraint(returnNode, bvsize));
+      break;
+    }
+    case kind::BITVECTOR_MULT:
+    {
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      /**
+       * we use a similar trick to the one used for addition.
+       * Tr(a*b) is Tr(a)*Tr(b)-(sigma*2^k),
+       * with k being the bit width,
+       * and sigma is between [0, 2^k - 1).
+       */
+      Node sigma = d_nm->mkSkolem(
+          "__bvToInt_sigma_var",
+          d_nm->integerType(),
+          "Variable introduced in bvToInt pass to avoid integer mod");
+      Node mult = d_nm->mkNode(kind::MULT, translated_children);
+      Node multSig = d_nm->mkNode(kind::MULT, sigma, pow2(bvsize));
+      returnNode = d_nm->mkNode(kind::MINUS, mult, multSig);
+      d_rangeAssertions.insert(
+          mkRangeConstraint(returnNode, bvsize));
+      if (translated_children[0].isConst() || translated_children[1].isConst())
+      {
+        /*
+         * based on equation (23), section 3.2.3 of:
+         * Bozzano et al.
+         * Encoding RTL Constructs for MathSAT: a Preliminary Report.
+         */
+        // this is an optimization when one of the children is constant
+        Node c = translated_children[0].isConst() ? translated_children[0]
+                                                  : translated_children[1];
+        d_rangeAssertions.insert(d_nm->mkNode(kind::LEQ, d_zero, sigma));
+        // the value of sigma is bounded by (c - 1)
+        // where c is the constant multiplicand
+        d_rangeAssertions.insert(d_nm->mkNode(kind::LT, sigma, c));
+      }
+      else
+      {
+        d_rangeAssertions.insert(mkRangeConstraint(sigma, bvsize));
+      }
+      break;
+    }
+    case kind::BITVECTOR_UDIV_TOTAL:
+    {
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      // we use an ITE for the case where the second operand is 0.
+      Node pow2BvSize = pow2(bvsize);
+      Node divNode =
+          d_nm->mkNode(kind::INTS_DIVISION_TOTAL, translated_children);
+      returnNode = d_nm->mkNode(
+          kind::ITE,
+          d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero),
+          d_nm->mkNode(kind::MINUS, pow2BvSize, d_one),
+          divNode);
+      break;
+    }
+    case kind::BITVECTOR_UREM_TOTAL:
+    {
+      // we use an ITE for the case where the second operand is 0.
+      Node modNode =
+          d_nm->mkNode(kind::INTS_MODULUS_TOTAL, translated_children);
+      returnNode = d_nm->mkNode(
+          kind::ITE,
+          d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero),
+          translated_children[0],
+          modNode);
+      break;
+    }
+    case kind::BITVECTOR_NOT:
+    {
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      // we use a specified function to generate the node.
+      returnNode = createBVNotNode(translated_children[0], bvsize);
+      break;
+    }
+    case kind::BITVECTOR_TO_NAT:
+    {
+      // In this case, we already translated the child to integer.
+      // So the result is the translated child.
+      returnNode = translated_children[0];
+      break;
+    }
+    case kind::BITVECTOR_AND:
+    {
+      // Construct an ite, based on granularity.
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      Assert(translated_children.size() == 2);
+      Node newNode = createBitwiseNode(translated_children[0],
+                                       translated_children[1],
+                                       bvsize,
+                                       options::BVAndIntegerGranularity(),
+                                       &oneBitAnd);
+      returnNode = newNode;
+      break;
+    }
+    case kind::BITVECTOR_SHL:
+    {
+      /**
+       * a << b is a*2^b.
+       * The exponentiation is simulated by an ite.
+       * Only cases where b <= bit width are considered.
+       * Otherwise, the result is 0.
+       */
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      returnNode = createShiftNode(translated_children, bvsize, true);
+      break;
+    }
+    case kind::BITVECTOR_LSHR:
+    {
+      /**
+       * a >> b is a div 2^b.
+       * The exponentiation is simulated by an ite.
+       * Only cases where b <= bit width are considered.
+       * Otherwise, the result is 0.
+       */
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      returnNode = createShiftNode(translated_children, bvsize, false);
+      break;
+    }
+    case kind::BITVECTOR_ASHR:
+    {
+      /*  From SMT-LIB2:
+       *  (bvashr s t) abbreviates
+       *     (ite (= ((_ extract |m-1| |m-1|) s) #b0)
+       *          (bvlshr s t)
+       *          (bvnot (bvlshr (bvnot s) t)))
+       *
+       *  Equivalently:
+       *  (bvashr s t) abbreviates
+       *      (ite (bvult s 100000...)
+       *           (bvlshr s t)
+       *           (bvnot (bvlshr (bvnot s) t)))
+       *
+       */
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      // signed_min is 100000...
+      Node signed_min = pow2(bvsize - 1);
+      Node condition =
+          d_nm->mkNode(kind::LT, translated_children[0], signed_min);
+      Node thenNode = createShiftNode(translated_children, bvsize, false);
+      vector<Node> children = {createBVNotNode(translated_children[0], bvsize),
+                               translated_children[1]};
+      Node elseNode =
+          createBVNotNode(createShiftNode(children, bvsize, false), bvsize);
+      returnNode = d_nm->mkNode(kind::ITE, condition, thenNode, elseNode);
+      break;
+    }
+    case kind::BITVECTOR_ITE:
+    {
+      // Lifted to a boolean ite.
+      Node cond = d_nm->mkNode(kind::EQUAL, translated_children[0], d_one);
+      returnNode = d_nm->mkNode(
+          kind::ITE, cond, translated_children[1], translated_children[2]);
+      break;
+    }
+    case kind::BITVECTOR_ZERO_EXTEND:
+    {
+      returnNode = translated_children[0];
+      break;
+    }
+    case kind::BITVECTOR_SIGN_EXTEND:
+    {
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      Node arg = translated_children[0];
+      if (arg.isConst())
+      {
+        Rational c(arg.getConst<Rational>());
+        Rational twoToKMinusOne(intpow2(bvsize - 1));
+        uint64_t amount = bv::utils::getSignExtendAmount(original);
+        /* 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 = arg;
+        }
+        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(sum);
+        }
+      }
+      else
+      {
+        uint64_t amount = bv::utils::getSignExtendAmount(original);
+        if (amount == 0)
+        {
+          returnNode = translated_children[0];
+        }
+        else
+        {
+          Rational twoToKMinusOne(intpow2(bvsize - 1));
+          Node minSigned = d_nm->mkConst(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, arg, minSigned);
+          Node thenResult = arg;
+          Node left = maxInt(amount);
+          Node mul = d_nm->mkNode(kind::MULT, left, pow2(bvsize));
+          Node sum = d_nm->mkNode(kind::PLUS, mul, arg);
+          Node elseResult = sum;
+          Node ite = d_nm->mkNode(kind::ITE, condition, thenResult, elseResult);
+          returnNode = ite;
+        }
+      }
+      break;
+    }
+    case kind::BITVECTOR_CONCAT:
+    {
+      // (concat a b) translates to a*2^k+b, k being the bitwidth of b.
+      uint64_t bvsizeRight = original[1].getType().getBitVectorSize();
+      Node pow2BvSizeRight = pow2(bvsizeRight);
+      Node a =
+          d_nm->mkNode(kind::MULT, translated_children[0], pow2BvSizeRight);
+      Node b = translated_children[1];
+      returnNode = d_nm->mkNode(kind::PLUS, a, b);
+      break;
+    }
+    case kind::BITVECTOR_EXTRACT:
+    {
+      // ((_ extract i j) a) is a / 2^j mod 2^{i-j+1}
+      // original = a[i:j]
+      uint64_t i = bv::utils::getExtractHigh(original);
+      uint64_t j = bv::utils::getExtractLow(original);
+      Assert(i >= j);
+      Node div = d_nm->mkNode(
+          kind::INTS_DIVISION_TOTAL, translated_children[0], pow2(j));
+      returnNode = modpow2(div, i - j + 1);
+      break;
+    }
+    case kind::EQUAL:
+    {
+      returnNode = d_nm->mkNode(kind::EQUAL, translated_children);
+      break;
+    }
+    case kind::BITVECTOR_ULT:
+    {
+      returnNode = d_nm->mkNode(kind::LT, translated_children);
+      break;
+    }
+    case kind::BITVECTOR_ULE:
+    {
+      returnNode = d_nm->mkNode(kind::LEQ, translated_children);
+      break;
+    }
+    case kind::BITVECTOR_UGT:
+    {
+      returnNode = d_nm->mkNode(kind::GT, translated_children);
+      break;
+    }
+    case kind::BITVECTOR_UGE:
+    {
+      returnNode = d_nm->mkNode(kind::GEQ, translated_children);
+      break;
+    }
+    case kind::LT:
+    {
+      returnNode = d_nm->mkNode(kind::LT, translated_children);
+      break;
+    }
+    case kind::LEQ:
+    {
+      returnNode = d_nm->mkNode(kind::LEQ, translated_children);
+      break;
+    }
+    case kind::GT:
+    {
+      returnNode = d_nm->mkNode(kind::GT, translated_children);
+      break;
+    }
+    case kind::GEQ:
+    {
+      returnNode = d_nm->mkNode(kind::GEQ, translated_children);
+      break;
+    }
+    case kind::ITE:
+    {
+      returnNode = d_nm->mkNode(oldKind, translated_children);
+      break;
+    }
+    case kind::APPLY_UF:
+    {
+      /**
+       * higher order logic allows comparing between functions
+       * The current translation does not support this,
+       * as the translated functions may be different outside
+       * of the bounds that were relevant for the original
+       * bit-vectors.
+       */
+      if (childrenTypesChanged(original) && options::ufHo())
+      {
+        throw TypeCheckingException(
+            original.toExpr(),
+            string("Cannot translate to Int: ") + original.toString());
+      }
+      // Insert the translated application term to the cache
+      returnNode = d_nm->mkNode(kind::APPLY_UF, translated_children);
+      // Add range constraints if necessary.
+      // If the original range was a BV sort, the original application of
+      // the function Must be within the range determined by the
+      // bitwidth.
+      if (original.getType().isBitVector())
+      {
+        d_rangeAssertions.insert(mkRangeConstraint(
+            returnNode, original.getType().getBitVectorSize()));
+      }
+      break;
+    }
+    default:
+    {
+      // In the default case, we have reached an operator that we do not
+      // translate directly to integers. The children whose types have
+      // changed from bv to int should be adjusted back to bv and then
+      // this term is reconstructed.
+      TypeNode resultingType;
+      if (original.getType().isBitVector())
+      {
+        resultingType = d_nm->integerType();
+      }
+      else
+      {
+        resultingType = original.getType();
+      }
+      Node reconstruction =
+          reconstructNode(original, resultingType, translated_children);
+      returnNode = reconstruction;
+      break;
+    }
+  }
+  Trace("bv-to-int-debug") << "original: " << original << endl;
+  Trace("bv-to-int-debug") << "returnNode: " << returnNode << endl;
+  return returnNode;
+}
+
+Node BVToInt::translateNoChildren(Node original)
+{
+  Node translation;
+  Assert(original.isVar() || original.isConst());
+  if (original.isVar())
+  {
+    if (original.getType().isBitVector())
+    {
+        Node newVar = d_nm->mkSkolem("__bvToInt_var",
+                                     d_nm->integerType(),
+                                     "Variable introduced in bvToInt "
+                                     "pass instead of original variable "
+                                         + original.toString());
+        uint64_t bvsize = original.getType().getBitVectorSize();
+        translation = newVar;
+        d_rangeAssertions.insert(mkRangeConstraint(newVar, bvsize));
+        std::vector<Expr> args;
+        Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize));
+        Node newNode = d_nm->mkNode(intToBVOp, newVar);
+        smt::currentSmtEngine()->defineFunction(
+            original.toExpr(), args, newNode.toExpr(), true);
+    }
+    else if (original.getType().isFunction())
+    {
+      translation = translateFunctionSymbol(original);
+    }
+    else
+    {
+      // variables other than bit-vector variables and function symbols
+      // are left intact
+      translation = original;
+    }
+  }
+  else
+  {
+    // original is a const
+    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>(c);
+    }
+    else
+    {
+      // Other constants stay the same.
+      translation = original;
+    }
+  }
+  return translation;
+}
+
+Node BVToInt::translateFunctionSymbol(Node bvUF)
+{
+  // construct the new function symbol.
+  Node intUF;
+  TypeNode tn = bvUF.getType();
+  TypeNode bvRange = tn.getRangeType();
+  // The function symbol has not been converted yet
+  vector<TypeNode> bvDomain = tn.getArgTypes();
+  vector<TypeNode> intDomain;
+  /**
+   * if the original range is a bit-vector sort,
+   * the new range should be an integer sort.
+   * Otherwise, we keep the original range.
+   * Similarly for the domains.
+   */
+  TypeNode intRange = bvRange.isBitVector() ? d_nm->integerType() : bvRange;
+  for (TypeNode d : bvDomain)
+  {
+    intDomain.push_back(d.isBitVector() ? d_nm->integerType() : d);
+  }
+  ostringstream os;
+  os << "__bvToInt_fun_" << bvUF << "_int";
+  intUF = d_nm->mkSkolem(
+      os.str(), d_nm->mkFunctionType(intDomain, intRange), "bv2int function");
+  // introduce a `define-fun` in the smt-engine to keep
+  // the correspondence between the original
+  // function symbol and the new one.
+  defineBVUFAsIntUF(bvUF, intUF);
+  return intUF;
+}
+
+void BVToInt::defineBVUFAsIntUF(Node bvUF, Node intUF)
 {
   // This function should only be called after translating
   // the function symbol to a new function symbol
   // with the right domain and range.
-  Assert(d_bvToIntCache.find(bvUF) != d_bvToIntCache.end());
 
   // get domain and range of the original function
   TypeNode tn = bvUF.getType();
   vector<TypeNode> bvDomain = tn.getArgTypes();
   TypeNode bvRange = tn.getRangeType();
 
-  // get the translated function symbol
-  Node intUF = d_bvToIntCache[bvUF];
-
-  // create a symbolic  application to be used in define-fun
-
   // symbolic arguments of original function
   vector<Expr> args;
   // children of the new symbolic application
@@ -1042,7 +1027,7 @@ Node BVToInt::createBitwiseNode(Node x,
    * If it is greater than bvsize, it is set to bvsize.
    * Otherwise, it is set to the closest (going down)  divider of bvsize.
    */
-  Assert(granularity > 0);
+  Assert(0 < granularity && granularity <= 8);
   if (granularity > bvsize)
   {
     granularity = bvsize;
diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h
index bec8a9a21..db2d08b7d 100644
--- a/src/preprocessing/passes/bv_to_int.h
+++ b/src/preprocessing/passes/bv_to_int.h
@@ -292,8 +292,33 @@ class BVToInt : public PreprocessingPass
    * This is useful, for example, when asking
    * for a model-value of a term that includes the
    * original UF f.
+   * @param bvUF the original function
+   * @param intUF the translated function
    */
-  void defineBVUFAsIntUF(Node bvUF);
+  void 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);
+
+  /**
+   * Performs the actual translation to integers for nodes
+   * that have children.
+   */
+  Node translateWithChildren(Node original,
+                             const vector<Node>& translated_children);
+
+  /**
+   * Performs the actual translation to integers for nodes
+   * that don't have children (variables, constants, uninterpreted function
+   * symbols).
+   */
+  Node translateNoChildren(Node original);
+
   /**
    * Caches for the different functions
    */