diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 21 |
1 files changed, 17 insertions, 4 deletions
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<TypeConstant>()) { - 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<Integer>(); 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<Rational>(); 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 ">"; |