Reduce allocations in hashconsing hash function

src/smtml/bitvector.ml

@@ -25,6 +25,11 @@ let of_int32 v = make (Z.of_int32 v) 32
 
 let of_int64 v = make (Z.of_int64 v) 64
 
+(* Optimized mixer (DJB2 variant). Inlines to simple arithmetic. *)
+let[@inline] combine h v = (h * 33) + v
+
+let hash a = combine (Z.hash a.value) a.width
+
 let equal a b = Z.equal a.value b.value && a.width = b.width
 
 let eqz v = Z.equal Z.zero v.value

src/smtml/bitvector.mli

@@ -18,6 +18,8 @@ val to_int64 : t -> Int64.t
 
 val numbits : t -> int
 
+val hash : t -> int
+
 val equal : t -> t -> bool
 
 val compare : t -> t -> int

src/smtml/expr.ml

@@ -66,24 +66,56 @@ module Expr = struct
       , _ ) ->
       false
 
+  (* Optimized mixer (DJB2 variant). Inlines to simple arithmetic. *)
+  let[@inline] combine h v = (h * 33) + v
+
   let hash (e : expr) : int =
-    let h x = Hashtbl.hash x in
     match e with
-    | Val v -> h v
-    | Ptr { base; offset } -> h (base, offset.tag)
-    | Loc l -> h l
-    | Symbol s -> h s
-    | List v -> h v
-    | App (x, es) -> h (x, es)
-    | Unop (ty, op, e) -> h (ty, op, e.tag)
-    | Cvtop (ty, op, e) -> h (ty, op, e.tag)
-    | Binop (ty, op, e1, e2) -> h (ty, op, e1.tag, e2.tag)
-    | Relop (ty, op, e1, e2) -> h (ty, op, e1.tag, e2.tag)
-    | Triop (ty, op, e1, e2, e3) -> h (ty, op, e1.tag, e2.tag, e3.tag)
-    | Naryop (ty, op, es) -> h (ty, op, es)
-    | Extract (e, hi, lo) -> h (e.tag, hi, lo)
-    | Concat (e1, e2) -> h (e1.tag, e2.tag)
-    | Binder (b, vars, e) -> h (b, vars, e.tag)
+    | Val v -> Value.hash v
+    | Ptr { base; offset } -> combine (Bitvector.hash base) offset.tag
+    | Loc l -> Loc.hash l
+    | Symbol s -> Symbol.hash s
+    | List l -> List.fold_left (fun acc x -> combine acc x.Hc.tag) 0 l
+    | App (s, es) ->
+      let h_s = Symbol.hash s in
+      List.fold_left (fun acc x -> combine acc x.Hc.tag) h_s es
+    | Unop (ty, op, e) ->
+      let h1 = Ty.hash ty in
+      let h2 = combine h1 (Ty.Unop.hash op) in
+      combine h2 e.tag
+    | Binop (ty, op, e1, e2) ->
+      let h = Ty.hash ty in
+      let h = combine h (Ty.Binop.hash op) in
+      let h = combine h e1.tag in
+      combine h e2.tag
+    | Triop (ty, op, e1, e2, e3) ->
+      let h = Ty.hash ty in
+      let h = combine h (Ty.Triop.hash op) in
+      let h = combine h e1.tag in
+      let h = combine h e2.tag in
+      combine h e3.tag
+    | Relop (ty, op, e1, e2) ->
+      let h = Ty.hash ty in
+      let h = combine h (Ty.Relop.hash op) in
+      let h = combine h e1.tag in
+      combine h e2.tag
+    | Cvtop (ty, op, e) ->
+      let h = Ty.hash ty in
+      let h = combine h (Ty.Cvtop.hash op) in
+      combine h e.tag
+    | Naryop (ty, op, es) ->
+      let h = Ty.hash ty in
+      let h = combine h (Ty.Naryop.hash op) in
+      List.fold_left (fun acc x -> combine acc x.Hc.tag) h es
+    | Extract (e, hi, lo) ->
+      let h = e.tag in
+      let h = combine h hi in
+      combine h lo
+    | Concat (e1, e2) -> combine e1.tag e2.tag
+    | Binder (b, vars, e) ->
+      let h = Hashtbl.hash b in
+      let h_vars = List.fold_left (fun acc x -> combine acc x.Hc.tag) h vars in
+      combine h_vars e.tag
 end
 
 module Hc = Hc.Make [@inlined hint] (Expr)

src/smtml/symbol.ml

@@ -44,6 +44,24 @@ let namespace { namespace; _ } = namespace
 
 let discr_namespace = function Attr -> 0 | Sort -> 1 | Term -> 2 | Var -> 3
 
