From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 5 May 2018 07:23:54 +0000 (-0500)
Subject: Fix handling of TO_REAL in cvc printer (#1876)
X-Git-Tag: cvc5-1.0.0~5083
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=884ad1a946ad6a04664ef97121ce1cebb5513d40;p=cvc5.git

Fix handling of TO_REAL in cvc printer (#1876)
---

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(";