From: Morgan Deters Date: Tue, 6 Dec 2011 00:34:32 +0000 (+0000) Subject: fix errors in smt-lib2 output; needed for debugging X-Git-Tag: cvc5-1.0.0~8366 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=00dc8a9ee3e893e86ccbcdf192617793b2754eb1;p=cvc5.git fix errors in smt-lib2 output; needed for debugging --- diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 0f5fcd73b..43649aa21 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -70,7 +70,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, switch(n.getKind()) { case kind::TYPE_CONSTANT: switch(n.getConst()) { - case BOOLEAN_TYPE: out << "Boolean"; break; + case BOOLEAN_TYPE: out << "Bool"; break; case REAL_TYPE: out << "Real"; break; case INTEGER_TYPE: out << "Int"; break; default: @@ -103,7 +103,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::CONST_INTEGER: { Integer i = n.getConst(); if(i < 0) { - out << "(- " << i << ')'; + out << "(- " << -i << ')'; } else { out << i; } @@ -112,12 +112,21 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::CONST_RATIONAL: { Rational r = n.getConst(); if(r < 0) { - out << "(- " << r << ')'; + if(r.getDenominator() == 1) { + out << "(- " << -r << ')'; + } else { + out << "(- (/ " << (-r).getNumerator() << ' ' << (-r).getDenominator() << "))"; + } } else { - out << r; + if(r.getDenominator() == 1) { + out << r; + } else { + out << "(/ " << r.getNumerator() << ' ' << r.getDenominator() << ')'; + } } break; } + default: // fall back on whatever operator<< does on underlying type; we // might luck out and be SMT-LIB v2 compliant @@ -163,6 +172,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::MINUS: case kind::UMINUS: case kind::DIVISION: + case kind::INTS_DIVISION: + case kind::INTS_MODULUS: case kind::LT: case kind::LEQ: case kind::GT: @@ -275,6 +286,8 @@ static string smtKindString(Kind k) throw() { case kind::MINUS: return "-"; case kind::UMINUS: return "-"; case kind::DIVISION: return "/"; + case kind::INTS_DIVISION: return "div"; + case kind::INTS_MODULUS: return "mod"; case kind::LT: return "<"; case kind::LEQ: return "<="; case kind::GT: return ">";