From 92e7cf5d0cbba4d2979f8643f73db2caf02c256c Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Tue, 18 Nov 2025 09:38:22 -0800
Subject: [PATCH] SMV: move parse tree output into a method

This makes the code for outputting a parse tree a method of the parse tree
class.
---
 src/smvlang/smv_language.cpp   | 52 +----------------------------
 src/smvlang/smv_parse_tree.cpp | 60 ++++++++++++++++++++++++++++++++++
 src/smvlang/smv_parse_tree.h   |  3 ++
 3 files changed, 64 insertions(+), 51 deletions(-)

diff --git a/src/smvlang/smv_language.cpp b/src/smvlang/smv_language.cpp
index 06235bb3f..fd9068822 100644
--- a/src/smvlang/smv_language.cpp
+++ b/src/smvlang/smv_language.cpp
@@ -129,57 +129,7 @@ Function: smv_languaget::show_parse
 
 void smv_languaget::show_parse(std::ostream &out, message_handlert &)
 {
-  for(smv_parse_treet::modulest::const_iterator
-      it=smv_parse_tree.modules.begin();
-      it!=smv_parse_tree.modules.end(); it++)
-  {
-    const smv_parse_treet::modulet &module=it->second;
-    out << "Module: " << module.name << std::endl << std::endl;
-
-    out << "  PARAMETERS:\n";
-
-    for(auto &parameter : module.parameters)
-      out << "    " << parameter << '\n';
-
-    out << '\n';
-
-    out << "  VARIABLES:" << std::endl;
-
-    for(auto &element : module.elements)
-      if(element.is_var() && element.expr.type().id() != ID_smv_submodule)
-      {
-        symbol_tablet symbol_table;
-        namespacet ns{symbol_table};
-        auto identifier = to_smv_identifier_expr(element.expr).identifier();
-        auto msg = type2smv(element.expr.type(), ns);
-        out << "    " << identifier << ": " << msg << ";\n";
-      }
-
-    out << std::endl;
-
-    out << "  SUBMODULES:" << std::endl;
-
-    for(auto &element : module.elements)
-      if(element.is_var() && element.expr.type().id() == ID_smv_submodule)
-      {
-        symbol_tablet symbol_table;
-        namespacet ns(symbol_table);
-        auto identifier = to_smv_identifier_expr(element.expr).identifier();
-        auto msg = type2smv(element.expr.type(), ns);
-        out << "    " << identifier << ": " << msg << ";\n";
-      }
-
-    out << std::endl;
-
-    out << "  ITEMS:" << std::endl;
-
-    for(auto &element : module.elements)
-    {
-      out << "    TYPE: " << to_string(element.element_type) << '\n';
-      out << "    EXPR: " << element.expr.pretty() << '\n';
-      out << std::endl;
-    }
-  }
+  smv_parse_tree.show(out);
 }
 
 /*******************************************************************\
diff --git a/src/smvlang/smv_parse_tree.cpp b/src/smvlang/smv_parse_tree.cpp
index 7a663499e..6b323d75a 100644
--- a/src/smvlang/smv_parse_tree.cpp
+++ b/src/smvlang/smv_parse_tree.cpp
@@ -8,6 +8,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "smv_parse_tree.h"
 
+#include <util/namespace.h>
+#include <util/symbol_table.h>
+
+#include "expr2smv.h"
+#include "smv_expr.h"
+
 /*******************************************************************\
 
 Function: smv_parse_treet::swap
@@ -90,3 +96,57 @@ std::string to_string(smv_parse_treet::modulet::elementt::element_typet i)
   
   return "";
 }
+
+void smv_parse_treet::show(std::ostream &out) const
+{
+  for(auto &module_it : modules)
+  {
+    auto &module = module_it.second;
+
+    out << "Module: " << module.name << std::endl << std::endl;
+
+    out << "  PARAMETERS:\n";
+
+    for(auto &parameter : module.parameters)
+      out << "    " << parameter << '\n';
+
+    out << '\n';
+
+    out << "  VARIABLES:" << std::endl;
+
+    for(auto &element : module.elements)
+      if(element.is_var() && element.expr.type().id() != ID_smv_submodule)
+      {
+        symbol_tablet symbol_table;
+        namespacet ns{symbol_table};
+        auto identifier = to_smv_identifier_expr(element.expr).identifier();
+        auto msg = type2smv(element.expr.type(), ns);
+        out << "    " << identifier << ": " << msg << ";\n";
+      }
+
+    out << std::endl;
+
+    out << "  SUBMODULES:" << std::endl;
+
+    for(auto &element : module.elements)
+      if(element.is_var() && element.expr.type().id() == ID_smv_submodule)
+      {
+        symbol_tablet symbol_table;
+        namespacet ns(symbol_table);
+        auto identifier = to_smv_identifier_expr(element.expr).identifier();
+        auto msg = type2smv(element.expr.type(), ns);
+        out << "    " << identifier << ": " << msg << ";\n";
+      }
+
+    out << std::endl;
+
+    out << "  ITEMS:" << std::endl;
+
+    for(auto &element : module.elements)
+    {
+      out << "    TYPE: " << to_string(element.element_type) << '\n';
+      out << "    EXPR: " << element.expr.pretty() << '\n';
+      out << std::endl;
+    }
+  }
+}
diff --git a/src/smvlang/smv_parse_tree.h b/src/smvlang/smv_parse_tree.h
index bc242cc6e..5dc88bcd7 100644
--- a/src/smvlang/smv_parse_tree.h
+++ b/src/smvlang/smv_parse_tree.h
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_expr.h>
 #include <util/string_hash.h>
 
+#include <iosfwd>
 #include <unordered_map>
 #include <unordered_set>
 
@@ -293,6 +294,8 @@ class smv_parse_treet
   
   void swap(smv_parse_treet &smv_parse_tree);
   void clear();
+
+  void show(std::ostream &) const;
 };
 
 #endif