diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-03-05 19:28:19 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-05 21:28:19 -0600 |
| commit | 59d9aad4839e64e0f6d6b57ff112c418ffbbe9fb (patch) | |
| tree | d0df100653994157bc631e9ca7fe422dd78e29ff /src/preprocessing/passes/bv_to_int.cpp | |
| parent | c6fffe4fd328401f7f7e0757303e8dea5f6c14a4 (diff) | |
Remove partial UDIV/UREM operators. (#6069)
This commit removes the partial UDIV/UREM operator handling. BITVECTOR_UDIV and BITVECTOR_UREM are now total.
Diffstat (limited to 'src/preprocessing/passes/bv_to_int.cpp')
| -rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 22 |
1 files changed, 2 insertions, 20 deletions
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 5043718ca..6ca4a23ec 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -191,20 +191,6 @@ Node BVToInt::eliminationPass(Node n) 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. @@ -357,10 +343,6 @@ 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: @@ -381,7 +363,7 @@ Node BVToInt::translateWithChildren(Node original, returnNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, mult, p2); break; } - case kind::BITVECTOR_UDIV_TOTAL: + case kind::BITVECTOR_UDIV: { uint64_t bvsize = original[0].getType().getBitVectorSize(); // we use an ITE for the case where the second operand is 0. @@ -395,7 +377,7 @@ Node BVToInt::translateWithChildren(Node original, divNode); break; } - case kind::BITVECTOR_UREM_TOTAL: + case kind::BITVECTOR_UREM: { // we use an ITE for the case where the second operand is 0. Node modNode = |