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/theory/quantifiers/bv_inverter.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/theory/quantifiers/bv_inverter.cpp')
| -rw-r--r-- | src/theory/quantifiers/bv_inverter.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 8d5e98780..bf0765180 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -108,10 +108,10 @@ static bool isInvertible(Kind k, unsigned index) return k == NOT || k == EQUAL || k == BITVECTOR_ULT || k == BITVECTOR_SLT || k == BITVECTOR_COMP || k == BITVECTOR_NOT || k == BITVECTOR_NEG || k == BITVECTOR_CONCAT || k == BITVECTOR_SIGN_EXTEND - || k == BITVECTOR_PLUS || k == BITVECTOR_MULT - || k == BITVECTOR_UREM_TOTAL || k == BITVECTOR_UDIV_TOTAL - || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR - || k == BITVECTOR_LSHR || k == BITVECTOR_ASHR || k == BITVECTOR_SHL; + || k == BITVECTOR_PLUS || k == BITVECTOR_MULT || k == BITVECTOR_UREM + || k == BITVECTOR_UDIV || k == BITVECTOR_AND || k == BITVECTOR_OR + || k == BITVECTOR_XOR || k == BITVECTOR_LSHR || k == BITVECTOR_ASHR + || k == BITVECTOR_SHL; } Node BvInverter::getPathToPv( @@ -314,11 +314,11 @@ Node BvInverter::solveBvLit(Node sv, { ic = utils::getICBvShl(pol, litk, k, index, x, s, t); } - else if (k == BITVECTOR_UREM_TOTAL) + else if (k == BITVECTOR_UREM) { ic = utils::getICBvUrem(pol, litk, k, index, x, s, t); } - else if (k == BITVECTOR_UDIV_TOTAL) + else if (k == BITVECTOR_UDIV) { ic = utils::getICBvUdiv(pol, litk, k, index, x, s, t); } |