From 6d7edbb60126d745a2d61431a6751bf38d242312 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 22 Mar 2021 13:06:44 -0400 Subject: [PATCH] fix(CC/monoid): in monoid, store N.t, not a term. make sure the sub-elements of the monoid are represented in the congruence closure before-hand. --- src/core/Sidekick_core.ml | 19 +++++++--------- src/th-cstor/Sidekick_th_cstor.ml | 12 +++++----- src/th-data/Sidekick_th_data.ml | 37 +++++++++++++++---------------- 3 files changed, 33 insertions(+), 35 deletions(-) diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 82d56a19..d93d1e92 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -730,13 +730,14 @@ module type MONOID_ARG = sig (** 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) + SI.CC.t -> SI.CC.N.t -> SI.T.Term.t -> + (t option * (SI.CC.N.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] + - [l] is a list of [(u, m_u)] where each [u]'s term + is a direct subterm of [t] and [m_u] is the monoid value attached to [u]. *) @@ -784,7 +785,7 @@ end = struct else None let on_new_term self cc n (t:T.t) : unit = - let maybe_m, l = M.of_term n t in + let maybe_m, l = M.of_term cc n t in begin match maybe_m with | Some v -> Log.debugf 20 @@ -795,14 +796,10 @@ end = struct | None -> () end; List.iter - (fun (u,m_u) -> + (fun (n_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 + M.name N.pp n N.pp n_u M.pp m_u); if N.get_field self.field_has_value n_u then ( let m_u' = try N_tbl.find self.values n_u @@ -819,7 +816,7 @@ end = struct 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); + M.name N.pp n N.pp n_u M.pp m_u_merged); N_tbl.add self.values n_u m_u_merged; ) else ( (* just add to [n_u] *) diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml index 279d4ac9..d568adfa 100644 --- a/src/th-cstor/Sidekick_th_cstor.ml +++ b/src/th-cstor/Sidekick_th_cstor.ml @@ -32,7 +32,7 @@ module Make(A : ARG) : S with module A = A = struct t: T.t; n: N.t; cstor: Fun.t; - args: T.t IArray.t; + args: N.t IArray.t; } let name = name @@ -40,15 +40,17 @@ 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 cc n (t:T.t) : _ option * _ = match A.view_as_cstor t with - | T_cstor (cstor,args) -> Some {n; t; cstor; args}, [] + | T_cstor (cstor,args) -> + let args = IArray.map (SI.CC.add_term cc) args in + Some {n; t; cstor; args}, [] | _ -> None, [] let merge cc n1 v1 n2 v2 e_n1_n2 : _ 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); + name N.pp n1 T.pp v1.t N.pp n2 T.pp v2.t); (* build full explanation of why the constructor terms are equal *) let expl = Expl.mk_list [ @@ -61,7 +63,7 @@ module Make(A : ARG) : S with module A = A = struct (* same function: injectivity *) assert (IArray.length v1.args = IArray.length v2.args); IArray.iter2 - (fun u1 u2 -> SI.CC.merge_t cc u1 u2 expl) + (fun u1 u2 -> SI.CC.merge cc u1 u2 expl) v1.args v2.args; Ok v1 ) else ( diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index afe359bc..2748a79e 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -149,16 +149,19 @@ module Make(A : ARG) : S with module A = A = struct type t = { c_n: N.t; c_cstor: A.Cstor.t; - c_args: T.t IArray.t; + c_args: N.t IArray.t; } let pp out (v:t) = - Fmt.fprintf out "(@[%s@ :cstor %a@ :n %a@])" name A.Cstor.pp v.c_cstor N.pp v.c_n + Fmt.fprintf out "(@[%s@ :cstor %a@ :n %a@ :args [@[%a@]]@])" + name A.Cstor.pp v.c_cstor N.pp v.c_n + (Util.pp_iarray N.pp) v.c_args (* attach data to constructor terms *) - let of_term n (t:T.t) : _ option * _ list = + let of_term cc n (t:T.t) : _ option * _ list = match A.view_as_data t with | T_cstor (cstor,args) -> + let args = IArray.map (SI.CC.add_term cc) args in Some {c_n=n;c_cstor=cstor; c_args=args}, [] | _ -> None, [] @@ -179,7 +182,7 @@ module Make(A : ARG) : S with module A = A = struct (* same function: injectivity *) assert (IArray.length c1.c_args = IArray.length c2.c_args); IArray.iter2 - (fun u1 u2 -> SI.CC.merge_t cc u1 u2 expl) + (fun u1 u2 -> SI.CC.merge cc u1 u2 expl) c1.c_args c2.c_args; Ok c1 ) else ( @@ -198,13 +201,13 @@ module Make(A : ARG) : S with module A = A = struct sel_n: N.t; sel_cstor: A.Cstor.t; sel_idx: int; - sel_arg: T.t; + sel_arg: N.t; } type is_a = { is_a_n: N.t; is_a_cstor: A.Cstor.t; - is_a_arg: T.t; + is_a_arg: N.t; } (* associate to each class a unique constructor term in the class (if any) *) @@ -223,15 +226,17 @@ module Make(A : ARG) : S with module A = A = struct (Util.pp_list pp_is_a) v.parent_is_a (* attach data to constructor terms *) - let of_term n (t:T.t) : _ option * _ list = + let of_term cc n (t:T.t) : _ option * _ list = match A.view_as_data t with | T_select (c, i, u) -> + let u = SI.CC.add_term cc u in let m_sel = { parent_select=[{sel_n=n; sel_idx=i; sel_cstor=c; sel_arg=u}]; parent_is_a=[]; } in None, [u, m_sel] | T_is_a (c, u) -> + let u = SI.CC.add_term cc u in let m_sel = { parent_is_a=[{is_a_n=n; is_a_cstor=c; is_a_arg=u;}]; parent_select=[]; @@ -317,8 +322,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 - let n_u_i = SI.CC.add_term cc u_i in - SI.CC.merge cc n n_u_i Expl.(mk_theory @@ mk_merge n_u cstor.c_n) + SI.CC.merge cc n u_i Expl.(mk_theory @@ mk_merge n_u cstor.c_n) | Some _ -> () | None -> N_tbl.add self.to_decide repr_u (); (* needs to be decided *) @@ -338,7 +342,7 @@ module Make(A : ARG) : S with module A = A = struct name Monoid_parents.pp_is_a is_a2 is_true N.pp n1 N.pp n2 Monoid_cstor.pp c1); 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_t (N.term n2) is_a2.is_a_arg] |> mk_theory) + mk_merge n2 is_a2.is_a_arg] |> mk_theory) 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 ( @@ -347,10 +351,9 @@ module Make(A : ARG) : S with module A = A = struct name N.pp n2 sel2.sel_idx Monoid_cstor.pp c1); assert (sel2.sel_idx < IArray.length c1.c_args); let u_i = IArray.get c1.c_args sel2.sel_idx in - let n_u_i = SI.CC.add_term cc u_i in - SI.CC.merge cc sel2.sel_n n_u_i + SI.CC.merge cc sel2.sel_n u_i Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n1 n2; - mk_merge_t (N.term n2) sel2.sel_arg] |> mk_theory); + mk_merge n2 sel2.sel_arg] |> mk_theory); ) in let merge_c_p n1 n2 = @@ -401,9 +404,7 @@ module Make(A : ARG) : S with module A = A = struct let g: graph = N_tbl.create ~size:32 () in let traverse_sub cstor : _ list = IArray.to_list_map - (fun sub_t -> - let sub_n = SI.CC.add_term cc sub_t in - sub_n, SI.CC.find cc sub_n) + (fun sub_n -> sub_n, SI.CC.find cc sub_n) cstor.Monoid_cstor.c_args in begin @@ -540,9 +541,7 @@ module Make(A : ARG) : S with module A = A = struct | None -> None | Some c -> Log.debugf 20 (fun k->k "(@[th-data.mk-model.find-cstor@ %a@])" Monoid_cstor.pp c); - let args = - IArray.map (fun t -> recurse si (SI.cc_add_term si t)) - c.c_args in + let args = IArray.map (recurse si) c.c_args in let t = A.mk_cstor self.tst c.c_cstor args in Some t