From 65f0dc22fe49c6c388e9413f3b7541d7fb49a3b3 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 3 Oct 2014 11:19:48 -0400
Subject: [PATCH] Fix output of integer-valued real constants in SMT-LIB models
 (thanks Christoph Sticksel for reporting).

---
 NEWS                              |  3 ++-
 src/expr/command.cpp              |  7 ++++++
 src/printer/smt2/smt2_printer.cpp | 41 ++++++++++++++++++++++---------
 3 files changed, 38 insertions(+), 13 deletions(-)

diff --git a/NEWS b/NEWS
index 64ded5339..4c0de2ce3 100644
--- a/NEWS
+++ b/NEWS
@@ -3,7 +3,8 @@ This file contains a summary of important user-visible changes.
 Changes since 1.4
 =================
 
-* nothing yet
+* In SMT-LIB model output, real-sorted but integer-valued constants are
+  now printed in accordance with the standard (e.g. "1.0").
 
 Changes since 1.3
 =================
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 16484a320..69bdd704b 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -896,6 +896,13 @@ void GetValueCommand::invoke(SmtEngine* smtEngine) throw() {
       smt::SmtScope scope(smtEngine);
       Node request = Node::fromExpr(options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i);
       Node value = Node::fromExpr(smtEngine->getValue(*i));
+      if(value.getType().isInteger() && request.getType() == nm->realType()) {
+        // Need to wrap in special marker so that output printers know this
+        // is an integer-looking constant that really should be output as
+        // a rational.  Necessary for SMT-LIB standards compliance, but ugly.
+        value = nm->mkNode(kind::APPLY_TYPE_ASCRIPTION,
+                           nm->mkConst(AscriptionType(em->realType())), value);
+      }
       result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr());
     }
     d_result = em->mkExpr(kind::SEXPR, result);
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index c9db1eece..903a1e6e3 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -245,7 +245,11 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   bool stillNeedToPrintParams = true;
   bool forceBinary = false; // force N-ary to binary when outputing children
   // operator
-  if(n.getNumChildren() != 0 && n.getKind()!=kind::INST_PATTERN_LIST) out << '(';
+  if(n.getNumChildren() != 0 &&
+     n.getKind() != kind::INST_PATTERN_LIST &&
+     n.getKind() != kind::APPLY_TYPE_ASCRIPTION) {
+    out << '(';
+  }
   switch(Kind k = n.getKind()) {
     // builtin theory
   case kind::APPLY: break;
@@ -307,7 +311,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::STORE:
   case kind::ARRAY_TYPE: out << smtKindString(k) << " "; break;
 
-  // string theory
+    // string theory
   case kind::STRING_CONCAT:
     if(d_variant == z3str_variant) {
       out << "Concat ";
@@ -425,12 +429,19 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
 
    // datatypes
   case kind::APPLY_TYPE_ASCRIPTION: {
-      out << "as ";
-      toStream(out, n[0], toDepth < 0 ? toDepth : toDepth - 1, types);
-      out << ' ';
       TypeNode t = TypeNode::fromType(n.getOperator().getConst<AscriptionType>().getType());
-      out << (t.isFunctionLike() ? t.getRangeType() : t);
-      out << ')';
+      if(t.getKind() == kind::TYPE_CONSTANT &&
+         t.getConst<TypeConstant>() == REAL_TYPE &&
+         n[0].getType().isInteger()) {
+        // Special case, in model output integer constants that should be
+        // Real-sorted are wrapped in a type ascription.  Handle that here.
+        toStream(out, n[0], -1, false);
+        out << ".0";
+        return;
+      }
+      out << "(as ";
+      toStream(out, n[0], toDepth < 0 ? toDepth : toDepth - 1, types);
+      out << ' ' << (t.isFunctionLike() ? t.getRangeType() : t) << ')';
       return;
     }
     break;
@@ -812,11 +823,11 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
   } else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) {
     const DeclareFunctionCommand* dfc = (const DeclareFunctionCommand*)c; 
     Node n = Node::fromExpr( dfc->getFunction() );
-    if(dfc->getPrintInModelSetByUser()){
-      if(!dfc->getPrintInModel()){
+    if(dfc->getPrintInModelSetByUser()) {
+      if(!dfc->getPrintInModel()) {
         return;
       }
-    }else if(n.getKind() == kind::SKOLEM) {
+    } else if(n.getKind() == kind::SKOLEM) {
       // don't print out internal stuff
       return;
     }
@@ -834,7 +845,13 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
         }
       }
       out << "(define-fun " << n << " () "
-          << n.getType() << " " << val << ")" << endl;
+          << n.getType() << " ";
+      if(val.getType().isInteger() && n.getType().isReal() && !n.getType().isInteger()) {
+        out << val << ".0";
+      } else {
+        out << val;
+      }
+      out << ")" << endl;
     }
 /*
     //for table format (work in progress)
@@ -859,7 +876,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
       }
     }
 */
-  }else{
+  } else {
     out << c << endl;
   }
 }
-- 
2.30.2