From 6aafaad48f3f58db2eec039347a42ba1c4511a6c Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 28 Dec 2019 06:15:50 -0600 Subject: [PATCH] feat(data): store is-a/select parents in a monoid --- src/cc/Sidekick_cc.ml | 4 +- src/core/Sidekick_core.ml | 80 ++++++++++++++++++---- src/main/sidekick_version.ml | 2 +- src/th-cstor/Sidekick_th_cstor.ml | 6 +- src/th-data/Sidekick_th_data.ml | 109 +++++++++++++++++++++++------- 5 files changed, 159 insertions(+), 42 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index d5946010..64b587c5 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -282,7 +282,9 @@ module Make (A: CC_ARG) let[@inline] true_ cc = Lazy.force cc.true_ let[@inline] false_ cc = Lazy.force cc.false_ let[@inline] term_state cc = cc.tst - let[@inline] allocate_bitfield cc = Bits.mk_field cc.bitgen + let allocate_bitfield ~descr cc = + Log.debugf 5 (fun k->k "(@[cc.allocate-bit-field@ :descr %s@])" descr); + Bits.mk_field cc.bitgen let[@inline] on_backtrack cc f : unit = Backtrack_stack.push_if_nonzero_level cc.undo f diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index c782138b..2688a5db 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -231,7 +231,7 @@ module type CC_S = sig t (** Create a new congruence closure. *) - val allocate_bitfield : t -> N.bitfield + val allocate_bitfield : descr:string -> t -> N.bitfield (** Allocate a new bitfield for the nodes. See {!N.bitfield}. *) @@ -668,11 +668,24 @@ module type MONOID_ARG = sig module SI : SOLVER_INTERNAL type t val pp : t Fmt.printer - val name : string (* name of the monoid's value (short) *) - val of_term : SI.CC.N.t -> SI.T.Term.t -> t option + val name : string + (** name of the monoid's value (short) *) + + val of_term : + SI.CC.N.t -> SI.T.Term.t -> + (t option * (SI.T.Term.t * t) list) + (** [of_term n t], where [t] is the term annotating node [n], + returns [maybe_m, l], where: + - [maybe_m = Some m] if [t] has monoid value [m]; + otherwise [maybe_m=None] + - [l] is a list of [(u, m_u)] where each [u] is a direct subterm of [t] + and [m_u] is the monoid value attached to [u]. + *) + val merge : SI.CC.t -> SI.CC.N.t -> t -> SI.CC.N.t -> t -> (t, SI.CC.Expl.t) result end +(** Keep track of monoid state per equivalence class *) module Monoid_of_repr(M : MONOID_ARG) : sig type t val create_and_setup : ?size:int -> M.SI.t -> t @@ -680,7 +693,7 @@ module Monoid_of_repr(M : MONOID_ARG) : sig val pop_levels : t -> int -> unit val mem : t -> M.SI.CC.N.t -> bool val get : t -> M.SI.CC.N.t -> M.t option - val iter_all : t -> (M.SI.CC.N.t * M.t) Iter.t + val iter_all : t -> (M.SI.CC.repr * M.t) Iter.t end = struct module SI = M.SI module T = SI.T.Term @@ -704,15 +717,52 @@ end = struct let get self n = N_tbl.get self.values n - let on_new_term self cc n (t:T.t) = - match M.of_term n t with - | Some v -> - Log.debugf 20 - (fun k->k "(@[monoid[%s].on-new-term@ :n %a@ :value %a@])" - M.name N.pp n M.pp v); - SI.CC.set_bitfield cc self.field_has_value true n; - N_tbl.add self.values n v - | None -> () + let on_new_term self cc n (t:T.t) : unit = + let maybe_m, l = M.of_term n t in + begin match maybe_m with + | Some v -> + Log.debugf 20 + (fun k->k "(@[monoid[%s].on-new-term@ :n %a@ :value %a@])" + M.name N.pp n M.pp v); + SI.CC.set_bitfield cc self.field_has_value true n; + N_tbl.add self.values n v + | None -> () + end; + List.iter + (fun (u,m_u) -> + Log.debugf 20 + (fun k->k "(@[monoid[%s].on-new-term.sub@ :n %a@ :sub-t %a@ :value %a@])" + M.name N.pp n T.pp u M.pp m_u); + let n_u = + try CC.find_t cc u + with Not_found -> Error.errorf "subterm %a does not have a repr" T.pp u + in + if N.get_field self.field_has_value n_u then ( + let m_u' = + try N_tbl.find self.values n_u + with Not_found -> + Error.errorf "node %a has bitfield but no value" N.pp n_u + in + match M.merge cc n_u m_u n_u m_u' with + | Error expl -> + Error.errorf + "when merging@ @[for node %a@],@ \ + values %a and %a:@ conflict %a" + N.pp n_u M.pp m_u M.pp m_u' CC.Expl.pp expl + | Ok m_u_merged -> + Log.debugf 20 + (fun k->k "(@[monoid[%s].on-new-term.sub.merged@ \ + :n %a@ :sub-t %a@ :value %a@])" + M.name N.pp n T.pp u M.pp m_u_merged); + N_tbl.add self.values n_u m_u_merged; + ) else ( + (* just add to [n_u] *) + SI.CC.set_bitfield cc self.field_has_value true n_u; + N_tbl.add self.values n_u m_u; + ) + ) + l; + () let iter_all (self:t) : _ Iter.t = N_tbl.to_iter self.values @@ -756,7 +806,9 @@ end = struct end let create_and_setup ?size (solver:SI.t) : t = - let field_has_value = SI.CC.allocate_bitfield (SI.cc solver) in + let field_has_value = + SI.CC.allocate_bitfield ~descr:("monoid."^M.name^".has-value") + (SI.cc solver) in let self = { values=N_tbl.create ?size (); field_has_value; } in SI.on_cc_new_term solver (on_new_term self); SI.on_cc_pre_merge solver (on_pre_merge self); diff --git a/src/main/sidekick_version.ml b/src/main/sidekick_version.ml index bcefbe83..2c10c6ef 100644 --- a/src/main/sidekick_version.ml +++ b/src/main/sidekick_version.ml @@ -1,2 +1,2 @@ -let version = {git|ef77e1e729f176c3db680de25df9f2f820795e47 +let version = {git|858ffb6f2587ca5593417be1c9f95fe727390e9e |git} \ No newline at end of file diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml index 688e5cbd..0c8f7a60 100644 --- a/src/th-cstor/Sidekick_th_cstor.ml +++ b/src/th-cstor/Sidekick_th_cstor.ml @@ -40,10 +40,10 @@ module Make(A : ARG) : S with module A = A = struct Fmt.fprintf out "(@[cstor %a@ :term %a@])" Fun.pp v.cstor T.pp v.t (* attach data to constructor terms *) - let of_term n (t:T.t) : _ option = + let of_term n (t:T.t) : _ option * _ = match A.view_as_cstor t with - | T_cstor (cstor,args) -> Some {n; t; cstor; args} - | _ -> None + | T_cstor (cstor,args) -> Some {n; t; cstor; args}, [] + | _ -> None, [] let merge cc n1 v1 n2 v2 : _ result = Log.debugf 5 diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index ebc4dc43..1ede288c 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -138,77 +138,139 @@ module Make(A : ARG) : S with module A = A = struct module Card = Compute_card(A) + (** Monoid mapping each class to the (unique) constructor it contains, + if any *) module Monoid_cstor = struct module SI = SI + let name = "th-data.cstor" (* associate to each class a unique constructor term in the class (if any) *) type t = { - t: T.t; - n: N.t; - cstor: A.Cstor.t; - args: T.t IArray.t; + c_n: N.t; + c_cstor: A.Cstor.t; + c_args: T.t IArray.t; } - let name = "th-data.cstor" let pp out (v:t) = - Fmt.fprintf out "(@[cstor %a@ :term %a@])" A.Cstor.pp v.cstor T.pp v.t + Fmt.fprintf out "(@[%s@ :cstor %a@])" name A.Cstor.pp v.c_cstor (* attach data to constructor terms *) - let of_term n (t:T.t) : _ option = + let of_term n (t:T.t) : _ option * _ list = match A.view_as_data t with - | T_cstor (cstor,args) -> Some {n; t; cstor; args} - | _ -> None + | T_cstor (cstor,args) -> + Some {c_n=n;c_cstor=cstor; c_args=args}, [] + | _ -> None, [] - let merge cc n1 v1 n2 v2 : _ result = + let merge cc n1 c1 n2 c2 : _ result = Log.debugf 5 - (fun k->k "(@[%s.merge@ @[:c1 %a (t %a)@]@ @[:c2 %a (t %a)@]@])" - name N.pp n1 T.pp v1.t N.pp n2 T.pp v2.t); + (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 *) let expl = Expl.mk_list [ - Expl.mk_merge n1 v1.n; - Expl.mk_merge n2 v2.n; + Expl.mk_merge n1 c1.c_n; + Expl.mk_merge n2 c2.c_n; Expl.mk_merge n1 n2; ] in - if A.Cstor.equal v1.cstor v2.cstor then ( + if A.Cstor.equal c1.c_cstor c2.c_cstor then ( (* same function: injectivity *) - assert (IArray.length v1.args = IArray.length v2.args); + assert (IArray.length c1.c_args = IArray.length c2.c_args); IArray.iter2 (fun u1 u2 -> SI.CC.merge_t cc u1 u2 expl) - v1.args v2.args; - Ok v1 + c1.c_args c2.c_args; + Ok c1 ) else ( (* different function: disjointness *) Error expl ) end + (** Monoid mapping each class to the set of is-a/select of which it + is the argument *) + module Monoid_parents = struct + module SI = SI + let name = "th-data.parents" + + type select = { + sel_n: N.t; + sel_cstor: A.Cstor.t; + sel_idx: int; + } + + type is_a = { + is_a_n: N.t; + is_a_cstor: A.Cstor.t; + } + + (* associate to each class a unique constructor term in the class (if any) *) + type t = { + parent_is_a: is_a list;(* parents that are [is-a] *) + parent_select: select list; (* parents that are [select] *) + } + + let pp_select out s = Fmt.fprintf out "sel[%d]-%a" s.sel_idx A.Cstor.pp s.sel_cstor + let pp_is_a out s = Fmt.fprintf out "is-%a" A.Cstor.pp s.is_a_cstor + let pp out (v:t) = + Fmt.fprintf out + "(@[%s@ @[:sel [@[%a@]]@]@ @[:is-a [@[%a@]]@]@])" + name + (Util.pp_list pp_select) v.parent_select + (Util.pp_list pp_is_a) v.parent_is_a + + (* attach data to constructor terms *) + let of_term n (t:T.t) : _ option * _ list = + match A.view_as_data t with + | T_select (c, i, u) -> + let m_sel = { + parent_select=[{sel_n=n; sel_idx=i; sel_cstor=c}]; + parent_is_a=[]; + } in + None, [u, m_sel] + | T_is_a (c, u) -> + let m_sel = { + parent_is_a=[{is_a_n=n; is_a_cstor=c}]; + parent_select=[]; + } in + None, [u, m_sel] + | T_cstor _ | T_other _ -> None, [] + + let merge cc n1 v1 n2 v2 : _ result = + Log.debugf 5 + (fun k->k "(@[%s.merge@ @[:c1 %a %a@]@ @[:c2 %a %a@]@])" + name N.pp n1 pp v1 N.pp n2 pp v2); + let parent_is_a = v1.parent_is_a @ v2.parent_is_a in + let parent_select = v1.parent_select @ v2.parent_select in + Ok {parent_is_a; parent_select;} + end + module ST_cstors = Sidekick_core.Monoid_of_repr(Monoid_cstor) + module ST_parents = Sidekick_core.Monoid_of_repr(Monoid_parents) module N_tbl = Backtrackable_tbl.Make(N) type t = { tst: T.state; cstors: ST_cstors.t; (* repr -> cstor for the class *) + parents: ST_parents.t; (* repr -> parents for the class *) cards: Card.t; (* remember finiteness *) to_decide: unit N_tbl.t; (* set of terms to decide. *) case_split_done: unit T.Tbl.t; (* set of terms for which case split is done *) - (* TODO: also allocate a bit in CC to filter out quickly classes without cstors? *) (* TODO: bitfield for types with less than 62 cstors, to quickly detect conflict? *) } let push_level self = ST_cstors.push_level self.cstors; + ST_parents.push_level self.parents; N_tbl.push_level self.to_decide; () let pop_levels self n = ST_cstors.pop_levels self.cstors n; + ST_parents.pop_levels self.parents n; N_tbl.pop_levels self.to_decide n; () (* TODO: select/is-a *) - (* TODO: acyclicity *) (* TODO: remove (* attach data to constructor terms *) @@ -310,12 +372,12 @@ module Make(A : ARG) : S with module A = A = struct Log.debugf 100 (fun k->k "(@[data.acycl.mk-path %a %a@])" N.pp n pp_parent parent); let acc = Expl.mk_merge_t (N.term n) parent.t_eq_n :: acc in - let acc = Expl.mk_merge parent.parent.n parent.parent.cstor.n :: acc in + let acc = Expl.mk_merge parent.parent.n parent.parent.n :: acc in match parent.parent.flag with | Current (Some p') -> mk_path acc parent.parent.n p' | _ -> acc in - let c0 = [Expl.mk_merge n st.cstor.n;] in + let c0 = [Expl.mk_merge n st.n;] in let c = match parent with | None -> c0 | Some parent -> mk_path c0 n parent @@ -331,7 +393,7 @@ module Make(A : ARG) : S with module A = A = struct | Some st' -> let parent = {parent=st; t_eq_n=sub_t} in traverse ~parent sub st') - st.cstor.args; + st.cstor.Monoid_cstor.c_args; in begin (* populate tbl with [repr->cstor] *) @@ -393,6 +455,7 @@ module Make(A : ARG) : S with module A = A = struct let self = { tst=SI.tst 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 (); case_split_done=T.Tbl.create 16; cards=Card.create();