simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-11 05:28:34 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(CC/monoid): in monoid, store N.t, not a term.

Browse source 
make sure the sub-elements of the monoid are represented in the
congruence closure before-hand.
This commit is contained in:
Simon Cruanes 2021-03-22 13:06:44 -04:00
parent 9e0c79f597
commit 6d7edbb601
3 changed files with 33 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/core/Sidekick_core.ml
View file

@ -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] *)

12
src/th-cstor/Sidekick_th_cstor.ml
View file

@ -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 (

37
src/th-data/Sidekick_th_data.ml
View file

@ -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