From d8114b46883510e4605b094691d5d0662c05d5b5 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 4 Sep 2020 13:38:40 -0700 Subject: [PATCH] [sledge] Improve: Normalize polarity of conditional formulas MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Summary: Normalize conditional formulas to ensure that their "condition" formula is not "negative". This avoids redundant formulas such as `(x = 0 ? p : q)` and `(x ≠ 0 ? q : p)`. The choice of which formulas are "negative" for this purpose is mostly arbitrary, with the only real constraint being that negating a negative formula should produce a positive one. Note that conditional formulas themselves are considered to be "positive" since negating them produces another conditional formula with the same condition formula. Reviewed By: ngorogiannis Differential Revision: D23487502 fbshipit-source-id: 63606d89c --- sledge/src/fol.ml | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index dc6128da7..439328b3f 100644 --- a/sledge/src/fol.ml +++ b/sledge/src/fol.ml @@ -282,6 +282,12 @@ end = struct let _UPosLit p x = UPosLit (p, x) let _UNegLit p x = UNegLit (p, x) + let is_negative = function + | Ff | Dq _ | Dq0 _ | Lt0 _ | Le0 _ | Or _ | Xor _ | UNegLit _ -> true + | Tt | Eq _ | Eq0 _ | Gt0 _ | Ge0 _ | And _ | Iff _ | UPosLit _ | Cond _ + -> + false + type equal_or_opposite = Equal | Opposite | Unknown let rec equal_or_opposite p q : equal_or_opposite = @@ -378,9 +384,13 @@ end = struct match equal_or_opposite pos neg with (* (c ? p : p) ==> c *) | Equal -> cnd - (* (c : p : ¬p) ==> c <=> p *) + (* (c ? p : ¬p) ==> c <=> p *) | Opposite -> _Iff cnd pos - | Unknown -> Cond {cnd; pos; neg} ) + (* (c ? p : n) <=> (¬c ? n : p) *) + | Unknown when is_negative cnd -> + Cond {cnd= _Not cnd; pos= neg; neg= pos} + (* (c ? p : n) *) + | _ -> Cond {cnd; pos; neg} ) end open Fml