diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-29 13:03:03 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-29 13:03:03 -0400 |
| commit | 79052f8209cb871e6159d148b0586c562948a2fd (patch) | |
| tree | d2c7ba8c1688addfaeb284eebf85b922a8eb91b6 /src/printer | |
| parent | fbc81b67ac1cfeb3afe37f3299180177faaa1ca6 (diff) | |
| parent | e6dc2c46fced4d8121d6d7bdd739d977f32d0462 (diff) | |
Merge branch '1.2.x'
Diffstat (limited to 'src/printer')
| -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 a2fe96271..fc2574036 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: @@ -421,11 +426,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"; |