Merge pull request #2978 from diffblue/format_expr_beautification

format(expr) beautification for quantifiers and = on booleans

Author: tautschnig

src/util/format_expr.cpp

@@ -78,6 +78,13 @@ static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src)
     operator_str = u8"\u2260"; // /=, U+2260
   else if(src.id() == ID_implies)
     operator_str = u8"\u21d2"; // =>, U+21D2
+  else if(src.id() == ID_equal)
+  {
+    if(!src.operands().empty() && src.op0().type().id() == ID_bool)
+      operator_str = u8"\u21d4"; // <=>, U+21D4
+    else
+      operator_str = "=";
+  }
   else
     operator_str = id2string(src.id());
 
@@ -217,13 +224,13 @@ std::ostream &format_rec(std::ostream &os, const exprt &expr)
   else if(id == ID_type)
     return format_rec(os, expr.type());
   else if(id == ID_forall)
-    return os << id << u8" \u2200 : "
-              << format(to_quantifier_expr(expr).symbol().type()) << " . "
-              << format(to_quantifier_expr(expr).where());
+    return os << u8"\u2200 " << format(to_quantifier_expr(expr).symbol())
+              << " : " << format(to_quantifier_expr(expr).symbol().type())
+              << " . " << format(to_quantifier_expr(expr).where());
   else if(id == ID_exists)
-    return os << id << u8" \u2203 : "
-              << format(to_quantifier_expr(expr).symbol().type()) << " . "
-              << format(to_quantifier_expr(expr).where());
+    return os << u8"\u2203 " << format(to_quantifier_expr(expr).symbol())
+              << " : " << format(to_quantifier_expr(expr).symbol().type())
+              << " . " << format(to_quantifier_expr(expr).where());
   else if(id == ID_let)
     return os << "LET " << format(to_let_expr(expr).symbol()) << " = "
               << format(to_let_expr(expr).value()) << " IN "