Remove Internals.has_to_ieee_bv in favour of option type

Author: filipeom

src/smtml/altergo_mappings.default.ml

@@ -49,8 +49,6 @@ module M = struct
       let caches_consts = false
 
       let is_available = true
-
-      let has_to_ieee_bv = false
     end
 
     type 'a sat_module = (module Sat_solver_sig.S with type t = 'a)

src/smtml/bitwuzla_mappings.default.ml

@@ -11,8 +11,6 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
     let caches_consts = false
 
     let is_available = true
-
-    let has_to_ieee_bv = false
   end
 
   type ty = Sort.t
@@ -414,8 +412,7 @@ 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
 
-    let to_ieee_bv _f =
-      Fmt.failwith "Bitwuzla_mappings: to_ieee_bv is not implemented"
+    let to_ieee_bv = None
   end
 
   module Func = struct

src/smtml/colibri2_mappings.default.ml

@@ -24,8 +24,6 @@ module M = struct
       let caches_consts = false
 
       let is_available = true
-
-      let has_to_ieee_bv = false
     end
 
     type model =

src/smtml/cvc5_mappings.default.ml

@@ -10,8 +10,6 @@ module Fresh_cvc5 () = struct
     let caches_consts = false
 
     let is_available = true
-
-    let has_to_ieee_bv = false
   end
 
   type ty = Sort.sort
@@ -411,7 +409,7 @@ module Fresh_cvc5 () = struct
       let op = Op.mk_op tm Kind.Floatingpoint_to_fp_from_ieee_bv [| i1; i2 |] in
       Term.mk_term_op tm op [| t |]
 
-    let to_ieee_bv _ = assert false
+    let to_ieee_bv = None
   end
 
   module Func = struct

src/smtml/dolmenexpr_to_expr.ml

@@ -341,7 +341,7 @@ module DolmenIntf = struct
 
     let of_ieee_bv eb sb bv = DTerm.Float.ieee_format_to_fp eb sb bv
 
-    let to_ieee_bv _fp = assert false
+    let to_ieee_bv = None
   end
 
   module Func = struct

src/smtml/dolmenexpr_to_expr.mli

@@ -324,7 +324,7 @@ module DolmenIntf : sig
 
     val of_ieee_bv : int -> int -> term -> term
 
-    val to_ieee_bv : term -> term
+    val to_ieee_bv : (term -> term) option
   end
 
   module Func : sig

src/smtml/mappings.ml

@@ -429,9 +429,10 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       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 ]
+    let to_ieee_bv =
+      match M.Float.to_ieee_bv with
+      | Some to_ieee_bv -> fun _ e -> to_ieee_bv e
+      | None -> fun f e -> M.Func.apply f [ e ]
 
     module I32 = Bitv_impl (struct
       type elt = int32

src/smtml/mappings.nop.ml

@@ -8,8 +8,6 @@ module Nop = struct
       let caches_consts = false
 
       let is_available = false
-
-      let has_to_ieee_bv = false
     end
 
     type ty = unit
@@ -323,7 +321,7 @@ module Nop = struct
 
       let of_ieee_bv _ = assert false
 
-      let to_ieee_bv _ = assert false
+      let to_ieee_bv = None
     end
 
     module Func = struct

src/smtml/mappings_intf.ml

@@ -13,18 +13,6 @@
     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
 
@@ -102,6 +90,14 @@ module type M = sig
   (** [exists vars body] constructs an existential quantification term. *)
   val exists : term list -> term -> term
 
+  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
+  end
+
   (** {2 Type Handling} *)
 
   module Types : sig
@@ -584,7 +580,7 @@ module type M = sig
 
     (** [to_ieee_bv t] converts the floating-point term [t] to an IEEE bitvector
         term. *)
-    val to_ieee_bv : term -> term
+    val to_ieee_bv : (term -> term) option
   end
 
   (** {2 Function Handling} *)

src/smtml/z3_mappings.default.ml

@@ -10,8 +10,6 @@ module M = struct
       let caches_consts = true
 
       let is_available = true
-
-      let has_to_ieee_bv = true
     end
 
     type ty = Z3.Sort.sort
@@ -393,7 +391,7 @@ module M = struct
       let of_ieee_bv eb sb bv =
         Z3.FloatingPoint.mk_to_fp_bv ctx bv (Types.float eb sb)
 
-      let to_ieee_bv fp = Z3.FloatingPoint.mk_to_ieee_bv ctx fp
+      let to_ieee_bv = Some (fun fp -> Z3.FloatingPoint.mk_to_ieee_bv ctx fp)
     end
 
     module Func = struct