Add is{Normal|Subnormal|Negative|Positive|Infinite} operators

Author: filipeom

src/smtml/bitwuzla_mappings.default.ml

@@ -370,8 +370,20 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
 
     let sqrt ~rm t = mk_term2 Kind.Fp_sqrt rm t
 
+    let is_normal t = mk_term1 Kind.Fp_is_normal t
+
+    let is_subnormal t = mk_term1 Kind.Fp_is_subnormal t
+
+    let is_negative t = mk_term1 Kind.Fp_is_neg t
+
+    let is_positive t = mk_term1 Kind.Fp_is_pos t
+
+    let is_infinite t = mk_term1 Kind.Fp_is_inf t
+
     let is_nan t = mk_term1 Kind.Fp_is_nan t
 
+    let is_zero t = mk_term1 Kind.Fp_is_zero t
+
     let round_to_integral ~rm t = mk_term2 Kind.Fp_rti rm t
 
     let add ~rm lhs rhs = mk_term3 Kind.Fp_add rm lhs rhs

src/smtml/cvc5_mappings.default.ml

@@ -356,8 +356,20 @@ module Fresh_cvc5 () = struct
 
     let sqrt ~rm t = Term.mk_term tm Kind.Floatingpoint_sqrt [| rm; t |]
 
+    let is_normal t = Term.mk_term tm Kind.Floatingpoint_is_normal [| t |]
+
+    let is_subnormal t = Term.mk_term tm Kind.Floatingpoint_is_subnormal [| t |]
+
+    let is_negative t = Term.mk_term tm Kind.Floatingpoint_is_neg [| t |]
+
+    let is_positive t = Term.mk_term tm Kind.Floatingpoint_is_pos [| t |]
+
+    let is_infinite t = Term.mk_term tm Kind.Floatingpoint_is_inf [| t |]
+
     let is_nan t = Term.mk_term tm Kind.Floatingpoint_is_nan [| t |]
 
+    let is_zero t = Term.mk_term tm Kind.Floatingpoint_is_zero [| t |]
+
     let round_to_integral ~rm t =
       Term.mk_term tm Kind.Floatingpoint_rti [| rm; t |]
 
@@ -373,7 +385,7 @@ module Fresh_cvc5 () = struct
 
     let max t1 t2 = Term.mk_term tm Kind.Floatingpoint_max [| t1; t2 |]
 
-    let fma ~rm a b c = Term.mk_term Kind.Floatingpoint_fma [| rm; a; b; c |]
+    let fma ~rm a b c = Term.mk_term tm Kind.Floatingpoint_fma [| rm; a; b; c |]
 
     let rem t1 t2 = Term.mk_term tm Kind.Floatingpoint_rem [| t1; t2 |]
 

src/smtml/dolmenexpr_to_expr.ml

@@ -313,8 +313,20 @@ module DolmenIntf = struct
 
     let sqrt ~rm t = DTerm.Float.sqrt rm t
 
+    let is_normal = DTerm.Float.isNormal
+
+    let is_subnormal = DTerm.Float.isSubnormal
+
+    let is_negative = DTerm.Float.isNegative
+
+    let is_positive = DTerm.Float.isPositive
+
+    let is_infinite = DTerm.Float.isInfinite
+
     let is_nan = DTerm.Float.isNaN
 
+    let is_zero = DTerm.Float.isZero
+
     let round_to_integral ~rm t = DTerm.Float.roundToIntegral rm t
 
     let add ~rm t1 t2 = DTerm.Float.add rm t1 t2

src/smtml/dolmenexpr_to_expr.mli

@@ -284,6 +284,18 @@ module DolmenIntf : sig
 
     val sqrt : rm:term -> term -> term
 
+    val is_normal : term -> term
+
+    val is_subnormal : term -> term
+
+    val is_negative : term -> term
+
+    val is_positive : term -> term
+
+    val is_infinite : term -> term
+
+    val is_zero : term -> term
+
     val is_nan : term -> term
 
     val round_to_integral : rm:term -> term -> term

