Add solver mappings Internals module and generic to_ieee_bv impl

- All the mappings now include a `Internals` module that will inform the
  `Mappings` module of internal behaviours, such as const caching and
  native support for the `to_ieee_bv` operator.

- Lift `to_ieee_bv` implementation to the `Mappings` module so that
  other solvers that don't have native support for `to_ieee_bv` use this
  aproximated implementation.

Author: filipeom

src/smtml/altergo_mappings.default.ml

@@ -318,6 +318,6 @@ module Fresh = struct
   end
 end
 
-let is_available = true
-
 include Fresh.Make ()
+
+let is_available = Internals.is_available

src/smtml/bitwuzla_mappings.default.ml

@@ -7,6 +7,14 @@ include Mappings_intf
 module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
   open B
 
+  module Internals = struct
+    let caches_consts = false
+
+    let is_available = true
+
+    let has_to_ieee_bv = false
+  end
+
   type ty = Sort.t
 
   type term = Term.t
@@ -24,9 +32,7 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
   type optimizer = unit
 
   (* Not supported *)
-  type func_decl = unit
-
-  let caches_consts = false
+  type func_decl = Term.t
 
   let true_ = mk_true ()
 
@@ -63,13 +69,13 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
   let exists _ = Fmt.failwith "Bitwuzla_mappings: exists not implemented"
 
   module Types = struct
-    let int = Obj.magic 0xdeadc0de
+    let int = mk_bool_sort ()
 
-    let real = Obj.magic 0xdeadbeef
+    let real = mk_bool_sort ()
 
     let bool = mk_bool_sort ()
 
-    let string = Obj.magic 0xbadcafe
+    let string = mk_bool_sort ()
 
     let bitv bitwidth = mk_bv_sort bitwidth
 
@@ -408,33 +414,19 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
 
     let of_ieee_bv eb sb bv = mk_term1_indexed2 Kind.Fp_to_fp_from_bv bv eb sb
 
-    (* TODO *)
-    let f32_to_i32 =
-      let args = [| Types.float 8 24 |] in
-      let ret = Types.bitv 32 in
-      let sort = B.mk_fun_sort args ret in
-      B.mk_const sort ~symbol:"f32_to_i32"
-
-    let f64_to_i64 =
-      let args = [| Types.float 11 53 |] in
-      let ret = Types.bitv 64 in
-      let sort = B.mk_fun_sort args ret in
-      B.mk_const sort ~symbol:"f64_to_i64"
-
-    let to_ieee_bv f =
-      let f_size = Sort.fp_exp_size (Term.sort f) + Sort.fp_sig_size (Term.sort f) in
-      if f_size = 32 then
-        mk_term2 Kind.Apply f32_to_i32 f
-      else if f_size = 64 then
-        mk_term2 Kind.Apply f64_to_i64 f
-      else
-        Fmt.failwith "Bitwuzla_mappings: Unsupported floating-point size"
+    let to_ieee_bv _f =
+      Fmt.failwith "Bitwuzla_mappings: to_ieee_bv is not implemented"
   end
 
   module Func = struct
-    let make _ _ _ = ()
-
-    let apply () _ = false_
+    let make symbol args return_ =
+      let args = Array.of_list args in
+      let sort = B.mk_fun_sort args return_ in
+      B.mk_const sort ~symbol
+
+    let apply f args =
+      let args = f :: args in
+      mk_term Kind.Apply @@ Array.of_list args
   end
 
   module Model = struct
@@ -527,9 +519,8 @@ end
 include (
   Mappings.Make (struct
     module Make () = Fresh_bitwuzla (Bitwuzla_cxx.Make ())
-
-    let is_available = true
-
     include Fresh_bitwuzla (Bitwuzla_cxx)
+
+    let is_available = Internals.is_available
   end) :
     S_with_fresh )

src/smtml/colibri2_mappings.default.ml

@@ -299,9 +299,9 @@ module M = struct
     end
   end
 
-  let is_available = true
-
   include Make ()
