perf, with lazy and no leaves

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

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 ();

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