From f12ca72f07a5e699d0ae60e2d6cd0945e4945b38 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 4 Sep 2020 13:37:44 -0700 Subject: [PATCH] [sledge] Fix: Replace Formula.disjuncts with DNF in Sh.pure Summary: Formula.disjuncts was a quickly written approximation of DNF. Reviewed By: ngorogiannis Differential Revision: D23459513 fbshipit-source-id: 79fd60a7b --- sledge/src/fol.ml | 41 ++++++++++++++++++++++++++++------ sledge/src/fol.mli | 4 +++- sledge/src/sh.ml | 9 ++++---- sledge/src/test/fol_test.ml | 21 +++++++++++++++++ sledge/src/test/solver_test.ml | 18 +++++++-------- 5 files changed, 71 insertions(+), 22 deletions(-) diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index 03469ff75..784bec2db 100644 --- a/sledge/src/fol.ml +++ b/sledge/src/fol.ml @@ -1198,15 +1198,32 @@ module Formula = struct let rename s e = map_vars ~f:(Var.Subst.apply s) e - let disjuncts p = - let rec disjuncts_ p ds = - match p with - | Or (a, b) -> disjuncts_ a (disjuncts_ b ds) + let fold_dnf : + meet1:('literal -> 'conjunction -> 'conjunction) + -> join1:('conjunction -> 'disjunction -> 'disjunction) + -> top:'conjunction + -> bot:'disjunction + -> 'formula + -> 'disjunction = + fun ~meet1 ~join1 ~top ~bot fml -> + let rec add_conjunct (cjn, splits) fml = + match fml with + | Tt | Ff | Eq _ | Dq _ | Eq0 _ | Dq0 _ | Gt0 _ | Ge0 _ | Lt0 _ + |Le0 _ | Iff _ | Xor _ | UPosLit _ | UNegLit _ -> + (meet1 fml cjn, splits) + | And (p, q) -> add_conjunct (add_conjunct (cjn, splits) p) q + | Or (p, q) -> (cjn, [p; q] :: splits) | Cond {cnd; pos; neg} -> - disjuncts_ (and_ cnd pos) (disjuncts_ (and_ (not_ cnd) neg) ds) - | d -> d :: ds + (cjn, [and_ cnd pos; and_ (not_ cnd) neg] :: splits) in - disjuncts_ p [] + let rec add_disjunct (cjn, splits) djn fml = + let cjn, splits = add_conjunct (cjn, splits) fml in + match splits with + | split :: splits -> + List.fold ~f:(add_disjunct (cjn, splits)) ~init:djn split + | [] -> join1 cjn djn + in + add_disjunct (top, []) bot fml end (* @@ -1541,6 +1558,16 @@ module Context = struct let vs', z = Ses.Equality.orN (vs_to_ses vs) xs in (vs_of_ses vs', z) + let dnf f = + let meet1 a (vs, p, x) = + let vs, x = add vs a x in + (vs, Formula.and_ p a, x) + in + let join1 = Iter.cons in + let top = (Var.Set.empty, Formula.tt, empty) in + let bot = Iter.empty in + Formula.fold_dnf ~meet1 ~join1 ~top ~bot f + let rename x sub = Ses.Equality.rename x (v_map_ses (Var.Subst.apply sub)) (* Substs *) diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli index ef197b3f1..f8805b886 100644 --- a/sledge/src/fol.mli +++ b/sledge/src/fol.mli @@ -181,7 +181,6 @@ and Formula : sig init:'a -> t -> f:('a -> Var.t -> 'a * Var.t) -> 'a * t val rename : Var.Subst.t -> t -> t - val disjuncts : t -> t list end (** Sets of assumptions, interpreted as conjunction, plus reasoning about @@ -212,6 +211,9 @@ module Context : sig (** Intersect contexts of assumptions. Possibly weaker than logical disjunction. *) + val dnf : Formula.t -> (Var.Set.t * Formula.t * t) iter + (** Disjunctive-normal form expansion. *) + val rename : t -> Var.Subst.t -> t (** Apply a renaming substitution to the context. *) diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index c03670370..c15289d53 100644 --- a/sledge/src/sh.ml +++ b/sledge/src/sh.ml @@ -522,12 +522,11 @@ let orN = function let pure (p : Formula.t) = [%Trace.call fun {pf} -> pf "%a" Formula.pp p] ; - List.fold (Formula.disjuncts p) ~init:(false_ Var.Set.empty) - ~f:(fun q p -> - let us = Formula.fv p in - let xs, ctx = Context.add us p Context.empty in + Iter.fold (Context.dnf p) ~init:(false_ Var.Set.empty) + ~f:(fun q (xs, pure, ctx) -> + let us = Formula.fv pure in if Context.is_unsat ctx then extend_us us q - else or_ q (exists_fresh xs {emp with us; ctx; pure= p}) ) + else or_ q (exists_fresh xs {emp with us; ctx; pure}) ) |> [%Trace.retn fun {pf} q -> pf "%a" pp q ; diff --git a/sledge/src/test/fol_test.ml b/sledge/src/test/fol_test.ml index 01ba4e153..718339f8b 100644 --- a/sledge/src/test/fol_test.ml +++ b/sledge/src/test/fol_test.ml @@ -498,4 +498,25 @@ let%test_module _ = rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]; [-1 ↦ ]; [0 ↦ ]]} |}] let%test _ = implies_eq r19 z !0 + + let%expect_test _ = + let f = + Formula.( + andN + [ eq x y + ; cond ~cnd:(eq x !0) ~pos:(eq z !2) ~neg:(eq z !3) + ; or_ (eq w !4) (eq w !5) ]) + in + printf Formula.pp f ; + printf Formula.pp + (Formula.orN (Iter.to_list (Iter.map ~f:snd3 (Context.dnf f)))) ; + [%expect + {| + (((%x_5 = %y_6) ∧ ((0 = %x_5) ? (%z_7 = 2) : (%z_7 = 3))) + ∧ ((%w_4 = 4) ∨ (%w_4 = 5))) + + (((((((%x_5 = %y_6) ∧ (%w_4 = 5)) ∧ (0 ≠ %x_5)) ∧ (%z_7 = 3)) + ∨ ((((%x_5 = %y_6) ∧ (%w_4 = 5)) ∧ (0 = %x_5)) ∧ (%z_7 = 2))) + ∨ ((((%x_5 = %y_6) ∧ (%w_4 = 4)) ∧ (0 ≠ %x_5)) ∧ (%z_7 = 3))) + ∨ ((((%x_5 = %y_6) ∧ (%w_4 = 4)) ∧ (0 = %x_5)) ∧ (%z_7 = 2))) |}] end ) diff --git a/sledge/src/test/solver_test.ml b/sledge/src/test/solver_test.ml index 26663f1ba..7cd2ebb03 100644 --- a/sledge/src/test/solver_test.ml +++ b/sledge/src/test/solver_test.ml @@ -239,27 +239,27 @@ let%test_module _ = ( infer_frame: %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(16 + (-8 × %n_9)),%a_3⟩ - * ( ( 2 = %n_9 ∧ emp) - ∨ ( 0 = %n_9 ∧ emp) + * ( ( 0 = %n_9 ∧ emp) + ∨ ( 2 = %n_9 ∧ emp) ∨ ( 1 = %n_9 ∧ emp) ) \- ∃ %a_1, %m_8 . %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩ ) infer_frame: - ( ( %a_1 = %a_2 - ∧ 2 = %n_9 + ( ( %a_3 = _ + ∧ 0 = %n_9 ∧ 16 = %m_8 - ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩) + ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1 + ∧ emp) ∨ ( %a_3 = _ ∧ 1 = %n_9 ∧ 16 = %m_8 ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1 ∧ emp) - ∨ ( %a_3 = _ - ∧ 0 = %n_9 + ∨ ( %a_1 = %a_2 + ∧ 2 = %n_9 ∧ 16 = %m_8 - ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1 - ∧ emp) + ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩) ) |}] (* Incompleteness: equivalent to above but using ≤ instead of ∨ *)