diff options
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 33 |
1 files changed, 25 insertions, 8 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index cfc91eb18..ed218832c 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -74,6 +74,20 @@ void CvcPrinter::toStream( } } +void toStreamRational(std::ostream& out, Node n, bool forceRational) +{ + Assert(n.getKind() == kind::CONST_RATIONAL); + const Rational& rat = n.getConst<Rational>(); + if (rat.isIntegral() && !forceRational) + { + out << rat.getNumerator(); + } + else + { + out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')'; + } +} + void CvcPrinter::toStream( std::ostream& out, TNode n, int depth, bool types, bool bracket) const { @@ -141,12 +155,7 @@ void CvcPrinter::toStream( out << (n.getConst<bool>() ? "TRUE" : "FALSE"); break; case kind::CONST_RATIONAL: { - const Rational& rat = n.getConst<Rational>(); - if(rat.isIntegral()) { - out << rat.getNumerator(); - } else { - out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')'; - } + toStreamRational(out, n, false); break; } case kind::TYPE_CONSTANT: @@ -566,8 +575,16 @@ void CvcPrinter::toStream( opType = PREFIX; break; case kind::TO_REAL: - // ignore, there is no to-real in CVC language - toStream(out, n[0], depth, types, false); + if (n[0].getKind() == kind::CONST_RATIONAL) + { + // print the constant as a rational + toStreamRational(out, n[0], true); + } + else + { + // ignore, there is no to-real in CVC language + toStream(out, n[0], depth, types, false); + } return; case kind::DIVISIBLE: out << "DIVISIBLE("; |