From 4aec4fe4917221c011a5a023ca077e88ff1f5b40 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 1 Aug 2022 20:42:45 -0400 Subject: [PATCH] refactor(proofs): make proof terms a recursive term --- src/core/proof_core.ml | 18 ++++----- src/core/proof_core.mli | 18 ++++----- src/core/proof_sat.ml | 12 +++--- src/core/proof_sat.mli | 6 +-- src/core/proof_term.ml | 38 +++++++++++++------ src/core/proof_term.mli | 19 ++++++++-- src/core/proof_trace.ml | 3 +- src/core/proof_trace.mli | 6 +-- src/th-bool-static/Sidekick_th_bool_static.ml | 38 +++++++++---------- src/th-cstor/Sidekick_th_cstor.ml | 2 +- src/th-cstor/Sidekick_th_cstor.mli | 2 +- src/th-data/th_intf.ml | 16 ++++---- src/th-lra/intf.ml | 2 +- 13 files changed, 102 insertions(+), 78 deletions(-) diff --git a/src/core/proof_core.ml b/src/core/proof_core.ml index b24d17e7..7ff4b619 100644 --- a/src/core/proof_core.ml +++ b/src/core/proof_core.ml @@ -6,24 +6,24 @@ type lit = Lit.t -let lemma_cc lits : Proof_term.data = Proof_term.make_data ~lits "core.lemma-cc" +let lemma_cc lits : Proof_term.t = Proof_term.apply_rule ~lits "core.lemma-cc" let define_term t1 t2 = - Proof_term.make_data ~terms:[ t1; t2 ] "core.define-term" + Proof_term.apply_rule ~terms:[ t1; t2 ] "core.define-term" -let proof_r1 p1 p2 = Proof_term.make_data ~premises:[ p1; p2 ] "core.r1" -let proof_p1 p1 p2 = Proof_term.make_data ~premises:[ p1; p2 ] "core.p1" +let proof_r1 p1 p2 = Proof_term.apply_rule ~premises:[ p1; p2 ] "core.r1" +let proof_p1 p1 p2 = Proof_term.apply_rule ~premises:[ p1; p2 ] "core.p1" let proof_res ~pivot p1 p2 = - Proof_term.make_data ~terms:[ pivot ] ~premises:[ p1; p2 ] "core.res" + Proof_term.apply_rule ~terms:[ pivot ] ~premises:[ p1; p2 ] "core.res" let with_defs pr defs = - Proof_term.make_data ~premises:(pr :: defs) "core.with-defs" + Proof_term.apply_rule ~premises:(pr :: defs) "core.with-defs" -let lemma_true t = Proof_term.make_data ~terms:[ t ] "core.true" +let lemma_true t = Proof_term.apply_rule ~terms:[ t ] "core.true" let lemma_preprocess t1 t2 ~using = - Proof_term.make_data ~terms:[ t1; t2 ] ~premises:using "core.preprocess" + Proof_term.apply_rule ~terms:[ t1; t2 ] ~premises:using "core.preprocess" let lemma_rw_clause pr ~res ~using = - Proof_term.make_data ~premises:(pr :: using) ~lits:res "core.rw-clause" + Proof_term.apply_rule ~premises:(pr :: using) ~lits:res "core.rw-clause" diff --git a/src/core/proof_core.mli b/src/core/proof_core.mli index 6e71e413..0a440a06 100644 --- a/src/core/proof_core.mli +++ b/src/core/proof_core.mli @@ -4,40 +4,40 @@ open Sidekick_core_logic type lit = Lit.t -val lemma_cc : lit list -> Proof_term.data +val lemma_cc : lit list -> Proof_term.t (** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory of uninterpreted functions. *) -val define_term : Term.t -> Term.t -> Proof_term.data +val define_term : Term.t -> Term.t -> Proof_term.t (** [define_term cst u proof] defines the new constant [cst] as being equal to [u]. The result is a proof of the clause [cst = u] *) -val proof_p1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.data +val proof_p1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.t (** [proof_p1 p1 p2], where [p1] proves the unit clause [t=u] (t:bool) and [p2] proves [C \/ t], is the Proof_term.t that produces [C \/ u], i.e unit paramodulation. *) -val proof_r1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.data +val proof_r1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.t (** [proof_r1 p1 p2], where [p1] proves the unit clause [|- t] (t:bool) and [p2] proves [C \/ ¬t], is the Proof_term.t that produces [C \/ u], i.e unit resolution. *) val proof_res : - pivot:Term.t -> Proof_term.step_id -> Proof_term.step_id -> Proof_term.data + pivot:Term.t -> Proof_term.step_id -> Proof_term.step_id -> Proof_term.t (** [proof_res ~pivot p1 p2], where [p1] proves the clause [|- C \/ l] and [p2] proves [D \/ ¬l], where [l] is either [pivot] or [¬pivot], is the Proof_term.t that produces [C \/ D], i.e boolean resolution. *) -val with_defs : Proof_term.step_id -> Proof_term.step_id list -> Proof_term.data +val with_defs : Proof_term.step_id -> Proof_term.step_id list -> Proof_term.t (** [with_defs pr defs] specifies that [pr] is valid only in a context where the definitions [defs] are present. *) -val lemma_true : Term.t -> Proof_term.data +val lemma_true : Term.t -> Proof_term.t (** [lemma_true (true) p] asserts the clause [(true)] *) val lemma_preprocess : - Term.t -> Term.t -> using:Proof_term.step_id list -> Proof_term.data + Term.t -> Term.t -> using:Proof_term.step_id list -> Proof_term.t (** [lemma_preprocess t u ~using p] asserts that [t = u] is a tautology and that [t] has been preprocessed into [u]. @@ -52,7 +52,7 @@ val lemma_rw_clause : Proof_term.step_id -> res:lit list -> using:Proof_term.step_id list -> - Proof_term.data + Proof_term.t (** [lemma_rw_clause prc ~res ~using], where [prc] is the proof of [|- c], uses the equations [|- p_i = q_i] from [using] to rewrite some literals of [c] into [res]. This is used to preprocess diff --git a/src/core/proof_sat.ml b/src/core/proof_sat.ml index 63707072..30733098 100644 --- a/src/core/proof_sat.ml +++ b/src/core/proof_sat.ml @@ -1,10 +1,10 @@ type lit = Lit.t -let sat_input_clause lits : Proof_term.data = - Proof_term.make_data "sat.input" ~lits +let sat_input_clause lits : Proof_term.t = + Proof_term.apply_rule "sat.input" ~lits -let sat_redundant_clause lits ~hyps : Proof_term.data = - Proof_term.make_data "sat.rup" ~lits ~premises:(Iter.to_rev_list hyps) +let sat_redundant_clause lits ~hyps : Proof_term.t = + Proof_term.apply_rule "sat.rup" ~lits ~premises:(Iter.to_rev_list hyps) -let sat_unsat_core lits : Proof_term.data = - Proof_term.make_data ~lits "sat.unsat-core" +let sat_unsat_core lits : Proof_term.t = + Proof_term.apply_rule ~lits "sat.unsat-core" diff --git a/src/core/proof_sat.mli b/src/core/proof_sat.mli index f26abdcf..7c94a270 100644 --- a/src/core/proof_sat.mli +++ b/src/core/proof_sat.mli @@ -4,12 +4,12 @@ open Proof_term type lit = Lit.t -val sat_input_clause : lit list -> Proof_term.data +val sat_input_clause : lit list -> Proof_term.t (** Emit an input clause. *) -val sat_redundant_clause : lit list -> hyps:step_id Iter.t -> Proof_term.data +val sat_redundant_clause : lit list -> hyps:step_id Iter.t -> Proof_term.t (** Emit a clause deduced by the SAT solver, redundant wrt previous clauses. The clause must be RUP wrt [hyps]. *) -val sat_unsat_core : lit list -> Proof_term.data +val sat_unsat_core : lit list -> Proof_term.t (** TODO: is this relevant here? *) diff --git a/src/core/proof_term.ml b/src/core/proof_term.ml index ae0db5b3..d4b81516 100644 --- a/src/core/proof_term.ml +++ b/src/core/proof_term.ml @@ -1,9 +1,10 @@ open Sidekick_core_logic type step_id = Proof_step.id +type local_ref = int type lit = Lit.t -type data = { +type rule_apply = { rule_name: string; lit_args: lit list; term_args: Term.t list; @@ -11,16 +12,31 @@ type data = { premises: step_id list; } -type t = unit -> data +type t = + | P_ref of step_id + | P_local of local_ref + | P_let of (local_ref * t) list * t + | P_apply of rule_apply + +type delayed = unit -> t let pp out _ = Fmt.string out "" (* TODO *) -let make_data ?(lits = []) ?(terms = []) ?(substs = []) ?(premises = []) - rule_name : data = - { - rule_name; - lit_args = lits; - subst_args = substs; - term_args = terms; - premises; - } +let local_ref id = P_local id +let ref_ id = P_ref id + +let let_ bs r = + match bs with + | [] -> r + | _ -> P_let (bs, r) + +let apply_rule ?(lits = []) ?(terms = []) ?(substs = []) ?(premises = []) + rule_name : t = + P_apply + { + rule_name; + lit_args = lits; + subst_args = substs; + term_args = terms; + premises; + } diff --git a/src/core/proof_term.mli b/src/core/proof_term.mli index c74a2ea4..351f9cfb 100644 --- a/src/core/proof_term.mli +++ b/src/core/proof_term.mli @@ -5,9 +5,10 @@ open Sidekick_core_logic type step_id = Proof_step.id +type local_ref = int type lit = Lit.t -type data = { +type rule_apply = { rule_name: string; lit_args: lit list; term_args: Term.t list; @@ -15,14 +16,24 @@ type data = { premises: step_id list; } -type t = unit -> data +type t = + | P_ref of step_id + | P_local of local_ref (** Local reference, in a let *) + | P_let of (local_ref * t) list * t + | P_apply of rule_apply + +type delayed = unit -> t include Sidekick_sigs.PRINT with type t := t -val make_data : +val ref_ : step_id -> t +val local_ref : local_ref -> t +val let_ : (local_ref * t) list -> t -> t + +val apply_rule : ?lits:lit list -> ?terms:Term.t list -> ?substs:Subst.t list -> ?premises:step_id list -> string -> - data + t diff --git a/src/core/proof_trace.ml b/src/core/proof_trace.ml index ea51bf3d..6b12bfce 100644 --- a/src/core/proof_trace.ml +++ b/src/core/proof_trace.ml @@ -1,6 +1,5 @@ type lit = Lit.t type step_id = Proof_step.id -type proof_term = Proof_term.t module Step_vec = struct type elt = step_id @@ -26,7 +25,7 @@ end module type DYN = sig val enabled : unit -> bool - val add_step : proof_term -> step_id + val add_step : Proof_term.delayed -> step_id val add_unsat : step_id -> unit val delete : step_id -> unit end diff --git a/src/core/proof_trace.mli b/src/core/proof_trace.mli index 0a3c563b..703308ec 100644 --- a/src/core/proof_trace.mli +++ b/src/core/proof_trace.mli @@ -17,8 +17,6 @@ type step_id = Proof_step.id module Step_vec : Vec_sig.BASE with type elt = step_id (** A vector indexed by steps. *) -type proof_term = Proof_term.t - (** {2 Traces} *) type t @@ -34,7 +32,7 @@ type t val enabled : t -> bool (** Is proof tracing enabled? *) -val add_step : t -> proof_term -> step_id +val add_step : t -> Proof_term.delayed -> step_id (** Create a new step in the trace. *) val add_unsat : t -> step_id -> unit @@ -57,7 +55,7 @@ val dummy : t module type DYN = sig val enabled : unit -> bool - val add_step : proof_term -> step_id + val add_step : Proof_term.delayed -> step_id val add_unsat : step_id -> unit val delete : step_id -> unit end diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index c0e61cad..130735c1 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -44,7 +44,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_ @@ A.P.lemma_bool_equiv t1 u; + (add_step_ @@ mk_step_ @@ fun () -> A.P.lemma_bool_equiv t1 u); ret u in @@ -83,11 +83,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_ @@ A.P.lemma_ite_true ~ite:t); + ~c0:(mk_step_ @@ fun () -> A.P.lemma_ite_true ~ite:t); ret b | B_bool false -> add_step_eq t c ~using:(Option.to_list prf_a) - ~c0:(mk_step_ @@ A.P.lemma_ite_false ~ite:t); + ~c0:(mk_step_ @@ fun () -> A.P.lemma_ite_false ~ite:t); ret c | _ -> None) | B_equiv (a, b) when is_true a -> ret_bequiv t b @@ -140,26 +140,26 @@ end = struct PA.add_clause [ Lit.neg lit; Lit.neg a; b ] (if is_xor then - mk_step_ @@ A.P.lemma_bool_c "xor-e+" [ t ] + mk_step_ @@ fun () -> A.P.lemma_bool_c "xor-e+" [ t ] else - mk_step_ @@ A.P.lemma_bool_c "eq-e" [ t; t_a ]); + mk_step_ @@ fun () -> A.P.lemma_bool_c "eq-e" [ t; t_a ]); PA.add_clause [ Lit.neg lit; Lit.neg b; a ] (if is_xor then - mk_step_ @@ A.P.lemma_bool_c "xor-e-" [ t ] + mk_step_ @@ fun () -> A.P.lemma_bool_c "xor-e-" [ t ] else - mk_step_ @@ A.P.lemma_bool_c "eq-e" [ t; t_b ]); + mk_step_ @@ fun () -> A.P.lemma_bool_c "eq-e" [ t; t_b ]); PA.add_clause [ lit; a; b ] (if is_xor then - mk_step_ @@ A.P.lemma_bool_c "xor-i" [ t; t_a ] + mk_step_ @@ fun () -> A.P.lemma_bool_c "xor-i" [ t; t_a ] else - mk_step_ @@ A.P.lemma_bool_c "eq-i+" [ t ]); + mk_step_ @@ fun () -> A.P.lemma_bool_c "eq-i+" [ t ]); PA.add_clause [ lit; Lit.neg a; Lit.neg b ] (if is_xor then - mk_step_ @@ A.P.lemma_bool_c "xor-i" [ t; t_b ] + mk_step_ @@ fun () -> A.P.lemma_bool_c "xor-i" [ t; t_b ] else - mk_step_ @@ A.P.lemma_bool_c "eq-i-" [ t ]) + mk_step_ @@ fun () -> A.P.lemma_bool_c "eq-i-" [ t ]) in (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *) @@ -177,11 +177,11 @@ end = struct (fun t_u u -> PA.add_clause [ Lit.neg lit; u ] - (mk_step_ @@ A.P.lemma_bool_c "and-e" [ t; t_u ])) + (mk_step_ @@ fun () -> A.P.lemma_bool_c "and-e" [ t; t_u ])) t_subs subs; PA.add_clause (lit :: List.map Lit.neg subs) - (mk_step_ @@ A.P.lemma_bool_c "and-i" [ t ]) + (mk_step_ @@ fun () -> A.P.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 @@ -192,10 +192,10 @@ end = struct (fun t_u u -> PA.add_clause [ Lit.neg u; lit ] - (mk_step_ @@ A.P.lemma_bool_c "or-i" [ t; t_u ])) + (mk_step_ @@ fun () -> A.P.lemma_bool_c "or-i" [ t; t_u ])) t_subs subs; PA.add_clause (Lit.neg lit :: subs) - (mk_step_ @@ A.P.lemma_bool_c "or-e" [ t ]) + (mk_step_ @@ fun () -> A.P.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 @@ -211,18 +211,18 @@ end = struct (fun t_u u -> PA.add_clause [ Lit.neg u; lit ] - (mk_step_ @@ A.P.lemma_bool_c "imp-i" [ t; t_u ])) + (mk_step_ @@ fun () -> A.P.lemma_bool_c "imp-i" [ t; t_u ])) (t_u :: t_args) subs; PA.add_clause (Lit.neg lit :: subs) - (mk_step_ @@ A.P.lemma_bool_c "imp-e" [ t ]) + (mk_step_ @@ fun () -> A.P.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_ @@ A.P.lemma_ite_true ~ite:t); + (mk_step_ @@ fun () -> A.P.lemma_ite_true ~ite:t); PA.add_clause [ lit_a; PA.mk_lit (eq self.tst t c) ] - (mk_step_ @@ A.P.lemma_ite_false ~ite:t) + (mk_step_ @@ fun () -> A.P.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-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml index 31c8ae3c..c309ceee 100644 --- a/src/th-cstor/Sidekick_th_cstor.ml +++ b/src/th-cstor/Sidekick_th_cstor.ml @@ -9,7 +9,7 @@ let name = "th-cstor" module type ARG = sig val view_as_cstor : Term.t -> (Const.t, Term.t) cstor_view - val lemma_cstor : Lit.t list -> Proof_term.data + val lemma_cstor : Lit.t list -> Proof_term.t end module Make (A : ARG) : sig diff --git a/src/th-cstor/Sidekick_th_cstor.mli b/src/th-cstor/Sidekick_th_cstor.mli index 024e06da..b292ba6b 100644 --- a/src/th-cstor/Sidekick_th_cstor.mli +++ b/src/th-cstor/Sidekick_th_cstor.mli @@ -7,7 +7,7 @@ type ('c, 't) cstor_view = T_cstor of 'c * 't array | T_other of 't module type ARG = sig val view_as_cstor : Term.t -> (Const.t, Term.t) cstor_view - val lemma_cstor : Lit.t list -> Proof_term.data + val lemma_cstor : Lit.t list -> Proof_term.t end val make : (module ARG) -> SMT.theory diff --git a/src/th-data/th_intf.ml b/src/th-data/th_intf.ml index 500f7b85..e26304da 100644 --- a/src/th-data/th_intf.ml +++ b/src/th-data/th_intf.ml @@ -22,35 +22,35 @@ type ('c, 'ty) data_ty_view = | Ty_other module type PROOF_RULES = sig - val lemma_isa_cstor : cstor_t:Term.t -> Term.t -> Proof_term.data + val lemma_isa_cstor : cstor_t:Term.t -> Term.t -> Proof_term.t (** [lemma_isa_cstor (d …) (is-c t)] returns the clause [(c …) = t |- is-c t] or [(d …) = t |- ¬ (is-c t)] *) - val lemma_select_cstor : cstor_t:Term.t -> Term.t -> Proof_term.data + val lemma_select_cstor : cstor_t:Term.t -> Term.t -> Proof_term.t (** [lemma_select_cstor (c t1…tn) (sel-c-i t)] returns a proof of [t = c t1…tn |- (sel-c-i t) = ti] *) - val lemma_isa_split : Term.t -> Lit.t list -> Proof_term.data + val lemma_isa_split : Term.t -> Lit.t list -> Proof_term.t (** [lemma_isa_split t lits] is the proof of [is-c1 t \/ is-c2 t \/ … \/ is-c_n t] *) - val lemma_isa_sel : Term.t -> Proof_term.data + val lemma_isa_sel : Term.t -> Proof_term.t (** [lemma_isa_sel (is-c t)] is the proof of [is-c t |- t = c (sel-c-1 t)…(sel-c-n t)] *) - val lemma_isa_disj : Lit.t -> Lit.t -> Proof_term.data + val lemma_isa_disj : Lit.t -> Lit.t -> Proof_term.t (** [lemma_isa_disj (is-c t) (is-d t)] is the proof of [¬ (is-c t) \/ ¬ (is-c t)] *) - val lemma_cstor_inj : Term.t -> Term.t -> int -> Proof_term.data + val lemma_cstor_inj : Term.t -> Term.t -> int -> Proof_term.t (** [lemma_cstor_inj (c t1…tn) (c u1…un) i] is the proof of [c t1…tn = c u1…un |- ti = ui] *) - val lemma_cstor_distinct : Term.t -> Term.t -> Proof_term.data + val lemma_cstor_distinct : Term.t -> Term.t -> Proof_term.t (** [lemma_isa_distinct (c …) (d …)] is the proof of the unit clause [|- (c …) ≠ (d …)] *) - val lemma_acyclicity : (Term.t * Term.t) list -> Proof_term.data + val lemma_acyclicity : (Term.t * Term.t) list -> Proof_term.t (** [lemma_acyclicity pairs] is a proof of [t1=u1, …, tn=un |- false] by acyclicity. *) end diff --git a/src/th-lra/intf.ml b/src/th-lra/intf.ml index 8e2cd63f..d1cdc516 100644 --- a/src/th-lra/intf.ml +++ b/src/th-lra/intf.ml @@ -44,7 +44,7 @@ module type ARG = sig val has_ty_real : Term.t -> bool (** Does this term have the type [Real] *) - val lemma_lra : Lit.t list -> Proof_term.data + val lemma_lra : Lit.t list -> Proof_term.t module Gensym : sig type t