diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-09 11:36:37 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-09 11:36:37 -0600 |
commit | 8ada7b0ac4b3832d8fbf5e31080cb85df330049f (patch) | |
tree | e58569b2544fe88daf6f41b1b6babbb63319f8be /src | |
parent | 22b211647501a4dad5cec66c2ea6383ea8e7b7bd (diff) |
Higher-order prep (#1338)
* Minor preparation for final higher-order merge.
* Format
Diffstat (limited to 'src')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 92 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 4 |
3 files changed, 63 insertions, 39 deletions
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<Node, Node, Node fm = def.getFormula(); } - Node instance = fm.substitute(formals.begin(), formals.end(), - n.begin(), n.end()); + Node instance = fm.substitute(formals.begin(), + formals.end(), + n.begin(), + n.begin() + formals.size()); Debug("expand") << "made : " << instance << endl; Node expanded = expandDefinitions(instance, cache, expandOnly); diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 0ffed5243..45c418996 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -105,6 +105,10 @@ void QuantifiersRewriter::computeArgs( std::vector< Node >& 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 ); } |