From 199626547727c6bea6ef2ce746d838c83a1f93be Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 31 Oct 2024 15:12:39 -0400
Subject: [PATCH] --show-formula splits up disjunctions into separate lines

This improves readability when viewing large disjunctions.
---
 .../ebmc/show-formula/show-formula1.desc      | 13 ++++++++++
 .../ebmc/show-formula/show-formula1.smv       |  9 +++++++
 src/ebmc/show_formula_solver.cpp              | 25 +++++++++++++++++--
 3 files changed, 45 insertions(+), 2 deletions(-)
 create mode 100644 regression/ebmc/show-formula/show-formula1.desc
 create mode 100644 regression/ebmc/show-formula/show-formula1.smv

diff --git a/regression/ebmc/show-formula/show-formula1.desc b/regression/ebmc/show-formula/show-formula1.desc
new file mode 100644
index 000000000..d3af5fe69
--- /dev/null
+++ b/regression/ebmc/show-formula/show-formula1.desc
@@ -0,0 +1,13 @@
+CORE
+show-formula1.smv
+--bound 2 --show-formula
+^\(1\) smv::main::var::x@0 = 1$
+^\(2\) smv::main::var::x@1 = 0$
+^\(3\) smv::main::var::x@2 = 0$
+^\(4\) smv::main::var::x@3 = 0$
+^\(5\) ¬\(smv::main::var::x@0 = 1\)$
+^  ∨ ¬\(smv::main::var::x@1 = 1\)$
+^  ∨ ¬\(smv::main::var::x@2 = 1\)$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/ebmc/show-formula/show-formula1.smv b/regression/ebmc/show-formula/show-formula1.smv
new file mode 100644
index 000000000..d8ac15d3a
--- /dev/null
+++ b/regression/ebmc/show-formula/show-formula1.smv
@@ -0,0 +1,9 @@
+MODULE main
+
+VAR x:0..1;
+
+ASSIGN
+init(x) := 1;
+next(x) := 0;
+
+SPEC AG x=1
diff --git a/src/ebmc/show_formula_solver.cpp b/src/ebmc/show_formula_solver.cpp
index dcf0004af..3d1cc5420 100644
--- a/src/ebmc/show_formula_solver.cpp
+++ b/src/ebmc/show_formula_solver.cpp
@@ -22,16 +22,37 @@ show_formula_solvert::show_formula_solvert()
 
 void show_formula_solvert::set_to(const exprt &expr, bool value)
 {
+  std::string number_str = '(' + std::to_string(++conjunct_counter) + ')';
+
   if(console)
     out << consolet::faint;
 
-  out << '(' << (++conjunct_counter) << ") ";
+  out << number_str << ' ';
 
   if(console)
     out << consolet::reset;
 
   if(value)
-    out << format(expr) << '\n';
+  {
+    // split up disjunctions into multiple lines for better readability
+    if(expr.id() == ID_or)
+    {
+      bool first = true;
+      for(auto &op : expr.operands())
+      {
+        if(first)
+          first = false;
+        else
+          out << std::string(number_str.size() - 1, ' ') << "\u2228 ";
+
+        out << format(op) << '\n';
+      }
+    }
+    else
+    {
+      out << format(expr) << '\n';
+    }
+  }
   else
     out << format(not_exprt(expr)) << '\n';
 }