From 81f159d25d8b402684413a751d4f6e0e19e543c7 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 10 Aug 2022 22:08:09 -0400 Subject: [PATCH] feat(th-bool): add proof_rules, use std gensym --- src/th-bool-static/Sidekick_th_bool_static.ml | 66 +++++++++---------- .../Sidekick_th_bool_static.mli | 1 + src/th-bool-static/intf.ml | 39 +---------- src/th-bool-static/proof_rules.ml | 19 ++++++ src/th-bool-static/proof_rules.mli | 20 ++++++ 5 files changed, 74 insertions(+), 71 deletions(-) create mode 100644 src/th-bool-static/proof_rules.ml create mode 100644 src/th-bool-static/proof_rules.mli diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index dde8ae39..bb982b86 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -2,6 +2,7 @@ open Sidekick_core module Intf = Intf open Intf module SI = SMT.Solver_internal +module Proof_rules = Proof_rules module T = Term module type ARG = Intf.ARG @@ -9,9 +10,9 @@ module type ARG = Intf.ARG module Make (A : ARG) : sig val theory : SMT.theory end = struct - type state = { tst: T.store; gensym: A.Gensym.t } + type state = { tst: T.store; gensym: Gensym.t } - let create tst : state = { tst; gensym = A.Gensym.create tst } + let create tst : state = { tst; gensym = Gensym.create tst } let[@inline] not_ tst t = A.mk_bool tst (B_not t) let[@inline] eq tst a b = A.mk_bool tst (B_eq (a, b)) @@ -44,7 +45,7 @@ end = struct let[@inline] ret u = Some (u, Iter.of_list !steps) in (* proof is [t <=> u] *) let ret_bequiv t1 u = - (add_step_ @@ mk_step_ @@ fun () -> A.P.lemma_bool_equiv t1 u); + (add_step_ @@ mk_step_ @@ fun () -> Proof_rules.lemma_bool_equiv t1 u); ret u in @@ -55,21 +56,21 @@ end = struct | B_not _ -> None | B_atom _ -> None | B_and a -> - if Iter.exists is_false a then + if List.exists is_false a then ret (T.false_ tst) - else if Iter.for_all is_true a then + else if List.for_all is_true a then ret (T.true_ tst) else None | B_or a -> - if Iter.exists is_true a then + if List.exists is_true a then ret (T.true_ tst) - else if Iter.for_all is_false a then + else if List.for_all is_false a then ret (T.false_ tst) else None | B_imply (args, u) -> - if Iter.exists is_false args then + if List.exists is_false args then ret (T.true_ tst) else if is_true u then ret (T.true_ tst) @@ -83,11 +84,11 @@ end = struct (match A.view_as_bool a with | B_bool true -> add_step_eq t b ~using:(Option.to_list prf_a) - ~c0:(mk_step_ @@ fun () -> A.P.lemma_ite_true ~ite:t); + ~c0:(mk_step_ @@ fun () -> Proof_rules.lemma_ite_true ~ite:t); ret b | B_bool false -> add_step_eq t c ~using:(Option.to_list prf_a) - ~c0:(mk_step_ @@ fun () -> A.P.lemma_ite_false ~ite:t); + ~c0:(mk_step_ @@ fun () -> Proof_rules.lemma_ite_false ~ite:t); ret c | _ -> None) | B_equiv (a, b) when is_true a -> ret_bequiv t b @@ -104,7 +105,7 @@ end = struct | B_eq _ | B_neq _ -> None let fresh_term self ~for_t ~pre ty = - let u = A.Gensym.fresh_term self.gensym ~pre ty in + let u = Gensym.fresh_term self.gensym ~pre ty in Log.debugf 20 (fun k -> k "(@[sidekick.bool.proxy@ :t %a@ :for %a@])" T.pp_debug u T.pp_debug for_t); @@ -139,26 +140,26 @@ end = struct PA.add_clause [ Lit.neg lit; Lit.neg a; b ] (if is_xor then - mk_step_ @@ fun () -> A.P.lemma_bool_c "xor-e+" [ t ] + mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "xor-e+" [ t ] else - mk_step_ @@ fun () -> A.P.lemma_bool_c "eq-e" [ t; t_a ]); + mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "eq-e" [ t; t_a ]); PA.add_clause [ Lit.neg lit; Lit.neg b; a ] (if is_xor then - mk_step_ @@ fun () -> A.P.lemma_bool_c "xor-e-" [ t ] + mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "xor-e-" [ t ] else - mk_step_ @@ fun () -> A.P.lemma_bool_c "eq-e" [ t; t_b ]); + mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "eq-e" [ t; t_b ]); PA.add_clause [ lit; a; b ] (if is_xor then - mk_step_ @@ fun () -> A.P.lemma_bool_c "xor-i" [ t; t_a ] + mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "xor-i" [ t; t_a ] else - mk_step_ @@ fun () -> A.P.lemma_bool_c "eq-i+" [ t ]); + mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "eq-i+" [ t ]); PA.add_clause [ lit; Lit.neg a; Lit.neg b ] (if is_xor then - mk_step_ @@ fun () -> A.P.lemma_bool_c "xor-i" [ t; t_b ] + mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "xor-i" [ t; t_b ] else - mk_step_ @@ fun () -> A.P.lemma_bool_c "eq-i-" [ t ]) + 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)] *) @@ -166,23 +167,21 @@ end = struct | B_bool _ -> () | B_not _ -> () | B_and l -> - let t_subs = Iter.to_list l in let lit = PA.mk_lit t in - let subs = List.map PA.mk_lit t_subs in + let subs = List.map PA.mk_lit l in (* add clauses *) List.iter2 (fun t_u u -> PA.add_clause [ Lit.neg lit; u ] - (mk_step_ @@ fun () -> A.P.lemma_bool_c "and-e" [ t; t_u ])) - t_subs subs; + (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "and-e" [ t; t_u ])) + l subs; PA.add_clause (lit :: List.map Lit.neg subs) - (mk_step_ @@ fun () -> A.P.lemma_bool_c "and-i" [ t ]) + (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "and-i" [ t ]) | B_or l -> - let t_subs = Iter.to_list l in - let subs = List.map PA.mk_lit t_subs in + let subs = List.map PA.mk_lit l in let lit = PA.mk_lit t in (* add clauses *) @@ -190,13 +189,12 @@ end = struct (fun t_u u -> PA.add_clause [ Lit.neg u; lit ] - (mk_step_ @@ fun () -> A.P.lemma_bool_c "or-i" [ t; t_u ])) - t_subs subs; + (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "or-i" [ t; t_u ])) + l subs; PA.add_clause (Lit.neg lit :: subs) - (mk_step_ @@ fun () -> A.P.lemma_bool_c "or-e" [ t ]) + (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 t_args = Iter.to_list t_args in 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 @@ -209,18 +207,18 @@ end = struct (fun t_u u -> PA.add_clause [ Lit.neg u; lit ] - (mk_step_ @@ fun () -> A.P.lemma_bool_c "imp-i" [ t; t_u ])) + (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "imp-i" [ t; t_u ])) (t_u :: t_args) subs; PA.add_clause (Lit.neg lit :: subs) - (mk_step_ @@ fun () -> A.P.lemma_bool_c "imp-e" [ t ]) + (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "imp-e" [ t ]) | B_ite (a, b, c) -> let lit_a = PA.mk_lit a in PA.add_clause [ Lit.neg lit_a; PA.mk_lit (eq self.tst t b) ] - (mk_step_ @@ fun () -> A.P.lemma_ite_true ~ite:t); + (mk_step_ @@ fun () -> Proof_rules.lemma_ite_true ~ite:t); PA.add_clause [ lit_a; PA.mk_lit (eq self.tst t c) ] - (mk_step_ @@ fun () -> A.P.lemma_ite_false ~ite:t) + (mk_step_ @@ fun () -> Proof_rules.lemma_ite_false ~ite:t) | B_eq _ | B_neq _ -> () | B_equiv (a, b) -> equiv_ si ~t ~is_xor:false a b | B_xor (a, b) -> equiv_ si ~t ~is_xor:true a b diff --git a/src/th-bool-static/Sidekick_th_bool_static.mli b/src/th-bool-static/Sidekick_th_bool_static.mli index b83dc6c6..98699c86 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.mli +++ b/src/th-bool-static/Sidekick_th_bool_static.mli @@ -4,6 +4,7 @@ *) module Intf = Intf +module Proof_rules = Proof_rules open Intf module type ARG = Intf.ARG diff --git a/src/th-bool-static/intf.ml b/src/th-bool-static/intf.ml index a348d9df..952b1023 100644 --- a/src/th-bool-static/intf.ml +++ b/src/th-bool-static/intf.ml @@ -19,46 +19,11 @@ type ('a, 'args) bool_view = ('a, 'args) Bool_view.t = | B_ite of 'a * 'a * 'a | B_atom of 'a -module type PROOF_RULES = sig - val lemma_bool_tauto : Lit.t Iter.t -> Proof_term.t - (** Boolean tautology lemma (clause) *) - - val lemma_bool_c : string -> term list -> Proof_term.t - (** Basic boolean logic lemma for a clause [|- c]. - [proof_bool_c b name cs] is the Proof_term.t designated by [name]. *) - - val lemma_bool_equiv : term -> term -> Proof_term.t - (** Boolean tautology lemma (equivalence) *) - - val lemma_ite_true : ite:term -> Proof_term.t - (** lemma [a ==> ite a b c = b] *) - - val lemma_ite_false : ite:term -> Proof_term.t - (** lemma [¬a ==> ite a b c = c] *) -end - (** Argument to the theory *) module type ARG = sig - val view_as_bool : term -> (term, term Iter.t) bool_view + val view_as_bool : term -> (term, term list) bool_view (** Project the term into the boolean view. *) - val mk_bool : Term.store -> (term, term array) bool_view -> term + val mk_bool : Term.store -> (term, term list) bool_view -> term (** Make a term from the given boolean view. *) - - module P : PROOF_RULES - - (** Fresh symbol generator. - - The theory needs to be able to create new terms with fresh names, - to be used as placeholders for complex formulas during Tseitin - encoding. *) - module Gensym : sig - type t - - val create : Term.store -> t - (** New (stateful) generator instance. *) - - val fresh_term : t -> pre:string -> ty -> term - (** Make a fresh term of the given type *) - end end diff --git a/src/th-bool-static/proof_rules.ml b/src/th-bool-static/proof_rules.ml new file mode 100644 index 00000000..82288385 --- /dev/null +++ b/src/th-bool-static/proof_rules.ml @@ -0,0 +1,19 @@ +open Sidekick_core + +type term = Term.t +type lit = Lit.t + +let lemma_bool_tauto lits : Proof_term.t = + Proof_term.apply_rule "bool.tauto" ~lits + +let lemma_bool_c name terms : Proof_term.t = + Proof_term.apply_rule ("bool.c." ^ name) ~terms + +let lemma_bool_equiv t u : Proof_term.t = + Proof_term.apply_rule "bool.equiv" ~terms:[ t; u ] + +let lemma_ite_true ~ite : Proof_term.t = + Proof_term.apply_rule "bool.ite.true" ~terms:[ ite ] + +let lemma_ite_false ~ite : Proof_term.t = + Proof_term.apply_rule "bool.ite.false" ~terms:[ ite ] diff --git a/src/th-bool-static/proof_rules.mli b/src/th-bool-static/proof_rules.mli new file mode 100644 index 00000000..0379b4c5 --- /dev/null +++ b/src/th-bool-static/proof_rules.mli @@ -0,0 +1,20 @@ +open Sidekick_core + +type term = Term.t +type lit = Lit.t + +val lemma_bool_tauto : lit list -> Proof_term.t +(** Boolean tautology lemma (clause) *) + +val lemma_bool_c : string -> term list -> Proof_term.t +(** Basic boolean logic lemma for a clause [|- c]. + [proof_bool_c b name cs] is the Proof_term.t designated by [name]. *) + +val lemma_bool_equiv : term -> term -> Proof_term.t +(** Boolean tautology lemma (equivalence) *) + +val lemma_ite_true : ite:term -> Proof_term.t +(** lemma [a ==> ite a b c = b] *) + +val lemma_ite_false : ite:term -> Proof_term.t +(** lemma [¬a ==> ite a b c = c] *)