Merge branch '1.4.x'

Conflicts:
	NEWS

5 files changed, 51 insertions, 17 deletions

diff --git a/NEWS b/NEWS
index 84debe315..7e3a30d74 100644
--- a/NEWS
+++ b/NEWS
@@ -7,6 +7,8 @@ Changes since 1.4
 * Simplification mode "incremental" no longer supported.
 * Support for array constants in constraints.
 * Syntax for array models have changed in some language front-ends.
+* 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 a3f5170fa..4d9ca9f30 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -899,6 +899,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/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 74c236dd1..aad365563 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -635,6 +635,13 @@ command returns [CVC4::Command* cmd = NULL]
         cmd = new EmptyCommand();
       }
     }
+  | IDENTIFIER SEMICOLON
+    { std::stringstream ss;
+      ss << "Unrecognized command `"
+         << AntlrInput::tokenText($IDENTIFIER)
+         << "'";
+      PARSER_STATE->parseError(ss.str());
+    }
   ;
 
 typeOrVarLetDecl[CVC4::parser::DeclarationCheck check]
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 2d89d3aff..ed5116bc6 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -152,6 +152,9 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       case BOOLEAN_TYPE:
         out << "BOOLEAN";
         break;
+      case STRING_TYPE:
+        out << "STRING";
+        break;
       default:
         out << tc;
         break;
@@ -162,11 +165,9 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       out << n.getConst<Datatype>().getName();
       break;
 
-    case kind::EMPTYSET: {
+    case kind::EMPTYSET:
       out << "{} :: " << n.getConst<EmptySet>().getType();
-      return;
       break;
-    }
 
     case kind::STORE_ALL: {
       const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>();
@@ -176,8 +177,8 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
     }
 
     default:
-      // fall back on whatever operator<< does on underlying type; we
-      // might luck out and print something reasonable
+      // Fall back to whatever operator<< does on underlying type; we
+      // might luck out and print something reasonable.
       kind::metakind::NodeValueConstPrinter::toStream(out, n);
     }
 
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index cb1fe87b2..3ca5674e9 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;
@@ -827,11 +838,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;
     }
@@ -849,7 +860,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)
@@ -874,7 +891,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
       }
     }
 */
-  }else{
+  } else {
     out << c << endl;
   }
 }