From 23c58a1ef6aa8ccc33d750921854ab9fb4b3cc42 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 26 Oct 2016 18:53:20 +0100 Subject: [PATCH] Added FPA numeral predicates to ML API --- src/api/ml/z3.ml | 6 ++++++ src/api/ml/z3.mli | 18 ++++++++++++++++++ 2 files changed, 24 insertions(+) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index dbf36c6a4..565adf976 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1332,6 +1332,12 @@ struct let get_numeral_significand_string = Z3native.fpa_get_numeral_significand_string let get_numeral_significand_uint = Z3native.fpa_get_numeral_significand_uint64 let get_numeral_significand_bv = Z3native.fpa_get_numeral_significand_bv + let is_numeral_nan = Z3native.fpa_is_numeral_nan + let is_numeral_inf = Z3native.fpa_is_numeral_inf + let is_numeral_zero = Z3native.fpa_is_numeral_zero + 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 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 2a73c08fb..a2ecf54c2 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -2168,6 +2168,24 @@ sig significand does not fit into an int. *) val get_numeral_significand_uint : context -> Expr.expr -> bool * int + (** Indicates whether a floating-point numeral is a NaN. *) + val is_numeral_nan : context -> Expr.expr -> bool + + (** Indicates whether a floating-point numeral is +oo or -oo. *) + val is_numeral_inf : context -> Expr.expr -> bool + + (** Indicates whether a floating-point numeral is +zero or -zero. *) + val is_numeral_zero : context -> Expr.expr -> bool + + (** Indicates whether a floating-point numeral is normal. *) + val is_numeral_normal : context -> Expr.expr -> bool + + (** Indicates whether a floating-point numeral is subnormal. *) + val is_numeral_subnormal : context -> Expr.expr -> bool + + (** Indicates whether a floating-point numeral is positive. *) + val is_numeral_positive : 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