+
+  let is_available = Internals.is_available
 end
 
 module M' : Mappings_intf.M_with_make = M

src/smtml/cvc5_mappings.default.ml

@@ -6,6 +6,14 @@ open Cvc5
 include Mappings_intf
 
 module Fresh_cvc5 () = struct
+  module Internals = struct
+    let caches_consts = false
+
+    let is_available = true
+
+    let has_to_ieee_bv = false
+  end
+
   type ty = Sort.sort
 
   type term = Term.term
@@ -22,8 +30,6 @@ module Fresh_cvc5 () = struct
 
   type func_decl = unit
 
-  let caches_consts = false
-
   let tm = TermManager.mk_tm ()
 
   let true_ = Term.mk_true tm
@@ -518,10 +524,9 @@ end
 
 module Cvc5_with_make : Mappings_intf.M_with_make = struct
   module Make () = Fresh_cvc5 ()
-
-  let is_available = true
-
   include Fresh_cvc5 ()
+
+  let is_available = Internals.is_available
 end
 
 include Mappings.Make (Cvc5_with_make)

src/smtml/dolmenexpr_to_expr.ml

@@ -75,14 +75,20 @@ end
 module DolmenIntf = struct
   include DTerm
 
+  module Internals = struct
+    let caches_consts = false
+
+    let is_available = true
+
+    let has_to_ieee_bv = false
+  end
+
   type ty = DTy.t
 
   type term = DTerm.t
 
   type func_decl = DTerm.Const.t
 
-  let caches_consts = false
-
   let true_ = DTerm._true
 
   let false_ = DTerm._false

src/smtml/dolmenexpr_to_expr.mli

@@ -37,14 +37,20 @@ module Builtin : sig
 end
 
 module DolmenIntf : sig
+  module Internals : sig
+    val caches_consts : bool
+
+    val is_available : bool
+
+    val has_to_ieee_bv : bool
+  end
+
   type ty = DTy.t
 
   type term = DTerm.t
 
   type func_decl = DTerm.Const.t
 
-  val caches_consts : bool
-
   val true_ : term
 
   val false_ : term

src/smtml/mappings.ml

@@ -50,6 +50,10 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
 
     let str_trim = M.Func.make "string_trim" [ M.Types.string ] M.Types.string
 
+    let f32_to_i32 = M.Func.make "f32_to_i32" [ f32 ] i32
+
+    let f64_to_i64 = M.Func.make "f64_to_i64" [ f64 ] i64
+
     let get_type = function
       | Ty_int -> M.Types.int
       | Ty_real -> M.Types.real
@@ -66,7 +70,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
 
     let make_symbol (ctx : symbol_ctx) (s : Symbol.t) : symbol_ctx * M.term =
       let name = match s.name with Simple name -> name | _ -> assert false in
-      if M.caches_consts then
+      if M.Internals.caches_consts then
         let sym = M.const name (get_type s.ty) in
         (Smap.add s sym ctx, sym)
       else
@@ -297,6 +301,8 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
 
       val bitwidth : int
 
+      val to_ieee_bv : M.term -> M.term
+
       module Ixx : sig
         val of_int : int -> elt
 
@@ -401,7 +407,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
           Float.to_sbv bitwidth ~rm:Float.Rounding_mode.rtz e
         | TruncUF32 | TruncUF64 ->
           Float.to_ubv bitwidth ~rm:Float.Rounding_mode.rtz e
-        | Reinterpret_float -> Float.to_ieee_bv e
+        | Reinterpret_float -> to_ieee_bv e
         | ToBool -> M.distinct [ e; v @@ Ixx.of_int 0 ]
         | OfBool -> ite e (v @@ Ixx.of_int 1) (v @@ Ixx.of_int 0)
         | _ -> assert false
@@ -414,20 +420,28 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
 
       let bitwidth = 8
 
+      let to_ieee_bv _ = assert false
+
       module Ixx = struct
         let of_int i = i [@@inline]
 
         let shift_left v i = v lsl i [@@inline]
       end
     end)
 
