format_expr: no parentheses if subexpression isn't an infix operator

Author: Daniel Kroening

src/util/format_expr.cpp

@@ -63,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) &&

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");
     }
   }
 }