src/smtml/mappings.ml

@@ -482,7 +482,13 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
         | Unop.Neg -> Float.neg e
         | Abs -> Float.abs e
         | Sqrt -> Float.sqrt ~rm:Float.Rounding_mode.rne e
+        | Is_normal -> Float.is_normal e
+        | Is_subnormal -> Float.is_subnormal e
+        | Is_negative -> Float.is_negative e
+        | Is_positive -> Float.is_positive e
+        | Is_infinite -> Float.is_infinite e
         | Is_nan -> Float.is_nan e
+        | Is_zero -> Float.is_zero e
         | Ceil -> Float.round_to_integral ~rm:Float.Rounding_mode.rtp e
         | Floor -> Float.round_to_integral ~rm:Float.Rounding_mode.rtn e
         | Trunc -> Float.round_to_integral ~rm:Float.Rounding_mode.rtz e

src/smtml/mappings.nop.ml

@@ -281,8 +281,20 @@ module Nop = struct
 
       let sqrt ~rm:_ = assert false
 
+      let is_normal _ = assert false
+
+      let is_subnormal _ = assert false
+
+      let is_negative _ = assert false
+
+      let is_positive _ = assert false
+
+      let is_infinite _ = assert false
+
       let is_nan _ = assert false
 
+      let is_zero _ = assert false
+
       let round_to_integral ~rm:_ = assert false
 
       let add ~rm:_ = assert false

src/smtml/mappings_intf.ml

@@ -496,6 +496,18 @@ module type M = sig
         using the rounding mode [rm]. *)
     val sqrt : rm:term -> term -> term
 
+    val is_normal : term -> term
+
+    val is_subnormal : term -> term
+
+    val is_negative : term -> term
+
+    val is_positive : term -> term
+
+    val is_infinite : term -> term
+
+    val is_zero : term -> term
+
     (** [is_nan t] checks if the floating-point term [t] is NaN. *)
     val is_nan : term -> term
 

src/smtml/smtlib.ml

@@ -124,19 +124,6 @@ module Term = struct
       Fmt.failwith "%acould not parse colon: %a %a" pp_loc loc Expr.pp symbol
         Expr.pp term
 
-  let combine_to_int64 sign_bit exponent_bit mantissa_bit =
-    let sign = Int64.of_string sign_bit in
-    let exponent = Int64.of_string exponent_bit in
-    let mantissa = Int64.of_string mantissa_bit in
-    let sign_shifted = Int64.shift_left sign 63 in
-    let exponent_shifted = Int64.shift_left exponent 52 in
-    Int64.logor sign_shifted (Int64.logor exponent_shifted mantissa)
-
-  let combine_to_int32 sign exponent mantissa =
-    let sign_shifted = Int32.shift_left sign 31 in
-    let exponent_shifted = Int32.shift_left exponent 23 in
-    Int32.logor sign_shifted (Int32.logor exponent_shifted mantissa)
-
   let make_fp_binop symbol (op : Ty.Binop.t) rm a b =
     match Expr.view rm with
     | Symbol { name = Simple "roundNearestTiesToEven"; _ } ->
@@ -227,6 +214,13 @@ module Term = struct
         if fp_sz = 32 then Expr.value (Num (F32 (Bitvector.to_int32 fp)))
         else if fp_sz = 64 then Expr.value (Num (F64 (Bitvector.to_int64 fp)))
         else Fmt.failwith "%afp size not supported" pp_loc loc
