From: yoni206 <yoni206@users.noreply.github.com>
Date: Fri, 19 Jun 2020 06:42:59 +0000 (-0700)
Subject: Bv to int elimination bugfix (#4435)
X-Git-Tag: cvc5-1.0.0~3201
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f7036fc10ccdebfc1ca7fffe692cd26dd5eb50fe;p=cvc5.git

Bv to int elimination bugfix (#4435)

fix 1:
------
The wrong flag was checked in the traversal, causing an assertion error [here](https://github.com/CVC4/CVC4/blob/8236d7f9bff3aef4f7b37a15d509b8a11551401f/src/preprocessing/passes/bv_to_int.cpp#L247)
This is fixed in this PR. A test was added as well.

fix 2:
------
It is desirable that bv-to-bool runs before bv-to-int, but this was not the case, and is fixed in this PR.

Do not merge until after competition release (label added).
---

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index e2a38b028..5b125b4b6 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -184,43 +184,41 @@ Node BVToInt::eliminationPass(Node n)
         (d_eliminationCache.find(current) != d_eliminationCache.end());
     bool inRebuildCache =
         (d_rebuildCache.find(current) != d_rebuildCache.end());
-    if (!inRebuildCache)
+    if (!inEliminationCache)
     {
-      // current is not the elimination of any previously-visited node
-      if (!inEliminationCache)
-      {
-        // current hasn't been eliminated yet.
-        // eliminate operators from it
-        Node currentEliminated =
-            FixpointRewriteStrategy<RewriteRule<UdivZero>,
-                                    RewriteRule<SdivEliminate>,
-                                    RewriteRule<SremEliminate>,
-                                    RewriteRule<SmodEliminate>,
-                                    RewriteRule<RepeatEliminate>,
-                                    RewriteRule<ZeroExtendEliminate>,
-                                    RewriteRule<SignExtendEliminate>,
-                                    RewriteRule<RotateRightEliminate>,
-                                    RewriteRule<RotateLeftEliminate>,
-                                    RewriteRule<CompEliminate>,
-                                    RewriteRule<SleEliminate>,
-                                    RewriteRule<SltEliminate>,
-                                    RewriteRule<SgtEliminate>,
-                                    RewriteRule<SgeEliminate>,
-                                    RewriteRule<ShlByConst>,
-                                    RewriteRule<LshrByConst> >::apply(current);
-        // save in the cache
-        d_eliminationCache[current] = currentEliminated;
-        // put the eliminated node in the rebuild cache, but mark that it hasn't
-        // yet been rebuilt by assigning null.
-        d_rebuildCache[currentEliminated] = Node();
-        // Push the eliminated node to the stack
-        toVisit.push_back(currentEliminated);
-        // Add the children to the stack for future processing.
-        toVisit.insert(
-            toVisit.end(), currentEliminated.begin(), currentEliminated.end());
-      }
+      // current hasn't been eliminated yet.
+      // eliminate operators from it
+      Node currentEliminated =
+          FixpointRewriteStrategy<RewriteRule<UdivZero>,
+                                  RewriteRule<SdivEliminate>,
+                                  RewriteRule<SremEliminate>,
+                                  RewriteRule<SmodEliminate>,
+                                  RewriteRule<RepeatEliminate>,
+                                  RewriteRule<ZeroExtendEliminate>,
+                                  RewriteRule<SignExtendEliminate>,
+                                  RewriteRule<RotateRightEliminate>,
+                                  RewriteRule<RotateLeftEliminate>,
+                                  RewriteRule<CompEliminate>,
+                                  RewriteRule<SleEliminate>,
+                                  RewriteRule<SltEliminate>,
+                                  RewriteRule<SgtEliminate>,
+                                  RewriteRule<SgeEliminate>,
+                                  RewriteRule<ShlByConst>,
+                                  RewriteRule<LshrByConst> >::apply(current);
+      // save in the cache
+      d_eliminationCache[current] = currentEliminated;
+      // also assign the eliminated now to itself to avoid revisiting.
+      d_eliminationCache[currentEliminated] = currentEliminated;
+      // put the eliminated node in the rebuild cache, but mark that it hasn't
+      // yet been rebuilt by assigning null.
+      d_rebuildCache[currentEliminated] = Node();
+      // Push the eliminated node to the stack
+      toVisit.push_back(currentEliminated);
+      // Add the children to the stack for future processing.
+      toVisit.insert(
+          toVisit.end(), currentEliminated.begin(), currentEliminated.end());
     }
-    else
+    if (inRebuildCache)
     {
       // current was already added to the rebuild cache.
       if (d_rebuildCache[current].isNull())
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index bb09a6dc0..e3b1163fc 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -357,6 +357,18 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     }
   }
 
+
+  if (options::solveBVAsInt() > 0)
+  {
+    /**
+     * Operations on 1 bits are better handled as Boolean operations
+     * than as integer operations.
+     * Therefore, we enable bv-to-bool, which runs before
+     * the translation to integers.
+     */
+    options::bitvectorToBool.set(true);
+  }
+
   // Disable options incompatible with unsat cores and proofs or output an
   // error if enabled explicitly
   if (options::unsatCores() || options::proof())
@@ -413,16 +425,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       options::preSkolemQuant.set(false);
     }
 
-    if (options::solveBVAsInt() > 0)
-    {
-      /**
-       * Operations on 1 bits are better handled as Boolean operations
-       * than as integer operations.
-       * Therefore, we enable bv-to-bool, which runs before
-       * the translation to integers.
-       */
-      options::bitvectorToBool.set(true);
-    }
 
     if (options::bitvectorToBool())
     {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5ae66f203..690135b54 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -215,8 +215,9 @@ set(regress_0_tests
   regress0/bv/bv_to_int2.smt2
   regress0/bv/bv_to_int_bvmul1.smt2
   regress0/bv/bv_to_int_bvmul2.smt2
-  regress0/bv/bv_to_int_zext.smt2
   regress0/bv/bv_to_int_bitwise.smt2
+  regress0/bv/bv_to_int_elim_err.smt2
+  regress0/bv/bv_to_int_zext.smt2
   regress0/bv/bvuf_to_intuf.smt2
   regress0/bv/bvuf_to_intuf_smtlib.smt2
   regress0/bv/bvuf_to_intuf_sorts.smt2
diff --git a/test/regress/regress0/bv/bv_to_int_elim_err.smt2 b/test/regress/regress0/bv/bv_to_int_elim_err.smt2
new file mode 100644
index 000000000..16731b01e
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_elim_err.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models 
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun _substvar_183_ () (_ BitVec 32))
+(assert (let ((?x15 ((_ sign_extend 0) _substvar_183_))) (bvsle ((_ zero_extend 24) ((_ extract 15 8) (bvadd ?x15 (_ bv4294966758 32)))) (bvadd ?x15 ?x15))))
+(check-sat)
+(exit)