Skip to content

Commit

Permalink
Improve efficency of get and add
Browse files Browse the repository at this point in the history
As we inlined the function `SimpleDomains_make` in `Enum_rel`, we can
write more efficient code for this theory.

We don't need to look in the map `t.domains` for constructor semantic
values as we always produce the same default domain for them, that is
a singleton without any explanation.
  • Loading branch information
Halbaroth committed Apr 4, 2024
1 parent 164986e commit ab374b0
Showing 1 changed file with 32 additions and 22 deletions.
54 changes: 32 additions & 22 deletions src/lib/reasoners/enum_rel.ml
Original file line number Diff line number Diff line change
Expand Up @@ -63,22 +63,19 @@ module Domain = struct
else
{ constrs; ex }

let default r =
match Th.embed r with
| Cons (c, _) ->
domain ~constrs:(HSS.singleton c) Ex.empty
let[@inline always] singleton ~ex c = { constrs = HSS.singleton c; ex }

let unknown ty =
match ty with
| Ty.Tsum (_, constrs) ->
(* Return the list of all the constructors of the type of [r]. *)
let constrs = HSS.of_list constrs in
assert (not @@ HSS.is_empty constrs);
{ constrs; ex = Ex.empty }
| _ ->
match X.type_info r with
| Ty.Tsum (_, constrs) ->
(* Return the list of all the constructors of the type of [r]. *)
let constrs = HSS.of_list constrs in
assert (not @@ HSS.is_empty constrs);
{ constrs; ex = Ex.empty }
| _ ->
(* Only Enum values can have a domain. This case shouldn't happen since
we check the type of [r] in [add] and [assume] functions of this
module. *)
assert false
(* Only Enum values can have a domain. This case shouldn't happen since
we check the type of semantic values in both [add] and [assume]. *)
assert false

let equal d1 d2 = HSS.equal d1.constrs d2.constrs

Expand Down Expand Up @@ -125,21 +122,34 @@ module Domains = struct
let changed = SX.add r t.changed in
{ domains; changed }

(** [get r t] returns the domain currently associated with [r] in [t]. *)
let get r t =
match Th.embed r with
| Cons (r, _) ->
(* For sake of efficiency, we don't look in the map if the
semantic value is a constructor. *)
Domain.singleton ~ex:Explanation.empty r
| _ ->
try MX.find r t.domains
with Not_found ->
Domain.unknown (X.type_info r)

(** [add r t] adds a domain for [r] in the domain map. If [r] does not
already have an associated domain, a fresh domain will be created for
[r] using [Domain.default]. *)
[r] and add to the map. *)
let add r t =
match MX.find r t.domains with
| _ -> t
| exception Not_found ->
let nd = Domain.default r in
let nd =
match Th.embed r with
| Cons (r, _) ->
Domain.singleton ~ex:Explanation.empty r
| _ ->
Domain.unknown (X.type_info r)
in
internal_update r nd t

(** [get r t] returns the domain currently associated with [r] in [t]. *)
let get r t =
try MX.find r t.domains
with Not_found -> Domain.default r

(** [update r d t] replaces the domain of [r] in [t] by [d]. The
representative [r] is marked [changed] after this call. *)
let update r d t =
Expand Down

0 comments on commit ab374b0

Please sign in to comment.