format_expr: use table and tweak precedences

regression/cbmc/show-vcc/main_prec.c

@@ -0,0 +1,8 @@
+int main()
+{
+  __CPROVER_bool a, b, c;
+  int x, y, z;
+  x = y + z;
+  a = (b == c);
+  __CPROVER_assert(0, "some property");
+}

regression/cbmc/show-vcc/main_prec.desc

@@ -0,0 +1,9 @@
+CORE
+main_prec.c
+--show-vcc
+^EXIT=0$
+^SIGNAL=0$
+^some property$
+^\{-.*\} main::1::x!0@1#2 = main::1::y!0@1#1 \+ main::1::z!0@1#1$
+^\{-.*\} main::1::a!0@1#2 ⇔ \(main::1::b!0@1#1 ⇔ main::1::c!0@1#1\)$
+--

src/util/format_expr.cpp

@@ -30,6 +30,29 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <ostream>
 #include <stack>
 
+// expressions that are rendered with infix operators
+struct infix_opt
+{
+  const char *rep;
+};
+
+const std::map<irep_idt, infix_opt> infix_map = {
+  {ID_plus, {"+"}},
+  {ID_minus, {"-"}},
+  {ID_mult, {"*"}},
+  {ID_div, {"/"}},
+  {ID_equal, {"="}},
+  {ID_notequal, {u8"\u2260"}}, // /=, U+2260
+  {ID_and, {u8"\u2227"}},      // wedge, U+2227
+  {ID_or, {u8"\u2228"}},       // vee, U+2228
+  {ID_xor, {u8"\u2295"}},      // + in circle, U+2295
+  {ID_implies, {u8"\u21d2"}},  // =>, U+21D2
+  {ID_le, {u8"\u2264"}},       // <=, U+2264
+  {ID_ge, {u8"\u2265"}},       // >=, U+2265
+  {ID_lt, {"<"}},
+  {ID_gt, {">"}},
+};
+
 /// We use the precendences that most readers expect
 /// (i.e., the ones you learn in primary school),
 /// and stay clear of the surprising ones that C has.
@@ -40,6 +63,10 @@ static bool bracket_subexpression(const exprt &sub_expr, const exprt &expr)
   if(!sub_expr.has_operands())
     return false;
 
+  // no need if subexpression isn't an infix operator
+  if(infix_map.find(sub_expr.id()) == infix_map.end())
+    return false;
+
   // * and / bind stronger than + and -
   if(
     (sub_expr.id() == ID_mult || sub_expr.id() == ID_div) &&
@@ -54,6 +81,16 @@ static bool bracket_subexpression(const exprt &sub_expr, const exprt &expr)
     (expr.id() == ID_and || expr.id() == ID_or))
     return false;
 
+  // +, -, *, / bind stronger than ==, !=, <, <=, >, >=
+  if(
+    (sub_expr.id() == ID_plus || sub_expr.id() == ID_minus ||
+     sub_expr.id() == ID_mult || sub_expr.id() == ID_div) &&
+    (expr.id() == ID_equal || expr.id() == ID_notequal || expr.id() == ID_lt ||
+     expr.id() == ID_gt || expr.id() == ID_le || expr.id() == ID_ge))
+  {
+    return false;
+  }
+
   return true;
 }
 
@@ -63,31 +100,20 @@ static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src)
 {
   bool first = true;
 
-  std::string operator_str;
-
-  if(src.id() == ID_and)
-    operator_str = u8"\u2227"; // wedge, U+2227
-  else if(src.id() == ID_or)
-    operator_str = u8"\u2228"; // vee, U+2228
-  else if(src.id() == ID_xor)
-    operator_str = u8"\u2295"; // + in circle, U+2295
-  else if(src.id() == ID_le)
-    operator_str = u8"\u2264"; // <=, U+2264
-  else if(src.id() == ID_ge)
-    operator_str = u8"\u2265"; // >=, U+2265
-  else if(src.id() == ID_notequal)
-    operator_str = u8"\u2260"; // /=, U+2260
-  else if(src.id() == ID_implies)
-    operator_str = u8"\u21d2"; // =>, U+21D2
-  else if(src.id() == ID_equal)
+  std::string operator_str = id2string(src.id()); // default
+
+  if(
+    src.id() == ID_equal && !src.operands().empty() &&
+    src.op0().type().id() == ID_bool)
   {
-    if(!src.operands().empty() && src.op0().type().id() == ID_bool)
-      operator_str = u8"\u21d4"; // <=>, U+21D4
-    else
-      operator_str = "=";
+    operator_str = u8"\u21d4"; // <=>, U+21D4
   }
   else
-    operator_str = id2string(src.id());
+  {
+    auto infix_map_it = infix_map.find(src.id());
+    if(infix_map_it != infix_map.end())
+      operator_str = infix_map_it->second.rep;
+  }
 
   for(const auto &op : src.operands())
   {

unit/solvers/miniBDD/miniBDD.cpp

@@ -347,7 +347,7 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]")
     {
       std::ostringstream oss;
       oss << format(o);
-      REQUIRE(oss.str() == "(a ∧ b) ∨ (¬a)");
+      REQUIRE(oss.str() == "(a ∧ b) ∨ ¬a");
     }
 
     bdd_exprt t(ns);
@@ -356,7 +356,7 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]")
     {
       std::ostringstream oss;
       oss << format(t.as_expr());
-      REQUIRE(oss.str() == "(¬a) ∨ b");
+      REQUIRE(oss.str() == "¬a ∨ b");
     }
   }
 }