From af901f54b179a014a1a16ae567b814f63cc43969 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 11 Oct 2021 19:57:25 -0400 Subject: [PATCH] proof production for th-data --- src/th-data/Sidekick_th_data.ml | 95 ++++++++++------------------- src/th-data/Sidekick_th_data.mli | 79 +----------------------- src/th-data/th_intf.ml | 100 +++++++++++++++++++++++++++++++ 3 files changed, 131 insertions(+), 143 deletions(-) create mode 100644 src/th-data/th_intf.ml diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 3f83f51c..725af38a 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -1,22 +1,7 @@ (** Theory for datatypes. *) -type ('c,'t) data_view = - | T_cstor of 'c * 't IArray.t - | T_select of 'c * int * 't - | T_is_a of 'c * 't - | T_other of 't - -(** View of types in a way that is directly useful for the theory of datatypes *) -type ('c, 'ty) data_ty_view = - | Ty_arrow of 'ty Iter.t * 'ty - | Ty_app of { - args: 'ty Iter.t; - } - | Ty_data of { - cstors: 'c; - } - | Ty_other +include Th_intf let name = "th-data" @@ -52,38 +37,6 @@ module C = struct let pp out self = Fmt.string out (to_string self) end -module type ARG = sig - module S : Sidekick_core.SOLVER - - module Cstor : sig - type t - val ty_args : t -> S.T.Ty.t Iter.t - val pp : t Fmt.printer - val equal : t -> t -> bool - end - - val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view - val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view - val mk_cstor : S.T.Term.store -> Cstor.t -> S.T.Term.t IArray.t -> S.T.Term.t - val mk_is_a: S.T.Term.store -> Cstor.t -> S.T.Term.t -> S.T.Term.t - val mk_sel : S.T.Term.store -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t - val mk_eq : S.T.Term.store -> S.T.Term.t -> S.T.Term.t -> S.T.Term.t - val ty_is_finite : S.T.Ty.t -> bool - val ty_set_is_finite : S.T.Ty.t -> bool -> 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 *) module Compute_card(A : ARG) : sig type t @@ -253,7 +206,7 @@ module Make(A : ARG) : S with module A = A = struct 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) + A.lemma_cstor_inj (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); @@ -266,7 +219,7 @@ module Make(A : ARG) : S with module A = A = struct let expl = mk_expl @@ - A.lemma_isa_disj (N.term c1.c_n) (N.term c2.c_n) (SI.CC.proof cc) + A.lemma_cstor_distinct (N.term c1.c_n) (N.term c2.c_n) (SI.CC.proof cc) in Error expl @@ -341,6 +294,7 @@ module Make(A : ARG) : S with module A = A = struct type t = { tst: T.store; + proof: SI.P.t; cstors: ST_cstors.t; (* repr -> cstor for the class *) parents: ST_parents.t; (* repr -> parents for the class *) cards: Card.t; (* remember finiteness *) @@ -397,8 +351,7 @@ 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 + let pr = A.lemma_isa_cstor ~cstor_t:(N.term cstor.c_n) t (SI.CC.proof cc) in SI.CC.merge cc n (SI.CC.n_bool cc is_true) Expl.(mk_theory pr [mk_merge n_u cstor.c_n]) end @@ -412,8 +365,7 @@ 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 - (* FIXME: needs [nu = cstor.c_n] as hyp? *) - let pr = A.lemma_select_cstor (N.term cstor.c_n) (SI.CC.proof cc) in + let pr = A.lemma_select_cstor ~cstor_t:(N.term cstor.c_n) t (SI.CC.proof cc) in SI.CC.merge cc n u_i Expl.(mk_theory pr [mk_merge n_u cstor.c_n]) | Some _ -> () @@ -433,9 +385,12 @@ module Make(A : ARG) : S with module A = A = struct Log.debugf 50 (fun k->k "(@[%s.on-merge.is-a.reduce@ %a@ :to %B@ :n1 %a@ :n2 %a@ :sub-cstor %a@])" name Monoid_parents.pp_is_a is_a2 is_true N.pp n1 N.pp n2 Monoid_cstor.pp c1); + let pr = + A.lemma_isa_cstor ~cstor_t:(N.term c1.c_n) (N.term is_a2.is_a_n) self.proof in SI.CC.merge cc is_a2.is_a_n (SI.CC.n_bool cc is_true) - Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n1 n2; - mk_merge n2 is_a2.is_a_arg] |> mk_theory) + Expl.(mk_theory pr + [mk_merge n1 c1.c_n; mk_merge n1 n2; + mk_merge n2 is_a2.is_a_arg]) in let merge_select n1 (c1:Monoid_cstor.t) n2 (sel2:Monoid_parents.select) = if A.Cstor.equal c1.c_cstor sel2.sel_cstor then ( @@ -443,10 +398,13 @@ module Make(A : ARG) : S with module A = A = struct (fun k->k "(@[%s.on-merge.select.reduce@ :n2 %a@ :sel get[%d]-%a@])" name N.pp n2 sel2.sel_idx Monoid_cstor.pp c1); assert (sel2.sel_idx < IArray.length c1.c_args); + let pr = + A.lemma_select_cstor ~cstor_t:(N.term c1.c_n) (N.term sel2.sel_n) self.proof in let u_i = IArray.get c1.c_args sel2.sel_idx in SI.CC.merge cc sel2.sel_n u_i - Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n1 n2; - mk_merge n2 sel2.sel_arg] |> mk_theory); + Expl.(mk_theory pr + [mk_merge n1 c1.c_n; mk_merge n1 n2; + mk_merge n2 sel2.sel_arg]); ) in let merge_c_p n1 n2 = @@ -530,6 +488,11 @@ module Make(A : ARG) : S with module A = A = struct | {flag=Open; cstor_n; _} as node -> (* conflict: the [path] forms a cycle *) let path = (n, node) :: path in + let pr = + A.lemma_acyclicity + (Iter.of_list path |> Iter.map (fun (a,b) -> N.term a, N.term b.repr)) + self.proof + in let expl = path |> CCList.flat_map @@ -537,7 +500,7 @@ module Make(A : ARG) : S with module A = A = struct [ Expl.mk_merge node.cstor_n node.repr; Expl.mk_merge n node.repr; ]) - |> Expl.mk_list |> Expl.mk_theory + |> Expl.mk_theory pr in Stat.incr self.stat_acycl_conflict; Log.debugf 5 @@ -571,12 +534,13 @@ module Make(A : ARG) : S with module A = A = struct Log.debugf 50 (fun k->k"(@[%s.assign-is-a@ :lhs %a@ :rhs %a@ :lit %a@])" name T.pp u T.pp rhs SI.Lit.pp lit); - SI.cc_merge_t solver acts u rhs (Expl.mk_theory @@ Expl.mk_lit lit) + let pr = A.lemma_isa_sel t self.proof in + SI.cc_merge_t solver acts u rhs (Expl.mk_theory pr [Expl.mk_lit lit]) | _ -> () in Iter.iter check_lit trail - (* add clauses [∨_c is-c(n)] and [¬(is-a n) ∨ ¬(is-b n)] *) + (* add clauses [\Or_c is-c(n)] and [¬(is-a n) ∨ ¬(is-b n)] *) let decide_class_ (self:t) (solver:SI.t) acts (n:N.t) : unit = let t = N.term n in (* [t] might have been expanded already, in case of duplicates in [l] *) @@ -593,13 +557,13 @@ module Make(A : ARG) : S with module A = A = struct |> Iter.to_rev_list in SI.add_clause_permanent solver acts c - (A.lemma_isa_split (Iter.of_list c)); + (A.lemma_isa_split t (Iter.of_list c) self.proof); Iter.diagonal_l c - (fun (c1,c2) -> + (fun (l1,l2) -> let pr = - A.lemma_isa_disj (Iter.of_list [SI.Lit.neg c1; SI.Lit.neg c2]) in + A.lemma_isa_disj (SI.Lit.neg l1) (SI.Lit.neg l2) self.proof in SI.add_clause_permanent solver acts - [SI.Lit.neg c1; SI.Lit.neg c2] pr); + [SI.Lit.neg l1; SI.Lit.neg l2] pr); ) (* on final check, check acyclicity, @@ -688,6 +652,7 @@ module Make(A : ARG) : S with module A = A = struct let create_and_setup (solver:SI.t) : t = let self = { tst=SI.tst solver; + proof=SI.proof solver; cstors=ST_cstors.create_and_setup ~size:32 solver; parents=ST_parents.create_and_setup ~size:32 solver; to_decide=N_tbl.create ~size:16 (); diff --git a/src/th-data/Sidekick_th_data.mli b/src/th-data/Sidekick_th_data.mli index 6366159d..c55519a7 100644 --- a/src/th-data/Sidekick_th_data.mli +++ b/src/th-data/Sidekick_th_data.mli @@ -1,83 +1,6 @@ (** Theory for datatypes. *) -(** Datatype-oriented view of terms. - - - ['c] is the representation of constructors - - ['t] is the representation of terms -*) -type ('c,'t) data_view = - | T_cstor of 'c * 't IArray.t (** [T_cstor (c,args)] is the term [c(args)] *) - | T_select of 'c * int * 't - (** [T_select (c,i,u)] means the [i]-th argument of [u], which should - start with constructor [c] *) - | T_is_a of 'c * 't (** [T_is_a (c,u)] means [u] starts with constructor [c] *) - | T_other of 't (** non-datatype term *) - -(* TODO: use ['ts] rather than IArray? *) - -(** View of types in a way that is directly useful for the theory of datatypes *) -type ('c, 'ty) data_ty_view = - | Ty_arrow of 'ty Iter.t * 'ty - | Ty_app of { - args: 'ty Iter.t; - } - | Ty_data of { - cstors: 'c; - } - | Ty_other - -(** Argument to the functor *) -module type ARG = sig - module S : Sidekick_core.SOLVER - - (** Constructor symbols. - - A constructor is an injective symbol, part of a datatype (or "sum type"). - For example, in [type option a = Some a | None], - the constructors are [Some] and [None]. *) - module Cstor : sig - type t - (** Constructor *) - - val ty_args : t -> S.T.Ty.t Iter.t - (** Type arguments, for a polymorphic constructor *) - - val pp : t Fmt.printer - val equal : t -> t -> bool - (** Comparison *) - end - - val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view - (** Try to view type as a datatype (with its constructors) *) - - val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view - (** Try to view term as a datatype term *) - - val mk_cstor : S.T.Term.store -> Cstor.t -> S.T.Term.t IArray.t -> S.T.Term.t - (** Make a constructor application term *) - - val mk_is_a: S.T.Term.store -> Cstor.t -> S.T.Term.t -> S.T.Term.t - (** Make a [is-a] term *) - - val mk_sel : S.T.Term.store -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t - (** Make a selector term *) - - val mk_eq : S.T.Term.store -> S.T.Term.t -> S.T.Term.t -> S.T.Term.t - (** Make a term equality *) - - val ty_is_finite : S.T.Ty.t -> bool - (** Is the given type known to be finite? For example a finite datatype - (an "enum" in C parlance), or [Bool], or [Array Bool Bool]. *) - - val ty_set_is_finite : S.T.Ty.t -> bool -> unit - (** Modify the "finite" field (see {!ty_is_finite}) *) - - (* TODO: should we store this ourself? would be simpler… *) - - 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 -end +include module type of Th_intf module type S = sig module A : ARG diff --git a/src/th-data/th_intf.ml b/src/th-data/th_intf.ml new file mode 100644 index 00000000..4218d975 --- /dev/null +++ b/src/th-data/th_intf.ml @@ -0,0 +1,100 @@ + +(** Datatype-oriented view of terms. + + - ['c] is the representation of constructors + - ['t] is the representation of terms +*) +type ('c,'t) data_view = + | T_cstor of 'c * 't IArray.t + | T_select of 'c * int * 't + | T_is_a of 'c * 't + | T_other of 't + +(** View of types in a way that is directly useful for the theory of datatypes *) +type ('c, 'ty) data_ty_view = + | Ty_arrow of 'ty Iter.t * 'ty + | Ty_app of { + args: 'ty Iter.t; + } + | Ty_data of { + cstors: 'c; + } + | Ty_other + +module type ARG = sig + module S : Sidekick_core.SOLVER + + (** Constructor symbols. + + A constructor is an injective symbol, part of a datatype (or "sum type"). + For example, in [type option a = Some a | None], + the constructors are [Some] and [None]. *) + module Cstor : sig + type t + (** Constructor *) + + val ty_args : t -> S.T.Ty.t Iter.t + (** Type arguments, for a polymorphic constructor *) + + val pp : t Fmt.printer + val equal : t -> t -> bool + (** Comparison *) + end + + val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view + (** Try to view type as a datatype (with its constructors) *) + + val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view + (** Try to view term as a datatype term *) + + val mk_cstor : S.T.Term.store -> Cstor.t -> S.T.Term.t IArray.t -> S.T.Term.t + (** Make a constructor application term *) + + val mk_is_a: S.T.Term.store -> Cstor.t -> S.T.Term.t -> S.T.Term.t + (** Make a [is-a] term *) + + val mk_sel : S.T.Term.store -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t + (** Make a selector term *) + + val mk_eq : S.T.Term.store -> S.T.Term.t -> S.T.Term.t -> S.T.Term.t + (** Make a term equality *) + + val ty_is_finite : S.T.Ty.t -> bool + (** Is the given type known to be finite? For example a finite datatype + (an "enum" in C parlance), or [Bool], or [Array Bool Bool]. *) + + val ty_set_is_finite : S.T.Ty.t -> bool -> unit + (** Modify the "finite" field (see {!ty_is_finite}) *) + + val lemma_isa_cstor : cstor_t:S.T.Term.t -> S.T.Term.t -> S.P.proof_rule + (** [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:S.T.Term.t -> S.T.Term.t -> S.P.proof_rule + (** [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 : S.T.Term.t -> S.Lit.t Iter.t -> S.P.proof_rule + (** [lemma_isa_split t lits] is the proof of + [is-c1 t \/ is-c2 t \/ … \/ is-c_n t] *) + + val lemma_isa_sel : S.T.Term.t -> S.P.proof_rule + (** [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 : S.Lit.t -> S.Lit.t -> S.P.proof_rule + (** [lemma_isa_disj (is-c t) (is-d t)] is the proof + of [¬ (is-c t) \/ ¬ (is-c t)] *) + + val lemma_cstor_inj : S.T.Term.t -> S.T.Term.t -> int -> S.P.proof_rule + (** [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 : S.T.Term.t -> S.T.Term.t -> S.P.proof_rule + (** [lemma_isa_distinct (c …) (d …)] is the proof + of the unit clause [|- (c …) ≠ (d …)] *) + + val lemma_acyclicity : (S.T.Term.t * S.T.Term.t) Iter.t -> S.P.proof_rule + (** [lemma_acyclicity pairs] is a proof of [t1=u1, …, tn=un |- false] + by acyclicity. *) +end