From 742f2b07dd1c0d4be12d3f820c3741812c878fd1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 14 Jan 2013 11:08:32 -0800
Subject: [PATCH] Add support for compact string representation in the RCF API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/api/api_rcf.cpp                  |  6 +++---
 src/api/python/z3rcf.py              |  5 ++++-
 src/api/z3_rcf.h                     |  4 ++--
 src/math/realclosure/realclosure.cpp | 13 ++++++++-----
 src/math/realclosure/realclosure.h   |  2 +-
 5 files changed, 18 insertions(+), 12 deletions(-)

diff --git a/src/api/api_rcf.cpp b/src/api/api_rcf.cpp
index 6b9826af7..145f8f824 100644
--- a/src/api/api_rcf.cpp
+++ b/src/api/api_rcf.cpp
@@ -268,13 +268,13 @@ extern "C" {
         Z3_CATCH_RETURN(Z3_FALSE);
     }
 
-    Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a) {
+    Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, Z3_bool compact) {
         Z3_TRY;
-        LOG_Z3_rcf_num_to_string(c, a);
+        LOG_Z3_rcf_num_to_string(c, a, compact);
         RESET_ERROR_CODE();
         reset_rcf_cancel(c);
         std::ostringstream buffer;
-        rcfm(c).display(buffer, to_rcnumeral(a));
+        rcfm(c).display(buffer, to_rcnumeral(a), compact != 0);
         return mk_c(c)->mk_external_string(buffer.str());
         Z3_CATCH_RETURN("");
     }
diff --git a/src/api/python/z3rcf.py b/src/api/python/z3rcf.py
index dd0696594..f63fc7efd 100644
--- a/src/api/python/z3rcf.py
+++ b/src/api/python/z3rcf.py
@@ -65,7 +65,10 @@ class RCFNum:
         return self.ctx.ref()
                   
     def __repr__(self):
-        return Z3_rcf_num_to_string(self.ctx_ref(), self.num)
+        return Z3_rcf_num_to_string(self.ctx_ref(), self.num, False)
+
+    def compact_str(self):
+        return Z3_rcf_num_to_string(self.ctx_ref(), self.num, True)
 
     def __add__(self, other):
         v = _to_rcfnum(other, self.ctx)
diff --git a/src/api/z3_rcf.h b/src/api/z3_rcf.h
index 87f376117..c46b43255 100644
--- a/src/api/z3_rcf.h
+++ b/src/api/z3_rcf.h
@@ -173,9 +173,9 @@ extern "C" {
     /**
        \brief Convert the RCF numeral into a string.
 
-       def_API('Z3_rcf_num_to_string', STRING, (_in(CONTEXT), _in(RCF_NUM)))
+       def_API('Z3_rcf_num_to_string', STRING, (_in(CONTEXT), _in(RCF_NUM), _in(BOOL)))
     */
-    Z3_string Z3_API Z3_rcf_num_to_string(__in Z3_context c, __in Z3_rcf_num a);
+    Z3_string Z3_API Z3_rcf_num_to_string(__in Z3_context c, __in Z3_rcf_num a, __in Z3_bool compact);
 
     /**
        \brief Convert the RCF numeral into a string in decimal notation.
diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp
index 947b8abfd..593a8c0d2 100644
--- a/src/math/realclosure/realclosure.cpp
+++ b/src/math/realclosure/realclosure.cpp
@@ -5658,15 +5658,18 @@ namespace realclosure {
                 display(out, a.m_value, true);
                 for (unsigned i = 0; i < c.m_found.size(); i++) {
                     algebraic * ext = c.m_found[i];
-                    out << ", r!" << ext->idx() << " = ";
+                    out << "; r!" << ext->idx() << " := ";
                     display_algebraic_def(out, ext, true);
                 }
                 out << "]";
             }
         }
 
-        void display(std::ostream & out, numeral const & a) const {
-            display(out, a.m_value, false);
+        void display(std::ostream & out, numeral const & a, bool compact=false) const {
+            if (compact)
+                display_compact(out, a);
+            else
+                display(out, a.m_value, false);
         }
 
         void display_non_rational_in_decimal(std::ostream & out, numeral const & a, unsigned precision) {
@@ -5927,9 +5930,9 @@ namespace realclosure {
         return gt(a, _b);
     }
 
-    void manager::display(std::ostream & out, numeral const & a) const {
+    void manager::display(std::ostream & out, numeral const & a, bool compact) const {
         save_interval_ctx ctx(this);
-        m_imp->display(out, a);
+        m_imp->display(out, a, compact);
     }
 
     void manager::display_decimal(std::ostream & out, numeral const & a, unsigned precision) const {
diff --git a/src/math/realclosure/realclosure.h b/src/math/realclosure/realclosure.h
index 146299b56..2b70d3be0 100644
--- a/src/math/realclosure/realclosure.h
+++ b/src/math/realclosure/realclosure.h
@@ -252,7 +252,7 @@ namespace realclosure {
         bool ge(numeral const & a, mpq const & b) { return !lt(a, b); }
         bool ge(numeral const & a, mpz const & b) { return !lt(a, b); }
         
-        void display(std::ostream & out, numeral const & a) const;
+        void display(std::ostream & out, numeral const & a, bool compact=false) const;
 
         /**
            \brief Display a real number in decimal notation.