From: yoni206 <yoni206@users.noreply.github.com>
Date: Tue, 8 Dec 2020 12:51:06 +0000 (-0800)
Subject: bv-to-int: Expand definitions of bvudiv and bvurem during bv-to-int preprocessing... 
X-Git-Tag: cvc5-1.0.0~2481
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c23652b991f064ada72427e2ab4098a105587bef;p=cvc5.git

bv-to-int: Expand definitions of bvudiv and bvurem during bv-to-int preprocessing pass (#5620)

#5544 enforces expandDefinition not to run before preprocessing.
The bv-to-int preprocessing pass used to rely on expandDefinition to replace BITVECTOR_UDIV and BITVECTOR_UREM with their _TOTAL versions.
This PR performs the replacement in the preprocessing pass itself.
A regression that timed out is now fixed and is brought back to the regressions.
---

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 8539e639d..47170c607 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -158,7 +158,7 @@ Node BVToInt::eliminationPass(Node n)
     {
       // current is not the elimination of any previously-visited node
       // current hasn't been eliminated yet.
-      // eliminate operators from it
+      // eliminate operators from it using rewrite rules
       Node currentEliminated =
           FixpointRewriteStrategy<RewriteRule<UdivZero>,
                                   RewriteRule<SdivEliminateFewerBitwiseOps>,
@@ -179,6 +179,21 @@ Node BVToInt::eliminationPass(Node n)
                                   RewriteRule<SltEliminate>,
                                   RewriteRule<SgtEliminate>,
                                   RewriteRule<SgeEliminate>>::apply(current);
+
+      // expanding definitions of udiv and urem
+      if (k == kind::BITVECTOR_UDIV)
+      {
+        currentEliminated = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL,
+                                         currentEliminated[0],
+                                         currentEliminated[1]);
+      }
+      else if (k == kind::BITVECTOR_UREM)
+      {
+        currentEliminated = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL,
+                                         currentEliminated[0],
+                                         currentEliminated[1]);
+      }
+
       // save in the cache
       d_eliminationCache[current] = currentEliminated;
       // also assign the eliminated now to itself to avoid revisiting.
@@ -331,6 +346,10 @@ Node BVToInt::translateWithChildren(Node original,
   // The following variable will only be used in assertions.
   CVC4_UNUSED uint64_t originalNumChildren = original.getNumChildren();
   Node returnNode;
+  // Assert that BITVECTOR_UDIV/UREM were replaced by their
+  // *_TOTAL versions
+  Assert(oldKind != kind::BITVECTOR_UDIV);
+  Assert(oldKind != kind::BITVECTOR_UREM);
   switch (oldKind)
   {
     case kind::BITVECTOR_PLUS:
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7b3f94c1a..56780278b 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2166,6 +2166,7 @@ set(regress_2_tests
   regress2/bv_to_int_ashr.smt2
   regress2/bv_to_int_bitwise.smt2
   regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
+  regress2/bv_to_int_bvmul1.smt2
   regress2/bv_to_int_inc1.smt2
   regress2/bv_to_int_mask_array_1.smt2
   regress2/bv_to_int_mask_array_2.smt2
@@ -2628,7 +2629,6 @@ set(regression_disabled_tests
   regress2/arith/real2int-test.smt2
   regress2/bug396.smt2
   # due to bv2int not handling unsigned/signed division
-  regress2/bv_to_int_bvmul1.smt2
   regress2/nl/dumortier-050317.smt2
   regress2/nl/nt-lemmas-bad.smt2
   regress2/quantifiers/ForElimination-scala-9.smt2