Merge pull request #265 from diffblue/transition_systemt_output

ebmc: move transition system printing code to its class

Author: tautschnig

src/ebmc/show_trans.cpp

@@ -243,17 +243,7 @@ int show_transt::show_trans()
 
   PRECONDITION(transition_system.trans_expr.has_value());
 
-  std::cout << "Initial state constraints:\n\n";
-
-  print_verilog_constraints(transition_system.trans_expr->init(), std::cout);
-
-  std::cout << "State constraints:\n\n";
-
-  print_verilog_constraints(transition_system.trans_expr->invar(), std::cout);
-
-  std::cout << "Transition constraints:\n\n";
-
-  print_verilog_constraints(transition_system.trans_expr->trans(), std::cout);
+  transition_system.output(std::cout);
 
   return 0;
 }

src/ebmc/transition_system.cpp

@@ -28,6 +28,49 @@ Author: Daniel Kroening, [email protected]
 #include <fstream>
 #include <iostream>
 
+static void output(
+  const exprt &expr,
+  std::ostream &out,
+  languaget &language,
+  const namespacet &ns)
+{
+  if(expr.id() == ID_and)
+  {
+    for(auto &conjunct : expr.operands())
+      output(conjunct, out, language, ns);
+  }
+  else
+  {
+    std::string text;
+
+    if(language.from_expr(expr, text, ns))
+    {
+      throw ebmc_errort() << "failed to convert expression";
+    }
+
+    out << "  " << text << '\n' << '\n';
+  }
+}
+
+void transition_systemt::output(std::ostream &out) const
+{
+  auto language = get_language_from_mode(main_symbol->mode);
+
+  const namespacet ns{symbol_table};
+
+  out << "Initial state constraints:\n\n";
+
+  ::output(trans_expr->init(), out, *language, ns);
+
+  out << "State constraints:\n\n";
+
+  ::output(trans_expr->invar(), out, *language, ns);
+
+  out << "Transition constraints:\n\n";
+
+  ::output(trans_expr->trans(), out, *language, ns);
+}
+
 int preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
 {
   messaget message(message_handler);

src/ebmc/transition_system.h

@@ -21,6 +21,8 @@ class transition_systemt
   symbol_tablet symbol_table;
   const symbolt *main_symbol;
   optionalt<transt> trans_expr; // transition system expression
+
+  void output(std::ostream &) const;
 };
 
 transition_systemt get_transition_system(const cmdlinet &, message_handlert &);