Skip to content

optimize Hashtbl.replace -> Hashtbl.add #596

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
filipeom merged 3 commits into from
Apr 13, 2026
Merged

optimize Hashtbl.replace -> Hashtbl.add #596

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c1be460
optimize Hashtbl.replace -> Hashtbl.add
redianthus Apr 13, 2026
ff9bc24
use List.equal instead of going through the list twice
redianthus Apr 13, 2026
1fc137b
refactor get_symbols to avoid duplication and remove the hastbl
redianthus Apr 13, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
89 changes: 24 additions & 65 deletions src/smtml/expr.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,9 +26,7 @@ and expr =
module Expr = struct
type t = expr

let list_eq (l1 : 'a list) (l2 : 'a list) : bool =
if List.compare_lengths l1 l2 = 0 then List.for_all2 phys_equal l1 l2
else false
let list_eq (l1 : 'a list) (l2 : 'a list) : bool = List.equal phys_equal l1 l2

let equal (e1 : expr) (e2 : expr) : bool =
match (e1, e2) with
Expand Down Expand Up @@ -182,38 +180,28 @@ let rec is_symbolic (v : t) : bool =
is_symbolic v1 || is_symbolic v2 || is_symbolic v3
| List vs | App (_, vs) | Naryop (_, _, vs) -> List.exists is_symbolic vs

let rec get_symbols_aux acc (hte : t) =
match view hte with
| Val _ -> acc
| Ptr { offset; _ } -> get_symbols_aux acc offset
| Symbol s -> s :: acc
| List es | App (_, es) | Naryop (_, _, es) ->
List.fold_left get_symbols_aux acc es
| Unop (_, _, e) | Cvtop (_, _, e) | Extract (e, _, _) ->
get_symbols_aux acc e
| Binop (_, _, e1, e2) | Relop (_, _, e1, e2) | Concat (e1, e2) ->
let acc = get_symbols_aux acc e1 in
get_symbols_aux acc e2
| Triop (_, _, e1, e2, e3) ->
let acc = get_symbols_aux acc e1 in
let acc = get_symbols_aux acc e2 in
get_symbols_aux acc e3
| Binder (_, vars, e) ->
let acc = List.fold_left get_symbols_aux acc vars in
get_symbols_aux acc e

let get_symbols (hte : t list) =
let tbl = Hashtbl.create 64 in
let rec symbols (hte : t) =
match view hte with
| Val _ -> ()
| Ptr { offset; _ } -> symbols offset
| Symbol s -> Hashtbl.replace tbl s ()
| List es -> List.iter symbols es
| App (_, es) -> List.iter symbols es
| Unop (_, _, e1) -> symbols e1
| Binop (_, _, e1, e2) ->
symbols e1;
symbols e2
| Triop (_, _, e1, e2, e3) ->
symbols e1;
symbols e2;
symbols e3
| Relop (_, _, e1, e2) ->
symbols e1;
symbols e2
| Cvtop (_, _, e) -> symbols e
| Naryop (_, _, es) -> List.iter symbols es
| Extract (e, _, _) -> symbols e
| Concat (e1, e2) ->
symbols e1;
symbols e2
| Binder (_, vars, e) ->
List.iter symbols vars;
symbols e
in
List.iter symbols hte;
Hashtbl.fold (fun k () acc -> k :: acc) tbl []
List.fold_left get_symbols_aux [] hte |> List.sort_uniq Symbol.compare

let rec pp_with ~printer fmt (hte : t) =
match view hte with
Expand Down Expand Up @@ -823,37 +811,8 @@ module Set = struct
v

let get_symbols (set : t) =
let tbl = Hashtbl.create 64 in
let rec symbols hte =
match view hte with
| Val _ -> ()
| Ptr { offset; _ } -> symbols offset
| Symbol s -> Hashtbl.replace tbl s ()
| List es -> List.iter symbols es
| App (_, es) -> List.iter symbols es
| Unop (_, _, e1) -> symbols e1
| Binop (_, _, e1, e2) ->
symbols e1;
symbols e2
| Triop (_, _, e1, e2, e3) ->
symbols e1;
symbols e2;
symbols e3
| Relop (_, _, e1, e2) ->
symbols e1;
symbols e2
| Cvtop (_, _, e) -> symbols e
| Naryop (_, _, es) -> List.iter symbols es
| Extract (e, _, _) -> symbols e
| Concat (e1, e2) ->
symbols e1;
symbols e2
| Binder (_, vars, e) ->
List.iter symbols vars;
symbols e
in
iter symbols set;
Hashtbl.fold (fun k () acc -> k :: acc) tbl []
fold (fun x acc -> get_symbols_aux acc x) set []
|> List.sort_uniq Symbol.compare

let map f set =
fold
Expand Down
4 changes: 2 additions & 2 deletions src/smtml/mappings.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -843,13 +843,13 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
List.iter
(fun sym ->
let v = value model0 (Expr.symbol sym) in
Hashtbl.replace m sym v )
Hashtbl.add m sym v )
symbols
| None ->
Smap.iter
(fun (sym : Symbol.t) term ->
let v = Encoder.value_of_term ~ctx model sym.ty term in
Hashtbl.replace m sym v )
Hashtbl.add m sym v )
ctx );
m

Expand Down
2 changes: 1 addition & 1 deletion src/smtml/smtlib.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -362,7 +362,7 @@ module Statement = struct
let name =
match Symbol.name id with Simple name -> name | _ -> assert false
in
Hashtbl.replace custom_sorts name (Expr.ty t);
Hashtbl.add custom_sorts name (Expr.ty t);
Echo ""

let datatypes ?loc:_ = assert false
Expand Down