From: Gereon Kremer <gkremer@stanford.edu>
Date: Sat, 15 Jan 2022 03:17:29 +0000 (-0800)
Subject: Change how RANs are printed (#7955)
X-Git-Tag: cvc5-1.0.0~535
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=558e2a06bdd961d906c265c4fbd3abbc85ed48a3;p=cvc5.git

Change how RANs are printed (#7955)

This PR adds real algebraic number as a special case in the smt2 printer.
---

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index eb1afb5c8..fd7825ac1 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -52,6 +52,7 @@
 #include "util/floatingpoint.h"
 #include "util/iand.h"
 #include "util/indexed_root_predicate.h"
+#include "util/real_algebraic_number.h"
 #include "util/regexp.h"
 #include "util/smt2_quote_string.h"
 #include "util/string.h"
@@ -651,6 +652,13 @@ void Smt2Printer::toStream(std::ostream& out,
       out << "(_ divisible " << n.getOperator().getConst<Divisible>().k << ")";
       stillNeedToPrintParams = false;
       break;
+    case kind::REAL_ALGEBRAIC_NUMBER:
+    {
+      const RealAlgebraicNumber& ran = n.getOperator().getConst<RealAlgebraicNumber>();
+      out << "(_ real_algebraic_number " << ran << ")";
+      stillNeedToPrintParams = false;
+      break;
+    }
     case kind::INDEXED_ROOT_PREDICATE_OP:
     {
       const IndexedRootPredicate& irp = n.getConst<IndexedRootPredicate>();