From: Andrew Reynolds Date: Thu, 9 Nov 2017 17:36:37 +0000 (-0600) Subject: Higher-order prep (#1338) X-Git-Tag: cvc5-1.0.0~5492 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8ada7b0ac4b3832d8fbf5e31080cb85df330049f;p=cvc5.git Higher-order prep (#1338) * Minor preparation for final higher-order merge. * Format --- diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index f292c0a2e..3caeeaaaa 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -116,43 +116,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, return; } - if( !force_nt.isNull() && n.getKind()!=kind::CONST_RATIONAL ){ - if( n.getType()!=force_nt ){ - if( force_nt.isReal() ){ - out << "(" << smtKindString( force_nt.isInteger() ? kind::TO_INTEGER : kind::TO_REAL) << " "; - toStream(out, n, toDepth, types, TypeNode::null()); - out << ")"; - }else{ - Node nn = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst(AscriptionType(force_nt.toType())), n ); - toStream(out, nn, toDepth, types, TypeNode::null()); - } - return; - } - } - - // variable - if(n.isVar()) { - string s; - if(n.getAttribute(expr::VarNameAttr(), s)) { - out << maybeQuoteSymbol(s); - } else { - if(n.getKind() == kind::VARIABLE) { - out << "var_"; - } else { - out << n.getKind() << '_'; - } - out << n.getId(); - } - if(types) { - // print the whole type, but not *its* type - out << ":"; - n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5); - } - - return; - } - // constant if(n.getMetaKind() == kind::metakind::CONSTANT) { switch(n.getKind()) { @@ -325,6 +288,61 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, return; } + if (!force_nt.isNull()) + { + if (n.getType() != force_nt) + { + if (force_nt.isReal()) + { + out << "(" << smtKindString(force_nt.isInteger() ? kind::TO_INTEGER + : kind::TO_REAL) + << " "; + toStream(out, n, toDepth, types, TypeNode::null()); + out << ")"; + } + else + { + Node nn = NodeManager::currentNM()->mkNode( + kind::APPLY_TYPE_ASCRIPTION, + NodeManager::currentNM()->mkConst( + AscriptionType(force_nt.toType())), + n); + toStream(out, nn, toDepth, types, TypeNode::null()); + } + return; + } + } + + // variable + if (n.isVar()) + { + string s; + if (n.getAttribute(expr::VarNameAttr(), s)) + { + out << maybeQuoteSymbol(s); + } + else + { + if (n.getKind() == kind::VARIABLE) + { + out << "var_"; + } + else + { + out << n.getKind() << '_'; + } + out << n.getId(); + } + if (types) + { + // print the whole type, but not *its* type + out << ":"; + n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5); + } + + return; + } + bool stillNeedToPrintParams = true; bool forceBinary = false; // force N-ary to binary when outputing children bool parametricTypeChildren = false; // parametric operators that are (op t1 ... tn) where t1...tn must have same type diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1634345e0..a1a15b25a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2424,8 +2424,10 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map& args, std::map< Node activeMap[ n ] = true; } }else{ + if (n.hasOperator()) + { + computeArgs(args, activeMap, n.getOperator(), visited); + } for( int i=0; i<(int)n.getNumChildren(); i++ ){ computeArgs( args, activeMap, n[i], visited ); }