From af18cd275f340d1896c3b635dbeecbea2e521db1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 5 Nov 2020 22:28:18 -0600 Subject: Simplify printing with respect to expression types (#5394) This removes infrastructure for stream property related to printing type annotations on all variables. This is towards refactoring the printers. --- src/printer/smt2/smt2_printer.cpp | 59 ++++++++++++++++++--------------------- src/printer/smt2/smt2_printer.h | 4 +-- 2 files changed, 28 insertions(+), 35 deletions(-) (limited to 'src/printer/smt2') diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 5ef1eca2b..439d2aa6e 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -61,8 +61,10 @@ static void toStreamRational(std::ostream& out, bool decimal, Variant v); -void Smt2Printer::toStream( - std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const +void Smt2Printer::toStream(std::ostream& out, + TNode n, + int toDepth, + size_t dag) const { if(dag != 0) { DagificationVisitor dv(dag); @@ -74,14 +76,14 @@ void Smt2Printer::toStream( theory::SubstitutionMap::const_iterator i_end = lets.end(); for(; i != i_end; ++ i) { out << "(let (("; - toStream(out, (*i).second, toDepth, types, TypeNode::null()); + toStream(out, (*i).second, toDepth, TypeNode::null()); out << ' '; - toStream(out, (*i).first, toDepth, types, TypeNode::null()); + toStream(out, (*i).first, toDepth, TypeNode::null()); out << ")) "; } } Node body = dv.getDagifiedBody(); - toStream(out, body, toDepth, types, TypeNode::null()); + toStream(out, body, toDepth, TypeNode::null()); if(!lets.empty()) { theory::SubstitutionMap::const_iterator i = lets.begin(); theory::SubstitutionMap::const_iterator i_end = lets.end(); @@ -90,7 +92,7 @@ void Smt2Printer::toStream( } } } else { - toStream(out, n, toDepth, types, TypeNode::null()); + toStream(out, n, toDepth, TypeNode::null()); } } @@ -113,7 +115,6 @@ static bool stringifyRegexp(Node n, stringstream& ss) { void Smt2Printer::toStream(std::ostream& out, TNode n, int toDepth, - bool types, TypeNode force_nt) const { // null @@ -394,7 +395,7 @@ void Smt2Printer::toStream(std::ostream& out, if(n.getNumChildren() != 0) { for(unsigned i = 0; i < n.getNumChildren(); ++i) { out << ' '; - toStream(out, n[i], toDepth, types, TypeNode::null()); + toStream(out, n[i], toDepth, TypeNode::null()); } out << ')'; } @@ -426,7 +427,7 @@ void Smt2Printer::toStream(std::ostream& out, << smtKindString(is_int ? kind::TO_INTEGER : kind::DIVISION, d_variant) << " "; - toStream(out, type_asc_arg, toDepth, types, TypeNode::null()); + toStream(out, type_asc_arg, toDepth, TypeNode::null()); if (!is_int) { out << " 1"; @@ -440,7 +441,6 @@ void Smt2Printer::toStream(std::ostream& out, toStream(out, type_asc_arg, toDepth < 0 ? toDepth : toDepth - 1, - types, TypeNode::null()); out << " " << force_nt << ")"; } @@ -467,13 +467,6 @@ void Smt2Printer::toStream(std::ostream& out, } 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; } @@ -501,7 +494,7 @@ void Smt2Printer::toStream(std::ostream& out, for (Node nc : n) { out << " "; - toStream(out, nc, toDepth, types, TypeNode::null()); + toStream(out, nc, toDepth, TypeNode::null()); } out << ")"; return; @@ -538,11 +531,11 @@ void Smt2Printer::toStream(std::ostream& out, args.insert(args.begin(), head[1]); head = head[0]; } - toStream(out, head, toDepth, types, TypeNode::null()); + toStream(out, head, toDepth, TypeNode::null()); for (unsigned i = 0, size = args.size(); i < size; ++i) { out << " "; - toStream(out, args[i], toDepth, types, TypeNode::null()); + toStream(out, args[i], toDepth, TypeNode::null()); } out << ")"; } @@ -551,7 +544,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::LAMBDA: out << smtKindString(k, d_variant) << " "; break; case kind::MATCH: out << smtKindString(k, d_variant) << " "; - toStream(out, n[0], toDepth, types, TypeNode::null()); + toStream(out, n[0], toDepth, TypeNode::null()); out << " ("; for (size_t i = 1, nchild = n.getNumChildren(); i < nchild; i++) { @@ -559,15 +552,15 @@ void Smt2Printer::toStream(std::ostream& out, { out << " "; } - toStream(out, n[i], toDepth, types, TypeNode::null()); + toStream(out, n[i], toDepth, TypeNode::null()); } out << "))"; return; case kind::MATCH_BIND_CASE: // ignore the binder - toStream(out, n[1], toDepth, types, TypeNode::null()); + toStream(out, n[1], toDepth, TypeNode::null()); out << " "; - toStream(out, n[2], toDepth, types, TypeNode::null()); + toStream(out, n[2], toDepth, TypeNode::null()); out << ")"; return; case kind::MATCH_CASE: @@ -887,7 +880,7 @@ void Smt2Printer::toStream(std::ostream& out, for (TNode::iterator i = n.begin(), iend = n.end(); i != iend;) { out << '('; - toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, types, 0); + toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, 0); out << ' '; out << (*i).getType(); out << ')'; @@ -936,7 +929,6 @@ void Smt2Printer::toStream(std::ostream& out, toStream(out, dt[cindex].getConstructor(), toDepth < 0 ? toDepth : toDepth - 1, - types, TypeNode::null()); out << ")"; }else{ @@ -944,11 +936,13 @@ void Smt2Printer::toStream(std::ostream& out, toStream(out, dt[cindex].getConstructor(), toDepth < 0 ? toDepth : toDepth - 1, - types, TypeNode::null()); } }else{ - toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null()); + toStream(out, + n.getOperator(), + toDepth < 0 ? toDepth : toDepth - 1, + TypeNode::null()); } } else { out << "(...)"; @@ -1028,9 +1022,10 @@ void Smt2Printer::toStream(std::ostream& out, Node cn = n[i]; std::map< unsigned, TypeNode >::iterator itfc = force_child_type.find( i ); if( itfc!=force_child_type.end() ){ - toStream(out, cn, toDepth < 0 ? toDepth : toDepth - c, types, itfc->second); + toStream(out, cn, toDepth < 0 ? toDepth : toDepth - c, itfc->second); }else{ - toStream(out, cn, toDepth < 0 ? toDepth : toDepth - c, types, TypeNode::null()); + toStream( + out, cn, toDepth < 0 ? toDepth : toDepth - c, TypeNode::null()); } } else { out << "(...)"; @@ -1452,7 +1447,7 @@ void Smt2Printer::toStream(std::ostream& out, out << "(define-fun " << n << " " << val[0] << " " << n.getType().getRangeType() << " "; // call toStream and force its type to be proper - toStream(out, val[1], -1, false, n.getType().getRangeType()); + toStream(out, val[1], -1, n.getType().getRangeType()); out << ")" << endl; } else @@ -1471,7 +1466,7 @@ void Smt2Printer::toStream(std::ostream& out, } out << "(define-fun " << n << " () " << n.getType() << " "; // call toStream and force its type to be proper - toStream(out, val, -1, false, n.getType()); + toStream(out, val, -1, n.getType()); out << ")" << endl; } } diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index ed04da983..1cece11c4 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -42,7 +42,6 @@ class Smt2Printer : public CVC4::Printer void toStream(std::ostream& out, TNode n, int toDepth, - bool types, size_t dag) const override; void toStream(std::ostream& out, const CommandStatus* s) const override; void toStream(std::ostream& out, const smt::Model& m) const override; @@ -228,8 +227,7 @@ class Smt2Printer : public CVC4::Printer std::ostream& out, const std::vector& sequence) const override; private: - void toStream( - std::ostream& out, TNode n, int toDepth, bool types, TypeNode nt) const; + void toStream(std::ostream& out, TNode n, int toDepth, TypeNode nt) const; void toStream(std::ostream& out, const smt::Model& m, const NodeCommand* c) const override; -- cgit v1.2.3