From 176ae91ee0ae5db7c5c7d594fa11381a702ac8cc Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 18 Sep 2018 15:53:26 +0100 Subject: [PATCH 1/2] format_expr: show quantified symbol in forall/exists This makes the output closer to usual mathematical convention. --- src/util/format_expr.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index 284dd2f8272..4addf6a493d 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -217,13 +217,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 " From 37f5b8eeb8a29ff7baff60f912cea01a2476f8ff Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 18 Sep 2018 15:56:51 +0100 Subject: [PATCH 2/2] format_expr: equality on booleans is now shown as 'iff' This makes the output closer to usual mathematical convention. --- src/util/format_expr.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index 4addf6a493d..66452eb30ee 100644 --- a/src/util/format_expr.cpp +++ b/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());