+    let to_ieee_bv f e =
+      if M.Internals.has_to_ieee_bv then M.Float.to_ieee_bv e
+      else M.Func.apply f [ e ]
+
     module I32 = Bitv_impl (struct
       type elt = int32
 
       let v i = M.Bitv.v (Int32.to_string i) 32
 
       let bitwidth = 32
 
+      let to_ieee_bv = to_ieee_bv f32_to_i32
+
       module Ixx = Int32
     end)
 
@@ -436,6 +450,8 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
 
       let v i = M.Bitv.v (Int64.to_string i) 64
 
+      let to_ieee_bv = to_ieee_bv f64_to_i64
+
       let bitwidth = 64
 
       module Ixx = Int64

src/smtml/mappings.nop.ml

@@ -4,6 +4,14 @@
 
 module Nop = struct
   module Make () = struct
+    module Internals = struct
+      let caches_consts = false
+
+      let is_available = false
+
+      let has_to_ieee_bv = false
+    end
+
     type ty = unit
 
     type term = unit
@@ -20,8 +28,6 @@ module Nop = struct
 
     type func_decl = unit
 
-    let caches_consts = false
-
     let true_ = ()
 
     let false_ = ()

src/smtml/mappings_intf.ml

@@ -13,6 +13,18 @@
     solvers, including term construction, type handling, and solver interaction.
 *)
 module type M = sig
+  module Internals : sig
+    (** [is_available] indicates whether the module is available for use. *)
+    val is_available : bool
+
+    (** [caches_consts] indicates whether the solver caches constants. *)
+    val caches_consts : bool
+
+    (** [has_to_ieee_bv] indicates whether the solver native support for the
+        [to_ieee_bv]. *)
+    val has_to_ieee_bv : bool
+  end
+
   (** The type of SMT sorts (types). *)
   type ty
 
@@ -37,9 +49,6 @@ module type M = sig
   (** The type of function declarations. *)
   type func_decl
 
-  (** [caches_consts] indicates whether the solver caches constants. *)
-  val caches_consts : bool
-
   (** [true_] represents the Boolean constant [true]. *)
   val true_ : term
 
@@ -74,7 +83,8 @@ module type M = sig
   (** [xor t1 t2] constructs the logical XOR of the terms [t1] and [t2]. *)
   val xor : term -> term -> term
 
-  (** [implies t1 t2] constructs the logical implication of the terms [t1] and [t2]. *)
+  (** [implies t1 t2] constructs the logical implication of the terms [t1] and
+      [t2]. *)
   val implies : term -> term -> term
 
   (** [eq t1 t2] constructs the equality of the terms [t1] and [t2]. *)
@@ -711,7 +721,10 @@ module type M_with_make = sig
   (** [Make ()] creates a new instance of the [M] module type. *)
   module Make () : M
 
-  (** [is_available] indicates whether the module is available for use. *)
+  (** [is_available] indicates whether the module is available for use.
+
+      Will be deprecated in the future, please use Internals.is_available
+      instead. *)
   val is_available : bool
 
   (** Include the [M] module type. *)

src/smtml/z3_mappings.default.ml

@@ -6,6 +6,14 @@ include Mappings_intf
 
 module M = struct
   module Make () = struct
+    module Internals = struct
+      let caches_consts = true
+
+      let is_available = true
+
+      let has_to_ieee_bv = true
+    end
+
     type ty = Z3.Sort.sort
 
     type term = Z3.Expr.expr
@@ -22,8 +30,6 @@ module M = struct
 
     type func_decl = Z3.FuncDecl.func_decl
 
-    let caches_consts = true
-
     let ctx = Z3.mk_context []
 
     let true_ = Z3.Boolean.mk_true ctx
@@ -554,9 +560,9 @@ module M = struct
     end
   end
 
-  let is_available = true
-
   include Make ()
+
+  let is_available = Internals.is_available
 end
 
 module M' : Mappings_intf.M_with_make = M