From 97629683735628431b92ffcfc4922c001e4fd45b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 22 Aug 2022 22:08:19 -0400 Subject: [PATCH] feat(bool): use lists for B_and/B_or, along with App_uncurried --- src/core/bool_view.ml | 4 +- src/th-bool-dyn/Sidekick_th_bool_dyn.ml | 56 +++++++++++++----- src/th-bool-dyn/intf.ml | 4 +- src/th-bool-static/Sidekick_th_bool_static.ml | 57 ++++++++++++++----- src/th-bool-static/intf.ml | 4 +- 5 files changed, 90 insertions(+), 35 deletions(-) diff --git a/src/core/bool_view.ml b/src/core/bool_view.ml index f348cec5..d033e6ab 100644 --- a/src/core/bool_view.ml +++ b/src/core/bool_view.ml @@ -4,8 +4,8 @@ type 'a t = | B_bool of bool | B_not of 'a - | B_and of 'a * 'a - | B_or of 'a * 'a + | B_and of 'a list + | B_or of 'a list | B_imply of 'a * 'a | B_equiv of 'a * 'a | B_xor of 'a * 'a diff --git a/src/th-bool-dyn/Sidekick_th_bool_dyn.ml b/src/th-bool-dyn/Sidekick_th_bool_dyn.ml index 68c044e7..43c388fc 100644 --- a/src/th-bool-dyn/Sidekick_th_bool_dyn.ml +++ b/src/th-bool-dyn/Sidekick_th_bool_dyn.ml @@ -46,6 +46,22 @@ end = struct | Some false -> true | _ -> false + let unfold_and t : T.Set.t = + let rec aux acc t = + match A.view_as_bool t with + | B_and l -> List.fold_left aux acc l + | _ -> T.Set.add t acc + in + aux T.Set.empty t + + let unfold_or t : T.Set.t = + let rec aux acc t = + match A.view_as_bool t with + | B_or l -> List.fold_left aux acc l + | _ -> T.Set.add t acc + in + aux T.Set.empty t + (* TODO: share this with th-bool-static by way of a library for boolean simplification? (also handle one-point rule and the likes) *) let simplify (self : state) (simp : Simplify.t) (t : T.t) : @@ -81,20 +97,32 @@ end = struct | B_not u when is_false u -> ret_bequiv t (T.true_ tst) | B_not _ -> None | B_atom _ -> None - | B_and (a, b) -> - if is_false a || is_false b then + | B_and _ -> + let set = unfold_and t in + if T.Set.exists is_false set then ret (T.false_ tst) - else if is_true a && is_true b then + else if T.Set.for_all is_true set then ret (T.true_ tst) - else - None - | B_or (a, b) -> - if is_true a || is_true b then + else ( + let t' = A.mk_bool tst (B_and (T.Set.to_list set)) in + if not (T.equal t t') then + ret_bequiv t t' + else + None + ) + | B_or _ -> + let set = unfold_or t in + if T.Set.exists is_true set then ret (T.true_ tst) - else if is_false a && is_false b then + else if T.Set.for_all is_false set then ret (T.false_ tst) - else - None + else ( + let t' = A.mk_bool tst (B_or (T.Set.to_list set)) in + if not (T.equal t t') then + ret_bequiv t t' + else + None + ) | B_imply (a, b) -> if is_false a || is_true b then ret (T.true_ tst) @@ -226,8 +254,8 @@ end = struct [ Lit.neg lit ] (mk_step_ @@ fun () -> Proof_core.lemma_true (Lit.term lit)) | _ when expanded self lit -> () (* already done *) - | B_and (a, b) -> - let subs = List.map (Lit.atom self.tst) [ a; b ] in + | B_and l -> + let subs = List.map (Lit.atom self.tst) l in if Lit.sign lit then (* assert [(and …t_i) => t_i] *) @@ -244,8 +272,8 @@ end = struct add_axiom c (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "and-i" [ t ]) ) - | B_or (a, b) -> - let subs = List.map (Lit.atom self.tst) [ a; b ] in + | B_or l -> + let subs = List.map (Lit.atom self.tst) l in if not @@ Lit.sign lit then (* propagate [¬sub_i \/ lit] *) diff --git a/src/th-bool-dyn/intf.ml b/src/th-bool-dyn/intf.ml index 1e36c444..8552ced8 100644 --- a/src/th-bool-dyn/intf.ml +++ b/src/th-bool-dyn/intf.ml @@ -9,8 +9,8 @@ type ty = Term.t type 'a bool_view = 'a Bool_view.t = | B_bool of bool | B_not of 'a - | B_and of 'a * 'a - | B_or of 'a * 'a + | B_and of 'a list + | B_or of 'a list | B_imply of 'a * 'a | B_equiv of 'a * 'a | B_xor of 'a * 'a diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 41c1c9c7..bb39457e 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -38,6 +38,22 @@ end = struct | Some false -> true | _ -> false + let unfold_and t : T.Set.t = + let rec aux acc t = + match A.view_as_bool t with + | B_and l -> List.fold_left aux acc l + | _ -> T.Set.add t acc + in + aux T.Set.empty t + + let unfold_or t : T.Set.t = + let rec aux acc t = + match A.view_as_bool t with + | B_or l -> List.fold_left aux acc l + | _ -> T.Set.add t acc + in + aux T.Set.empty t + let simplify (self : state) (simp : Simplify.t) (t : T.t) : (T.t * Proof_step.id Iter.t) option = let tst = self.tst in @@ -71,20 +87,32 @@ end = struct | B_not u when is_false u -> ret_bequiv t (T.true_ tst) | B_not _ -> None | B_atom _ -> None - | B_and (a, b) -> - if is_false a || is_false b then + | B_and _ -> + let set = unfold_and t in + if T.Set.exists is_false set then ret (T.false_ tst) - else if is_true a && is_true b then + else if T.Set.for_all is_true set then ret (T.true_ tst) - else - None - | B_or (a, b) -> - if is_true a || is_true b then + else ( + let t' = A.mk_bool tst (B_and (T.Set.to_list set)) in + if not (T.equal t t') then + ret_bequiv t t' + else + None + ) + | B_or _ -> + let set = unfold_or t in + if T.Set.exists is_true set then ret (T.true_ tst) - else if is_false a && is_false b then + else if T.Set.for_all is_false set then ret (T.false_ tst) - else - None + else ( + let t' = A.mk_bool tst (B_or (T.Set.to_list set)) in + if not (T.equal t t') then + ret_bequiv t t' + else + None + ) | B_imply (a, b) -> if is_false a || is_true b then ret (T.true_ tst) @@ -185,13 +213,12 @@ end = struct mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "eq-i-" [ t ]) in - (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *) (match A.view_as_bool t with | B_bool _ -> () | B_not _ -> () - | B_and (a, b) -> + | B_and l -> let lit = PA.mk_lit t in - let subs = List.map PA.mk_lit [ a; b ] in + let subs = List.map PA.mk_lit l in (* add clauses *) List.iter @@ -207,8 +234,8 @@ end = struct PA.add_clause (lit :: List.map Lit.neg subs) (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "and-i" [ t ]) - | B_or (a, b) -> - let subs = List.map PA.mk_lit [ a; b ] in + | B_or l -> + let subs = List.map PA.mk_lit l in let lit = PA.mk_lit t in (* add clauses *) diff --git a/src/th-bool-static/intf.ml b/src/th-bool-static/intf.ml index 1e36c444..8552ced8 100644 --- a/src/th-bool-static/intf.ml +++ b/src/th-bool-static/intf.ml @@ -9,8 +9,8 @@ type ty = Term.t type 'a bool_view = 'a Bool_view.t = | B_bool of bool | B_not of 'a - | B_and of 'a * 'a - | B_or of 'a * 'a + | B_and of 'a list + | B_or of 'a list | B_imply of 'a * 'a | B_equiv of 'a * 'a | B_xor of 'a * 'a