module FloatingPoint:sig
..end
module RoundingMode:sig
..end
val mk_sort : context -> int -> int -> Sort.sort
val mk_sort_half : context -> Sort.sort
val mk_sort_16 : context -> Sort.sort
val mk_sort_single : context -> Sort.sort
val mk_sort_32 : context -> Sort.sort
val mk_sort_double : context -> Sort.sort
val mk_sort_64 : context -> Sort.sort
val mk_sort_quadruple : context -> Sort.sort
val mk_sort_128 : context -> Sort.sort
val mk_nan : context -> Sort.sort -> Expr.expr
val mk_inf : context -> Sort.sort -> bool -> Expr.expr
val mk_zero : context -> Sort.sort -> bool -> Expr.expr
val mk_fp : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
This is the operator named `fp' in the SMT FP theory definition.
Note that \c sign is required to be a bit-vector of size 1. Significand and exponent
are required to be greater than 1 and 2 respectively. The FloatingPoint sort
of the resulting expression is automatically determined from the bit-vector sizes
of the arguments.
val mk_numeral_f : context -> float -> Sort.sort -> Expr.expr
This function is used to create numerals that fit in a float value.
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
val mk_numeral_i : context -> int -> Sort.sort -> Expr.expr
val mk_numeral_i_u : context -> bool -> int -> int -> Sort.sort -> Expr.expr
val mk_numeral_s : context -> string -> Sort.sort -> Expr.expr
val is_fp : Expr.expr -> bool
val is_abs : Expr.expr -> bool
val is_neg : Expr.expr -> bool
val is_add : Expr.expr -> bool
val is_sub : Expr.expr -> bool
val is_mul : Expr.expr -> bool
val is_div : Expr.expr -> bool
val is_fma : Expr.expr -> bool
val is_sqrt : Expr.expr -> bool
val is_rem : Expr.expr -> bool
val is_round_to_integral : Expr.expr -> bool
val is_min : Expr.expr -> bool
val is_max : Expr.expr -> bool
val is_leq : Expr.expr -> bool
val is_lt : Expr.expr -> bool
val is_geq : Expr.expr -> bool
val is_gt : Expr.expr -> bool
val is_eq : Expr.expr -> bool
val is_is_normal : Expr.expr -> bool
val is_is_subnormal : Expr.expr -> bool
val is_is_zero : Expr.expr -> bool
val is_is_infinite : Expr.expr -> bool
val is_is_nan : Expr.expr -> bool
val is_is_negative : Expr.expr -> bool
val is_is_positive : Expr.expr -> bool
val is_to_fp : Expr.expr -> bool
val is_to_fp_unsigned : Expr.expr -> bool
val is_to_ubv : Expr.expr -> bool
val is_to_sbv : Expr.expr -> bool
val is_to_real : Expr.expr -> bool
val is_to_ieee_bv : Expr.expr -> bool
val numeral_to_string : Expr.expr -> string
val mk_const : context -> Symbol.symbol -> Sort.sort -> Expr.expr
val mk_const_s : context -> string -> Sort.sort -> Expr.expr
val mk_abs : context -> Expr.expr -> Expr.expr
val mk_neg : context -> Expr.expr -> Expr.expr
val mk_add : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
val mk_sub : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
val mk_mul : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
val mk_div : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
val mk_fma : context ->
Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
val mk_sqrt : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_rem : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_round_to_integral : context -> Expr.expr -> Expr.expr -> Expr.expr
Rounds a floating-point number to the closest integer,
again represented as a floating-point number.
val mk_min : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_max : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_leq : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_lt : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_geq : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_gt : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_eq : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_is_normal : context -> Expr.expr -> Expr.expr
val mk_is_subnormal : context -> Expr.expr -> Expr.expr
val mk_is_zero : context -> Expr.expr -> Expr.expr
val mk_is_infinite : context -> Expr.expr -> Expr.expr
val mk_is_nan : context -> Expr.expr -> Expr.expr
val mk_is_negative : context -> Expr.expr -> Expr.expr
val mk_is_positive : context -> Expr.expr -> Expr.expr
val mk_to_fp_bv : context -> Expr.expr -> Sort.sort -> Expr.expr
val mk_to_fp_float : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr
val mk_to_fp_real : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr
val mk_to_fp_signed : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr
val mk_to_fp_unsigned : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr
val mk_to_ubv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr
val mk_to_sbv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr
val mk_to_real : context -> Expr.expr -> Expr.expr
val get_ebits : context -> Sort.sort -> int
val get_sbits : context -> Sort.sort -> int
val get_numeral_sign : context -> Expr.expr -> bool * int
val get_numeral_significand_string : context -> Expr.expr -> string
val get_numeral_exponent_string : context -> Expr.expr -> string
val get_numeral_exponent_int : context -> Expr.expr -> bool * int
val mk_to_ieee_bv : context -> Expr.expr -> Expr.expr
val mk_to_fp_int_real : context ->
Expr.expr -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr
val numeral_to_string : Expr.expr -> string