diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-29 09:48:40 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-29 10:07:26 -0400 |
| commit | a7eba5fcb468399181d06a3684e760aae7185229 (patch) | |
| tree | 255489edc1db176f7ac66f526332ed8ae5855d67 | |
| parent | ebc6c79589ac7065d13f35e5997efdca869a5c58 (diff) | |
SMT-LIB printer updates (some missing cases).
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index c59df6269..b84d86a49 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -241,11 +241,16 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::MULT: case kind::MINUS: case kind::UMINUS: - case kind::DIVISION: case kind::LT: case kind::LEQ: case kind::GT: - case kind::GEQ: out << smtKindString(k) << " "; break; + case kind::GEQ: + case kind::DIVISION: + case kind::DIVISION_TOTAL: + case kind::INTS_DIVISION: + case kind::INTS_DIVISION_TOTAL: + case kind::INTS_MODULUS: + case kind::INTS_MODULUS_TOTAL: out << smtKindString(k) << " "; break; // arrays theory case kind::SELECT: @@ -399,11 +404,16 @@ static string smtKindString(Kind k) throw() { case kind::MULT: return "*"; case kind::MINUS: return "-"; case kind::UMINUS: return "-"; - case kind::DIVISION: return "/"; case kind::LT: return "<"; case kind::LEQ: return "<="; case kind::GT: return ">"; case kind::GEQ: return ">="; + case kind::DIVISION: + case kind::DIVISION_TOTAL: return "/"; + case kind::INTS_DIVISION: + case kind::INTS_DIVISION_TOTAL: return "div"; + case kind::INTS_MODULUS: + case kind::INTS_MODULUS_TOTAL: return "mod"; // arrays theory case kind::SELECT: return "select"; |