From 7f8a34d2e11e99ff5272de113bfbe382b16bb0cd Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sun, 28 Dec 2014 13:31:30 +0000
Subject: [PATCH] Adjusted default model display for float literals.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 src/ast/ast_smt2_pp.cpp | 38 +++++++++++++++++++++++++-------------
 src/ast/ast_smt2_pp.h   |  2 +-
 2 files changed, 26 insertions(+), 14 deletions(-)

diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index 00ce6aa8f..a9e223c55 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -222,7 +222,7 @@ format * smt2_pp_environment::pp_bv_literal(app * t, bool use_bv_lits, bool bv_n
     return vf;
 }
 
-format * smt2_pp_environment::pp_float_literal(app * t, bool use_bv_lits) {
+format * smt2_pp_environment::pp_float_literal(app * t, bool use_bv_lits, bool use_float_real_lits) {
     mpf_manager & fm = get_futil().fm();
     scoped_mpf v(fm);
     ast_manager & m = get_manager();
@@ -231,28 +231,38 @@ format * smt2_pp_environment::pp_float_literal(app * t, bool use_bv_lits) {
     VERIFY(get_futil().is_value(t, v));
     if (fm.is_nan(v)) {
         buf << "(_ NaN " << v.get().get_ebits() << " " << v.get().get_sbits() << ")";
-        return mk_string(get_manager(), buf.c_str());
+        return mk_string(m, buf.c_str());
     }
     else if (fm.is_pinf(v)) {
         buf << "(_ +oo " << v.get().get_ebits() << " " << v.get().get_sbits() << ")";
-        return mk_string(get_manager(), buf.c_str());
+        return mk_string(m, buf.c_str());
     }
     else if (fm.is_ninf(v)) {
         buf << "(_ -oo " << v.get().get_ebits() << " " << v.get().get_sbits() << ")";
-        return mk_string(get_manager(), buf.c_str());
+        return mk_string(m, buf.c_str());
     }
     else if (fm.is_pzero(v)) {        
         buf << "(_ +zero " << v.get().get_ebits() << " " << v.get().get_sbits() << ")";
-        return mk_string(get_manager(), buf.c_str());
+        return mk_string(m, buf.c_str());
     }
     else if (fm.is_nzero(v)) {
         buf << "(_ -zero " << v.get().get_ebits() << " " << v.get().get_sbits() << ")";
-        return mk_string(get_manager(), buf.c_str());
+        return mk_string(m, buf.c_str());
     }
-    else {        
-        buf << "(fp #b" << (fm.sgn(v) ? 1 : 0);
-        body = mk_string(get_manager(), buf.c_str());        
-        body = mk_compose(m, body, mk_string(get_manager(), " "));
+    else if (use_float_real_lits)
+    {
+        buf << "((_ to_fp " << v.get().get_ebits() << " " << 
+                               v.get().get_sbits() << ") RTZ " << 
+                               fm.to_string(v).c_str() << ")";        
+        return mk_string(m, buf.c_str());
+    }
+    else {
+        if (use_bv_lits)
+            buf << "(fp #b" << (fm.sgn(v) ? 1 : 0);
+        else
+            buf << "(fp (_ bv" << (fm.sgn(v) ? 1 : 0) << " 1)";
+        body = mk_string(m, buf.c_str());
+        body = mk_compose(m, body, mk_string(m, " "));
 
         mpf_exp_t exp = fm.exp(v);
         const mpz & bias = fm.m_powers2.m1(v.get().get_ebits() - 1);
@@ -260,7 +270,7 @@ format * smt2_pp_environment::pp_float_literal(app * t, bool use_bv_lits) {
         app_ref e_biased_exp(m);
         e_biased_exp = get_bvutil().mk_numeral(biased_exp, v.get().get_ebits());
         body = mk_compose(m, body, pp_bv_literal(e_biased_exp, use_bv_lits, false));
-        body = mk_compose(m, body, mk_string(get_manager(), " "));
+        body = mk_compose(m, body, mk_string(m, " "));
 
         scoped_mpz sig(fm.mpz_manager());
         sig = fm.sig(v);
@@ -268,7 +278,7 @@ format * smt2_pp_environment::pp_float_literal(app * t, bool use_bv_lits) {
         e_sig = get_bvutil().mk_numeral(rational(sig), v.get().get_sbits() - 1);
         body = mk_compose(m, body, pp_bv_literal(e_sig, use_bv_lits, false));
         
-        body = mk_compose(m, body, mk_string(get_manager(), ")"));        
+        body = mk_compose(m, body, mk_string(m, ")"));
         return body;
     }
 }
@@ -446,6 +456,7 @@ class smt2_printer {
     bool     m_pp_decimal;
     unsigned m_pp_decimal_precision;
     bool     m_pp_bv_lits;
+    bool     m_pp_float_real_lits;
     bool     m_pp_bv_neg;
     unsigned m_pp_max_depth;
     unsigned m_pp_min_alias_size;
@@ -565,7 +576,7 @@ class smt2_printer {
             f = m_env.pp_bv_literal(c, m_pp_bv_lits, m_pp_bv_neg);
         }
         else if (m_env.get_futil().is_value(c)) {
-            f = m_env.pp_float_literal(c, m_pp_bv_lits);
+            f = m_env.pp_float_literal(c, m_pp_bv_lits, m_pp_float_real_lits);
         }
         else if (m_env.get_dlutil().is_numeral(c)) {
             f = m_env.pp_datalog_literal(c);
@@ -1008,6 +1019,7 @@ public:
         m_pp_decimal = p.decimal();
         m_pp_decimal_precision = p.decimal_precision();
         m_pp_bv_lits = p.bv_literals();
+        m_pp_float_real_lits = p.fp_real_literals();
         m_pp_bv_neg  = p.bv_neg();
         m_pp_max_depth = p.max_depth();
         m_pp_min_alias_size = p.min_alias_size();
diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h
index 93feec8d5..37d13e57a 100644
--- a/src/ast/ast_smt2_pp.h
+++ b/src/ast/ast_smt2_pp.h
@@ -52,7 +52,7 @@ public:
     virtual format_ns::format * pp_fdecl(func_decl * f, unsigned & len);
     virtual format_ns::format * pp_bv_literal(app * t, bool use_bv_lits, bool bv_neg);
     virtual format_ns::format * pp_arith_literal(app * t, bool decimal, unsigned prec);
-    virtual format_ns::format * pp_float_literal(app * t, bool use_bv_lits);
+    virtual format_ns::format * pp_float_literal(app * t, bool use_bv_lits, bool use_float_real_lits);
     virtual format_ns::format * pp_datalog_literal(app * t);
     virtual format_ns::format * pp_sort(sort * s);
     virtual format_ns::format * pp_fdecl_ref(func_decl * f);