From 1cecdb3b4d8be47d446be5d33cc4d3063061d2b3 Mon Sep 17 00:00:00 2001
From: yoni206 <yoni206@users.noreply.github.com>
Date: Tue, 13 Oct 2020 23:28:36 -0700
Subject: bv2int: rewritings and unsat cores (#5263)

This commit fixes several issues with bv-to-int preprocessing pass, mostly raised by @ajreynol:

1. make sure to rewrite the processed node before and after processing it
2. use the new `mkAnd` function
3. remove `--no-check-unsat-cores` from tests whenever possible
4. add new tests from #5230 . These tests now pass, and so this PR closes #5230 if merged. This also makes #5253 redundant.
5. remove an unused test
---
 src/preprocessing/passes/bv_to_int.cpp | 53 +++++++++++-----------------------
 1 file changed, 17 insertions(+), 36 deletions(-)

(limited to 'src/preprocessing/passes')

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 6f6ff3bae..8906ddeea 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -260,6 +260,8 @@ Node BVToInt::eliminationPass(Node n)
  */
 Node BVToInt::bvToInt(Node n)
 {
+  // make sure the node is re-written before processing it.
+  n = Rewriter::rewrite(n);
   n = makeBinary(n);
   n = eliminationPass(n);
   // binarize again, in case the elimination pass introduced
@@ -947,26 +949,17 @@ PreprocessingPassResult BVToInt::applyInternal(
 void BVToInt::addFinalizeRangeAssertions(
     AssertionPipeline* assertionsToPreprocess)
 {
+  // collect the range assertions from d_rangeAssertions
+  // (which is a context-dependent set)
+  // into a vector.
   vector<Node> vec_range;
   vec_range.assign(d_rangeAssertions.key_begin(), d_rangeAssertions.key_end());
-  if (vec_range.size() == 0)
-  {
-    return;
-  }
-  if (vec_range.size() == 1)
-  {
-    assertionsToPreprocess->push_back(vec_range[0]);
-    Trace("bv-to-int-debug")
-        << "range constraints: " << vec_range[0].toString() << std::endl;
-  }
-  else if (vec_range.size() >= 2)
-  {
-    Node rangeAssertions =
-        Rewriter::rewrite(d_nm->mkNode(kind::AND, vec_range));
-    assertionsToPreprocess->push_back(rangeAssertions);
-    Trace("bv-to-int-debug")
-        << "range constraints: " << rangeAssertions.toString() << std::endl;
-  }
+  // conjoin all range assertions and add the conjunction
+  // as a new assertion
+  Node rangeAssertions = Rewriter::rewrite(d_nm->mkAnd(vec_range));
+  assertionsToPreprocess->push_back(rangeAssertions);
+  Trace("bv-to-int-debug") << "range constraints: "
+                           << rangeAssertions.toString() << std::endl;
 }
 
 Node BVToInt::createShiftNode(vector<Node> children,
@@ -1046,24 +1039,12 @@ Node BVToInt::translateQuantifiedFormula(Node quantifiedNode)
                              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);
-  }
-
+  Node ranges = d_nm->mkAnd(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);
-- 
cgit v1.2.3