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.

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
@@ -92,56 +92,6 @@ public:
 };/* 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).
  */
 class CVC4_PUBLIC ExprDag {
@@ -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);
   }
 
   /**
@@ -853,17 +850,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).
    */
   typedef expr::ExprDag dag;
@@ -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<true>::fromExpr(const Expr& e) {
  */
 static void __attribute__((used)) debugPrintNode(const NodeTemplate<true>& 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<true>& n) {
 }
 static void __attribute__((used)) debugPrintNodeNoDag(const NodeTemplate<true>& 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<true>& n)
 
 static void __attribute__((used)) debugPrintTNode(const NodeTemplate<false>& 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<false>& n)
 }
 static void __attribute__((used)) debugPrintTNodeNoDag(const NodeTemplate<false>& 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<T>::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
@@ -24,15 +24,6 @@ header = "options/expr_options.h"
   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"
   long       = "type-checking"
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<api::Sort> 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<Command*>& 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<AscriptionType>().getType();
-        out << (t.isFunctionLike() ? t.getRangeType() : t);
+      toStream(out, n[0], depth, false);
+      out << "::";
+      TypeNode t = n.getOperator().getConst<AscriptionType>().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<TupleUpdate>().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<RecordUpdate>().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<Divisible>().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<BitVectorRepeat>() << ')';
       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<BitVectorZeroExtend>() << ')';
       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<BitVectorRotateLeft>() << ')';
       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<BitVectorRotateRight>() << ')';
       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<Command*>& 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<Command*>& 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());