diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-03 15:15:45 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-03 15:15:45 -0400 |
commit | 9323af51596eece5107b6ee4f7423ad56c9385b8 (patch) | |
tree | 65675635487223e5e679dd49cf8703ae1752ef19 | |
parent | 6294adeb83155c54539b2d2d31fa9e3a5b6f1a00 (diff) | |
parent | 65f0dc22fe49c6c388e9413f3b7541d7fb49a3b3 (diff) |
Merge branch '1.4.x'
Conflicts:
NEWS
-rw-r--r-- | NEWS | 2 | ||||
-rw-r--r-- | src/expr/command.cpp | 7 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 7 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 11 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 41 |
5 files changed, 51 insertions, 17 deletions
@@ -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; } } |