perf

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

src/lib/reasoners/shostak.ml

@@ -57,7 +57,13 @@ struct
     | Bitv of BITV.t
     | Adt of ADT.t
 
-  type r = {v : rview ; id : int}
+  type r = {v : rview ; mutable id : int ; mutable leaves : r list }
+
+  let uninit v =
+    { v
+    ; id = -1000 (* dummy *)
+    ; leaves = [] (* dummy *)
+    }
 
   (*BISECT-IGNORE-BEGIN*)
   module Debug = struct
@@ -156,7 +162,7 @@ struct
 
     type elt = r
 
-    let set_id tag r = { r with id=tag }
+    let set_id tag r = r.id <- tag; r
 
     let hash r =
       let res = match r.v with
@@ -193,14 +199,28 @@ struct
   let reinit_cache () =
     HC.reinit_cache ()
 
-  let hcons v = HC.make v
+  let leaves0 r =
+    match r.v with
+    | Arith t -> ARITH.leaves t
+    | Records t -> RECORDS.leaves t
+    | Bitv t -> BITV.leaves t
+    | Adt t -> ADT.leaves t
+    | Ac t -> r :: (AC.leaves t)
+    | Term _ -> [r]
+
+  let hcons rv =
+    let v = uninit rv in
+    let v' = HC.make v in
+    if v' == v then
+      v'.leaves <- leaves0 v';
+    v'
 
   (* end: Hconsing modules and functions *)
 
-  let embed1 x = hcons {v = Arith x; id = -1000 (* dummy *)}
-  let embed2 x = hcons {v = Records x; id = -1000 (* dummy *)}
-  let embed3 x = hcons {v = Bitv x; id = -1000 (* dummy *)}
-  let embed4 x = hcons {v = Adt x; id = -1000 (* dummy *)}
+  let embed1 x = hcons (Arith x)
+  let embed2 x = hcons (Records x)
+  let embed3 x = hcons (Bitv x)
+  let embed4 x = hcons (Adt x)
 
   let ac_embed ({ Sig.l; _ } as t) =
     match l with
@@ -210,9 +230,9 @@ struct
     | l     ->
       let sort = List.fast_sort (fun (x,_) (y,_) -> CX.str_cmp x y) in
       let ac = { t with Sig.l = List.rev (sort l) } in
-      hcons {v = Ac ac; id = -1000 (* dummy *)}
+      hcons (Ac ac)
 
-  let term_embed t = hcons {v = Term t; id = -1000 (* dummy *)}
+  let term_embed t = hcons (Term t)
 
   let extract1 = function { v=Arith r; _ } -> Some r | _ -> None
   let extract2 = function { v=Records r; _ } -> Some r | _ -> None
@@ -315,14 +335,7 @@ struct
 
   module SX = Set.Make(struct type t = r let compare = CX.hash_cmp end)
 
-  let leaves r =
-    match r.v with
-    | Arith t -> ARITH.leaves t
-    | Records t -> RECORDS.leaves t
-    | Bitv t -> BITV.leaves t
-    | Adt t -> ADT.leaves t
-    | Ac t -> r :: (AC.leaves t)
-    | Term _ -> [r]
+  let leaves r = r.leaves
 
   let is_constant r =
     match r.v with