+      | "fp.isNormal", [ a ] -> Expr.raw_unop Ty_none Is_normal a
+      | "fp.isSubnormal", [ a ] -> Expr.raw_unop Ty_none Is_subnormal a
+      | "fp.isNegative", [ a ] -> Expr.raw_unop Ty_none Is_negative a
+      | "fp.isPositive", [ a ] -> Expr.raw_unop Ty_none Is_positive a
+      | "fp.isInfinite", [ a ] -> Expr.raw_unop Ty_none Is_infinite a
+      | "fp.isNaN", [ a ] -> Expr.raw_unop Ty_none Is_nan a
+      | "fp.isZero", [ a ] -> Expr.raw_unop Ty_none Is_zero a
       | "fp.abs", [ a ] -> Expr.raw_unop Ty_none Abs a
       | "fp.neg", [ a ] -> Expr.raw_unop Ty_none Neg a
       | "fp.add", [ rm; a; b ] -> make_fp_binop symbol Add rm a b

src/smtml/ty.ml

@@ -98,7 +98,13 @@ module Unop = struct
     (* Float *)
     | Abs
     | Sqrt
+    | Is_normal
+    | Is_subnormal
+    | Is_negative
+    | Is_positive
+    | Is_infinite
     | Is_nan
+    | Is_zero
     | Ceil
     | Floor
     | Trunc
@@ -125,7 +131,13 @@ module Unop = struct
     | Ctz, Ctz
     | Abs, Abs
     | Sqrt, Sqrt
+    | Is_normal, Is_normal
+    | Is_subnormal, Is_subnormal
+    | Is_negative, Is_negative
+    | Is_positive, Is_positive
+    | Is_infinite, Is_infinite
     | Is_nan, Is_nan
+    | Is_zero, Is_zero
     | Ceil, Ceil
     | Floor, Floor
     | Trunc, Trunc
@@ -141,9 +153,11 @@ module Unop = struct
     | Regexp_opt, Regexp_opt
     | Regexp_comp, Regexp_comp ->
       true
-    | ( ( Neg | Not | Clz | Popcnt | Ctz | Abs | Sqrt | Is_nan | Ceil | Floor
-        | Trunc | Nearest | Head | Tail | Reverse | Length | Trim | Regexp_star
-        | Regexp_loop _ | Regexp_plus | Regexp_opt | Regexp_comp )
+    | ( ( Neg | Not | Clz | Popcnt | Ctz | Abs | Sqrt | Is_normal | Is_subnormal
+        | Is_negative | Is_positive | Is_infinite | Is_nan | Is_zero | Ceil
+        | Floor | Trunc | Nearest | Head | Tail | Reverse | Length | Trim
+        | Regexp_star | Regexp_loop _ | Regexp_plus | Regexp_opt | Regexp_comp
+          )
       , _ ) ->
       false
 
@@ -155,7 +169,13 @@ module Unop = struct
     | Popcnt -> Fmt.string fmt "popcnt"
     | Abs -> Fmt.string fmt "abs"
     | Sqrt -> Fmt.string fmt "sqrt"
+    | Is_normal -> Fmt.string fmt "isNormal"
+    | Is_subnormal -> Fmt.string fmt "isSubnormal"
+    | Is_negative -> Fmt.string fmt "isNegative"
+    | Is_positive -> Fmt.string fmt "isPositive"
+    | Is_infinite -> Fmt.string fmt "isInfinite"
     | Is_nan -> Fmt.string fmt "is_nan"
+    | Is_zero -> Fmt.string fmt "isZero"
     | Ceil -> Fmt.string fmt "ceil"
     | Floor -> Fmt.string fmt "floor"
     | Trunc -> Fmt.string fmt "trunc"

src/smtml/ty.mli

@@ -70,7 +70,13 @@ module Unop : sig
     (* Float operations *)
     | Abs  (** Absolute value. *)
     | Sqrt  (** Square root. *)
+    | Is_normal
+    | Is_subnormal
+    | Is_negative
+    | Is_positive
+    | Is_infinite
     | Is_nan  (** Check if NaN. *)
+    | Is_zero
     | Ceil  (** Ceiling. *)
     | Floor  (** Floor. *)
     | Trunc  (** Truncate. *)