From af18cd275f340d1896c3b635dbeecbea2e521db1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 5 Nov 2020 22:28:18 -0600 Subject: [PATCH] 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/expr/expr_iomanip.cpp | 33 ------ src/expr/expr_iomanip.h | 62 ------------ src/expr/expr_template.cpp | 9 +- src/expr/expr_template.h | 7 +- src/expr/node.h | 21 +--- src/expr/node_value.cpp | 12 ++- src/expr/node_value.h | 4 - src/expr/type_node.cpp | 2 +- src/expr/type_node.h | 4 +- src/options/expr_options.toml | 9 -- src/parser/parser.cpp | 2 - src/printer/ast/ast_printer.cpp | 29 ++---- src/printer/ast/ast_printer.h | 3 +- src/printer/cvc/cvc_printer.cpp | 161 +++++++++++++++--------------- src/printer/cvc/cvc_printer.h | 4 +- src/printer/printer.h | 1 - src/printer/smt2/smt2_printer.cpp | 59 +++++------ src/printer/smt2/smt2_printer.h | 4 +- src/printer/tptp/tptp_printer.cpp | 8 +- src/printer/tptp/tptp_printer.h | 1 - src/smt/command.cpp | 99 +++++++++--------- src/smt/command.h | 95 +++++++++--------- src/smt/node_command.cpp | 5 - src/smt/node_command.h | 5 - src/smt/options_manager.cpp | 15 --- src/smt/update_ostream.h | 3 - test/unit/expr/node_black.h | 2 +- 27 files changed, 240 insertions(+), 419 deletions(-) diff --git a/src/expr/expr_iomanip.cpp b/src/expr/expr_iomanip.cpp index c4353cb00..0ff29663c 100644 --- a/src/expr/expr_iomanip.cpp +++ b/src/expr/expr_iomanip.cpp @@ -26,11 +26,8 @@ namespace CVC4 { namespace expr { const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc(); -const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc(); const int ExprDag::s_iosIndex = std::ios_base::xalloc(); - - ExprSetDepth::ExprSetDepth(long depth) : d_depth(depth) {} void ExprSetDepth::applyDepth(std::ostream& out) { @@ -71,31 +68,6 @@ ExprSetDepth::Scope::~Scope() { ExprSetDepth::setDepth(d_out, d_oldDepth); } - -ExprPrintTypes::ExprPrintTypes(bool printTypes) : d_printTypes(printTypes) {} - -void ExprPrintTypes::applyPrintTypes(std::ostream& out) { - out.iword(s_iosIndex) = d_printTypes; -} - -bool ExprPrintTypes::getPrintTypes(std::ostream& out) { - return out.iword(s_iosIndex); -} - -void ExprPrintTypes::setPrintTypes(std::ostream& out, bool printTypes) { - out.iword(s_iosIndex) = printTypes; -} - -ExprPrintTypes::Scope::Scope(std::ostream& out, bool printTypes) - : d_out(out), - d_oldPrintTypes(ExprPrintTypes::getPrintTypes(out)) { - ExprPrintTypes::setPrintTypes(out, printTypes); -} - -ExprPrintTypes::Scope::~Scope() { - ExprPrintTypes::setPrintTypes(d_out, d_oldPrintTypes); -} - ExprDag::ExprDag(bool dag) : d_dag(dag ? 1 : 0) {} ExprDag::ExprDag(int dag) : d_dag(dag < 0 ? 0 : dag) {} @@ -145,11 +117,6 @@ std::ostream& operator<<(std::ostream& out, ExprDag d) { return out; } -std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) { - pt.applyPrintTypes(out); - return out; -} - std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) { sd.applyDepth(out); return out; diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h index 82358bb68..e90366a81 100644 --- a/src/expr/expr_iomanip.h +++ b/src/expr/expr_iomanip.h @@ -91,56 +91,6 @@ public: long d_depth; };/* class ExprSetDepth */ -/** - * IOStream manipulator to print type ascriptions or not. - * - * // let a, b, c, and d be variables of sort U - * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) - * out << e; - * - * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but - */ -class CVC4_PUBLIC ExprPrintTypes { -public: - /** - * Construct a ExprPrintTypes with the given setting. - */ - ExprPrintTypes(bool printTypes); - - void applyPrintTypes(std::ostream& out); - - static bool getPrintTypes(std::ostream& out); - - static void setPrintTypes(std::ostream& out, bool printTypes); - - /** - * Set the print-types state on the output stream for the current - * stack scope. This makes sure the old state is reset on the - * stream after normal OR exceptional exit from the scope, using the - * RAII C++ idiom. - */ - class Scope { - public: - Scope(std::ostream& out, bool printTypes); - ~Scope(); - - private: - std::ostream& d_out; - bool d_oldPrintTypes; - };/* class ExprPrintTypes::Scope */ - - private: - /** - * The allocated index in ios_base for our setting. - */ - static const int s_iosIndex; - - /** - * When this manipulator is used, the setting is stored here. - */ - bool d_printTypes; -};/* class ExprPrintTypes */ - /** * IOStream manipulator to print expressions as a dag (or not). */ @@ -209,18 +159,6 @@ public: */ std::ostream& operator<<(std::ostream& out, ExprDag d) CVC4_PUBLIC; - -/** - * Sets the default print-types setting when pretty-printing an Expr - * to an ostream. Use like this: - * - * // let out be an ostream, e an Expr - * out << Expr::printtypes(true) << e << endl; - * - * The setting stays permanently (until set again) with the stream. - */ -std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) CVC4_PUBLIC; - /** * Sets the default depth when pretty-printing a Expr to an ostream. * Use like this: diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 4fcbe8597..f9a743cf6 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -593,10 +593,13 @@ bool Expr::hasFreeVariable() const return expr::hasFreeVar(*d_node); } -void Expr::toStream(std::ostream& out, int depth, bool types, size_t dag, - OutputLanguage language) const { +void Expr::toStream(std::ostream& out, + int depth, + size_t dag, + OutputLanguage language) const +{ ExprManagerScope ems(*this); - d_node->toStream(out, depth, types, dag, language); + d_node->toStream(out, depth, dag, language); } Node Expr::getNode() const { return *d_node; } diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 88c43c9a2..4c863184e 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -513,13 +513,12 @@ public: * @param out the stream to serialize this expression to * @param toDepth the depth to which to print this expression, or -1 * to print it fully - * @param types set to true to ascribe types to the output - * expressions (might break language compliance, but good for - * debugging expressions) * @param dag the dagification threshold to use (0 == off) * @param language the language in which to output */ - void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const; /** diff --git a/src/expr/node.h b/src/expr/node.h index bb014bbaf..f18f27c81 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -821,19 +821,16 @@ public: * @param out the stream to serialize this node to * @param toDepth the depth to which to print this expression, or -1 to * print it fully - * @param types set to true to ascribe types to the output expressions - * (might break language compliance, but good for debugging expressions) * @param language the language in which to output */ inline void toStream( std::ostream& out, int toDepth = -1, - bool types = false, size_t dagThreshold = 1, OutputLanguage language = language::output::LANG_AUTO) const { assertTNodeNotExpired(); - d_nv->toStream(out, toDepth, types, dagThreshold, language); + d_nv->toStream(out, toDepth, dagThreshold, language); } /** @@ -852,17 +849,6 @@ public: */ typedef expr::ExprSetDepth setdepth; - /** - * IOStream manipulator to print type ascriptions or not. - * - * // let a, b, c, and d be variables of sort U - * Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d))) - * out << n; - * - * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but - */ - typedef expr::ExprPrintTypes printtypes; - /** * IOStream manipulator to print expressions as DAGs (or not). */ @@ -909,7 +895,6 @@ public: inline std::ostream& operator<<(std::ostream& out, TNode n) { n.toStream(out, Node::setdepth::getDepth(out), - Node::printtypes::getPrintTypes(out), Node::dag::getDag(out), Node::setlanguage::getLanguage(out)); return out; @@ -1523,7 +1508,6 @@ inline Node NodeTemplate::fromExpr(const Expr& e) { */ static void __attribute__((used)) debugPrintNode(const NodeTemplate& n) { Warning() << Node::setdepth(-1) - << Node::printtypes(false) << Node::dag(true) << Node::setlanguage(language::output::LANG_AST) << n << std::endl; @@ -1531,7 +1515,6 @@ static void __attribute__((used)) debugPrintNode(const NodeTemplate& n) { } static void __attribute__((used)) debugPrintNodeNoDag(const NodeTemplate& n) { Warning() << Node::setdepth(-1) - << Node::printtypes(false) << Node::dag(false) << Node::setlanguage(language::output::LANG_AST) << n << std::endl; @@ -1544,7 +1527,6 @@ static void __attribute__((used)) debugPrintRawNode(const NodeTemplate& n) static void __attribute__((used)) debugPrintTNode(const NodeTemplate& n) { Warning() << Node::setdepth(-1) - << Node::printtypes(false) << Node::dag(true) << Node::setlanguage(language::output::LANG_AST) << n << std::endl; @@ -1552,7 +1534,6 @@ static void __attribute__((used)) debugPrintTNode(const NodeTemplate& n) } static void __attribute__((used)) debugPrintTNodeNoDag(const NodeTemplate& n) { Warning() << Node::setdepth(-1) - << Node::printtypes(false) << Node::dag(false) << Node::setlanguage(language::output::LANG_AST) << n << std::endl; diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 58e5cebd9..8ceb5476a 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -39,19 +39,21 @@ string NodeValue::toString() const { OutputLanguage outlang = (this == &null()) ? language::output::LANG_AUTO : options::outputLanguage(); - toStream(ss, -1, false, false, outlang); + toStream(ss, -1, false, outlang); return ss.str(); } -void NodeValue::toStream(std::ostream& out, int toDepth, bool types, size_t dag, - OutputLanguage language) const { +void NodeValue::toStream(std::ostream& out, + int toDepth, + size_t dag, + OutputLanguage language) const +{ // Ensure that this node value is live for the length of this call. // It really breaks things badly if we don't have a nonzero ref // count, even just for printing. RefCountGuard guard(this); - Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, types, - dag); + Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, dag); } void NodeValue::printAst(std::ostream& out, int ind) const { diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 03fcaaa3c..66a7952c7 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -235,7 +235,6 @@ class NodeValue void toStream(std::ostream& out, int toDepth = -1, - bool types = false, size_t dag = 1, OutputLanguage = language::output::LANG_AUTO) const; @@ -517,7 +516,6 @@ inline T NodeValue::iterator::operator*() const { inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) { nv.toStream(out, Node::setdepth::getDepth(out), - Node::printtypes::getPrintTypes(out), Node::dag::getDag(out), Node::setlanguage::getLanguage(out)); return out; @@ -533,7 +531,6 @@ inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) { */ static void __attribute__((used)) debugPrintNodeValue(const expr::NodeValue* nv) { Warning() << Node::setdepth(-1) - << Node::printtypes(false) << Node::dag(true) << Node::setlanguage(language::output::LANG_AST) << *nv << std::endl; @@ -541,7 +538,6 @@ static void __attribute__((used)) debugPrintNodeValue(const expr::NodeValue* nv) } static void __attribute__((used)) debugPrintNodeValueNoDag(const expr::NodeValue* nv) { Warning() << Node::setdepth(-1) - << Node::printtypes(false) << Node::dag(false) << Node::setlanguage(language::output::LANG_AST) << *nv << std::endl; diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index ce3bd7438..0818ca8c1 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -675,7 +675,7 @@ bool TypeNode::isSygusDatatype() const std::string TypeNode::toString() const { std::stringstream ss; OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage(); - d_nv->toStream(ss, -1, false, 0, outlang); + d_nv->toStream(ss, -1, 0, outlang); return ss.str(); } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 41adc1d3b..90c1daf24 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -385,7 +385,7 @@ public: * @param language the language in which to output */ inline void toStream(std::ostream& out, OutputLanguage language = language::output::LANG_AUTO) const { - d_nv->toStream(out, -1, false, 0, language); + d_nv->toStream(out, -1, 0, language); } /** @@ -1121,7 +1121,6 @@ inline unsigned TypeNode::getBitVectorSize() const { */ static void __attribute__((used)) debugPrintTypeNode(const TypeNode& n) { Warning() << Node::setdepth(-1) - << Node::printtypes(false) << Node::dag(true) << Node::setlanguage(language::output::LANG_AST) << n << std::endl; @@ -1129,7 +1128,6 @@ static void __attribute__((used)) debugPrintTypeNode(const TypeNode& n) { } static void __attribute__((used)) debugPrintTypeNodeNoDag(const TypeNode& n) { Warning() << Node::setdepth(-1) - << Node::printtypes(false) << Node::dag(false) << Node::setlanguage(language::output::LANG_AST) << n << std::endl; diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml index 037d46169..368fb34e4 100644 --- a/src/options/expr_options.toml +++ b/src/options/expr_options.toml @@ -23,15 +23,6 @@ header = "options/expr_options.h" read_only = true help = "dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)" -[[option]] - name = "printExprTypes" - category = "regular" - long = "print-expr-types" - type = "bool" - default = "false" - read_only = true - help = "print types with variables when printing exprs" - [[option]] name = "typeChecking" category = "regular" diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 6feb298c2..af2faa505 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -28,7 +28,6 @@ #include "api/cvc4cpp.h" #include "base/output.h" #include "expr/expr.h" -#include "expr/expr_iomanip.h" #include "expr/kind.h" #include "expr/type.h" #include "options/options.h" @@ -435,7 +434,6 @@ std::vector Parser::bindMutualDatatypeTypes( for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) { const api::DatatypeConstructor& ctor = dt[j]; - expr::ExprPrintTypes::Scope pts(Debug("parser-idt"), true); api::Term constructor = ctor.getConstructorTerm(); Debug("parser-idt") << "+ define " << constructor << std::endl; string constructorName = ctor.getName(); diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 1ed9d146c..76549d01d 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -35,8 +35,10 @@ namespace CVC4 { namespace printer { namespace ast { -void AstPrinter::toStream( - std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const +void AstPrinter::toStream(std::ostream& out, + TNode n, + int toDepth, + size_t dag) const { if(dag != 0) { DagificationVisitor dv(dag); @@ -54,26 +56,23 @@ void AstPrinter::toStream( } else { first = false; } - toStream(out, (*i).second, toDepth, types, false); + toStream(out, (*i).second, toDepth, false); out << " := "; - toStream(out, (*i).first, toDepth, types, false); + toStream(out, (*i).first, toDepth, false); } out << " IN "; } Node body = dv.getDagifiedBody(); - toStream(out, body, toDepth, types); + toStream(out, body, toDepth); if(!lets.empty()) { out << ')'; } } else { - toStream(out, n, toDepth, types); + toStream(out, n, toDepth); } } -void AstPrinter::toStream(std::ostream& out, - TNode n, - int toDepth, - bool types) const +void AstPrinter::toStream(std::ostream& out, TNode n, int toDepth) const { // null if(n.getKind() == kind::NULL_EXPR) { @@ -89,12 +88,6 @@ void AstPrinter::toStream(std::ostream& out, } else { out << "var_" << n.getId(); } - if(types) { - // print the whole type, but not *its* type - out << ":"; - n.getType().toStream(out, language::output::LANG_AST); - } - return; } @@ -108,7 +101,7 @@ void AstPrinter::toStream(std::ostream& out, if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { out << ' '; if(toDepth != 0) { - toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types); + toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1); } else { out << "(...)"; } @@ -121,7 +114,7 @@ void AstPrinter::toStream(std::ostream& out, out << ' '; } if(toDepth != 0) { - toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, types); + toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1); } else { out << "(...)"; } diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index f01436b8a..ce621d8e1 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -34,7 +34,6 @@ class AstPrinter : 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; @@ -172,7 +171,7 @@ class AstPrinter : public CVC4::Printer std::ostream& out, const std::vector& sequence) const override; private: - void toStream(std::ostream& out, TNode n, int toDepth, bool types) const; + void toStream(std::ostream& out, TNode n, int toDepth) const; void toStream(std::ostream& out, const smt::Model& m, const NodeCommand* c) const override; diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 2a55cb972..236c87b91 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -45,8 +45,10 @@ namespace CVC4 { namespace printer { namespace cvc { -void CvcPrinter::toStream( - std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const +void CvcPrinter::toStream(std::ostream& out, + TNode n, + int toDepth, + size_t dag) const { if(dag != 0) { DagificationVisitor dv(dag); @@ -64,16 +66,16 @@ void CvcPrinter::toStream( } else { first = false; } - toStream(out, (*i).second, toDepth, types, false); + toStream(out, (*i).second, toDepth, false); out << " = "; - toStream(out, (*i).first, toDepth, types, false); + toStream(out, (*i).first, toDepth, false); } out << " IN "; } Node body = dv.getDagifiedBody(); - toStream(out, body, toDepth, types, false); + toStream(out, body, toDepth, false); } else { - toStream(out, n, toDepth, types, false); + toStream(out, n, toDepth, false); } } @@ -91,8 +93,10 @@ void toStreamRational(std::ostream& out, Node n, bool forceRational) } } -void CvcPrinter::toStream( - std::ostream& out, TNode n, int depth, bool types, bool bracket) const +void CvcPrinter::toStream(std::ostream& out, + TNode n, + int depth, + bool bracket) const { if (depth == 0) { out << "(...)"; @@ -119,11 +123,6 @@ void CvcPrinter::toStream( } out << n.getId(); } - if(types) { - // print the whole type, but not *its* type - out << ":"; - n.getType().toStream(out, language::output::LANG_CVC4); - } return; } if(n.isNullaryOp()) { @@ -287,11 +286,11 @@ void CvcPrinter::toStream( break; case kind::ITE: out << "IF "; - toStream(out, n[0], depth, types, true); + toStream(out, n[0], depth, true); out << " THEN "; - toStream(out, n[1], depth, types, true); + toStream(out, n[1], depth, true); out << " ELSE "; - toStream(out, n[2], depth, types, true); + toStream(out, n[2], depth, true); out << " ENDIF"; return; break; @@ -301,7 +300,7 @@ void CvcPrinter::toStream( if (i > 0) { out << ", "; } - toStream(out, n[i], depth, types, false); + toStream(out, n[i], depth, false); } out << ']'; return; @@ -311,22 +310,22 @@ void CvcPrinter::toStream( break; case kind::LAMBDA: out << "(LAMBDA"; - toStream(out, n[0], depth, types, true); + toStream(out, n[0], depth, true); out << ": "; - toStream(out, n[1], depth, types, true); + toStream(out, n[1], depth, true); out << ")"; return; break; case kind::WITNESS: out << "(WITNESS"; - toStream(out, n[0], depth, types, false); + toStream(out, n[0], depth, false); out << " : "; - toStream(out, n[1], depth, types, false); + toStream(out, n[1], depth, false); out << ')'; return; case kind::DISTINCT: // distinct not supported directly, blast it away with the rewriter - toStream(out, theory::Rewriter::rewrite(n), depth, types, true); + toStream(out, theory::Rewriter::rewrite(n), depth, true); return; case kind::SORT_TYPE: { @@ -361,9 +360,7 @@ void CvcPrinter::toStream( break; // UF - case kind::APPLY_UF: - toStream(op, n.getOperator(), depth, types, false); - break; + case kind::APPLY_UF: toStream(op, n.getOperator(), depth, false); break; case kind::CARDINALITY_CONSTRAINT: case kind::COMBINED_CARDINALITY_CONSTRAINT: out << "CARDINALITY_CONSTRAINT"; @@ -378,14 +375,14 @@ void CvcPrinter::toStream( if (i > 1) { out << ", "; } - toStream(out, n[i - 1], depth, types, false); + toStream(out, n[i - 1], depth, false); } if (n.getNumChildren() > 2) { out << ')'; } } out << " -> "; - toStream(out, n[n.getNumChildren() - 1], depth, types, false); + toStream(out, n[n.getNumChildren() - 1], depth, false); return; break; @@ -407,10 +404,10 @@ void CvcPrinter::toStream( return; break; case kind::APPLY_TYPE_ASCRIPTION: { - toStream(out, n[0], depth, types, false); - out << "::"; - TypeNode t = n.getOperator().getConst().getType(); - out << (t.isFunctionLike() ? t.getRangeType() : t); + toStream(out, n[0], depth, false); + out << "::"; + TypeNode t = n.getOperator().getConst().getType(); + out << (t.isFunctionLike() ? t.getRangeType() : t); } return; break; @@ -433,14 +430,14 @@ void CvcPrinter::toStream( out << ", "; } out << recCons[i].getName() << " := "; - toStream(out, n[i], depth, types, false); + toStream(out, n[i], depth, false); } out << " #)"; return; } else { - toStream(op, n.getOperator(), depth, types, false); + toStream(op, n.getOperator(), depth, false); if (n.getNumChildren() == 0) { // for datatype constants d, we print "d" and not "d()" @@ -456,11 +453,11 @@ void CvcPrinter::toStream( Node opn = n.getOperator(); if (!t.isDatatype()) { - toStream(op, opn, depth, types, false); + toStream(op, opn, depth, false); } else if (t.isTuple() || t.isRecord()) { - toStream(out, n[0], depth, types, true); + toStream(out, n[0], depth, true); out << '.'; const DType& dt = t.getDType(); if (t.isTuple()) @@ -479,11 +476,11 @@ void CvcPrinter::toStream( } else { - toStream(out, opn, depth, types, false); + toStream(out, opn, depth, false); } return; }else{ - toStream(op, opn, depth, types, false); + toStream(op, opn, depth, false); } } break; @@ -492,7 +489,7 @@ void CvcPrinter::toStream( op << "is_"; unsigned cindex = DType::indexOf(n.getOperator()); const DType& dt = DType::datatypeOf(n.getOperator()); - toStream(op, dt[cindex].getConstructor(), depth, types, false); + toStream(op, dt[cindex].getConstructor(), depth, false); } break; case kind::CONSTRUCTOR_TYPE: @@ -505,45 +502,45 @@ void CvcPrinter::toStream( if(i > 0) { out << ", "; } - toStream(out, n[i], depth, types, false); + toStream(out, n[i], depth, false); } if(n.getNumChildren() > 2) { out << ')'; } out << " -> "; } - toStream(out, n[n.getNumChildren() - 1], depth, types, false); + toStream(out, n[n.getNumChildren() - 1], depth, false); return; case kind::TESTER_TYPE: - toStream(out, n[0], depth, types, false); + toStream(out, n[0], depth, false); out << " -> BOOLEAN"; return; break; case kind::TUPLE_UPDATE: - toStream(out, n[0], depth, types, true); + toStream(out, n[0], depth, true); out << " WITH ." << n.getOperator().getConst().getIndex() << " := "; - toStream(out, n[1], depth, types, true); + toStream(out, n[1], depth, true); return; break; case kind::RECORD_UPDATE: - toStream(out, n[0], depth, types, true); + toStream(out, n[0], depth, true); out << " WITH ." << n.getOperator().getConst().getField() << " := "; - toStream(out, n[1], depth, types, true); + toStream(out, n[1], depth, true); return; break; // ARRAYS case kind::ARRAY_TYPE: out << "ARRAY "; - toStream(out, n[0], depth, types, false); + toStream(out, n[0], depth, false); out << " OF "; - toStream(out, n[1], depth, types, false); + toStream(out, n[1], depth, false); return; break; case kind::SELECT: - toStream(out, n[0], depth, types, true); + toStream(out, n[0], depth, true); out << '['; - toStream(out, n[1], depth, types, false); + toStream(out, n[1], depth, false); out << ']'; return; break; @@ -557,18 +554,18 @@ void CvcPrinter::toStream( out << '('; } TNode x = stk.top(); - toStream(out, x[0], depth, types, false); + toStream(out, x[0], depth, false); out << " WITH ["; - toStream(out, x[1], depth, types, false); + toStream(out, x[1], depth, false); out << "] := "; - toStream(out, x[2], depth, types, false); + toStream(out, x[2], depth, false); stk.pop(); while(!stk.empty()) { x = stk.top(); out << ", ["; - toStream(out, x[1], depth, types, false); + toStream(out, x[1], depth, false); out << "] := "; - toStream(out, x[2], depth, types, false); + toStream(out, x[2], depth, false); stk.pop(); } if (bracket) { @@ -654,13 +651,13 @@ void CvcPrinter::toStream( else { // ignore, there is no to-real in CVC language - toStream(out, n[0], depth, types, false); + toStream(out, n[0], depth, false); } return; } case kind::DIVISIBLE: out << "DIVISIBLE("; - toStream(out, n[0], depth, types, false); + toStream(out, n[0], depth, false); out << ", " << n.getOperator().getConst().k << ")"; return; @@ -761,16 +758,16 @@ void CvcPrinter::toStream( out << "BVPLUS("; out << BitVectorType(n.getType().toType()).getSize(); out << ','; - toStream(out, n[child], depth, types, false); + toStream(out, n[child], depth, false); out << ','; ++child; } out << "BVPLUS("; out << BitVectorType(n.getType().toType()).getSize(); out << ','; - toStream(out, n[child], depth, types, false); + toStream(out, n[child], depth, false); out << ','; - toStream(out, n[child + 1], depth, types, false); + toStream(out, n[child + 1], depth, false); while (child > 0) { out << ')'; --child; @@ -784,9 +781,9 @@ void CvcPrinter::toStream( Assert(n.getType().isBitVector()); out << BitVectorType(n.getType().toType()).getSize(); out << ','; - toStream(out, n[0], depth, types, false); + toStream(out, n[0], depth, false); out << ','; - toStream(out, n[1], depth, types, false); + toStream(out, n[1], depth, false); out << ')'; return; break; @@ -798,16 +795,16 @@ void CvcPrinter::toStream( out << "BVMULT("; out << BitVectorType(n.getType().toType()).getSize(); out << ','; - toStream(out, n[child], depth, types, false); + toStream(out, n[child], depth, false); out << ','; ++child; } out << "BVMULT("; out << BitVectorType(n.getType().toType()).getSize(); out << ','; - toStream(out, n[child], depth, types, false); + toStream(out, n[child], depth, false); out << ','; - toStream(out, n[child + 1], depth, types, false); + toStream(out, n[child + 1], depth, false); while (child > 0) { out << ')'; --child; @@ -826,31 +823,31 @@ void CvcPrinter::toStream( break; case kind::BITVECTOR_REPEAT: out << "BVREPEAT("; - toStream(out, n[0], depth, types, false); + toStream(out, n[0], depth, false); out << ", " << n.getOperator().getConst() << ')'; return; break; case kind::BITVECTOR_ZERO_EXTEND: out << "BVZEROEXTEND("; - toStream(out, n[0], depth, types, false); + toStream(out, n[0], depth, false); out << ", " << n.getOperator().getConst() << ')'; return; break; case kind::BITVECTOR_SIGN_EXTEND: out << "SX("; - toStream(out, n[0], depth, types, false); + toStream(out, n[0], depth, false); out << ", " << BitVectorType(n.getType().toType()).getSize() << ')'; return; break; case kind::BITVECTOR_ROTATE_LEFT: out << "BVROTL("; - toStream(out, n[0], depth, types, false); + toStream(out, n[0], depth, false); out << ", " << n.getOperator().getConst() << ')'; return; break; case kind::BITVECTOR_ROTATE_RIGHT: out << "BVROTR("; - toStream(out, n[0], depth, types, false); + toStream(out, n[0], depth, false); out << ", " << n.getOperator().getConst() << ')'; return; break; @@ -858,7 +855,7 @@ void CvcPrinter::toStream( // SETS case kind::SET_TYPE: out << "SET OF "; - toStream(out, n[0], depth, types, false); + toStream(out, n[0], depth, false); return; break; case kind::UNION: @@ -911,7 +908,7 @@ void CvcPrinter::toStream( break; case kind::SINGLETON: out << "{"; - toStream(out, n[0], depth, types, false); + toStream(out, n[0], depth, false); out << "}"; return; break; @@ -921,13 +918,13 @@ void CvcPrinter::toStream( } out << '{'; size_t i = 0; - toStream(out, n[i++], depth, types, false); + toStream(out, n[i++], depth, false); for(;i+1 < n.getNumChildren(); ++i) { out << ", "; - toStream(out, n[i], depth, types, false); + toStream(out, n[i], depth, false); } out << "} | "; - toStream(out, n[i], depth, types, true); + toStream(out, n[i], depth, true); if(bracket) { out << ')'; } @@ -936,7 +933,7 @@ void CvcPrinter::toStream( } case kind::CARD: { out << "CARD("; - toStream(out, n[0], depth, types, false); + toStream(out, n[0], depth, false); out << ")"; return; break; @@ -945,17 +942,17 @@ void CvcPrinter::toStream( // Quantifiers case kind::FORALL: out << "(FORALL"; - toStream(out, n[0], depth, types, false); + toStream(out, n[0], depth, false); out << " : "; - toStream(out, n[1], depth, types, false); + toStream(out, n[1], depth, false); out << ')'; // TODO: user patterns? return; case kind::EXISTS: out << "(EXISTS"; - toStream(out, n[0], depth, types, false); + toStream(out, n[0], depth, false); out << " : "; - toStream(out, n[1], depth, types, false); + toStream(out, n[1], depth, false); out << ')'; // TODO: user patterns? return; @@ -968,7 +965,9 @@ void CvcPrinter::toStream( if(i > 0) { out << ", "; } - toStream(out, n[i], -1, true, false); // ascribe types + toStream(out, n[i], -1, false); + out << ":"; + n[i].getType().toStream(out, language::output::LANG_CVC4); } out << ')'; return; @@ -1022,7 +1021,7 @@ void CvcPrinter::toStream( out << ", "; } } - toStream(out, n[i], depth, types, opType == INFIX); + toStream(out, n[i], depth, opType == INFIX); } switch (opType) { diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index 4047f0d8b..934caf91b 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -35,7 +35,6 @@ class CvcPrinter : 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; @@ -173,8 +172,7 @@ class CvcPrinter : public CVC4::Printer std::ostream& out, const std::vector& sequence) const override; private: - void toStream( - std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const; + void toStream(std::ostream& out, TNode n, int toDepth, bool bracket) const; void toStream(std::ostream& out, const smt::Model& m, const NodeCommand* c) const override; diff --git a/src/printer/printer.h b/src/printer/printer.h index 85b16175f..84262d992 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -51,7 +51,6 @@ class Printer virtual void toStream(std::ostream& out, TNode n, int toDepth, - bool types, size_t dag) const = 0; /** Write a CommandStatus out to a stream with this Printer. */ 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; diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index d18d0c1fd..92bbc52e8 100644 --- a/src/printer/tptp/tptp_printer.cpp +++ b/src/printer/tptp/tptp_printer.cpp @@ -35,10 +35,12 @@ namespace CVC4 { namespace printer { namespace tptp { -void TptpPrinter::toStream( - std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const +void TptpPrinter::toStream(std::ostream& out, + TNode n, + int toDepth, + size_t dag) const { - n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5); + n.toStream(out, toDepth, dag, language::output::LANG_SMTLIB_V2_5); }/* TptpPrinter::toStream() */ void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h index 84bb3e576..449fe409c 100644 --- a/src/printer/tptp/tptp_printer.h +++ b/src/printer/tptp/tptp_printer.h @@ -34,7 +34,6 @@ class TptpPrinter : 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; diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 8a5247dec..d6fb470a3 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -53,7 +53,6 @@ std::ostream& operator<<(std::ostream& out, const Command& c) { c.toStream(out, Node::setdepth::getDepth(out), - Node::printtypes::getPrintTypes(out), Node::dag::getDag(out), Node::setlanguage::getLanguage(out)); return out; @@ -227,7 +226,7 @@ std::string EmptyCommand::getCommandName() const { return "empty"; } void EmptyCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -262,7 +261,7 @@ std::string EchoCommand::getCommandName() const { return "echo"; } void EchoCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -305,7 +304,7 @@ std::string AssertCommand::getCommandName() const { return "assert"; } void AssertCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -338,7 +337,7 @@ std::string PushCommand::getCommandName() const { return "push"; } void PushCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -371,7 +370,7 @@ std::string PopCommand::getCommandName() const { return "pop"; } void PopCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -429,7 +428,7 @@ std::string CheckSatCommand::getCommandName() const { return "check-sat"; } void CheckSatCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -504,7 +503,7 @@ std::string CheckSatAssumingCommand::getCommandName() const void CheckSatAssumingCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -559,7 +558,7 @@ std::string QueryCommand::getCommandName() const { return "query"; } void QueryCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -597,7 +596,7 @@ std::string DeclareSygusVarCommand::getCommandName() const void DeclareSygusVarCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -654,7 +653,7 @@ std::string SynthFunCommand::getCommandName() const void SynthFunCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -703,7 +702,7 @@ std::string SygusConstraintCommand::getCommandName() const void SygusConstraintCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -759,7 +758,7 @@ std::string SygusInvConstraintCommand::getCommandName() const void SygusInvConstraintCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -833,7 +832,7 @@ std::string CheckSynthCommand::getCommandName() const { return "check-synth"; } void CheckSynthCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -862,7 +861,7 @@ std::string ResetCommand::getCommandName() const { return "reset"; } void ResetCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -898,7 +897,7 @@ std::string ResetAssertionsCommand::getCommandName() const void ResetAssertionsCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -920,7 +919,7 @@ std::string QuitCommand::getCommandName() const { return "exit"; } void QuitCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -944,7 +943,7 @@ std::string CommentCommand::getCommandName() const { return "comment"; } void CommentCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -1041,7 +1040,7 @@ std::string CommandSequence::getCommandName() const { return "sequence"; } void CommandSequence::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -1055,7 +1054,7 @@ void CommandSequence::toStream(std::ostream& out, void DeclarationSequence::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -1125,7 +1124,7 @@ std::string DeclareFunctionCommand::getCommandName() const void DeclareFunctionCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -1163,7 +1162,7 @@ std::string DeclareSortCommand::getCommandName() const void DeclareSortCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -1207,7 +1206,7 @@ std::string DefineSortCommand::getCommandName() const { return "define-sort"; } void DefineSortCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -1284,7 +1283,7 @@ std::string DefineFunctionCommand::getCommandName() const void DefineFunctionCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -1329,7 +1328,7 @@ Command* DefineNamedFunctionCommand::clone() const void DefineNamedFunctionCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -1409,7 +1408,7 @@ std::string DefineFunctionRecCommand::getCommandName() const void DefineFunctionRecCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -1493,7 +1492,7 @@ std::string SetUserAttributeCommand::getCommandName() const void SetUserAttributeCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -1548,7 +1547,7 @@ std::string SimplifyCommand::getCommandName() const { return "simplify"; } void SimplifyCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -1637,7 +1636,7 @@ std::string GetValueCommand::getCommandName() const { return "get-value"; } void GetValueCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -1709,7 +1708,7 @@ std::string GetAssignmentCommand::getCommandName() const void GetAssignmentCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -1771,7 +1770,7 @@ std::string GetModelCommand::getCommandName() const { return "get-model"; } void GetModelCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -1814,7 +1813,7 @@ std::string BlockModelCommand::getCommandName() const { return "block-model"; } void BlockModelCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -1872,7 +1871,7 @@ std::string BlockModelValuesCommand::getCommandName() const void BlockModelValuesCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -1900,7 +1899,7 @@ std::string GetProofCommand::getCommandName() const { return "get-proof"; } void GetProofCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -1953,7 +1952,7 @@ std::string GetInstantiationsCommand::getCommandName() const void GetInstantiationsCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -2005,7 +2004,7 @@ std::string GetSynthSolutionCommand::getCommandName() const void GetSynthSolutionCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -2095,7 +2094,7 @@ std::string GetInterpolCommand::getCommandName() const void GetInterpolCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -2181,7 +2180,7 @@ std::string GetAbductCommand::getCommandName() const { return "get-abduct"; } void GetAbductCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -2257,7 +2256,7 @@ std::string GetQuantifierEliminationCommand::getCommandName() const void GetQuantifierEliminationCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -2320,7 +2319,7 @@ std::string GetUnsatAssumptionsCommand::getCommandName() const void GetUnsatAssumptionsCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -2386,7 +2385,7 @@ std::string GetUnsatCoreCommand::getCommandName() const void GetUnsatCoreCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -2444,7 +2443,7 @@ std::string GetAssertionsCommand::getCommandName() const void GetAssertionsCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -2492,7 +2491,7 @@ std::string SetBenchmarkStatusCommand::getCommandName() const void SetBenchmarkStatusCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -2542,7 +2541,7 @@ std::string SetBenchmarkLogicCommand::getCommandName() const void SetBenchmarkLogicCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -2587,7 +2586,7 @@ std::string SetInfoCommand::getCommandName() const { return "set-info"; } void SetInfoCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -2654,7 +2653,7 @@ std::string GetInfoCommand::getCommandName() const { return "get-info"; } void GetInfoCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -2698,7 +2697,7 @@ std::string SetOptionCommand::getCommandName() const { return "set-option"; } void SetOptionCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -2752,7 +2751,7 @@ std::string GetOptionCommand::getCommandName() const { return "get-option"; } void GetOptionCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -2788,7 +2787,7 @@ std::string SetExpressionNameCommand::getCommandName() const void SetExpressionNameCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { @@ -2835,7 +2834,7 @@ std::string DatatypeDeclarationCommand::getCommandName() const void DatatypeDeclarationCommand::toStream(std::ostream& out, int toDepth, - bool types, + size_t dag, OutputLanguage language) const { diff --git a/src/smt/command.h b/src/smt/command.h index 7088c09ed..d2ce99f2f 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -208,7 +208,7 @@ class CVC4_PUBLIC Command virtual void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const = 0; @@ -282,7 +282,7 @@ class CVC4_PUBLIC EmptyCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -305,7 +305,7 @@ class CVC4_PUBLIC EchoCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -331,7 +331,7 @@ class CVC4_PUBLIC AssertCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class AssertCommand */ @@ -345,7 +345,7 @@ class CVC4_PUBLIC PushCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class PushCommand */ @@ -359,7 +359,7 @@ class CVC4_PUBLIC PopCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class PopCommand */ @@ -398,7 +398,7 @@ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DeclareFunctionCommand */ @@ -421,7 +421,7 @@ class CVC4_PUBLIC DeclareSortCommand : public DeclarationDefinitionCommand void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DeclareSortCommand */ @@ -447,7 +447,7 @@ class CVC4_PUBLIC DefineSortCommand : public DeclarationDefinitionCommand void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DefineSortCommand */ @@ -475,7 +475,7 @@ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -511,7 +511,7 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DefineNamedFunctionCommand */ @@ -543,7 +543,7 @@ class CVC4_PUBLIC DefineFunctionRecCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -582,7 +582,7 @@ class CVC4_PUBLIC SetUserAttributeCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -617,7 +617,7 @@ class CVC4_PUBLIC CheckSatCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -646,7 +646,7 @@ class CVC4_PUBLIC CheckSatAssumingCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -674,7 +674,7 @@ class CVC4_PUBLIC QueryCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class QueryCommand */ @@ -704,7 +704,7 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -754,7 +754,7 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -792,7 +792,7 @@ class CVC4_PUBLIC SygusConstraintCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -836,7 +836,7 @@ class CVC4_PUBLIC SygusInvConstraintCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -873,7 +873,7 @@ class CVC4_PUBLIC CheckSynthCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -905,7 +905,7 @@ class CVC4_PUBLIC SimplifyCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SimplifyCommand */ @@ -929,7 +929,7 @@ class CVC4_PUBLIC GetValueCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetValueCommand */ @@ -950,7 +950,7 @@ class CVC4_PUBLIC GetAssignmentCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetAssignmentCommand */ @@ -969,7 +969,7 @@ class CVC4_PUBLIC GetModelCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -989,7 +989,7 @@ class CVC4_PUBLIC BlockModelCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class BlockModelCommand */ @@ -1007,7 +1007,7 @@ class CVC4_PUBLIC BlockModelValuesCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1027,7 +1027,7 @@ class CVC4_PUBLIC GetProofCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetProofCommand */ @@ -1044,7 +1044,7 @@ class CVC4_PUBLIC GetInstantiationsCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1064,7 +1064,7 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1103,7 +1103,7 @@ class CVC4_PUBLIC GetInterpolCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1155,7 +1155,7 @@ class CVC4_PUBLIC GetAbductCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1194,7 +1194,7 @@ class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetQuantifierEliminationCommand */ @@ -1211,7 +1211,7 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1233,7 +1233,7 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1260,7 +1260,6 @@ class CVC4_PUBLIC GetAssertionsCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetAssertionsCommand */ @@ -1281,7 +1280,6 @@ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SetBenchmarkStatusCommand */ @@ -1301,7 +1299,6 @@ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SetBenchmarkLogicCommand */ @@ -1324,7 +1321,6 @@ class CVC4_PUBLIC SetInfoCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SetInfoCommand */ @@ -1348,7 +1344,6 @@ class CVC4_PUBLIC GetInfoCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetInfoCommand */ @@ -1371,7 +1366,7 @@ class CVC4_PUBLIC SetOptionCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SetOptionCommand */ @@ -1395,7 +1390,7 @@ class CVC4_PUBLIC GetOptionCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetOptionCommand */ @@ -1422,7 +1417,7 @@ class CVC4_PUBLIC SetExpressionNameCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SetExpressionNameCommand */ @@ -1443,7 +1438,7 @@ class CVC4_PUBLIC DatatypeDeclarationCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DatatypeDeclarationCommand */ @@ -1458,7 +1453,7 @@ class CVC4_PUBLIC ResetCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class ResetCommand */ @@ -1473,7 +1468,7 @@ class CVC4_PUBLIC ResetAssertionsCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class ResetAssertionsCommand */ @@ -1488,7 +1483,7 @@ class CVC4_PUBLIC QuitCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class QuitCommand */ @@ -1508,7 +1503,7 @@ class CVC4_PUBLIC CommentCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class CommentCommand */ @@ -1545,7 +1540,7 @@ class CVC4_PUBLIC CommandSequence : public Command void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class CommandSequence */ @@ -1555,7 +1550,7 @@ class CVC4_PUBLIC DeclarationSequence : public CommandSequence void toStream( std::ostream& out, int toDepth = -1, - bool types = false, + size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp index d1a8c5c28..eb2493c87 100644 --- a/src/smt/node_command.cpp +++ b/src/smt/node_command.cpp @@ -37,7 +37,6 @@ std::ostream& operator<<(std::ostream& out, const NodeCommand& nc) { nc.toStream(out, Node::setdepth::getDepth(out), - Node::printtypes::getPrintTypes(out), Node::dag::getDag(out), Node::setlanguage::getLanguage(out)); return out; @@ -60,7 +59,6 @@ DeclareFunctionNodeCommand::DeclareFunctionNodeCommand(const std::string& id, void DeclareFunctionNodeCommand::toStream(std::ostream& out, int toDepth, - bool types, size_t dag, OutputLanguage language) const { @@ -103,7 +101,6 @@ DeclareTypeNodeCommand::DeclareTypeNodeCommand(const std::string& id, void DeclareTypeNodeCommand::toStream(std::ostream& out, int toDepth, - bool types, size_t dag, OutputLanguage language) const { @@ -132,7 +129,6 @@ DeclareDatatypeNodeCommand::DeclareDatatypeNodeCommand( void DeclareDatatypeNodeCommand::toStream(std::ostream& out, int toDepth, - bool types, size_t dag, OutputLanguage language) const { @@ -160,7 +156,6 @@ DefineFunctionNodeCommand::DefineFunctionNodeCommand( void DefineFunctionNodeCommand::toStream(std::ostream& out, int toDepth, - bool types, size_t dag, OutputLanguage language) const { diff --git a/src/smt/node_command.h b/src/smt/node_command.h index 1153f8786..8cf9a5e10 100644 --- a/src/smt/node_command.h +++ b/src/smt/node_command.h @@ -41,7 +41,6 @@ class NodeCommand virtual void toStream( std::ostream& out, int toDepth = -1, - bool types = false, size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const = 0; @@ -65,7 +64,6 @@ class DeclareFunctionNodeCommand : public NodeCommand void toStream( std::ostream& out, int toDepth = -1, - bool types = false, size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; NodeCommand* clone() const override; @@ -93,7 +91,6 @@ class DeclareDatatypeNodeCommand : public NodeCommand void toStream( std::ostream& out, int toDepth = -1, - bool types = false, size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; NodeCommand* clone() const override; @@ -113,7 +110,6 @@ class DeclareTypeNodeCommand : public NodeCommand void toStream( std::ostream& out, int toDepth = -1, - bool types = false, size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; NodeCommand* clone() const override; @@ -140,7 +136,6 @@ class DefineFunctionNodeCommand : public NodeCommand void toStream( std::ostream& out, int toDepth = -1, - bool types = false, size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; NodeCommand* clone() const override; diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp index 5492202bf..81e13c446 100644 --- a/src/smt/options_manager.cpp +++ b/src/smt/options_manager.cpp @@ -39,10 +39,6 @@ OptionsManager::OptionsManager(Options* opts, ResourceManager* rm) { notifySetOption(options::defaultDagThresh.getName()); } - if (opts->wasSetByUser(options::printExprTypes)) - { - notifySetOption(options::printExprTypes.getName()); - } if (opts->wasSetByUser(options::dumpModeString)) { notifySetOption(options::dumpModeString.getName()); @@ -95,17 +91,6 @@ void OptionsManager::notifySetOption(const std::string& key) Warning.getStream() << expr::ExprDag(dag); Dump.getStream() << expr::ExprDag(dag); } - else if (key == options::printExprTypes.getName()) - { - bool value = (*d_options)[options::printExprTypes]; - Debug.getStream() << expr::ExprPrintTypes(value); - Trace.getStream() << expr::ExprPrintTypes(value); - Notice.getStream() << expr::ExprPrintTypes(value); - Chat.getStream() << expr::ExprPrintTypes(value); - Message.getStream() << expr::ExprPrintTypes(value); - Warning.getStream() << expr::ExprPrintTypes(value); - // intentionally exclude Dump stream from this list - } else if (key == options::dumpModeString.getName()) { const std::string& value = (*d_options)[options::dumpModeString]; diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h index 5b74cf30c..e2a482e30 100644 --- a/src/smt/update_ostream.h +++ b/src/smt/update_ostream.h @@ -37,21 +37,18 @@ class ChannelSettings { ChannelSettings(std::ostream& out) : d_dagSetting(expr::ExprDag::getDag(out)), d_exprDepthSetting(expr::ExprSetDepth::getDepth(out)), - d_printtypesSetting(expr::ExprPrintTypes::getPrintTypes(out)), d_languageSetting(language::SetLanguage::getLanguage(out)) {} void apply(std::ostream& out) { out << expr::ExprDag(d_dagSetting); out << expr::ExprSetDepth(d_exprDepthSetting); - out << expr::ExprPrintTypes(d_printtypesSetting); out << language::SetLanguage(d_languageSetting); } private: const int d_dagSetting; const size_t d_exprDepthSetting; - const bool d_printtypesSetting; const OutputLanguage d_languageSetting; }; /* class ChannelSettings */ diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 9589d4cc0..5b82e0a58 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -550,7 +550,7 @@ class NodeBlack : public CxxTest::TestSuite { TS_ASSERT(sstr.str() == "(AND w (OR x y) z)"); sstr.str(string()); - o.toStream(sstr, -1, false, 0); + o.toStream(sstr, -1, 0); TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))"); sstr.str(string()); -- 2.30.2