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.

2 files changed, 28 insertions, 35 deletions

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;