Optimize bitvector numeral creation in solvers

src/smtml/bitvector.mli

@@ -16,6 +16,8 @@ val of_int64 : Int64.t -> t
 
 val view : t -> Z.t
 
+val to_signed : t -> Z.t
+
 val to_int32 : t -> Int32.t
 
 val to_int64 : t -> Int64.t

src/smtml/bitwuzla_mappings.default.ml

@@ -272,6 +272,12 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
   module Bitv = struct
     let v str bitwidth = mk_bv_value (Types.bitv bitwidth) str 10
 
+    let of_z v bitwidth =
+      let ty = Types.bitv bitwidth in
+      if Z.fits_int v then mk_bv_value_int ty (Z.to_int v)
+      else if Z.fits_int64 v then mk_bv_value_int64 ty (Z.to_int64 v)
+      else mk_bv_value ty (Z.to_string v) 10
+
     let neg t = mk_term1 Kind.Bv_neg t
 
     let lognot t = mk_term1 Kind.Bv_not t

src/smtml/cvc5_mappings.default.ml

@@ -259,6 +259,8 @@ module Fresh_cvc5 () = struct
   module Bitv = struct
     let v v_str bitwidth = Term.mk_bv_s tm bitwidth v_str 10
 
+    let of_z v bitwidth = Term.mk_bv_s tm bitwidth (Z.to_string v) 10
+
     let neg t = Term.mk_term tm Kind.Bitvector_neg [| t |]
 
     let lognot t = Term.mk_term tm Kind.Bitvector_not [| t |]

src/smtml/dolmenexpr_to_expr.ml

@@ -307,6 +307,8 @@ module DolmenIntf = struct
       let bv = int_to_bitvector (Z.of_string i) n in
       DTerm.Bitv.mk bv
 
+    let of_z (v : Z.t) (n : int) = DTerm.Bitv.mk (int_to_bitvector v n)
+
     let lognot = DTerm.Bitv.not
 
     let to_int ~signed:_ = DTerm.Bitv.to_nat

src/smtml/dolmenexpr_to_expr.mli

@@ -249,6 +249,8 @@ module DolmenIntf : sig
   module Bitv : sig
     val v : string -> int -> term
 
+    val of_z : Z.t -> int -> term
+
     val neg : term -> term
 
     val lognot : term -> term

src/smtml/mappings.ml

@@ -296,9 +296,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       module Bitv_impl = struct
         open M
 
-        let v bv =
-          let numbits = Bitvector.numbits bv in
-          Bitv.v (Bitvector.to_string bv) numbits
+        let v bv = Bitv.of_z (Bitvector.to_signed bv) (Bitvector.numbits bv)
 
         (* Stolen from @krtab in OCamlPro/owi#195 *)
         let clz bitwidth n =
@@ -560,7 +558,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
         | Str v -> String_impl.v v
         | Num (F32 x) -> Float32_impl.v x
         | Num (F64 x) -> Float64_impl.v x
-        | Bitv bv -> M.Bitv.v (Bitvector.to_string bv) (Bitvector.numbits bv)
+        | Bitv bv -> Bitv_impl.v bv
         | Re_none -> M.Re.none ()
         | Re_all -> M.Re.all ()
         | Re_allchar -> M.Re.allchar ()

src/smtml/mappings.nop.ml

@@ -229,6 +229,8 @@ module M = struct
     module Bitv = struct
       let v _ = assert false
 
+      let of_z _ = assert false
+
       let neg _ = assert false
 
       let lognot _ = assert false

src/smtml/mappings_intf.ml

@@ -404,6 +404,8 @@ module type M = sig
     (** [v s n] constructs a bitvector term from the string [s] of width [n]. *)
     val v : string -> int -> term
 
+    val of_z : Z.t -> int -> term
+
     (** [neg t] constructs the negation of the bitvector term [t]. *)
     val neg : term -> term
 

src/smtml/z3_mappings.default.ml

@@ -299,6 +299,11 @@ module M = struct
     module Bitv = struct
       let v bv bitwidth = Z3.BitVector.mk_numeral ctx bv bitwidth
 
+      let of_z v bitwidth =
+        let ty = Types.bitv bitwidth in
+        if Z.fits_int v then Z3.Expr.mk_numeral_int ctx (Z.to_int v) ty
+        else Z3.Expr.mk_numeral_string ctx (Z.to_string v) ty
+
       let neg e = Z3.BitVector.mk_neg ctx e
 
       let lognot e = Z3.BitVector.mk_not ctx e