diff options
Diffstat (limited to 'src/preprocessing/passes')
| -rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 21 |
1 files changed, 20 insertions, 1 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<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: |