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/printer | |
| 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/printer')
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 6 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 8 |
2 files changed, 2 insertions, 12 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 7ac2da40b..2733e9eef 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -663,15 +663,9 @@ void CvcPrinter::toStreamNode(std::ostream& out, case kind::BITVECTOR_UDIV: op << "BVUDIV"; break; - case kind::BITVECTOR_UDIV_TOTAL: - op << "BVUDIV_TOTAL"; - break; case kind::BITVECTOR_UREM: op << "BVUREM"; break; - case kind::BITVECTOR_UREM_TOTAL: - op << "BVUREM_TOTAL"; - break; case kind::BITVECTOR_SDIV: op << "BVSDIV"; break; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 4f4343128..a34496401 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -741,10 +741,8 @@ void Smt2Printer::toStream(std::ostream& out, case kind::BITVECTOR_PLUS: out << "bvadd "; forceBinary = true; break; case kind::BITVECTOR_SUB: out << "bvsub "; break; case kind::BITVECTOR_NEG: out << "bvneg "; break; - case kind::BITVECTOR_UDIV: - case kind::BITVECTOR_UDIV_TOTAL: out << "bvudiv "; break; - case kind::BITVECTOR_UREM: - case kind::BITVECTOR_UREM_TOTAL: out << "bvurem "; break; + case kind::BITVECTOR_UDIV: out << "bvudiv "; break; + case kind::BITVECTOR_UREM: out << "bvurem "; break; case kind::BITVECTOR_SDIV: out << "bvsdiv "; break; case kind::BITVECTOR_SREM: out << "bvsrem "; break; case kind::BITVECTOR_SMOD: out << "bvsmod "; break; @@ -1144,9 +1142,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::BITVECTOR_PLUS: return "bvadd"; case kind::BITVECTOR_SUB: return "bvsub"; case kind::BITVECTOR_NEG: return "bvneg"; - case kind::BITVECTOR_UDIV_TOTAL: case kind::BITVECTOR_UDIV: return "bvudiv"; - case kind::BITVECTOR_UREM_TOTAL: case kind::BITVECTOR_UREM: return "bvurem"; case kind::BITVECTOR_SDIV: return "bvsdiv"; case kind::BITVECTOR_SREM: return "bvsrem"; |