From 1779b7115a2bd99a11df841557233f832b4ce4d4 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 11 Oct 2021 14:27:14 -0400 Subject: [PATCH] wip: proof production (incl. better tracking of proofs in CC) --- src/cc/Sidekick_cc.ml | 24 ++-- src/core/Sidekick_core.ml | 30 +++-- src/lra/sidekick_arith_lra.ml | 105 ++++++++++++------ src/smt-solver/Sidekick_smt_solver.ml | 15 +-- src/th-bool-static/Sidekick_th_bool_static.ml | 57 ++++++---- src/th-data/Sidekick_th_data.ml | 49 +++++--- 6 files changed, 177 insertions(+), 103 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 9ab10f1f..1c10e187 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -96,7 +96,7 @@ module Make (A: CC_ARG) | E_merge_t of term * term | E_congruence of node * node (* caused by normal congruence *) | E_and of explanation * explanation - | E_theory of explanation + | E_theory of proof_step * explanation list type repr = node @@ -167,7 +167,7 @@ module Make (A: CC_ARG) | E_congruence (n1,n2) -> Fmt.fprintf out "(@[congruence@ %a@ %a@])" N.pp n1 N.pp n2 | E_merge (a,b) -> Fmt.fprintf out "(@[merge@ %a@ %a@])" N.pp a N.pp b | E_merge_t (a,b) -> Fmt.fprintf out "(@[merge@ @[:n1 %a@]@ @[:n2 %a@]@])" Term.pp a Term.pp b - | E_theory e -> Fmt.fprintf out "(@[th@ %a@])" pp e + | E_theory (_p,es) -> Fmt.fprintf out "(@[th@ %a@])" (Util.pp_list pp) es | E_and (a,b) -> Format.fprintf out "(@[and@ %a@ %a@])" pp a pp b @@ -176,7 +176,7 @@ module Make (A: CC_ARG) let[@inline] mk_merge a b : t = if N.equal a b then mk_reduction else E_merge (a,b) let[@inline] mk_merge_t a b : t = if Term.equal a b then mk_reduction else E_merge_t (a,b) let[@inline] mk_lit l : t = E_lit l - let mk_theory e = E_theory e + let[@inline] mk_theory p es = E_theory (p,es) let rec mk_list l = match l with @@ -242,6 +242,7 @@ module Make (A: CC_ARG) type t = { tst: term_store; tbl: node T_tbl.t; + proof: proof; (* internalization [term -> node] *) signatures_tbl : node Sig_tbl.t; (* map a signature to the corresponding node in some equivalence class. @@ -288,6 +289,7 @@ module Make (A: CC_ARG) let[@inline] n_false cc = Lazy.force cc.false_ let n_bool cc b = if b then n_true cc else n_false cc let[@inline] term_store cc = cc.tst + let[@inline] proof cc = cc.proof let allocate_bitfield ~descr cc = Log.debugf 5 (fun k->k "(@[cc.allocate-bit-field@ :descr %s@])" descr); Bits.mk_field cc.bitgen @@ -456,8 +458,16 @@ module Make (A: CC_ARG) assert false end | E_lit lit -> lit :: acc - | E_theory e' -> - th := true; explain_decompose_expl cc ~th acc e' + | E_theory (_pr, sub_l) -> + (* FIXME: use pr as a subproof. We need to accumulate subproofs too, because + there is some amount of resolution done inside the congruence closure + itself to resolve Horn clauses produced by theories. + + maybe we need to store [t=u] where [pr] is the proof of [Gamma |- t=u], + add [t=u] to the explanation, and use a subproof to resolve + it away using [pr] and add [Gamma] to the mix *) + th := true; + List.fold_left (explain_decompose_expl cc ~th) acc sub_l | E_merge (a,b) -> explain_equal_rec_ cc ~th acc a b | E_merge_t (a,b) -> (* find nodes for [a] and [b] on the fly *) @@ -878,12 +888,12 @@ module Make (A: CC_ARG) ?(on_pre_merge=[]) ?(on_post_merge=[]) ?(on_new_term=[]) ?(on_conflict=[]) ?(on_propagate=[]) ?(on_is_subterm=[]) ?(size=`Big) - (tst:term_store) : t = + (tst:term_store) (proof:proof) : t = let size = match size with `Small -> 128 | `Big -> 2048 in let bitgen = Bits.mk_gen () in let field_marked_explain = Bits.mk_field bitgen in let rec cc = { - tst; + tst; proof; tbl = T_tbl.create size; signatures_tbl = Sig_tbl.create size; bitgen; diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 37714868..4200cb85 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -230,6 +230,10 @@ module type PROOF = sig and [p2] proves [C \/ t], is the rule that produces [C \/ u], i.e unit paramodulation. *) + val with_defs : proof_step -> proof_step Iter.t -> proof_rule + (** [with_defs pr defs] specifies that [pr] is valid only in + a context where the definitions [defs] are present. *) + val lemma_true : term -> proof_rule (** [lemma_true (true) p] asserts the clause [(true)] *) @@ -244,9 +248,9 @@ module type PROOF = sig From now on, [t] and [u] will be used interchangeably. @return a proof_rule ID for the clause [(t=u)]. *) - val lemma_rw_clause : proof_step -> lit_rw:proof_step Iter.t -> proof_rule - (** [lemma_rw_clause prc ~lit_rw], where [prc] is the proof of [|- c], - uses the equations [|- p_i = q_i] from [lit_rw] + val lemma_rw_clause : proof_step -> using:proof_step Iter.t -> proof_rule + (** [lemma_rw_clause prc ~using], where [prc] is the proof of [|- c], + uses the equations [|- p_i = q_i] from [using] to rewrite some literals of [c] into [c']. This is used to preprocess literals of a clause (using {!lemma_preprocess} individually). *) end @@ -476,7 +480,14 @@ module type CC_S = sig val mk_merge_t : term -> term -> t val mk_lit : lit -> t val mk_list : t list -> t - val mk_theory : t -> t (* TODO: indicate what theory, or even provide a lemma *) + val mk_theory : proof_step -> t list -> t + (* FIXME: this should probably take [t, u, proof(Gamma |- t=u), expls], + where [expls] is a list of explanation of the equations in [Gamma]. + + For example for the lemma [a=b] deduced by injectivity from [Some a=Some b] + in the theory of datatypes, + the arguments would be [a, b, proof(Some a=Some b |- a=b), e0] + where [e0] is an explanation of [Some a=Some b] *) end type node = N.t @@ -491,6 +502,8 @@ module type CC_S = sig val term_store : t -> term_store + val proof : t -> proof + val find : t -> node -> repr (** Current representative *) @@ -547,6 +560,7 @@ module type CC_S = sig ?on_is_subterm:ev_on_is_subterm list -> ?size:[`Small | `Big] -> term_store -> + proof -> t (** Create a new congruence closure. @@ -709,13 +723,6 @@ module type SOLVER_INTERNAL = sig type lit = Lit.t - (** {3 Proof helpers} *) - - val define_const : t -> const:term -> rhs:term -> unit - (** [define_const si ~const ~rhs] adds the definition [const := rhs] - to the (future) proof. [const] should be a fresh constant that - occurs nowhere else, and [rhs] a term defined without [const]. *) - (** {3 Congruence Closure} *) (** Congruence closure instance *) @@ -723,6 +730,7 @@ module type SOLVER_INTERNAL = sig with module T = T and module Lit = Lit and type proof = proof + and type proof_step = proof_step and type P.t = proof and type P.lit = lit and type Actions.t = theory_actions diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml index 844f0be6..aab666da 100644 --- a/src/lra/sidekick_arith_lra.ml +++ b/src/lra/sidekick_arith_lra.ml @@ -60,7 +60,7 @@ module type ARG = sig val has_ty_real : term -> bool (** Does this term have the type [Real] *) - val lemma_lra : S.Lit.t Iter.t -> S.proof -> unit + val lemma_lra : S.Lit.t Iter.t -> S.P.proof_rule module Gensym : sig type t @@ -82,6 +82,7 @@ module type S = sig type state val create : ?stat:Stat.t -> + A.S.P.t -> A.S.T.Term.store -> A.S.T.Ty.store -> state @@ -140,6 +141,7 @@ module Make(A : ARG) : S with module A = A = struct type state = { tst: T.store; ty_st: Ty.store; + proof: SI.P.t; simps: T.t T.Tbl.t; (* cache *) gensym: A.Gensym.t; encoded_eqs: unit T.Tbl.t; (* [a=b] gets clause [a = b <=> (a >= b /\ a <= b)] *) @@ -150,8 +152,9 @@ module Make(A : ARG) : S with module A = A = struct stat_th_comb: int Stat.counter; } - let create ?(stat=Stat.create()) tst ty_st : state = + let create ?(stat=Stat.create()) proof tst ty_st : state = { tst; ty_st; + proof; simps=T.Tbl.create 128; gensym=A.Gensym.create tst; encoded_eqs=T.Tbl.create 8; @@ -232,18 +235,25 @@ module Make(A : ARG) : S with module A = A = struct ); proxy - let add_clause_lra_ (module PA:SI.PREPROCESS_ACTS) lits = - let pr = A.lemma_lra (Iter.of_list lits) in + let add_clause_lra_ ?using (module PA:SI.PREPROCESS_ACTS) lits = + let pr = A.lemma_lra (Iter.of_list lits) PA.proof in + let pr = match using with + | None -> pr + | Some using -> SI.P.lemma_rw_clause pr ~using PA.proof in PA.add_clause lits pr (* preprocess linear expressions away *) let preproc_lra (self:state) si (module PA:SI.PREPROCESS_ACTS) - (t:T.t) : T.t option = + (t:T.t) : (T.t * SI.proof_step Iter.t) option = Log.debugf 50 (fun k->k "(@[lra.preprocess@ %a@])" T.pp t); let tst = SI.tst si in (* preprocess subterm *) - let preproc_t t = SI.preprocess_term si (module PA) t in + let preproc_t ~steps t = + let u, pr = SI.preprocess_term si (module PA) t in + CCOpt.iter (fun s -> steps := s :: !steps) pr; + u + in (* tell the CC this term exists *) let declare_term_to_cc t = @@ -262,9 +272,9 @@ module Make(A : ARG) : S with module A = A = struct T.Tbl.add self.encoded_eqs t (); (* encode [t <=> (u1 /\ u2)] *) - let lit_t = PA.mk_lit t in - let lit_u1 = PA.mk_lit u1 in - let lit_u2 = PA.mk_lit u2 in + let lit_t = PA.mk_lit_nopreproc t in + let lit_u1 = PA.mk_lit_nopreproc u1 in + let lit_u2 = PA.mk_lit_nopreproc u2 in add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u1]; add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u2]; add_clause_lra_ (module PA) @@ -273,8 +283,9 @@ module Make(A : ARG) : S with module A = A = struct None | LRA_pred (pred, t1, t2) -> - let l1 = as_linexp ~f:preproc_t t1 in - let l2 = as_linexp ~f:preproc_t t2 in + let steps = ref [] in + let l1 = as_linexp ~f:(preproc_t ~steps) t1 in + let l2 = as_linexp ~f:(preproc_t ~steps) t2 in let le = LE.(l1 - l2) in let le_comb, le_const = LE.comb le, LE.const le in let le_const = A.Q.neg le_const in @@ -284,6 +295,8 @@ module Make(A : ARG) : S with module A = A = struct | None, _ -> (* non trivial linexp, give it a fresh name in the simplex *) let proxy = var_encoding_comb self ~pre:"_le" le_comb in + let pr_def = SI.P.define_term proxy t PA.proof in + steps := pr_def :: !steps; declare_term_to_cc proxy; let op = @@ -297,14 +310,13 @@ module Make(A : ARG) : S with module A = A = struct let new_t = A.mk_lra tst (LRA_simplex_pred (proxy, op, le_const)) in begin - let lit = PA.mk_lit new_t in + let lit = PA.mk_lit_nopreproc new_t in let constr = SimpSolver.Constraint.mk proxy op le_const in SimpSolver.declare_bound self.simplex constr (Tag.Lit lit); end; Log.debugf 10 (fun k->k "lra.preprocess:@ %a@ :into %a" T.pp t T.pp new_t); - (* FIXME: emit proof: by def proxy + LRA *) - Some new_t + Some (new_t, Iter.of_list !steps) | Some (coeff, v), pred -> (* [c . v <= const] becomes a direct simplex constraint [v <= const/c] *) @@ -323,28 +335,31 @@ module Make(A : ARG) : S with module A = A = struct let new_t = A.mk_lra tst (LRA_simplex_pred (v, op, q)) in begin - let lit = PA.mk_lit new_t in + let lit = PA.mk_lit_nopreproc new_t in let constr = SimpSolver.Constraint.mk v op q in SimpSolver.declare_bound self.simplex constr (Tag.Lit lit); end; Log.debugf 10 (fun k->k "lra.preprocess@ :%a@ :into %a" T.pp t T.pp new_t); - (* FIXME: preprocess proof *) - Some new_t + Some (new_t, Iter.of_list !steps) end | LRA_op _ | LRA_mult _ -> - let le = as_linexp ~f:preproc_t t in + let steps = ref [] in + let le = as_linexp ~f:(preproc_t ~steps) t in let le_comb, le_const = LE.comb le, LE.const le in if A.Q.(le_const = zero) then ( (* if there is no constant, define [proxy] as [proxy := le_comb] and return [proxy] *) let proxy = var_encoding_comb self ~pre:"_le" le_comb in + begin + let pr_def = SI.P.define_term proxy t PA.proof in + steps := pr_def :: !steps; + end; declare_term_to_cc proxy; - (* FIXME: proof by def of proxy *) - Some proxy + Some (proxy, Iter.of_list !steps) ) else ( (* a bit more complicated: we cannot just define [proxy := le_comb] because of the coefficient. @@ -352,7 +367,14 @@ module Make(A : ARG) : S with module A = A = struct variable [proxy2 := le_comb - proxy] and asserting [proxy2 = -le_const] *) let proxy = fresh_term self ~pre:"_le" (T.ty t) in + begin + let pr_def = SI.P.define_term proxy t PA.proof in + steps := pr_def :: !steps; + end; let proxy2 = fresh_term self ~pre:"_le_diff" (T.ty t) in + let pr_def2 = + SI.P.define_term proxy (A.mk_lra tst (LRA_op (Minus, t, proxy))) PA.proof + in SimpSolver.add_var self.simplex proxy; LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb; @@ -367,29 +389,39 @@ module Make(A : ARG) : S with module A = A = struct declare_term_to_cc proxy; declare_term_to_cc proxy2; - PA.add_clause [ - PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const))) - ] (fun _ -> ()); (* TODO: by-def proxy2 + LRA *) - PA.add_clause [ - PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const))) - ] (fun _ -> ()); (* TODO: by-def proxy2 + LRA *) + add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [ + PA.mk_lit_nopreproc (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const))) + ]; + add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [ + PA.mk_lit_nopreproc (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const))) + ]; - (* FIXME: actual proof *) - Some proxy + Some (proxy, Iter.of_list !steps) ) | LRA_other t when A.has_ty_real t -> None | LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ -> None - let simplify (self:state) (_recurse:_) (t:T.t) : T.t option = + let simplify (self:state) (_recurse:_) (t:T.t) : (T.t * SI.proof_step Iter.t) option = + + let proof_eq t u = + A.lemma_lra + (Iter.return (SI.Lit.atom self.tst (A.mk_eq self.tst t u))) self.proof + in + let proof_bool t ~sign:b = + let lit = SI.Lit.atom ~sign:b self.tst t in + A.lemma_lra (Iter.return lit) self.proof + in + match A.view_as_lra t with | LRA_op _ | LRA_mult _ -> let le = as_linexp_id t in if LE.is_const le then ( let c = LE.const le in - (* FIXME: proof *) - Some (A.mk_lra self.tst (LRA_const c)) + let u = A.mk_lra self.tst (LRA_const c) in + let pr = proof_eq t u in + Some (u, Iter.return pr) ) else None | LRA_pred (pred, l1, l2) -> let le = LE.(as_linexp_id l1 - as_linexp_id l2) in @@ -403,8 +435,9 @@ module Make(A : ARG) : S with module A = A = struct | Eq -> A.Q.(c = zero) | Neq -> A.Q.(c <> zero) in - (* FIXME: proof *) - Some (A.mk_bool self.tst is_true) + let u = A.mk_bool self.tst is_true in + let pr = proof_bool t ~sign:is_true in + Some (u, Iter.return pr) ) else None | _ -> None @@ -418,7 +451,7 @@ module Make(A : ARG) : S with module A = A = struct |> CCList.flat_map (Tag.to_lits si) |> List.rev_map SI.Lit.neg in - let pr = A.lemma_lra (Iter.of_list confl) in + let pr = A.lemma_lra (Iter.of_list confl) (SI.proof si) in SI.raise_conflict si acts confl pr let on_propagate_ si acts lit ~reason = @@ -428,7 +461,7 @@ module Make(A : ARG) : S with module A = A = struct SI.propagate si acts lit ~reason:(fun() -> let lits = CCList.flat_map (Tag.to_lits si) reason in - let pr = A.lemma_lra Iter.(cons lit (of_list lits)) in + let pr = A.lemma_lra Iter.(cons lit (of_list lits)) (SI.proof si) in CCList.flat_map (Tag.to_lits si) reason, pr) | _ -> () @@ -604,7 +637,7 @@ module Make(A : ARG) : S with module A = A = struct let create_and_setup si = Log.debug 2 "(th-lra.setup)"; let stat = SI.stats si in - let st = create ~stat (SI.tst si) (SI.ty_st si) in + let st = create ~stat (SI.proof si) (SI.tst si) (SI.ty_st si) in SI.add_simplifier si (simplify st); SI.on_preprocess si (preproc_lra st); SI.on_final_check si (final_check_ st); diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml index 6e73f1fc..a3d3a864 100644 --- a/src/smt-solver/Sidekick_smt_solver.ml +++ b/src/smt-solver/Sidekick_smt_solver.ml @@ -235,9 +235,6 @@ module Make(A : ARG) let[@inline] proof self = self.proof let stats t = t.stat - let define_const (self:t) ~const ~rhs : unit = - self.t_defs <- (const,rhs) :: self.t_defs - let simplifier self = self.simp let simplify_t self (t:Term.t) : _ option = Simplify.normalize self.simp t let simp_t self (t:Term.t) : Term.t * _ = Simplify.normalize_t self.simp t @@ -397,8 +394,7 @@ module Make(A : ARG) let steps = ref [] in let c' = CCList.map (preprocess_lit ~steps) c in let pr_c' = - if !steps=[] then pr_c - else A.P.lemma_rw_clause pr_c ~lit_rw:(Iter.of_list !steps) proof + A.P.lemma_rw_clause pr_c ~using:(Iter.of_list !steps) proof in A0.add_clause c' pr_c' @@ -459,10 +455,7 @@ module Make(A : ARG) let pacts = preprocess_acts_of_acts self acts in let c = CCList.map (preprocess_lit_ ~steps self pacts) c in let pr = - if !steps=[] then proof - else ( - P.lemma_rw_clause proof ~lit_rw:(Iter.of_list !steps) self.proof - ) + P.lemma_rw_clause proof ~using:(Iter.of_list !steps) self.proof in c, pr @@ -785,9 +778,7 @@ module Make(A : ARG) (* TODO: if c != c0 then P.emit_redundant_clause c because we jsut preprocessed it away? *) let pr = P.emit_input_clause (Iter.of_list c) self.proof in - let pr = if !steps=[] then pr - else P.lemma_rw_clause pr ~lit_rw:(Iter.of_list !steps) self.proof - in + let pr = P.lemma_rw_clause pr ~using:(Iter.of_list !steps) self.proof in add_clause_l self c pr let assert_term self t = assert_terms self [t] diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 6178ed41..46540f73 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -46,11 +46,11 @@ module type ARG = sig val lemma_bool_equiv : term -> term -> S.P.proof_rule (** Boolean tautology lemma (equivalence) *) - val lemma_ite_true : a:term -> ite:term -> S.P.proof_rule - (** lemma [a => ite a b c = b] *) + val lemma_ite_true : ite:term -> S.P.proof_rule + (** lemma [a ==> ite a b c = b] *) - val lemma_ite_false : a:term -> ite:term -> S.P.proof_rule - (** lemma [¬a => ite a b c = c] *) + val lemma_ite_false : ite:term -> S.P.proof_rule + (** lemma [¬a ==> ite a b c = c] *) (** Fresh symbol generator. @@ -118,6 +118,8 @@ module Make(A : ARG) : S with module A = A = struct let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : (T.t * SI.proof_step Iter.t) option = let tst = self.tst in + + let proof = SI.Simplify.proof simp in let steps = ref [] in let add_step_ s = steps := s :: !steps in @@ -155,11 +157,15 @@ module Make(A : ARG) : S with module A = A = struct CCOpt.iter add_step_ prf_a; begin match A.view_as_bool a with | B_bool true -> - add_step_ @@ A.lemma_ite_true ~a ~ite:t @@ SI.Simplify.proof simp; + add_step_ @@ SI.P.lemma_rw_clause ~using:(Iter.of_opt prf_a) + (A.lemma_ite_true ~ite:t proof) proof; ret b + | B_bool false -> - add_step_ @@ A.lemma_ite_false ~a ~ite:t @@ SI.Simplify.proof simp; + add_step_ @@ SI.P.lemma_rw_clause ~using:(Iter.of_opt prf_a) + (A.lemma_ite_false ~ite:t proof) proof; ret c + | _ -> None end @@ -195,7 +201,8 @@ module Make(A : ARG) : S with module A = A = struct let pr_p1 p s1 s2 = SI.P.proof_p1 s1 s2 p (* preprocess "ite" away *) - let preproc_ite self si (module PA:SI.PREPROCESS_ACTS) (t:T.t) : (T.t * SI.proof_step Iter.t) option = + let preproc_ite self si (module PA:SI.PREPROCESS_ACTS) + (t:T.t) : (T.t * SI.proof_step Iter.t) option = let steps = ref [] in let add_step_ s = steps := s :: !steps in @@ -207,25 +214,27 @@ module Make(A : ARG) : S with module A = A = struct CCOpt.iter add_step_ pr_a; begin match A.view_as_bool a' with | B_bool true -> - (* [a=true |- ite a b c=b], [|- a=true] ==> [|- t=b] *) - add_step_ @@ A.lemma_ite_true ~a:a' ~ite:t PA.proof; + (* [a |- ite a b c=b], [a=true] implies [ite a b c=b] *) + add_step_ @@ SI.P.lemma_rw_clause ~using:(Iter.of_opt pr_a) + (A.lemma_ite_true ~ite:t PA.proof) PA.proof; ret b + | B_bool false -> - (* [a=false |- ite a b c=c], [|- a=false] ==> [|- t=c] *) - add_step_ @@ A.lemma_ite_false ~a:a' ~ite:t PA.proof; + (* [¬a |- ite a b c=c], [a=false] implies [ite a b c=c] *) + add_step_ @@ SI.P.lemma_rw_clause ~using:(Iter.of_opt pr_a) + (A.lemma_ite_false ~ite:t PA.proof) PA.proof; ret c + | _ -> let t_ite = fresh_term self ~for_t:t ~pre:"ite" (T.ty b) in - SI.define_const si ~const:t_ite ~rhs:t; let pr_def = SI.P.define_term t_ite t PA.proof in let lit_a = PA.mk_lit_nopreproc a' in - (* TODO: use unit paramod on each clause with side t=t_ite and on a=a' *) PA.add_clause [Lit.neg lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite b)] - (pr_p1 PA.proof pr_def @@ pr_p1_opt PA.proof pr_a @@ - A.lemma_ite_true ~a:a' ~ite:t PA.proof); + (SI.P.lemma_rw_clause ~using:Iter.(append (return pr_def) (of_opt pr_a)) + (A.lemma_ite_true ~ite:t PA.proof) PA.proof); PA.add_clause [lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite c)] - (pr_p1 PA.proof pr_def @@ pr_p1_opt PA.proof pr_a @@ - A.lemma_ite_false ~a:a' ~ite:t PA.proof); + (SI.P.lemma_rw_clause ~using:Iter.(append (return pr_def) (of_opt pr_a)) + (A.lemma_ite_false ~ite:t PA.proof) PA.proof); ret t_ite end | _ -> None @@ -238,13 +247,12 @@ module Make(A : ARG) : S with module A = A = struct let[@inline] add_step s = steps := s :: !steps in (* handle boolean equality *) - let equiv_ si ~is_xor ~for_t t_a t_b : Lit.t = + let equiv_ _si ~is_xor ~for_t t_a t_b : Lit.t = let a = PA.mk_lit_nopreproc t_a in let b = PA.mk_lit_nopreproc t_b in let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *) let t_proxy, proxy = fresh_lit ~for_t ~mk_lit:PA.mk_lit_nopreproc ~pre:"equiv_" self in - SI.define_const si ~const:t_proxy ~rhs:for_t; let pr_def = SI.P.define_term t_proxy for_t PA.proof in add_step pr_def; @@ -284,7 +292,6 @@ module Make(A : ARG) : S with module A = A = struct let t_subs = Iter.to_list l in let subs = List.map PA.mk_lit_nopreproc t_subs in let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"and_" self in - SI.define_const si ~const:t_proxy ~rhs:t; let pr_def = SI.P.define_term t_proxy t PA.proof in add_step pr_def; @@ -303,7 +310,6 @@ module Make(A : ARG) : S with module A = A = struct let t_subs = Iter.to_list l in let subs = List.map PA.mk_lit_nopreproc t_subs in let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"or_" self in - SI.define_const si ~const:t_proxy ~rhs:t; let pr_def = SI.P.define_term t_proxy t PA.proof in add_step pr_def; @@ -328,7 +334,6 @@ module Make(A : ARG) : S with module A = A = struct (* now the or-encoding *) let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"implies_" self in - SI.define_const si ~const:t_proxy ~rhs:t; let pr_def = SI.P.define_term t_proxy t PA.proof in add_step pr_def; @@ -377,11 +382,15 @@ module Make(A : ARG) : S with module A = A = struct all_terms (fun t -> match cnf_of t with | None -> () - | Some u -> + | Some (u, pr_t_u) -> Log.debugf 5 (fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@])" T.pp t T.pp u); - SI.CC.merge_t cc_ t u (SI.CC.Expl.mk_list []); + + (* produce a single step proof of [|- t=u] *) + let proof = SI.proof si in + let pr = SI.P.lemma_preprocess t u ~using:pr_t_u proof in + SI.CC.merge_t cc_ t u (SI.CC.Expl.mk_theory pr []); ()); end; () diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 26392232..3f83f51c 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -71,9 +71,17 @@ module type ARG = sig val ty_is_finite : S.T.Ty.t -> bool val ty_set_is_finite : S.T.Ty.t -> bool -> unit - val lemma_isa_split : S.Lit.t Iter.t -> S.proof -> unit - val lemma_isa_disj : S.Lit.t Iter.t -> S.proof -> unit - val lemma_cstor_inj : S.Lit.t Iter.t -> S.proof -> unit + val lemma_isa_cstor : S.T.Term.t -> S.P.proof_rule + (** [lemma_isa_cstor (is-c (c …))] + or [lemma_isa_cstor (is-c (d …))] returns a unit clause *) + + val lemma_select_cstor : S.T.Term.t -> S.P.proof_rule + (** [lemma_select_cstor (sel-c-i (c t1…tn))] + returns a proof of [(sel-c-i (c t1…tn)) = ti] *) + + val lemma_isa_split : S.T.Term.t -> S.Lit.t Iter.t -> S.P.proof_rule + val lemma_isa_disj : S.T.Term.t -> S.T.Term.t -> S.P.proof_rule + val lemma_cstor_inj : Cstor.t -> S.T.Term.t -> S.T.Term.t -> int -> S.P.proof_rule end (** Helper to compute the cardinality of types *) @@ -231,26 +239,36 @@ module Make(A : ARG) : S with module A = A = struct Log.debugf 5 (fun k->k "(@[%s.merge@ (@[:c1 %a@ %a@])@ (@[:c2 %a@ %a@])@])" name N.pp n1 pp c1 N.pp n2 pp c2); - (* build full explanation of why the constructor terms are equal *) - (* TODO: have a sort of lemma (injectivity) here to justify this in the proof *) - let expl = - Expl.mk_theory @@ Expl.mk_list [ + + let mk_expl pr = + Expl.mk_theory pr @@ [ e_n1_n2; Expl.mk_merge n1 c1.c_n; Expl.mk_merge n2 c2.c_n; ] in + if A.Cstor.equal c1.c_cstor c2.c_cstor then ( (* same function: injectivity *) - (* FIXME proof *) + + let expl_merge i = + mk_expl @@ + A.lemma_cstor_inj c1.c_cstor (N.term c1.c_n) (N.term c2.c_n) i (SI.CC.proof cc) + in + assert (IArray.length c1.c_args = IArray.length c2.c_args); - IArray.iter2 - (fun u1 u2 -> SI.CC.merge cc u1 u2 expl) + IArray.iteri2 + (fun i u1 u2 -> SI.CC.merge cc u1 u2 (expl_merge i)) c1.c_args c2.c_args; Ok c1 ) else ( (* different function: disjointness *) - (* FIXME proof *) + + let expl = + mk_expl @@ + A.lemma_isa_disj (N.term c1.c_n) (N.term c2.c_n) (SI.CC.proof cc) + in + Error expl ) end @@ -379,8 +397,10 @@ module Make(A : ARG) : S with module A = A = struct Log.debugf 5 (fun k->k "(@[%s.on-new-term.is-a.reduce@ :t %a@ :to %B@ :n %a@ :sub-cstor %a@])" name T.pp t is_true N.pp n Monoid_cstor.pp cstor); + (* FIXME: needs [nu = cstor.c_n] as hyp? *) + let pr = A.lemma_isa_cstor (N.term cstor.c_n) (SI.CC.proof cc) in SI.CC.merge cc n (SI.CC.n_bool cc is_true) - Expl.(mk_theory @@ mk_merge n_u cstor.c_n) + Expl.(mk_theory pr [mk_merge n_u cstor.c_n]) end | T_select (c_t, i, u) -> let n_u = SI.CC.add_term cc u in @@ -392,7 +412,10 @@ module Make(A : ARG) : S with module A = A = struct name N.pp n i A.Cstor.pp c_t); assert (i < IArray.length cstor.c_args); let u_i = IArray.get cstor.c_args i in - SI.CC.merge cc n u_i Expl.(mk_theory @@ mk_merge n_u cstor.c_n) + (* FIXME: needs [nu = cstor.c_n] as hyp? *) + let pr = A.lemma_select_cstor (N.term cstor.c_n) (SI.CC.proof cc) in + SI.CC.merge cc n u_i + Expl.(mk_theory pr [mk_merge n_u cstor.c_n]) | Some _ -> () | None -> N_tbl.add self.to_decide repr_u (); (* needs to be decided *)