From cc835c6e6410543deb7da7446cf7f7da8942b0d2 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 20 Oct 2020 02:35:51 -0700 Subject: [PATCH] [sledge] Improve printing of conditional terms Reviewed By: jvillard Differential Revision: D24306062 fbshipit-source-id: d95debd08 --- sledge/src/fol.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index 7d1158377..b55bb3d88 100644 --- a/sledge/src/fol.ml +++ b/sledge/src/fol.ml @@ -575,7 +575,8 @@ let ppx_f strength fs fml = | Or (x, y) -> pf "(%a@ @<2>∨ %a)" pp x pp y | Iff (x, y) -> pf "(%a@ <=> %a)" pp x pp y | Xor (x, y) -> pf "(%a@ xor %a)" pp x pp y - | Cond {cnd; pos; neg} -> pf "(%a@ ? %a@ : %a)" pp cnd pp pos pp neg + | Cond {cnd; pos; neg} -> + pf "@[(%a@ ? %a@ : %a)@]" pp cnd pp pos pp neg | UPosLit (p, x) -> pf "%a(%a)" Predsym.pp p pp_t x | UNegLit (p, x) -> pf "@<1>¬%a(%a)" Predsym.pp p pp_t x in