Skip to content

Commit 3629a4a

Browse files
author
Daniel Kroening
committed
format_expr: equality on booleans is now shown as 'iff'
This makes the output closer to usual mathematical convention.
1 parent 04674ba commit 3629a4a

File tree

1 file changed

+7
-0
lines changed

1 file changed

+7
-0
lines changed

src/util/format_expr.cpp

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,13 @@ static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src)
8080
operator_str = u8"\u21d2"; // =>, U+21D2
8181
else if(src.id() == ID_iff)
8282
operator_str = u8"\u21d4"; // <=>, U+21D4
83+
else if(src.id() == ID_equal)
84+
{
85+
if(!src.operands().empty() && src.op0().type().id() == ID_bool)
86+
operator_str = u8"\u21d4"; // <=>, U+21D4
87+
else
88+
operator_str = "=";
89+
}
8390
else
8491
operator_str = id2string(src.id());
8592

0 commit comments

Comments
 (0)