NF

src/lib/reasoners/bitv_rel.ml

@@ -437,8 +437,81 @@ module Interval_domain = struct
       ) (point Z.zero) (Shostak.Bitv.embed r)
 end
 
+let normal_form_bv bv =
+  let rec loop cte mask r_sz acc = function
+    | [] -> List.rev acc, (cte, mask, r_sz)
+    | { Bitv.bv = Bitv.Cte n ; sz } :: bv' ->
+      let cte = Z.(cte lsl sz lor n) in
+      let mask = Z.(mask lsl sz lor (extract minus_one 0 sz)) in
+      let acc =
+        match acc with
+        | [] -> []
+        | _ -> { Bitv.bv = Bitv.Cte Z.zero ; sz } :: acc
+      in
+      loop cte mask (r_sz + sz) acc bv'
+    | x :: bv' ->
+      let cte = Z.(cte lsl x.sz) in
+      let mask = Z.(mask lsl x.sz) in
+      loop cte mask (r_sz + x.sz) (x :: acc) bv'
+  in loop Z.zero Z.zero 0 [] bv
+
+let normal_form_r r =
+  let bv, ofs = normal_form_bv (Shostak.Bitv.embed r) in
+  match bv with
+  | [] -> None, ofs
+  | bv -> Some (Shostak.Bitv.is_mine bv), ofs
+
+module NF = struct
+  type expr = X.r
+
+  type var = X.r
+
+  type ofs = Z.t * Z.t * int
+
+  let pp_ofs ppf (cte, mask, sz) =
+    Fmt.pf ppf "%s & %s [%d]"
+      (Z.format "%b" cte) (Z.format "%b" mask) sz
+
+  let ofs_sub (cte1, mask1, sz1) (cte2, mask2, sz2) =
+    assert (sz1 = sz2);
+    assert (Z.equal (Z.logand mask2 (Z.lognot mask1)) Z.zero);
+    assert (Z.equal (Z.logand mask2 cte1) cte2);
+    let cte = Z.sub cte1 cte2 in
+    assert (Z.equal cte (Z.logand cte1 (Z.lognot mask2)));
+    let sz = Z.numbits (Z.extract (Z.lognot mask2) 0 sz1) in
+    (Z.extract cte 0 sz, Z.extract mask1 0 sz, sz)
+
+  let decompose = normal_form_r
+end
+
+module IDD = struct
+  type var = X.r
+
+  type ofs = Z.t * Z.t * int
+
+  let default_domain r =
+    Interval_domain.map_leaves (fun r ->
+        Interval_domain.unknown (X.type_info r)
+      ) r
+
+  type domain = Interval_domain.t
+
+  let constant (cte, _, _) =
+    Intervals.Int.of_bounds (Closed cte) (Closed cte)
+
+  let add_offset (cte, _, _) d =
+    Intervals.Int.add d (Intervals.Int.of_bounds (Closed cte) (Closed cte))
+
+  let sub_offset _ (cte, _, _) d =
+    Intervals.Int.sub d (Intervals.Int.of_bounds (Closed cte) (Closed cte))
+end
+
 module Interval_domains =
-  Rel_utils.Domains_make(Interval_domain)(Rel_utils.Explained(Constraint))
+  Rel_utils.Domains_make
+    (Interval_domain)
+    (Rel_utils.Explained(Constraint))
+    (IDD)
+    (NF)
 
 module Interval_domains_uf =
   Rel_utils.UfDomainMap(Interval_domain)(Interval_domains)
@@ -499,8 +572,44 @@ module Domain : Rel_utils.Domain with type t = Bitlist.t = struct
       invalid_arg "unknown"
 end
 
+module BDD = struct
+  type var = X.r
+
+  type ofs = Z.t * Z.t * int
+
+  type domain = Bitlist.t
+
+  let default_domain r =
+    Domain.map_leaves (fun r ->
+        Domain.unknown (X.type_info r)
+      ) r
+
+  let widen sz d =
+    let width = Bitlist.width d in
+    assert (width <= sz);
+    if width = sz then d else
+      Bitlist.concat (Bitlist.exact (sz - width) Z.zero Explanation.empty) d
+
+  let constant (cte, _, sz) =
+    Bitlist.exact sz cte Explanation.empty
+
+  let add_offset (cte, mask, sz) d =
+    assert (sz > 0);
+    let d = widen sz d in
+    let mask = Bitlist.exact sz mask Explanation.empty in
+    let cte = Bitlist.exact sz cte Explanation.empty in
+    Bitlist.logor d (Bitlist.logand cte mask)
+
+  let sub_offset r (_cte, mask, sz) d =
+    let r_sz = match X.type_info r with Tbitv n -> n | _ -> assert false in
+    assert (sz > 0);
+    assert (Bitlist.width d = sz);
+    let mask = Bitlist.exact sz mask Explanation.empty in
+    Bitlist.extract (Bitlist.logand d (Bitlist.lognot mask)) 0 (r_sz - 1)
+end
+
 module Domains =
-  Rel_utils.Domains_make(Domain)(Rel_utils.Explained(Constraint))
+  Rel_utils.Domains_make(Domain)(Rel_utils.Explained(Constraint))(BDD)(NF)
 module Domains_uf =
   Rel_utils.UfDomainMap(Domain)(Domains)
 
@@ -1218,7 +1327,7 @@ let propagate_bitlist queue dom =
     let update r d = update ~ex:Explanation.empty (handle dom r) d
     in
     if X.is_a_leaf r then
-      Domains.Variables.iter_parents r (fun p ->
+      Domains.VS.iter_parents r (fun p ->
           if X.is_a_leaf p then
             assert (X.equal r p)
           else
@@ -1243,7 +1352,7 @@ let propagate_intervals queue dom =
     let update r d = update ~ex:Explanation.empty (handle dom r) d
     in
     if X.is_a_leaf r then
-      Interval_domains_uf.Variables.iter_parents r (fun p ->
+      Interval_domains.VS.iter_parents r (fun p ->
           if X.is_a_leaf p then
             assert (X.equal r p)
           else
@@ -1391,18 +1500,6 @@ let rec propagate_all uf eqs bdom idom =
   else
     eqs, bdom, idom
 
-module Watch = struct
-  type t = int
-
-  let pp ppf n = Fmt.pf ppf "w%d" n
-
-  let equal = Int.equal
-
-  let compare = Int.compare
-
-  let hash : int -> int = Hashtbl.hash
-end
-
 type t =
   { delayed : Rel_utils.Delayed.t
   ; terms : SX.t