int2bv and bv2nat: smart constructors

src/lib/structures/expr.ml

@@ -2908,9 +2908,6 @@ module BV = struct
     assert (size t = m);
     m
 
-  let int2bv n t = mk_term (Op (Int2BV n)) [t] (Tbitv n)
-  let bv2nat t = mk_term (Op BV2Nat) [t] Tint
-
   (* Function symbols for concatenation *)
   let concat s t =
     let n = size s and m = size t in
@@ -2952,6 +2949,22 @@ module BV = struct
       else
         concat (extract (i - 1) 0 t) (extract (m - 1) i t)
 
+  (* int2bv and bv2nat *)
+  let int2bv n t =
+    match term_view t with
+    | { f = Op BV2Nat; xs = [ t ]; ty = Tbitv m; _ } ->
+      if m > n then
+        extract (n - 1) 0 t
+      else
+        zero_extend (n - m) t
+    | _ -> mk_term (Op (Int2BV n)) [t] (Tbitv n)
+
+  let bv2nat t =
+    match term_view t with
+    | { f = Op Int2BV n; xs = [ t ]; _ } ->
+      Ints.(t mod ~$Z.(pow ~$2 n))
+    | _ -> mk_term (Op BV2Nat) [t] Tint
+
   (* Bit-wise operations *)
   let bvnot s = mk_term (Op BVnot) [s] (type_info s)
   let bvand s t = mk_term (Op BVand) [s; t] (type_info s)