From 69d1fffee2953fda34e543bce1a7b207b9c807de Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <129742207+bclement-ocp@users.noreply.github.com> Date: Wed, 12 Jul 2023 07:51:28 +0000 Subject: [PATCH] [refactor] Always represent classes as sets (#721) Most representations of UF classes uses Expr.Set.t, but `class_of` specifically converts the class to a list. There doesn't seem to be any real reason for that, and it simply causes a bit of memory overhead by creating the list instead of iterating over the expression set directly. This patch is a first step towards abstracting the representation of UF classes by using a common type for all their representations. It is not entirely trivial to abstract the representation, because of cyclic dependencies with `Explanation.Inconsistent`. --- src/lib/reasoners/arrays_rel.ml | 18 +++++++++--------- src/lib/reasoners/ccx.ml | 4 ++-- src/lib/reasoners/ccx.mli | 2 +- src/lib/reasoners/matching.ml | 12 ++++++------ src/lib/reasoners/matching.mli | 2 +- src/lib/reasoners/uf.ml | 2 -- src/lib/reasoners/uf.mli | 2 +- 7 files changed, 20 insertions(+), 22 deletions(-) diff --git a/src/lib/reasoners/arrays_rel.ml b/src/lib/reasoners/arrays_rel.ml index e15ce6237..5622ce62e 100644 --- a/src/lib/reasoners/arrays_rel.ml +++ b/src/lib/reasoners/arrays_rel.ml @@ -229,8 +229,8 @@ let update_env are_eq are_dist dep env acc gi si p p_ded n n_ded = ---------------------------------------------------------------------*) let get_of_set are_eq are_dist gtype (env,acc) class_of = let {g=get; gt=gtab; gi=gi; gty=gty} = gtype in - L.fold_left - (fun (env,acc) set -> + E.Set.fold + (fun set (env,acc) -> if Tmap.splited get set env.seen then (env,acc) else let env = {env with seen = Tmap.update get set env.seen} in @@ -253,16 +253,16 @@ let get_of_set are_eq are_dist gtype (env,acc) class_of = update_env are_eq are_dist dep env acc gi si p p_ded n n_ded | _ -> (env,acc) - ) (env,acc) (class_of gtab) + ) (class_of gtab) (env,acc) (*---------------------------------------------------------------------- set(-,-,-) modulo egalite ---------------------------------------------------------------------*) let get_from_set _are_eq _are_dist stype (env,acc) class_of = let sets = - L.fold_left - (fun acc t -> S.union acc (TBS.find t env.tbset)) - (S.singleton stype) (class_of stype.st) + E.Set.fold + (fun t acc -> S.union acc (TBS.find t env.tbset)) + (class_of stype.st) (S.singleton stype) in S.fold (fun { s = set; si = si; sv = sv; _ } (env,acc) -> @@ -285,9 +285,9 @@ let get_and_set are_eq are_dist gtype (env,acc) class_of = let {g=get; gt=gtab; gi=gi; gty=gty} = gtype in let suff_sets = - L.fold_left - (fun acc t -> S.union acc (TBS.find t env.tbset)) - S.empty (class_of gtab) + E.Set.fold + (fun t acc -> S.union acc (TBS.find t env.tbset)) + (class_of gtab) S.empty in S.fold (fun {s=set; st=stab; si=si; sv=sv; _ } (env,acc) -> diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml index 4beed658f..11cbabc15 100644 --- a/src/lib/reasoners/ccx.ml +++ b/src/lib/reasoners/ccx.ml @@ -71,7 +71,7 @@ module type S = sig (r Xliteral.view * bool * Th_util.lit_origin) list * t val query : t -> E.t -> Th_util.answer val new_terms : t -> Expr.Set.t - val class_of : t -> Expr.t -> Expr.t list + val class_of : t -> Expr.t -> Expr.Set.t val are_equal : t -> Expr.t -> Expr.t -> init_terms:bool -> Th_util.answer val are_distinct : t -> Expr.t -> Expr.t -> Th_util.answer val cl_extract : t -> Expr.Set.t list @@ -341,7 +341,7 @@ module Main : S = struct match E.term_view t1 with | { E.f = f1; xs = [x]; _ } -> let ty_x = Expr.type_info x in - List.iter + E.Set.iter (fun t2 -> match E.term_view t2 with | { E.f = f2 ; xs = [y]; _ } when Sy.equal f1 f2 -> diff --git a/src/lib/reasoners/ccx.mli b/src/lib/reasoners/ccx.mli index 1cb76a22a..c49af116e 100644 --- a/src/lib/reasoners/ccx.mli +++ b/src/lib/reasoners/ccx.mli @@ -63,7 +63,7 @@ module type S = sig (r Xliteral.view * bool * Th_util.lit_origin) list * t val query : t -> Expr.t -> Th_util.answer val new_terms : t -> Expr.Set.t - val class_of : t -> Expr.t -> Expr.t list + val class_of : t -> Expr.t -> Expr.Set.t val are_equal : t -> Expr.t -> Expr.t -> init_terms:bool -> Th_util.answer val are_distinct : t -> Expr.t -> Expr.t -> Th_util.answer val cl_extract : t -> Expr.Set.t list diff --git a/src/lib/reasoners/matching.ml b/src/lib/reasoners/matching.ml index 4bc44d509..a0adb91c5 100644 --- a/src/lib/reasoners/matching.ml +++ b/src/lib/reasoners/matching.ml @@ -62,7 +62,7 @@ module type Arg = sig type t val term_repr : t -> E.t -> init_term:bool -> E.t val are_equal : t -> E.t -> E.t -> init_terms:bool -> Th_util.answer - val class_of : t -> E.t -> E.t list + val class_of : t -> E.t -> E.Set.t end module Make (X : Arg) : S with type theory = X.t = struct @@ -161,7 +161,7 @@ module Make (X : Arg) : S with type theory = X.t = struct ~module_name:"Matching" ~function_name:"match_class_of" "class_of (%a) = { %a }" E.print t - (fun fmt -> List.iter (Format.fprintf fmt "%a , " E.print)) cl + (fun fmt -> E.Set.iter (Format.fprintf fmt "%a , " E.print)) cl let candidate_substitutions pat_info res = let open Matching_types in @@ -404,13 +404,13 @@ module Make (X : Arg) : S with type theory = X.t = struct are_equal_light tbox pat t != None then [gsb] else - let cl = if mconf.Util.no_ematching then [t] + let cl = if mconf.Util.no_ematching then E.Set.singleton t else X.class_of tbox t in Debug.match_class_of t cl; let cl = - List.fold_left - (fun l t -> + E.Set.fold + (fun t l -> let { E.f = f; xs = xs; ty = ty; _ } = E.term_view t in if Symbols.compare f_pat f = 0 then xs::l else @@ -420,7 +420,7 @@ module Make (X : Arg) : S with type theory = X.t = struct (xs_modulo_records t record) :: l | _ -> l end - )[] cl + ) cl [] in let cl = filter_classes mconf cl tbox in let cl = diff --git a/src/lib/reasoners/matching.mli b/src/lib/reasoners/matching.mli index 1d87acf8c..d8057f5d8 100644 --- a/src/lib/reasoners/matching.mli +++ b/src/lib/reasoners/matching.mli @@ -60,7 +60,7 @@ module type Arg = sig type t val term_repr : t -> Expr.t -> init_term:bool -> Expr.t val are_equal : t -> Expr.t -> Expr.t -> init_terms:bool -> Th_util.answer - val class_of : t -> Expr.t -> Expr.t list + val class_of : t -> Expr.t -> Expr.Set.t end diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index 4d7a9ed77..81dd4095a 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -900,8 +900,6 @@ let term_repr uf t = try SE.min_elt st with Not_found -> t -let class_of env t = SE.elements (class_of env t) - let empty () = let env = { make = ME.empty; diff --git a/src/lib/reasoners/uf.mli b/src/lib/reasoners/uf.mli index 09159f66b..ddd80b567 100644 --- a/src/lib/reasoners/uf.mli +++ b/src/lib/reasoners/uf.mli @@ -55,7 +55,7 @@ val are_equal : t -> Expr.t -> Expr.t -> added_terms:bool -> Th_util.answer val are_distinct : t -> Expr.t -> Expr.t -> Th_util.answer val already_distinct : t -> r list -> bool -val class_of : t -> Expr.t -> Expr.t list +val class_of : t -> Expr.t -> Expr.Set.t val rclass_of : t -> r -> Expr.Set.t val cl_extract : t -> Expr.Set.t list