From b73c1bf46494b73d07597409c85be22127e3dcfd Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 10 Aug 2022 22:41:53 -0400 Subject: [PATCH] feat(bool): use binary symbols for boolean operators this helps in simplifying only fully applied boolean operators, and avoiding simplifying the binary function `(or)` to `(false)` --- src/base/Form.ml | 31 ++++------ src/base/Form.mli | 12 ++-- src/core/bool_view.ml | 8 +-- src/simplify/sidekick_simplify.ml | 14 +++-- src/th-bool-static/Sidekick_th_bool_static.ml | 59 ++++++++++--------- src/th-bool-static/intf.ml | 12 ++-- 6 files changed, 69 insertions(+), 67 deletions(-) diff --git a/src/base/Form.ml b/src/base/Form.ml index e931c08f..9a4971a2 100644 --- a/src/base/Form.ml +++ b/src/base/Form.ml @@ -5,12 +5,12 @@ module T = Term type ty = Term.t type term = Term.t -type ('a, 'args) view = ('a, 'args) Sidekick_core.Bool_view.t = +type 'a view = 'a Sidekick_core.Bool_view.t = | B_bool of bool | B_not of 'a - | B_and of 'args - | B_or of 'args - | B_imply of 'args * 'a + | B_and of 'a * 'a + | B_or of 'a * 'a + | B_imply of 'a * 'a | B_equiv of 'a * 'a | B_xor of 'a * 'a | B_eq of 'a * 'a @@ -29,18 +29,13 @@ let id_imply = ID.make "=>" exception Not_a_th_term let view_id_ fid args = - if ID.equal fid id_and then - B_and args - else if ID.equal fid id_or then - B_or args - else if ID.equal fid id_imply then ( - match args with - | [ arg; concl ] -> B_imply ([ arg ], concl) - | _ -> raise_notrace Not_a_th_term - ) else - raise_notrace Not_a_th_term + match args with + | [ a; b ] when ID.equal fid id_and -> B_and (a, b) + | [ a; b ] when ID.equal fid id_or -> B_or (a, b) + | [ a; b ] when ID.equal fid id_imply -> B_imply (a, b) + | _ -> raise_notrace Not_a_th_term -let view (t : T.t) : (T.t, _) view = +let view (t : T.t) : T.t view = let hd, args = T.unfold_app t in match T.view hd, args with | E_const { Const.c_view = T.C_true; _ }, [] -> B_bool true @@ -118,9 +113,9 @@ let distinct_l tst l = let mk_of_view tst = function | B_bool b -> T.bool_val tst b | B_atom t -> t - | B_and l -> and_l tst l - | B_or l -> or_l tst l - | B_imply (a, b) -> imply_l tst a b + | B_and (a, b) -> and_ tst a b + | B_or (a, b) -> or_ tst a b + | B_imply (a, b) -> imply tst a b | B_ite (a, b, c) -> ite tst a b c | B_equiv (a, b) -> equiv tst a b | B_xor (a, b) -> not_ tst (equiv tst a b) diff --git a/src/base/Form.mli b/src/base/Form.mli index d8015407..6b9c2c4f 100644 --- a/src/base/Form.mli +++ b/src/base/Form.mli @@ -11,12 +11,12 @@ open Types_ type term = Term.t -type ('a, 'args) view = ('a, 'args) Sidekick_core.Bool_view.t = +type 'a view = 'a Sidekick_core.Bool_view.t = | B_bool of bool | B_not of 'a - | B_and of 'args - | B_or of 'args - | B_imply of 'args * 'a + | B_and of 'a * 'a + | B_or of 'a * 'a + | B_imply of 'a * 'a | B_equiv of 'a * 'a | B_xor of 'a * 'a | B_eq of 'a * 'a @@ -24,7 +24,7 @@ type ('a, 'args) view = ('a, 'args) Sidekick_core.Bool_view.t = | B_ite of 'a * 'a * 'a | B_atom of 'a -val view : term -> (term, term list) view +val view : term -> term view val bool : Term.store -> bool -> term val not_ : Term.store -> term -> term val and_ : Term.store -> term -> term -> term @@ -42,7 +42,7 @@ val distinct_l : Term.store -> term list -> term val and_l : Term.store -> term list -> term val or_l : Term.store -> term list -> term val imply_l : Term.store -> term list -> term -> term -val mk_of_view : Term.store -> (term, term list) view -> term +val mk_of_view : Term.store -> term view -> term (* TODO? val make : Term.store -> (term, term list) view -> term diff --git a/src/core/bool_view.ml b/src/core/bool_view.ml index 6842efc7..f348cec5 100644 --- a/src/core/bool_view.ml +++ b/src/core/bool_view.ml @@ -1,12 +1,12 @@ (** Boolean-oriented view of terms *) (** View *) -type ('a, 'args) t = +type 'a t = | B_bool of bool | B_not of 'a - | B_and of 'args - | B_or of 'args - | B_imply of 'args * 'a + | B_and of 'a * 'a + | B_or of 'a * 'a + | B_imply of 'a * 'a | B_equiv of 'a * 'a | B_xor of 'a * 'a | B_eq of 'a * 'a diff --git a/src/simplify/sidekick_simplify.ml b/src/simplify/sidekick_simplify.ml index 3a49c947..c2abd434 100644 --- a/src/simplify/sidekick_simplify.ml +++ b/src/simplify/sidekick_simplify.ml @@ -26,10 +26,14 @@ let normalize (self : t) (t : Term.t) : (Term.t * Proof_step.id) option = match Term.Tbl.find self.cache t with | res -> res | exception Not_found -> - let steps_u = ref Bag.empty in - let u = aux_rec ~steps:steps_u t self.hooks in - Term.Tbl.add self.cache t (u, !steps_u); - u, !steps_u + if Term.is_a_type t then + t, Bag.empty + else ( + let steps_u = ref Bag.empty in + let u = aux_rec ~steps:steps_u t self.hooks in + Term.Tbl.add self.cache t (u, !steps_u); + u, !steps_u + ) and loop_add ~steps t = let u, pr_u = loop t in steps := Bag.append !steps pr_u; @@ -39,7 +43,7 @@ let normalize (self : t) (t : Term.t) : (Term.t * Proof_step.id) option = match hooks with | [] -> let u = - Term.map_shallow self.tst ~f:(fun _inb u -> loop_add ~steps u) t + Term.map_shallow self.tst t ~f:(fun _inb sub_t -> loop_add ~steps sub_t) in if Term.equal t u then t diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index bb982b86..7c3b074f 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -55,25 +55,25 @@ end = struct | B_not u when is_false u -> ret_bequiv t (T.true_ tst) | B_not _ -> None | B_atom _ -> None - | B_and a -> - if List.exists is_false a then + | B_and (a, b) -> + if is_false a || is_false b then ret (T.false_ tst) - else if List.for_all is_true a then + else if is_true a && is_true b then ret (T.true_ tst) else None - | B_or a -> - if List.exists is_true a then + | B_or (a, b) -> + if is_true a || is_true b then ret (T.true_ tst) - else if List.for_all is_false a then + else if is_false a && is_false b then ret (T.false_ tst) else None - | B_imply (args, u) -> - if List.exists is_false args then - ret (T.true_ tst) - else if is_true u then + | B_imply (a, b) -> + if is_false a || is_true b then ret (T.true_ tst) + else if is_true a && is_false b then + ret (T.false_ tst) else None | B_ite (a, b, c) -> @@ -166,49 +166,52 @@ end = struct (match A.view_as_bool t with | B_bool _ -> () | B_not _ -> () - | B_and l -> + | B_and (a, b) -> let lit = PA.mk_lit t in - let subs = List.map PA.mk_lit l in + let subs = List.map PA.mk_lit [ a; b ] in (* add clauses *) - List.iter2 - (fun t_u u -> + List.iter + (fun u -> + let t_u = Lit.term u in PA.add_clause [ Lit.neg lit; u ] (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "and-e" [ t; t_u ])) - l subs; + subs; PA.add_clause (lit :: List.map Lit.neg subs) (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "and-i" [ t ]) - | B_or l -> - let subs = List.map PA.mk_lit l in + | B_or (a, b) -> + let subs = List.map PA.mk_lit [ a; b ] in let lit = PA.mk_lit t in (* add clauses *) - List.iter2 - (fun t_u u -> + List.iter + (fun u -> + let t_u = Lit.term u in PA.add_clause [ Lit.neg u; lit ] (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "or-i" [ t; t_u ])) - l subs; + subs; PA.add_clause (Lit.neg lit :: subs) (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "or-e" [ t ]) - | B_imply (t_args, t_u) -> - (* transform into [¬args \/ u] on the fly *) - let args = List.map (fun t -> Lit.neg (PA.mk_lit t)) t_args in - let u = PA.mk_lit t_u in - let subs = u :: args in + | B_imply (a, b) -> + (* transform into [¬a \/ b] on the fly *) + let n_a = PA.mk_lit ~sign:false a in + let b = PA.mk_lit b in + let subs = [ n_a; b ] in (* now the or-encoding *) let lit = PA.mk_lit t in (* add clauses *) - List.iter2 - (fun t_u u -> + List.iter + (fun u -> + let t_u = Lit.term u in PA.add_clause [ Lit.neg u; lit ] (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "imp-i" [ t; t_u ])) - (t_u :: t_args) subs; + subs; PA.add_clause (Lit.neg lit :: subs) (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "imp-e" [ t ]) | B_ite (a, b, c) -> diff --git a/src/th-bool-static/intf.ml b/src/th-bool-static/intf.ml index 952b1023..1e36c444 100644 --- a/src/th-bool-static/intf.ml +++ b/src/th-bool-static/intf.ml @@ -6,12 +6,12 @@ type term = Term.t type ty = Term.t (** Boolean-oriented view of terms *) -type ('a, 'args) bool_view = ('a, 'args) Bool_view.t = +type 'a bool_view = 'a Bool_view.t = | B_bool of bool | B_not of 'a - | B_and of 'args - | B_or of 'args - | B_imply of 'args * 'a + | B_and of 'a * 'a + | B_or of 'a * 'a + | B_imply of 'a * 'a | B_equiv of 'a * 'a | B_xor of 'a * 'a | B_eq of 'a * 'a @@ -21,9 +21,9 @@ type ('a, 'args) bool_view = ('a, 'args) Bool_view.t = (** Argument to the theory *) module type ARG = sig - val view_as_bool : term -> (term, term list) bool_view + val view_as_bool : term -> term bool_view (** Project the term into the boolean view. *) - val mk_bool : Term.store -> (term, term list) bool_view -> term + val mk_bool : Term.store -> term bool_view -> term (** Make a term from the given boolean view. *) end