Collapse @ chains in SMT2 printer (#3140)

diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml
index 89ae3b559996a4b23e917657fbd5db5f0d23d4f4..c1871259c3bc38a826db30e89083f046e0b84931 100644 (file)
--- a/src/options/printer_options.toml
+++ b/src/options/printer_options.toml
@@ -21,3 +21,11 @@ header = "options/printer_options.h"
   handler    = "stringToInstFormatMode"
   includes   = ["options/printer_modes.h"]
   help       = "print format mode for instantiations, see --inst-format=help"
+
+[[option]]
+  name       = "flattenHOChains"
+  category   = "regular"
+  long       = "flatten-ho-chains"
+  type       = "bool"
+  default    = "false"
+  help       = "print (binary) application chains in a flattened way, e.g. (a b c) rather than ((a b) c)"

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 163c8acadc59ccf1212f478998508f7b35abe965..fd8b4ce85f862a1f7c7248d15ca9187c956d0464 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -24,6 +24,7 @@
 #include "expr/node_manager_attributes.h"
 #include "options/bv_options.h"
 #include "options/language.h"
+#include "options/printer_options.h"
 #include "options/smt_options.h"
 #include "printer/dagification_visitor.h"
 #include "smt/smt_engine.h"
@@ -509,7 +510,34 @@ void Smt2Printer::toStream(std::ostream& out,
   // uf theory
   case kind::APPLY_UF: typeChildren = true; break;
   // higher-order
-  case kind::HO_APPLY: break;
+  case kind::HO_APPLY:
+    if (!options::flattenHOChains())
+    {
+      break;
+    }
+    // collapse "@" chains, i.e.
+    //
+    // ((a b) c) --> (a b c)
+    //
+    // (((a b) ((c d) e)) f) --> (a b (c d e) f)
+    {
+      Node head = n;
+      std::vector<Node> args;
+      while (head.getKind() == kind::HO_APPLY)
+      {
+        args.insert(args.begin(), head[1]);
+        head = head[0];
+      }
+      toStream(out, head, toDepth, types, TypeNode::null());
+      for (unsigned i = 0, size = args.size(); i < size; ++i)
+      {
+        out << " ";
+        toStream(out, args[i], toDepth, types, TypeNode::null());
+      }
+      out << ")";
+    }
+    return;
+
   case kind::LAMBDA:
     out << smtKindString(k, d_variant) << " ";
     break;