[sledge] Strengthen normalization of And and Or formulas

Summary: Exclude their units as subformulas.

Reviewed By: ngorogiannis

Differential Revision: D24532361

fbshipit-source-id: 1ac5ce2e8

sledge/nonstdlib/set.ml

@@ -33,6 +33,7 @@ end) : S with type elt = Elt.t = struct
   let add x s = S.add x s
   let add_option = Option.fold ~f:add
   let add_list xs s = S.add_list s xs
+  let remove x s = S.remove x s
   let diff = S.diff
   let inter = S.inter
   let union = S.union
@@ -69,6 +70,14 @@ end) : S with type elt = Elt.t = struct
       | _ -> None )
     | None -> None
 
+  let classify s =
+    match root_elt s with
+    | None -> `Zero
+    | Some elt -> (
+      match S.split elt s with
+      | l, true, r when is_empty l && is_empty r -> `One elt
+      | _ -> `Many )
+
   let pop_exn s =
     let elt = choose_exn s in
     (elt, S.remove elt s)

sledge/nonstdlib/set_intf.ml

@@ -26,6 +26,7 @@ module type S = sig
   val add : elt -> t -> t
   val add_option : elt option -> t -> t
   val add_list : elt list -> t -> t
+  val remove : elt -> t -> t
   val diff : t -> t -> t
   val inter : t -> t -> t
   val union : t -> t -> t
@@ -41,6 +42,7 @@ module type S = sig
   val disjoint : t -> t -> bool
   val max_elt : t -> elt option
   val only_elt : t -> elt option
+  val classify : t -> [`Zero | `One of elt | `Many]
 
   val pop_exn : t -> elt * t
   (** Find and remove an unspecified element. [O(1)]. *)

sledge/src/propositional.ml

@@ -75,20 +75,29 @@ module Make (Trm : TERM) = struct
       | Tt | Eq _ | Eq0 _ | Pos _ | Lit _ | Iff _ -> Not p )
       |> check invariant
 
-    let _Join cons zero ~pos ~neg =
-      if not (Fmls.disjoint pos neg) then zero
-      else if Fmls.is_empty neg then
-        match Fmls.only_elt pos with Some p -> p | _ -> cons ~pos ~neg
-      else if Fmls.is_empty pos then
-        match Fmls.only_elt neg with
-        | Some n -> _Not n
+    let _Join cons unit zero ~pos ~neg =
+      let pos = Fmls.remove unit pos in
+      let neg = Fmls.remove zero neg in
+      if
+        Fmls.mem zero pos
+        || Fmls.mem unit neg
+        || not (Fmls.disjoint pos neg)
+      then zero
+      else
+        match Fmls.classify neg with
+        | `Zero -> (
+          match Fmls.classify pos with
+          | `Zero -> unit
+          | `One p -> p
+          | `Many -> cons ~pos ~neg )
+        | `One n when Fmls.is_empty pos -> _Not n
         | _ -> cons ~pos ~neg
-      else cons ~pos ~neg
 
     let _And ~pos ~neg =
-      _Join (fun ~pos ~neg -> And {pos; neg}) ff ~pos ~neg
+      _Join (fun ~pos ~neg -> And {pos; neg}) tt ff ~pos ~neg
 
-    let _Or ~pos ~neg = _Join (fun ~pos ~neg -> Or {pos; neg}) tt ~pos ~neg
+    let _Or ~pos ~neg =
+      _Join (fun ~pos ~neg -> Or {pos; neg}) ff tt ~pos ~neg
 
     let join _Cons zero split_pos_neg p q =
       ( if equal p zero || equal q zero then zero

sledge/src/test/sh_test.ml

@@ -156,7 +156,7 @@ let%test_module _ =
         {|
         ∃ %x_6 .   %x_6 = %x_6^ ∧ (-1 + %y_7) = %y_7^ ∧ emp
 
-          (tt ∧ ((1 + %y_7^) = %y_7)) ∧ emp
+          ((1 + %y_7^) = %y_7) ∧ emp
 
           (-1 + %y_7) = %y_7^ ∧ emp |}]