+(* Optimized mixer (DJB2 variant). Inlines to simple arithmetic. *)
+let[@inline] combine h v = (h * 33) + v
+
+let hash_name n =
+  match n with
+  | Simple s ->
+    (* Hashtbl.hash is fine for strings (it's a C primitive) *)
+    combine 0 (Hashtbl.hash s)
+  | Indexed { basename; indices } ->
+    let h = combine 1 (Hashtbl.hash basename) in
+    (* Fold over indices to avoid list allocation *)
+    List.fold_left (fun acc s -> combine acc (Hashtbl.hash s)) h indices
+
+let hash { ty; name; namespace } =
+  let h = Ty.hash ty in
+  let h = combine h (hash_name name) in
+  combine h (discr_namespace namespace)
+
 let compare_namespace a b = compare (discr_namespace a) (discr_namespace b)
 
 let compare_name a b =

src/smtml/symbol.mli

@@ -86,6 +86,8 @@ val type_of : t -> Ty.t
 
 (** {1 Comparison} *)
 
+val hash : t -> int
+
 (** [compare sym1 sym2] performs a total order comparison of [sym1] and [sym2].
 *)
 val compare : t -> t -> int

src/smtml/ty.ml

@@ -35,6 +35,23 @@ let discr = function
   | Ty_bitv n -> 10 + n
   | Ty_fp n -> 11 + n
 
+(* Optimized mixer (DJB2 variant). Inlines to simple arithmetic. *)
+let[@inline] combine h v = (h * 33) + v
+
+let hash = function
+  | Ty_app -> 1
+  | Ty_bitv width -> combine 2 width
+  | Ty_bool -> 3
+  | Ty_fp width -> combine 4 width
+  | Ty_int -> 5
+  | Ty_list -> 6
+  | Ty_none -> 7
+  | Ty_real -> 8
+  | Ty_str -> 9
+  | Ty_unit -> 10
+  | Ty_regexp -> 11
+  | Ty_roundingMode -> 12
+
 let compare t1 t2 = compare (discr t1) (discr t2)
 
 let equal t1 t2 = compare t1 t2 = 0
@@ -128,6 +145,42 @@ module Unop = struct
     | Regexp_comp
   [@@deriving ord]
 
+  let hash = function
+    | Neg -> 0
+    | Not -> 1
+    | Clz -> 2
+    | Ctz -> 3
+    | Popcnt -> 4
+    (* Float *)
+    | Abs -> 5
+    | Sqrt -> 6
+    | Is_normal -> 7
+    | Is_subnormal -> 8
+    | Is_negative -> 9
+    | Is_positive -> 10
+    | Is_infinite -> 11
+    | Is_nan -> 12
+    | Is_zero -> 13
+    | Ceil -> 14
+    | Floor -> 15
+    | Trunc -> 16
+    | Nearest -> 17
+    | Head -> 18
+    | Tail -> 19
+    | Reverse -> 20
+    | Length -> 21
+    (* String *)
+    | Trim -> 22
+    (* RegExp *)
+    | Regexp_star -> 23
+    | Regexp_loop (min, max) ->
+      let h = 24 in
+      let h = combine h min in
+      combine h max
+    | Regexp_plus -> 25
+    | Regexp_opt -> 26
+    | Regexp_comp -> 27
+
   let equal o1 o2 =
     match (o1, o2) with
     | Neg, Neg
@@ -235,6 +288,41 @@ module Binop = struct
     | Regexp_diff
   [@@deriving ord]
 
+  let hash = function
+    | Add -> 0
+    | Sub -> 1
+    | Mul -> 2
+    | Div -> 3
+    | DivU -> 4
+    | Rem -> 5
+    | RemU -> 6
+    | Shl -> 7
+    | ShrA -> 8
+    | ShrL -> 9
+    | And -> 10
+    | Or -> 11
+    | Xor -> 12
+    | Implies -> 13
+    | Pow -> 14
+    | Min -> 15
+    | Max -> 16
+    | Copysign -> 17
+    | Rotl -> 18
+    | Rotr -> 19
+    | At -> 20
+    | List_cons -> 21
+    | List_append -> 22
+    (* String *)
+    | String_prefix -> 23
+    | String_suffix -> 24
+    | String_contains -> 25
+    | String_last_index -> 26
+    | String_in_re -> 27
+    (* Regexp *)
+    | Regexp_range -> 28
+    | Regexp_inter -> 29
+    | Regexp_diff -> 30
+
   let equal o1 o2 =
     match (o1, o2) with
     | Add, Add
@@ -325,6 +413,18 @@ module Relop = struct
     | GeU
   [@@deriving ord]
 
+  let hash = function
+    | Eq -> 0
+    | Ne -> 1
+    | Lt -> 2
+    | LtU -> 3
+    | Gt -> 4
+    | GtU -> 5
+    | Le -> 6
+    | LeU -> 7
+    | Ge -> 8
+    | GeU -> 9
+
   let equal op1 op2 =
     match (op1, op2) with
     | Eq, Eq
@@ -366,6 +466,17 @@ module Triop = struct
     | String_replace_re_all
   [@@deriving ord]
 
+  let hash = function
+    | Ite -> 0
+    | List_set -> 1
+    (* String *)
+    | String_extract -> 2
+    | String_replace -> 3
+    | String_index -> 4
+    | String_replace_all -> 5
+    | String_replace_re -> 6
+    | String_replace_re_all -> 7
+
   let equal op1 op2 =
     match (op1, op2) with
     | Ite, Ite
@@ -427,6 +538,38 @@ module Cvtop = struct
     | String_to_re
   [@@deriving ord]
 
+  let hash = function
+    | ToString -> 0
+    | OfString -> 1
+    | ToBool -> 2
+    | OfBool -> 3
+    | Reinterpret_int -> 4
+    | Reinterpret_float -> 5
+    | DemoteF64 -> 6
+    | PromoteF32 -> 7
+    | ConvertSI32 -> 8
+    | ConvertUI32 -> 9
+    | ConvertSI64 -> 10
+    | ConvertUI64 -> 11
+    | TruncSF32 -> 12
+    | TruncUF32 -> 13
+    | TruncSF64 -> 14
+    | TruncUF64 -> 15
+    | Trunc_sat_f32_s -> 16
+    | Trunc_sat_f32_u -> 17
+    | Trunc_sat_f64_s -> 18
+    | Trunc_sat_f64_u -> 19
+    | WrapI64 -> 20
+    | Sign_extend i -> combine 21 i
+    | Zero_extend i -> combine 22 i
+    (* String *)
+    | String_to_code -> 23
+    | String_from_code -> 24
+    | String_to_int -> 25
+    | String_from_int -> 26
+    | String_to_float -> 27
+    | String_to_re -> 28
+
   let equal op1 op2 =
     match (op1, op2) with
     | ToString, ToString
@@ -508,6 +651,12 @@ module Naryop = struct
     | Regexp_union
   [@@deriving ord]
 
+  let hash = function
+    | Logand -> 0
+    | Logor -> 1
+    | Concat -> 2
+    | Regexp_union -> 3
+
   let equal op1 op2 =
     match (op1, op2) with
     | Logand, Logand

src/smtml/ty.mli

@@ -34,6 +34,8 @@ type t =
 
 (** {1 Type Comparison} *)
 
+val hash : t -> int
+
 (** [compare t1 t2] performs a total order comparison of types [t1] and [t2]. *)
 val compare : t -> t -> int
 
@@ -97,6 +99,8 @@ module Unop : sig
     | Regexp_comp  (** Complement. *)
   [@@deriving ord]
 
+  val hash : t -> int
+
   (** [equal op1 op2] checks if unary operations [op1] and [op2] are equal. *)
   val equal : t -> t -> bool
 
@@ -149,6 +153,8 @@ module Binop : sig
     | Regexp_diff  (** Difference of regular expressions. *)
   [@@deriving ord]
 
+  val hash : t -> int
+
   (** [equal op1 op2] checks if binary operations [op1] and [op2] are equal. *)
   val equal : t -> t -> bool
 
@@ -174,6 +180,8 @@ module Relop : sig
     | GeU  (** Unsigned greater than or equal. *)
   [@@deriving ord]
 
+  val hash : t -> int
+
   (** [equal op1 op2] checks if relational operations [op1] and [op2] are equal.
   *)
   val equal : t -> t -> bool
@@ -207,6 +215,8 @@ module Triop : sig
           (str.replace_re_all String RegLan String) *)
   [@@deriving ord]
 
+  val hash : t -> int
+
   (** [equal op1 op2] checks if ternary operations [op1] and [op2] are equal. *)
   val equal : t -> t -> bool
 
@@ -254,6 +264,8 @@ module Cvtop : sig
     | String_to_re  (** Convert string to regular expression. *)
   [@@deriving ord]
 
+  val hash : t -> int
+
   (** [equal op1 op2] checks if conversion operations [op1] and [op2] are equal.
   *)
   val equal : t -> t -> bool
@@ -274,6 +286,8 @@ module Naryop : sig
     | Regexp_union  (** Union of regular expressions. *)
   [@@deriving ord]
 
+  val hash : t -> int
+
   (** [equal op1 op2] checks if n-ary operations [op1] and [op2] are equal. *)
   val equal : t -> t -> bool