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

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