diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-24 19:35:58 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-24 20:07:39 -0400 |
| commit | 0a3422299da7e882bae22c5fa3e5ec3c80b42046 (patch) | |
| tree | d00f31a33f03f11608ee046b851f4c63e194fe87 /src/printer | |
| parent | 30d21b25af6ee619e5f53d1ca8821b710fad4cb7 (diff) | |
Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk allows linearization of div,mod,/ by a constant.
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index f4abee292..007b4ea82 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -256,7 +256,16 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::INTS_DIVISION: case kind::INTS_DIVISION_TOTAL: case kind::INTS_MODULUS: - case kind::INTS_MODULUS_TOTAL: out << smtKindString(k) << " "; break; + case kind::INTS_MODULUS_TOTAL: + case kind::ABS: out << smtKindString(k) << " "; break; + case kind::IS_INTEGER: + case kind::TO_INTEGER: + case kind::TO_REAL: out << smtKindString(k) << " "; break; + + case kind::DIVISIBLE: + out << "(_ divisible " << n.getOperator().getConst<Divisible>().k << ")"; + stillNeedToPrintParams = false; + break; // arrays theory case kind::SELECT: @@ -442,6 +451,10 @@ static string smtKindString(Kind k) throw() { case kind::INTS_DIVISION_TOTAL: return "div"; case kind::INTS_MODULUS: case kind::INTS_MODULUS_TOTAL: return "mod"; + case kind::ABS: return "abs"; + case kind::IS_INTEGER: return "is_int"; + case kind::TO_INTEGER: return "to_int"; + case kind::TO_REAL: return "to_real"; // arrays theory case kind::SELECT: return "select"; |