From a7eba5fcb468399181d06a3684e760aae7185229 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 29 May 2013 09:48:40 -0400 Subject: [PATCH] SMT-LIB printer updates (some missing cases). --- src/printer/smt2/smt2_printer.cpp | 16 +++++++++++++--- 1 file 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"; -- 2.30.2