diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 565adf976..2051a2c48 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1338,6 +1338,7 @@ struct let is_numeral_normal = Z3native.fpa_is_numeral_normal let is_numeral_subnormal = Z3native.fpa_is_numeral_subnormal let is_numeral_positive = Z3native.fpa_is_numeral_positive + let is_numeral_negative = Z3native.fpa_is_numeral_negative let mk_to_ieee_bv = Z3native.mk_fpa_to_ieee_bv let mk_to_fp_int_real = Z3native.mk_fpa_to_fp_int_real let numeral_to_string x = Z3native.get_numeral_string (Expr.gc x) x diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index a2ecf54c2..979e0cfab 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -2185,6 +2185,9 @@ sig (** Indicates whether a floating-point numeral is positive. *) val is_numeral_positive : context -> Expr.expr -> bool + + (** Indicates whether a floating-point numeral is negative. *) + val is_numeral_negative : context -> Expr.expr -> bool (** Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. *) val mk_to_ieee_bv : context -> Expr.expr -> Expr.expr