From 8baec586f0436b6a9ef4d444268675a2ce91825a Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 2 Feb 2021 04:36:52 -0800 Subject: [PATCH] [sledge] Optimize Context.dnf by iterating disjuncts lazily Summary: This diff replaces Fml.fold_dnf, which eagerly enumerates a disjunctive-normal form expansion, with iter_dnf which can be iterated lazily. Fml.iter_dnf is then used in Context.dnf. This means that the full DNF expansion does not need to be allocated by e.g. Smtlib.check_sat, which yields huge peak memory savings. Reviewed By: jvillard Differential Revision: D25946111 fbshipit-source-id: e6d179e9f --- sledge/src/fol/context.ml | 4 +--- sledge/src/fol/fml.ml | 15 ++++++++++----- sledge/src/fol/fml.mli | 9 ++------- sledge/src/test/solver_test.ml | 8 ++++---- 4 files changed, 17 insertions(+), 19 deletions(-) diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index 9eef78307..0e4f944dd 100644 --- a/sledge/src/fol/context.ml +++ b/sledge/src/fol/context.ml @@ -862,10 +862,8 @@ let dnf f = let vs, x = add vs a x in (vs, Fml.and_ p a, x) in - let join1 = Iter.cons in let top = (Var.Set.empty, Fml.tt, empty) in - let bot = Iter.empty in - Fml.fold_dnf ~meet1 ~join1 ~top ~bot f + Iter.from_labelled_iter (Fml.iter_dnf ~meet1 ~top f) let rename x sub = [%trace] diff --git a/sledge/src/fol/fml.ml b/sledge/src/fol/fml.ml index f13441540..bc36dd24b 100644 --- a/sledge/src/fol/fml.ml +++ b/sledge/src/fol/fml.ml @@ -174,7 +174,12 @@ let fold_pos_neg ~pos ~neg s ~f = let f_not p s = f (not_ p) s in Set.fold ~f:f_not neg (Set.fold ~f pos s) -let fold_dnf ~meet1 ~join1 ~top ~bot fml = +let iter_pos_neg ~pos ~neg ~f = + let f_not p = f (not_ p) in + Set.iter ~f pos ; + Set.iter ~f:f_not neg + +let iter_dnf ~meet1 ~top fml ~f = let rec add_conjunct fml (cjn, splits) = match fml with | Tt | Eq _ | Eq0 _ | Pos _ | Iff _ | Lit _ | Not _ -> @@ -184,13 +189,13 @@ let fold_dnf ~meet1 ~join1 ~top ~bot fml = | Cond {cnd; pos; neg} -> add_conjunct (or_ (and_ cnd pos) (and_ (not_ cnd) neg)) (cjn, splits) in - let rec add_disjunct (cjn, splits) fml djn = + let rec add_disjunct (cjn, splits) fml = let cjn, splits = add_conjunct fml (cjn, splits) in match splits with | (pos, neg) :: splits -> - fold_pos_neg ~f:(add_disjunct (cjn, splits)) ~pos ~neg djn - | [] -> join1 cjn djn + iter_pos_neg ~f:(add_disjunct (cjn, splits)) ~pos ~neg + | [] -> f cjn in - add_disjunct (top, []) fml bot + add_disjunct (top, []) fml let vars p = Iter.flat_map ~f:Trm.vars (trms p) diff --git a/sledge/src/fol/fml.mli b/sledge/src/fol/fml.mli index a5c281f90..6cf1c30cb 100644 --- a/sledge/src/fol/fml.mli +++ b/sledge/src/fol/fml.mli @@ -74,13 +74,8 @@ val map_pos_neg : val fold_pos_neg : pos:set -> neg:set -> 'a -> f:(t -> 'a -> 'a) -> 'a -val fold_dnf : - meet1:(t -> 'conjunction -> 'conjunction) - -> join1:('conjunction -> 'disjunction -> 'disjunction) - -> top:'conjunction - -> bot:'disjunction - -> t - -> 'disjunction +val iter_dnf : + meet1:(t -> 'a -> 'a) -> top:'a -> t -> f:('a -> unit) -> unit val vars : t -> Var.t iter val trms : t -> Trm.t iter diff --git a/sledge/src/test/solver_test.ml b/sledge/src/test/solver_test.ml index 576011588..1ee764944 100644 --- a/sledge/src/test/solver_test.ml +++ b/sledge/src/test/solver_test.ml @@ -236,19 +236,19 @@ let%test_module _ = {| ( infer_frame: 12 %l_6 -[ %l_6, 16 )-> ⟨8×%n_9,%a_2⟩^⟨(16 + -8×%n_9),%a_3⟩ - * ( ( 0 = %n_9 ∧ emp) - ∨ ( 1 = %n_9 ∧ emp) + * ( ( 1 = %n_9 ∧ emp) + ∨ ( 0 = %n_9 ∧ emp) ∨ ( 2 = %n_9 ∧ emp) ) \- ∃ %a_1, %m_8 . %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩ ) infer_frame: - ( ( 0 = %n_9 ∧ 16 = %m_8 ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1 ∧ emp) + ( ( 1 = %n_9 ∧ 16 = %m_8 ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1 ∧ emp) ∨ ( %a_1 = %a_2 ∧ 2 = %n_9 ∧ 16 = %m_8 ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩) - ∨ ( 1 = %n_9 ∧ 16 = %m_8 ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1 ∧ emp) + ∨ ( 0 = %n_9 ∧ 16 = %m_8 ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1 ∧ emp) ) |}] (* Incompleteness: equivalent to above but using ≤ instead of ∨ *)