[sledge] Improve: Normalize polarity of conditional formulas

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

@@ -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