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 | |
| 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')
| -rw-r--r-- | src/preprocessing/passes/bv_gauss.cpp | 4 | ||||
| -rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 22 | ||||
| -rw-r--r-- | src/preprocessing/passes/unconstrained_simplifier.cpp | 2 |
3 files changed, 4 insertions, 24 deletions
diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index d8b309609..b743f580d 100644 --- a/src/preprocessing/passes/bv_gauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -164,7 +164,7 @@ unsigned BVGauss::getMinBwExpr(Node expr) break; } - case kind::BITVECTOR_UREM_TOTAL: + case kind::BITVECTOR_UREM: case kind::BITVECTOR_LSHR: case kind::BITVECTOR_ASHR: { @@ -213,7 +213,7 @@ unsigned BVGauss::getMinBwExpr(Node expr) default: { - /* BITVECTOR_UDIV_TOTAL (since x / 0 = -1) + /* BITVECTOR_UDIV (since x / 0 = -1) * BITVECTOR_NOT * BITVECTOR_NEG * BITVECTOR_SHL */ 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 = diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index e50548ff8..a7cc36630 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -364,8 +364,6 @@ void UnconstrainedSimplifier::processUnconstrained() case kind::BITVECTOR_ASHR: case kind::BITVECTOR_UDIV: case kind::BITVECTOR_UREM: - case kind::BITVECTOR_UDIV_TOTAL: - case kind::BITVECTOR_UREM_TOTAL: case kind::BITVECTOR_SDIV: case kind::BITVECTOR_SREM: case kind::BITVECTOR_SMOD: |