Higher-order prep (#1338)

* Minor preparation for final higher-order merge.

* Format

1 files changed, 55 insertions, 37 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index f292c0a2e..3caeeaaaa 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -116,43 +116,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     return;
   }
 
-  if( !force_nt.isNull() && n.getKind()!=kind::CONST_RATIONAL ){
-    if( n.getType()!=force_nt ){
-      if( force_nt.isReal() ){
-        out << "(" << smtKindString( force_nt.isInteger() ? kind::TO_INTEGER : kind::TO_REAL) << " ";
-        toStream(out, n, toDepth, types, TypeNode::null());
-        out << ")";
-      }else{            
-        Node nn = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
-                                                   NodeManager::currentNM()->mkConst(AscriptionType(force_nt.toType())), n );
-        toStream(out, nn, toDepth, types, TypeNode::null());                                 
-      }
-      return;  
-    }
-  }
-
-  // variable
-  if(n.isVar()) {
-    string s;
-    if(n.getAttribute(expr::VarNameAttr(), s)) {
-      out << maybeQuoteSymbol(s);
-    } else {
-      if(n.getKind() == kind::VARIABLE) {
-        out << "var_";
-      } else {
-        out << n.getKind() << '_';
-      }
-      out << n.getId();
-    }
-    if(types) {
-      // print the whole type, but not *its* type
-      out << ":";
-      n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5);
-    }
-
-    return;
-  }
-
   // constant
   if(n.getMetaKind() == kind::metakind::CONSTANT) {
     switch(n.getKind()) {
@@ -325,6 +288,61 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     return;
   }
 
+  if (!force_nt.isNull())
+  {
+    if (n.getType() != force_nt)
+    {
+      if (force_nt.isReal())
+      {
+        out << "(" << smtKindString(force_nt.isInteger() ? kind::TO_INTEGER
+                                                         : kind::TO_REAL)
+            << " ";
+        toStream(out, n, toDepth, types, TypeNode::null());
+        out << ")";
+      }
+      else
+      {
+        Node nn = NodeManager::currentNM()->mkNode(
+            kind::APPLY_TYPE_ASCRIPTION,
+            NodeManager::currentNM()->mkConst(
+                AscriptionType(force_nt.toType())),
+            n);
+        toStream(out, nn, toDepth, types, TypeNode::null());
+      }
+      return;
+    }
+  }
+
+  // variable
+  if (n.isVar())
+  {
+    string s;
+    if (n.getAttribute(expr::VarNameAttr(), s))
+    {
+      out << maybeQuoteSymbol(s);
+    }
+    else
+    {
+      if (n.getKind() == kind::VARIABLE)
+      {
+        out << "var_";
+      }
+      else
+      {
+        out << n.getKind() << '_';
+      }
+      out << n.getId();
+    }
+    if (types)
+    {
+      // print the whole type, but not *its* type
+      out << ":";
+      n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5);
+    }
+
+    return;
+  }
+
   bool stillNeedToPrintParams = true;
   bool forceBinary = false; // force N-ary to binary when outputing children
   bool parametricTypeChildren = false;   // parametric operators that are (op t1 ... tn) where t1...tn must have same type