From f92c4476e335322c1eeaa9e15ff5e1fda06181fe Mon Sep 17 00:00:00 2001
From: yoni206 <yoni206@users.noreply.github.com>
Date: Fri, 18 Sep 2020 10:12:04 -0700
Subject: bv2int: quantifiers support (#5080)

This PR adds quantifiers support for bv2int preprocessing pass, and adds regressions that use quantifiers.
---
 src/preprocessing/passes/bv_to_int.cpp | 93 ++++++++++++++++++++++++++++++++++
 src/preprocessing/passes/bv_to_int.h   | 10 ++++
 2 files changed, 103 insertions(+)

(limited to 'src/preprocessing')

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 13ad086e8..2aca33df4 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -645,6 +645,21 @@ Node BVToInt::translateWithChildren(Node original,
       }
       break;
     }
+    case kind::BOUND_VAR_LIST:
+    {
+      returnNode = d_nm->mkNode(oldKind, translated_children);
+      break;
+    }
+    case kind::FORALL:
+    {
+      returnNode = translateQuantifiedFormula(original);
+      break;
+    }
+    case kind::EXISTS:
+    {
+      // Exists is eliminated by the rewriter.
+      Assert(false);
+    }
     default:
     {
       // In the default case, we have reached an operator that we do not
@@ -679,6 +694,20 @@ Node BVToInt::translateNoChildren(Node original)
   {
     if (original.getType().isBitVector())
     {
+      // For bit-vector variables, we create fresh integer variables.
+      if (original.getKind() == kind::BOUND_VARIABLE)
+      {
+        // Range constraints for the bound integer variables are not added now.
+        // they will be added once the quantifier itself is handled.
+        std::stringstream ss;
+        ss << original;
+        translation = d_nm->mkBoundVar(ss.str() + "_int", d_nm->integerType());
+      }
+      else
+      {
+        // New integer variables  that are not bound (symbolic constants)
+        // are added together with range constraints induced by the 
+        // bit-width of the original bit-vector variables.
         Node newVar = d_nm->mkSkolem("__bvToInt_var",
                                      d_nm->integerType(),
                                      "Variable introduced in bvToInt "
@@ -688,6 +717,7 @@ Node BVToInt::translateNoChildren(Node original)
         translation = newVar;
         d_rangeAssertions.insert(mkRangeConstraint(newVar, bvsize));
         defineBVUFAsIntUF(original, newVar);
+      }
     }
     else if (original.getType().isFunction())
     {
@@ -954,6 +984,69 @@ Node BVToInt::createShiftNode(vector<Node> children,
   return ite;
 }
 
+Node BVToInt::translateQuantifiedFormula(Node quantifiedNode)
+{
+  kind::Kind_t k = quantifiedNode.getKind();
+  Node boundVarList = quantifiedNode[0];
+  Assert(boundVarList.getKind() == kind::BOUND_VAR_LIST);
+  // Since bit-vector variables are being translated to
+  // integer variables, we need to substitute the new ones
+  // for the old ones.
+  vector<Node> oldBoundVars;
+  vector<Node> newBoundVars;
+  vector<Node> rangeConstraints;
+  for (Node bv : quantifiedNode[0])
+  {
+    oldBoundVars.push_back(bv);
+    if (bv.getType().isBitVector())
+    {
+      // bit-vector variables are replaced by integer ones.
+      // the new variables induce range constraints based on the
+      // original bit-width.
+      Node newBoundVar = d_bvToIntCache[bv];
+      newBoundVars.push_back(newBoundVar);
+      rangeConstraints.push_back(
+          mkRangeConstraint(newBoundVar, bv.getType().getBitVectorSize()));
+    }
+    else
+    {
+      // variables that are not bit-vectors are not changed
+      newBoundVars.push_back(bv);
+    }
+  }
+
+  // the body of the quantifier
+  Node matrix = d_bvToIntCache[quantifiedNode[1]];
+  // make the substitution
+  matrix = matrix.substitute(oldBoundVars.begin(),
+                             oldBoundVars.end(),
+                             newBoundVars.begin(),
+                             newBoundVars.end());
+  // A node to represent all the range constraints.
+  Node ranges;
+  if (rangeConstraints.size() > 0)
+  {
+    if (rangeConstraints.size() == 1)
+    {
+      ranges = rangeConstraints[0];
+    }
+    else
+    {
+      ranges = d_nm->mkNode(kind::AND, rangeConstraints);
+    }
+    // Add the range constraints to the body of the quantifier.
+    // For "exists", this is added conjunctively
+    // For "forall", this is added to the left side of an implication.
+    matrix = d_nm->mkNode(
+        k == kind::FORALL ? kind::IMPLIES : kind::AND, ranges, matrix);
+  }
+
+  // create the new quantified formula and return it.
+  Node newBoundVarsList = d_nm->mkNode(kind::BOUND_VAR_LIST, newBoundVars);
+  Node result = d_nm->mkNode(kind::FORALL, newBoundVarsList, matrix);
+  return result;
+}
+
 Node BVToInt::createITEFromTable(
     Node x,
     Node y,
diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h
index b84726878..41d8f4904 100644
--- a/src/preprocessing/passes/bv_to_int.h
+++ b/src/preprocessing/passes/bv_to_int.h
@@ -253,6 +253,16 @@ class BVToInt : public PreprocessingPass
    */
   void addFinalizeRangeAssertions(AssertionPipeline* assertionsToPreprocess);
 
+  /**
+   * @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.
-- 
cgit v1.2.3