Skip to content

Commit 1944788

Browse files
committed
Refactoring Enum_rel using domains on class representatives only
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.
1 parent cee8b5a commit 1944788

3 files changed

Lines changed: 367 additions & 249 deletions

File tree

src/lib/reasoners/bitv_rel.ml

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ let is_bv_ty = function
7777

7878
let is_bv_r r = is_bv_ty @@ X.type_info r
7979

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

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

127-
let unknown = function
127+
let unknown r =
128+
match X.type_info r with
128129
| Ty.Tbitv n -> unknown n Ex.empty
129130
| _ ->
130131
(* Only bit-vector values can have bitlist domains. *)

0 commit comments

Comments
 (0)