From 48dcd01547f9dd8e6b64e9f5f0c0622e43d6a0e5 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 29 Oct 2020 13:26:32 -0700 Subject: [PATCH] [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 | 9 +++++++++ sledge/nonstdlib/set_intf.ml | 2 ++ sledge/src/propositional.ml | 29 +++++++++++++++++++---------- sledge/src/test/sh_test.ml | 2 +- 4 files changed, 31 insertions(+), 11 deletions(-) diff --git a/sledge/nonstdlib/set.ml b/sledge/nonstdlib/set.ml index 544408c8d..0c388e3b3 100644 --- a/sledge/nonstdlib/set.ml +++ b/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) diff --git a/sledge/nonstdlib/set_intf.ml b/sledge/nonstdlib/set_intf.ml index 6329df90c..d457f105c 100644 --- a/sledge/nonstdlib/set_intf.ml +++ b/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)]. *) diff --git a/sledge/src/propositional.ml b/sledge/src/propositional.ml index 81d4d3f7c..48c562035 100644 --- a/sledge/src/propositional.ml +++ b/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 diff --git a/sledge/src/test/sh_test.ml b/sledge/src/test/sh_test.ml index fedeffc3c..58583f13c 100644 --- a/sledge/src/test/sh_test.ml +++ b/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 |}]