Refactoring Enum_rel using domains on class representatives only

OCamlPro · Apr 2, 2024 · afebbd6 · afebbd6
1 parent cee8b5a
commit afebbd6
Show file tree

Hide file tree

Showing 3 changed files with 367 additions and 249 deletions.
diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml
@@ -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. *)
 
@@ -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. *)