Skip to content

Commit

Permalink
Refactoring Enum_rel using domains on class representatives only
Browse files Browse the repository at this point in the history
This PR refactors the `Enum` relations in order to use a proper type
for the domains of enum semantic values.

Now, we only store domains for class representatives and I believe that the new
implementation is simpler to understand and to maintain.

I don't use the functor `Domains_make` of `Rel_utils` as domain's
propagations performed in `Enum_rel` are much simpler than the propagations in
the BV theory.
  • Loading branch information
Halbaroth committed Apr 2, 2024
1 parent cee8b5a commit 8d62c62
Show file tree
Hide file tree
Showing 3 changed files with 342 additions and 249 deletions.
5 changes: 3 additions & 2 deletions src/lib/reasoners/bitv_rel.ml
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ let is_bv_ty = function

let is_bv_r r = is_bv_ty @@ X.type_info r

module Domain : Rel_utils.Domain with type t = Bitlist.t = struct
module Domain = struct
(* Note: these functions are not in [Bitlist] proper in order to avoid a
(direct) dependency from [Bitlist] to the [Shostak] module. *)

Expand Down Expand Up @@ -124,7 +124,8 @@ module Domain : Rel_utils.Domain with type t = Bitlist.t = struct
| Ext (r, _r_size, i, j) -> extract (map_signed f r acc) i j
) empty (Shostak.Bitv.embed r)

let unknown = function
let unknown r =
match X.type_info r with
| Ty.Tbitv n -> unknown n Ex.empty
| _ ->
(* Only bit-vector values can have bitlist domains. *)
Expand Down
Loading

0 comments on commit 8d62c62

Please sign in to comment.