From c23652b991f064ada72427e2ab4098a105587bef Mon Sep 17 00:00:00 2001 From: yoni206 Date: Tue, 8 Dec 2020 04:51:06 -0800 Subject: [PATCH] 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. --- src/preprocessing/passes/bv_to_int.cpp | 21 ++++++++++++++++++++- test/regress/CMakeLists.txt | 2 +- 2 files changed, 21 insertions(+), 2 deletions(-) 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, @@ -179,6 +179,21 @@ Node BVToInt::eliminationPass(Node n) RewriteRule, RewriteRule, RewriteRule>::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 -- 2.30.2