--show-formula splits up disjunctions into separate lines

This improves readability when viewing large disjunctions.

Author: kroening

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$
+--

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

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';
 }