From 8d05387bc91d57dbfc4ebd578004a638568f577f Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 5 Jun 2021 17:42:08 -0400 Subject: [PATCH] use named version of Bool_c --- src/base-term/Proof.ml | 10 +++--- src/base-term/Proof.mli | 2 +- src/th-bool-static/Sidekick_th_bool_static.ml | 34 +++++++++---------- 3 files changed, 24 insertions(+), 22 deletions(-) diff --git a/src/base-term/Proof.ml b/src/base-term/Proof.ml index aad62b13..5e0e3776 100644 --- a/src/base-term/Proof.ml +++ b/src/base-term/Proof.ml @@ -49,7 +49,7 @@ type t = | Bool_true_is_true | Bool_true_neq_false | Bool_eq of term * term (* equal by pure boolean reasoning *) - | Bool_c of clause (* boolean tautology *) + | Bool_c of bool_c_name * clause (* boolean tautology *) | Ite_true of term (* given [if a b c] returns [a=T |- if a b c=b] *) | Ite_false of term | LRA of clause @@ -59,6 +59,8 @@ type t = steps: composite_step array; (* last step is the proof *) } +and bool_c_name = string + and composite_step = | S_step_c of { name: string; (* name *) @@ -131,7 +133,7 @@ let ite_false t = Ite_false t let true_is_true : t = Bool_true_is_true let true_neq_false : t = Bool_true_neq_false let bool_eq a b : t = Bool_eq (a,b) -let bool_c c : t = Bool_c c +let bool_c name c : t = Bool_c (name, c) let hres_l c l : t = Hres (c,l) let hres_iter c i : t = Hres (c, Iter.to_list i) @@ -166,7 +168,7 @@ let iter_p (p:t) ~f_t ~f_step ~f_clause ~f_p : unit = | DT_cstor_inj (_, _c, ts, us) -> List.iter f_t ts; List.iter f_t us | Bool_true_is_true | Bool_true_neq_false -> () | Bool_eq (t, u) -> f_t t; f_t u - | Bool_c c -> f_clause c + | Bool_c (_,c) -> f_clause c | Ite_true t | Ite_false t -> f_t t | LRA c -> f_clause c | Composite { assumptions; steps } -> @@ -317,7 +319,7 @@ module Quip = struct | Bool_eq (a,b) -> Fmt.fprintf out "(@[bool-eq@ %a@ %a@])" pp_t a pp_t b - | Bool_c c -> Fmt.fprintf out "(@[bool-c@ %a@])" pp_cl c + | Bool_c (name,c) -> Fmt.fprintf out "(@[bool-c %s@ %a@])" name pp_cl c | Assertion t -> Fmt.fprintf out "(@[assert@ %a@])" pp_t t | Assertion_c c -> Fmt.fprintf out "(@[assert-c@ %a@])" pp_cl c diff --git a/src/base-term/Proof.mli b/src/base-term/Proof.mli index 83c09c1b..6a0df914 100644 --- a/src/base-term/Proof.mli +++ b/src/base-term/Proof.mli @@ -9,7 +9,7 @@ val isa_disj : ty -> term -> term -> t val cstor_inj : Cstor.t -> int -> term list -> term list -> t val bool_eq : term -> term -> t -val bool_c : lit list -> t +val bool_c : string -> lit list -> t val ite_true : term -> t val ite_false : term -> t diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 67435845..c842f761 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -37,7 +37,7 @@ module type ARG = sig val proof_bool_eq : S.T.Term.t -> S.T.Term.t -> S.P.t (** Basic boolean logic for a clause [|- c] *) - val proof_bool_c : S.P.lit list -> S.P.t + val proof_bool_c : string -> S.P.lit list -> S.P.t val mk_bool : S.T.Term.state -> (term, term IArray.t) bool_view -> term (** Make a term from the given boolean view. *) @@ -209,9 +209,9 @@ module Make(A : ARG) : S with module A = A = struct let[@inline] pr_def_refl _proxy t = SI.P.(refl t) (* prove clause [l] by boolean lemma *) - let pr_bool_c _proxy l : SI.P.t = + let pr_bool_c name _proxy l : SI.P.t = let cl = List.rev_map pr_lit l in - (A.proof_bool_c cl) + (A.proof_bool_c name cl) (* TODO: polarity? *) let cnf (self:state) (si:SI.t) ~mk_lit ~add_clause (t:T.t) : (T.t * SI.P.t) option = @@ -242,16 +242,16 @@ module Make(A : ARG) : S with module A = A = struct let t_proxy, proxy = fresh_lit ~for_ ~mk_lit ~pre:"equiv_" self in SI.define_const si ~const:t_proxy ~rhs:for_; - let add_clause c = - add_clause c (pr_bool_c t_proxy c) + let add_clause ~elim c = + add_clause c (pr_bool_c (if elim then "eq-e" else "eq-i") t_proxy c) in (* proxy => a<=> b, ¬proxy => a xor b *) - add_clause [Lit.neg proxy; Lit.neg a; b]; - add_clause [Lit.neg proxy; Lit.neg b; a]; - add_clause [proxy; a; b]; - add_clause [proxy; Lit.neg a; Lit.neg b]; + add_clause ~elim:true [Lit.neg proxy; Lit.neg a; b]; + add_clause ~elim:true [Lit.neg proxy; Lit.neg b; a]; + add_clause ~elim:false [proxy; a; b]; + add_clause ~elim:false [proxy; Lit.neg a; Lit.neg b]; proxy, pr_def_refl t_proxy for_ (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *) @@ -266,8 +266,8 @@ module Make(A : ARG) : S with module A = A = struct lit in - let add_clause_by_def_ proxy c : unit = - let pr = pr_bool_c proxy c in + let add_clause_by_def_ name proxy c : unit = + let pr = pr_bool_c name proxy c in add_clause c pr in @@ -284,9 +284,9 @@ module Make(A : ARG) : S with module A = A = struct SI.define_const si ~const:t_proxy ~rhs:t; (* add clauses *) List.iter - (fun u -> add_clause_by_def_ t_proxy [Lit.neg proxy; u]) + (fun u -> add_clause_by_def_ "and-e" t_proxy [Lit.neg proxy; u]) subs; - add_clause_by_def_ t_proxy (proxy :: List.map Lit.neg subs); + add_clause_by_def_ "and-i" t_proxy (proxy :: List.map Lit.neg subs); proxy, pr_def_refl t_proxy t | B_or l -> @@ -294,8 +294,8 @@ module Make(A : ARG) : S with module A = A = struct let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"or_" self in SI.define_const si ~const:t_proxy ~rhs:t; (* add clauses *) - List.iter (fun u -> add_clause_by_def_ t_proxy [Lit.neg u; proxy]) subs; - add_clause_by_def_ t_proxy (Lit.neg proxy :: subs); + List.iter (fun u -> add_clause_by_def_ "or-i" t_proxy [Lit.neg u; proxy]) subs; + add_clause_by_def_ "or-e" t_proxy (Lit.neg proxy :: subs); proxy, pr_def_refl t_proxy t | B_imply (args, u) -> @@ -309,8 +309,8 @@ module Make(A : ARG) : S with module A = A = struct SI.define_const si ~const:t_proxy ~rhs:t; (* add clauses *) - List.iter (fun u -> add_clause_by_def_ t_proxy [Lit.neg u; proxy]) subs; - add_clause_by_def_ t_proxy (Lit.neg proxy :: subs); + List.iter (fun u -> add_clause_by_def_ "imp-i" t_proxy [Lit.neg u; proxy]) subs; + add_clause_by_def_ "imp-e" t_proxy (Lit.neg proxy :: subs); proxy, pr_def_refl t_proxy t | B_ite _ | B_eq _ | B_neq _ -> mk_lit t, SI.P.refl t