From 83d1176e5b306b3fcd29517122b39502496e932d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Thu, 25 Jul 2024 12:06:12 +0200 Subject: [PATCH] perf: Improve performance of literal de-duplication This patch improves the different code paths that are used to ensure literal uniqueness. There are a couple of performance bugs here that are fixed by this patch: - In Rel_utils, we use a set of Xliteral *views*, which are converted to actual Xliterals in the comparison function. This means that we hash the literal views repeatedly (each time a comparison is performed). - Everywhere, we use sets of literals as temporary caches for uniqueness, where we could use hash maps (with better access times) instead. - In Adt_rel, we de-deduplicate input literals, but this is (almost) already done in the Ccx module. Almost, because the Ccx module allows multiple literals as long as they originally come from different expressions in the input problem -- which should occur rarely enough that we don't need the double deduplication. On a development branch and a specific problem that was creating a lot of literals, the first change was a 3x speedup (from 36s to 12s), and the two second changes combined were an additional 25% speedup (from 12s to 9s). On our internal dataset, the full patch is a speedup of about 3-4%. --- src/lib/reasoners/adt_rel.ml | 15 ----------- src/lib/reasoners/ccx.ml | 47 +++++++++++++++++++--------------- src/lib/reasoners/rel_utils.ml | 33 +++++++++++++----------- 3 files changed, 44 insertions(+), 51 deletions(-) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index bd98369030..bc6dbd60fa 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -542,19 +542,6 @@ let propagate_domains new_terms domains = eqs, new_terms ) ([], new_terms) domains -(* Remove duplicate literals in the list [la]. *) -let remove_redundancies la = - let cache = ref SLR.empty in - List.filter - (fun (a, _, _, _) -> - let a = LR.make a in - if SLR.mem a !cache then false - else begin - cache := SLR.add a !cache; - true - end - ) la - (* Update the counter of case split size in [env]. *) let count_splits env la = List.fold_left @@ -568,8 +555,6 @@ let assume env uf la = let ds = Uf.domains uf in let domains = Uf.GlobalDomains.find (module Domains) ds in Debug.pp_domains "before assume" domains; - (* should be done globally in CCX *) - let la = remove_redundancies la in let delayed, result = Rel_utils.Delayed.assume env.delayed uf la in let domains = try diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml index ac732db92d..cdd871f514 100644 --- a/src/lib/reasoners/ccx.ml +++ b/src/lib/reasoners/ccx.ml @@ -433,35 +433,40 @@ module Main : S = struct env ) {env with uf=uf} res - module LRE = - Map.Make (struct + module HLR = + Hashtbl.Make (struct type t = LR.t * E.t option - let compare (x, y) (x', y') = - let c = LR.compare x x' in - if c <> 0 then c - else match y, y' with - | None, None -> 0 - | Some _, None -> 1 - | None, Some _ -> -1 - | Some a, Some a' -> E.compare a a' + let equal (x, y) (x', y') = + LR.equal x x' && + match y, y' with + | None, None -> true + | Some _, None -> false + | None, Some _ -> false + | Some a, Some a' -> E.equal a a' + + let hash (x, y) = + match y with + | None -> Hashtbl.hash (LR.hash x, 0) + | Some e -> Hashtbl.hash (LR.hash x, E.hash e) end) let make_unique sa = - let mp = - List.fold_left - (fun mp ((ra, aopt ,_ , _) as e) -> + match sa with + | [] | [ _ ] -> sa + | _ -> + let table = HLR.create 17 in + List.iter + (fun ((ra, aopt ,_ , _) as e) -> (* Make sure to prefer equalities of [Subst] origin because they are used for partial computations (see {!Rel_utils}). In general, we want to make sure that the relations see all the equalities from representative changes in the union-find. *) - LRE.update (LR.make ra, aopt) (function - | Some ((_, _, _, Th_util.Subst) as e') -> Some e' - | _ -> Some e - ) mp - - ) LRE.empty sa - in - LRE.fold (fun _ e acc -> e::acc) mp [] + let lra = LR.make ra in + match HLR.find table (lra, aopt) with + | (_, _, _, Th_util.Subst) -> () + | _ | exception Not_found -> HLR.replace table (lra, aopt) e + ) sa; + HLR.fold (fun _ e acc -> e::acc) table [] let replay_atom env sa = Options.exec_thread_yield (); diff --git a/src/lib/reasoners/rel_utils.ml b/src/lib/reasoners/rel_utils.ml index 854077ff20..7620471026 100644 --- a/src/lib/reasoners/rel_utils.ml +++ b/src/lib/reasoners/rel_utils.ml @@ -31,11 +31,7 @@ module SX = Shostak.SXH module HX = Shostak.HX module L = Xliteral module LR = Uf.LX -module SR = Set.Make( - struct - type t = X.r L.view - let compare a b = LR.compare (LR.make a) (LR.make b) - end) +module HLR = Hashtbl.Make(LR) (** [assume_nontrivial_eqs eqs la] can be used by theories to remove from the equations [eqs] both duplicates and those that are implied by the @@ -44,16 +40,23 @@ let assume_nontrivial_eqs (eqs : X.r Sig_rel.input list) (la : X.r Sig_rel.input list) : X.r Sig_rel.fact list = - let la = - List.fold_left (fun m (a, _, _, _) -> SR.add a m) SR.empty la - in - let eqs, _ = - List.fold_left - (fun ((eqs, m) as acc) ((sa, _, _, _) as e) -> - if SR.mem sa m then acc else e :: eqs, SR.add sa m - )([], la) eqs - in - List.rev_map (fun (sa, _, ex, orig) -> Literal.LSem sa, ex, orig) eqs + match eqs with + | [] -> [] + | eqs -> + let table = HLR.create 17 in + List.iter (fun (a, _, _, _) -> HLR.add table (LR.make a) ()) la; + let eqs = + List.fold_left + (fun eqs ((sa, _, _, _) as e) -> + let sa = LR.make sa in + if HLR.mem table sa then eqs + else ( + HLR.replace table sa (); + e :: eqs + ) + ) [] eqs + in + List.rev_map (fun (sa, _, ex, orig) -> Literal.LSem sa, ex, orig) eqs (* The type of delayed functions. A delayed function is given an [Uf.t] instance for resolving expressions to semantic values, the operator to compute, and a