feat(BV): Only store domains on variable parts

CHANGES.md

@@ -46,7 +46,8 @@
 ### Theory reasoning
 
  - Add word-level propagators for the BV theory (#944, #1004, #1007, #1010,
-   #1011, #1012, #1040, #1044, #1054, #1055, #1056, #1057, #1065, #1073, #1144)
+   #1011, #1012, #1040, #1044, #1054, #1055, #1056, #1057, #1065, #1073, #1144,
+   #1152)
  - Add interval domains and arithmetic propagators for the BV theory (#1058,
    #1083, #1084, #1085)
  - Fix incompleteness issues in the BV solver (#978, #979)

src/lib/dune

@@ -52,7 +52,7 @@
     Instances IntervalCalculus Intervals_intf Intervals_core Intervals
     Ite_rel Matching Matching_types Polynome Records Records_rel
     Satml_frontend_hybrid Satml_frontend Satml Sat_solver Sat_solver_sig
-    Sig Sig_rel Theory Uf Use Rel_utils Bitlist
+    Sig Sig_rel Theory Uf Use Domains Domains_intf Rel_utils Bitlist
     ; structures
     Commands Errors Explanation Fpa_rounding
     Parsed Profiling Satml_types Symbols

src/lib/reasoners/adt_rel.ml

@@ -198,7 +198,7 @@ module Domains = struct
       with Not_found ->
         Domain.unknown (X.type_info r)
 
-  let add r t =
+  let init r t =
     match Th.embed r with
     | Alien _ when not (MX.mem r t.domains) ->
       (* We have to add a default domain if the key `r` is not in map in order
@@ -243,7 +243,7 @@ module Domains = struct
       let t = remove r t in
       tighten nr nd t
 
-    | exception Not_found -> add nr t
+    | exception Not_found -> init nr t
 
   (* [propagate f a t] iterates on all the changed domains of [t] since the
      last call of [propagate]. The list of changed domains is flushed after
@@ -438,7 +438,7 @@ let add r uf domains =
   | Ty.Tadt _ ->
     Debug.add r;
     let rr, _ = Uf.find_r uf r in
-    Domains.add rr domains
+    Domains.init rr domains
   | _ ->
     domains