Start making migration from Num (IXX) to Bitv

src/bitvector/bitvector.ml

@@ -35,15 +35,15 @@ let clz bv =
     if i >= bv.width || Z.testbit bv.value (bv.width - 1 - i) then i
     else count_zeros (i + 1)
   in
-  count_zeros 0
+  make (Z.of_int @@ count_zeros 0) bv.width
 
 let ctz bv =
   let rec count_zeros i =
     if i >= bv.width || Z.testbit bv.value i then i else count_zeros (i + 1)
   in
-  count_zeros 0
+  make (Z.of_int @@ count_zeros 0) bv.width
 
-let popcnt bv = Z.popcount bv.value
+let popcnt bv = make (Z.of_int @@ Z.popcount bv.value) bv.width
 
 (* Binop *)
 let add a b =
@@ -104,14 +104,14 @@ let rem_u a b =
   make (Z.rem a.value b.value) a.width
 
 let rotate_left bv n =
-  let n = n mod bv.width in
+  let n = Z.to_int n.value mod bv.width in
   let left_part = Z.shift_left bv.value n in
   let right_part = Z.shift_right bv.value (bv.width - n) in
   let rotated = Z.logor left_part right_part in
   make rotated bv.width
 
 let rotate_right bv n =
-  let n = n mod bv.width in
+  let n = Z.to_int n.value mod bv.width in
   let right_part = Z.shift_right bv.value n in
   let left_part = Z.shift_left bv.value (bv.width - n) in
   let rotated = Z.logor left_part right_part in

src/bitvector/bitvector.mli

@@ -16,11 +16,11 @@ val neg : t -> t
 
 val lognot : t -> t
 
-val clz : t -> int
+val clz : t -> t
 
-val ctz : t -> int
+val ctz : t -> t
 
-val popcnt : t -> int
+val popcnt : t -> t
 
 val add : t -> t -> t
 
@@ -48,9 +48,9 @@ val rem : t -> t -> t
 
 val rem_u : t -> t -> t
 
-val rotate_left : t -> int -> t
+val rotate_left : t -> t -> t
 
-val rotate_right : t -> int -> t
+val rotate_right : t -> t -> t
 
 val lt : t -> t -> bool
 

src/smtml/altergo_mappings.default.ml

@@ -210,9 +210,7 @@ module Fresh = struct
       | { f = False; _ } -> False
       | { f = Int z; _ } -> Int (Z.to_int z)
       | { f = Real q; _ } -> Real (Q.to_float q)
-      | { f = Bitv (8, z); _ } -> Num (I8 (Z.to_int z))
-      | { f = Bitv (32, z); _ } -> Num (I32 (Z.to_int32 z))
-      | { f = Bitv (64, z); _ } -> Num (I64 (Z.to_int64 z))
+      | { f = Bitv (n, z); _ } -> Bitv (Bitvector.make z n)
       | _ ->
         Fmt.failwith "Altergo_mappings: ae_expr_to_value(%a)" AEL.Expr.print e
 
@@ -238,9 +236,7 @@ module Fresh = struct
           | Some q -> Real (Q.to_float q)
           | None -> (
             match (DM.Value.extract ~ops:DM.Bitv.ops v, ty) with
-            | Some z, Ty_bitv 8 -> Num (I8 (Z.to_int z))
-            | Some z, Ty_bitv 32 -> Num (I32 (Z.to_int32 z))
-            | Some z, Ty_bitv 64 -> Num (I64 (Z.to_int64 z))
+            | Some z, Ty_bitv n -> Bitv (Bitvector.make z n)
             | _ ->
               Fmt.failwith "Altergo_mappings: dvalue_to_value(%a)"
                 DM.Value.print v ) ) )

src/smtml/dolmenexpr_to_expr.ml

@@ -526,9 +526,12 @@ let encode_val : Value.t -> expr = function
   | Int v -> I.encode_val v
   | Real v -> Real.encode_val v
   | Str _ -> assert false
-  | Num (I8 x) -> Bv.encode_val C8 x
-  | Num (I32 x) -> Bv.encode_val C32 x
-  | Num (I64 x) -> Bv.encode_val C64 x
+  | Bitv _bv ->
+    (* TODO: fix this *)
+    (* Bv.encode_val C8 x *)
+    (* Bv.encode_val C32 x *)
+    (* Bv.encode_val C64 x *)
+    assert false
   | Num (F32 x) -> Fp.encode_val C32 x
   | Num (F64 x) -> Fp.encode_val C64 x
   | v -> Fmt.failwith {|Unsupported value "%a"|} Value.pp v
@@ -593,7 +596,7 @@ let encode_expr_acc ?(record_sym = fun acc _ -> acc) acc e =
     match Expr.view e with
     | Val v -> (acc, encode_val v)
     | Ptr { base; offset } ->
-      let base' = encode_val (Num (I32 base)) in
+      let base' = encode_val (Bitv (Bitvector.make (Z.of_int32 base) 32)) in
       let acc, offset' = aux acc offset in
       (acc, DTerm.Bitv.add base' offset')
     | Symbol s ->

src/smtml/dune

@@ -55,6 +55,7 @@
  (flags
   (:standard -open Smtml_prelude))
  (libraries
+  bitvector
   bos
   cmdliner
   dolmen