path: root/tool_bin/lib/linux/z3/include/z3_fpa.h

/*++
Copyright (c) 2013 Microsoft Corporation

Module Name:

    z3_fpa.h

Abstract:

    Additional APIs for floating-point arithmetic (FP).

Author:

    Christoph M. Wintersteiger (cwinter) 2013-06-05

Notes:

--*/
#ifndef Z3_FPA_H_
#define Z3_FPA_H_

#ifdef __cplusplus
extern "C" {
#endif // __cplusplus

    /** \defgroup capi C API */
    /*@{*/

    /** @name Floating-Point Arithmetic */
    /*@{*/
    /**
        \brief Create the RoundingMode sort.

        \param c logical context

        def_API('Z3_mk_fpa_rounding_mode_sort', SORT, (_in(CONTEXT),))
    */
    Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c);

    /**
        \brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.

        \param c logical context

        def_API('Z3_mk_fpa_round_nearest_ties_to_even', AST, (_in(CONTEXT),))
    */
    Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c);

    /**
        \brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.

        \param c logical context

        def_API('Z3_mk_fpa_rne', AST, (_in(CONTEXT),))
    */
    Z3_ast Z3_API Z3_mk_fpa_rne(Z3_context c);

    /**
        \brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.

        \param c logical context

        def_API('Z3_mk_fpa_round_nearest_ties_to_away', AST, (_in(CONTEXT),))
    */
    Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c);

    /**
        \brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.

        \param c logical context

        def_API('Z3_mk_fpa_rna', AST, (_in(CONTEXT),))
    */
    Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c);

    /**
        \brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.

        \param c logical context

        def_API('Z3_mk_fpa_round_toward_positive', AST, (_in(CONTEXT),))
    */
    Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c);

    /**
        \brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.

        \param c logical context

        def_API('Z3_mk_fpa_rtp', AST, (_in(CONTEXT),))
    */
    Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c);

    /**
        \brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.

        \param c logical context

        def_API('Z3_mk_fpa_round_toward_negative', AST, (_in(CONTEXT),))
    */
    Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c);

    /**
        \brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.

        \param c logical context

        def_API('Z3_mk_fpa_rtn', AST, (_in(CONTEXT),))
    */
    Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c);

    /**
        \brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.

        \param c logical context

        def_API('Z3_mk_fpa_round_toward_zero', AST, (_in(CONTEXT),))
    */
    Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c);

    /**
        \brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.

        \param c logical context

        def_API('Z3_mk_fpa_rtz', AST, (_in(CONTEXT),))
    */
    Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c);

    /**
        \brief Create a FloatingPoint sort.

        \param c logical context
        \param ebits number of exponent bits
        \param sbits number of significand bits

        \remark \c ebits must be larger than 1 and \c sbits must be larger than 2.

        def_API('Z3_mk_fpa_sort', SORT, (_in(CONTEXT), _in(UINT), _in(UINT)))
    */
    Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits);

    /**
        \brief Create the half-precision (16-bit) FloatingPoint sort.

        \param c logical context

        def_API('Z3_mk_fpa_sort_half', SORT, (_in(CONTEXT),))
    */
    Z3_sort Z3_API Z3_mk_fpa_sort_half(Z3_context c);

    /**
        \brief Create the half-precision (16-bit) FloatingPoint sort.

        \param c logical context

        def_API('Z3_mk_fpa_sort_16', SORT, (_in(CONTEXT),))
    */
    Z3_sort Z3_API Z3_mk_fpa_sort_16(Z3_context c);

    /**
        \brief Create the single-precision (32-bit) FloatingPoint sort.

        \param c logical context.

        def_API('Z3_mk_fpa_sort_single', SORT, (_in(CONTEXT),))
    */
    Z3_sort Z3_API Z3_mk_fpa_sort_single(Z3_context c);

    /**
        \brief Create the single-precision (32-bit) FloatingPoint sort.

        \param c logical context

        def_API('Z3_mk_fpa_sort_32', SORT, (_in(CONTEXT),))
    */
    Z3_sort Z3_API Z3_mk_fpa_sort_32(Z3_context c);

    /**
        \brief Create the double-precision (64-bit) FloatingPoint sort.

        \param c logical context

        def_API('Z3_mk_fpa_sort_double', SORT, (_in(CONTEXT),))
    */
    Z3_sort Z3_API Z3_mk_fpa_sort_double(Z3_context c);

    /**
        \brief Create the double-precision (64-bit) FloatingPoint sort.

        \param c logical context

        def_API('Z3_mk_fpa_sort_64', SORT, (_in(CONTEXT),))
    */
    Z3_sort Z3_API Z3_mk_fpa_sort_64(Z3_context c);

    /**
        \brief Create the quadruple-precision (128-bit) FloatingPoint sort.

        \param c logical context

        def_API('Z3_mk_fpa_sort_quadruple', SORT, (_in(CONTEXT),))
    */
    Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(Z3_context c);

    /**
        \brief Create the quadruple-precision (128-bit) FloatingPoint sort.

        \param c logical context

        def_API('Z3_mk_fpa_sort_128', SORT, (_in(CONTEXT),))
    */
    Z3_sort Z3_API Z3_mk_fpa_sort_128(Z3_context c);

    /**
        \brief Create a floating-point NaN of sort \c s.

        \param c logical context
        \param s target sort

        def_API('Z3_mk_fpa_nan', AST, (_in(CONTEXT),_in(SORT)))
    */
    Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s);

    /**
        \brief Create a floating-point infinity of sort \c s.

        \param c logical context
        \param s target sort
        \param negative indicates whether the result should be negative

        When \c negative is \c true, -oo will be generated instead of +oo.

        def_API('Z3_mk_fpa_inf', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
    */
    Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative);

    /**
        \brief Create a floating-point zero of sort \c s.

        \param c logical context
        \param s target sort
        \param negative indicates whether the result should be negative

        When \c negative is \c true, -zero will be generated instead of +zero.

        def_API('Z3_mk_fpa_zero', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
    */
    Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, bool negative);

    /**
        \brief Create an expression of FloatingPoint sort from three bit-vector expressions.

        This is the operator named `fp' in the SMT FP theory definition.
        Note that \c sgn is required to be a bit-vector of size 1. Significand and exponent
        are required to be longer than 1 and 2 respectively. The FloatingPoint sort
        of the resulting expression is automatically determined from the bit-vector sizes
        of the arguments. The exponent is assumed to be in IEEE-754 biased representation.

        \param c logical context
        \param sgn sign
        \param exp exponent
        \param sig significand

        def_API('Z3_mk_fpa_fp', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig);

    /**
        \brief Create a numeral of FloatingPoint sort from a float.

        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.

        \param c logical context
        \param v value
        \param ty sort

        \c ty must be a FloatingPoint sort

        \sa Z3_mk_numeral

        def_API('Z3_mk_fpa_numeral_float', AST, (_in(CONTEXT), _in(FLOAT), _in(SORT)))
    */
    Z3_ast Z3_API Z3_mk_fpa_numeral_float(Z3_context c, float v, Z3_sort ty);

    /**
        \brief Create a numeral of FloatingPoint sort from a double.

        This function is used to create numerals that fit in a double value.
        It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.

        \param c logical context
        \param v value
        \param ty sort

        \c ty must be a FloatingPoint sort

        \sa Z3_mk_numeral

        def_API('Z3_mk_fpa_numeral_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT)))
    */
    Z3_ast Z3_API Z3_mk_fpa_numeral_double(Z3_context c, double v, Z3_sort ty);

    /**
        \brief Create a numeral of FloatingPoint sort from a signed integer.

        \param c logical context
        \param v value
        \param ty result sort

        \c ty must be a FloatingPoint sort

        \sa Z3_mk_numeral

        def_API('Z3_mk_fpa_numeral_int', AST, (_in(CONTEXT), _in(INT), _in(SORT)))
    */
    Z3_ast Z3_API Z3_mk_fpa_numeral_int(Z3_context c, signed v, Z3_sort ty);

    /**
        \brief Create a numeral of FloatingPoint sort from a sign bit and two integers.

        \param c logical context
        \param sgn sign bit (true == negative)
        \param sig significand
        \param exp exponent
        \param ty result sort

        \c ty must be a FloatingPoint sort

        \sa Z3_mk_numeral

        def_API('Z3_mk_fpa_numeral_int_uint', AST, (_in(CONTEXT), _in(BOOL), _in(INT), _in(UINT), _in(SORT)))
    */
    Z3_ast Z3_API Z3_mk_fpa_numeral_int_uint(Z3_context c, bool sgn, signed exp, unsigned sig, Z3_sort ty);

    /**
        \brief Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.

        \param c logical context
        \param sgn sign bit (true == negative)
        \param sig significand
        \param exp exponent
        \param ty result sort

        \c ty must be a FloatingPoint sort

        \sa Z3_mk_numeral

        def_API('Z3_mk_fpa_numeral_int64_uint64', AST, (_in(CONTEXT), _in(BOOL), _in(INT64), _in(UINT64), _in(SORT)))
    */
    Z3_ast Z3_API Z3_mk_fpa_numeral_int64_uint64(Z3_context c, bool sgn, int64_t exp, uint64_t sig, Z3_sort ty);

    /**
        \brief Floating-point absolute value

        \param c logical context
        \param t term of FloatingPoint sort

        def_API('Z3_mk_fpa_abs', AST, (_in(CONTEXT),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t);

    /**
        \brief Floating-point negation

        \param c logical context
        \param t term of FloatingPoint sort

        def_API('Z3_mk_fpa_neg', AST, (_in(CONTEXT),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t);

    /**
        \brief Floating-point addition

        \param c logical context
        \param rm term of RoundingMode sort
        \param t1 term of FloatingPoint sort
        \param t2 term of FloatingPoint sort

        \c rm must be of RoundingMode sort, \c t1 and \c t2 must have the same FloatingPoint sort.

        def_API('Z3_mk_fpa_add', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);

    /**
        \brief Floating-point subtraction

        \param c logical context
        \param rm term of RoundingMode sort
        \param t1 term of FloatingPoint sort
        \param t2 term of FloatingPoint sort

        \c rm must be of RoundingMode sort, \c t1 and \c t2 must have the same FloatingPoint sort.

        def_API('Z3_mk_fpa_sub', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);

    /**
        \brief Floating-point multiplication

        \param c logical context
        \param rm term of RoundingMode sort
        \param t1 term of FloatingPoint sort
        \param t2 term of FloatingPoint sort

        \c rm must be of RoundingMode sort, \c t1 and \c t2 must have the same FloatingPoint sort.

        def_API('Z3_mk_fpa_mul', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);

    /**
        \brief Floating-point division

        \param c logical context
        \param rm term of RoundingMode sort
        \param t1 term of FloatingPoint sort.
        \param t2 term of FloatingPoint sort

        The nodes \c rm must be of RoundingMode sort, \c t1 and \c t2 must have the same FloatingPoint sort.

        def_API('Z3_mk_fpa_div', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);

    /**
        \brief Floating-point fused multiply-add.

        \param c logical context
        \param rm term of RoundingMode sort
        \param t1 term of FloatingPoint sort
        \param t2 term of FloatingPoint sort
        \param t3 term of FloatingPoint sort

        The result is \ccode{round((t1 * t2) + t3)}.

        \c rm must be of RoundingMode sort, \c t1, \c t2, and \c t3 must have the same FloatingPoint sort.

        def_API('Z3_mk_fpa_fma', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3);

    /**
        \brief Floating-point square root

        \param c logical context
        \param rm term of RoundingMode sort
        \param t term of FloatingPoint sort

        \c rm must be of RoundingMode sort, \c t must have FloatingPoint sort.

        def_API('Z3_mk_fpa_sqrt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t);

    /**
        \brief Floating-point remainder

        \param c logical context
        \param t1 term of FloatingPoint sort
        \param t2 term of FloatingPoint sort

        \c t1 and \c t2 must have the same FloatingPoint sort.

        def_API('Z3_mk_fpa_rem', AST, (_in(CONTEXT),_in(AST),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2);

    /**
        \brief Floating-point roundToIntegral. Rounds a floating-point number to
        the closest integer, again represented as a floating-point number.

        \param c logical context
        \param rm term of RoundingMode sort
        \param t term of FloatingPoint sort

        \c t must be of FloatingPoint sort.

        def_API('Z3_mk_fpa_round_to_integral', AST, (_in(CONTEXT),_in(AST),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t);

    /**
        \brief Minimum of floating-point numbers.

        \param c logical context
        \param t1 term of FloatingPoint sort
        \param t2 term of FloatingPoint sort

        \c t1, \c t2 must have the same FloatingPoint sort.

        def_API('Z3_mk_fpa_min', AST, (_in(CONTEXT),_in(AST),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2);

    /**
        \brief Maximum of floating-point numbers.

        \param c logical context
        \param t1 term of FloatingPoint sort
        \param t2 term of FloatingPoint sort

        \c t1, \c t2 must have the same FloatingPoint sort.

        def_API('Z3_mk_fpa_max', AST, (_in(CONTEXT),_in(AST),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2);

     /**
        \brief Floating-point less than or equal.

        \param c logical context
        \param t1 term of FloatingPoint sort
        \param t2 term of FloatingPoint sort

        \c t1 and \c t2 must have the same FloatingPoint sort.

        def_API('Z3_mk_fpa_leq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2);

     /**
        \brief Floating-point less than.

        \param c logical context
        \param t1 term of FloatingPoint sort
        \param t2 term of FloatingPoint sort

        \c t1 and \c t2 must have the same FloatingPoint sort.

        def_API('Z3_mk_fpa_lt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2);

    /**
        \brief Floating-point greater than or equal.

        \param c logical context
        \param t1 term of FloatingPoint sort
        \param t2 term of FloatingPoint sort

        \c t1 and \c t2 must have the same FloatingPoint sort.

        def_API('Z3_mk_fpa_geq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2);

    /**
        \brief Floating-point greater than.

        \param c logical context
        \param t1 term of FloatingPoint sort
        \param t2 term of FloatingPoint sort

        \c t1 and \c t2 must have the same FloatingPoint sort.

        def_API('Z3_mk_fpa_gt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2);

    /**
        \brief Floating-point equality.

        \param c logical context
        \param t1 term of FloatingPoint sort
        \param t2 term of FloatingPoint sort

        Note that this is IEEE 754 equality (as opposed to SMT-LIB \ccode{=}).

        \c t1 and \c t2 must have the same FloatingPoint sort.

        def_API('Z3_mk_fpa_eq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2);

    /**
        \brief Predicate indicating whether \c t is a normal floating-point number.

        \param c logical context
        \param t term of FloatingPoint sort

        \c t must have FloatingPoint sort.

        def_API('Z3_mk_fpa_is_normal', AST, (_in(CONTEXT),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t);

    /**
        \brief Predicate indicating whether \c t is a subnormal floating-point number.

        \param c logical context
        \param t term of FloatingPoint sort

        \c t must have FloatingPoint sort.

        def_API('Z3_mk_fpa_is_subnormal', AST, (_in(CONTEXT),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_is_subnormal(Z3_context c, Z3_ast t);

    /**
        \brief Predicate indicating whether \c t is a floating-point number with zero value, i.e., +zero or -zero.

        \param c logical context
        \param t term of FloatingPoint sort

        \c t must have FloatingPoint sort.

        def_API('Z3_mk_fpa_is_zero', AST, (_in(CONTEXT),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_is_zero(Z3_context c, Z3_ast t);

   /**
        \brief Predicate indicating whether \c t is a floating-point number representing +oo or -oo.

        \param c logical context
        \param t term of FloatingPoint sort

        \c t must have FloatingPoint sort.

        def_API('Z3_mk_fpa_is_infinite', AST, (_in(CONTEXT),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t);

    /**
        \brief Predicate indicating whether \c t is a NaN.

        \param c logical context
        \param t term of FloatingPoint sort

        \c t must have FloatingPoint sort.

        def_API('Z3_mk_fpa_is_nan', AST, (_in(CONTEXT),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t);

    /**
        \brief Predicate indicating whether \c t is a negative floating-point number.

        \param c logical context
        \param t term of FloatingPoint sort

        \c t must have FloatingPoint sort.

        def_API('Z3_mk_fpa_is_negative', AST, (_in(CONTEXT),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_is_negative(Z3_context c, Z3_ast t);

    /**
        \brief Predicate indicating whether \c t is a positive floating-point number.

        \param c logical context
        \param t term of FloatingPoint sort

        \c t must have FloatingPoint sort.

        def_API('Z3_mk_fpa_is_positive', AST, (_in(CONTEXT),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_is_positive(Z3_context c, Z3_ast t);

    /**
        \brief Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.

        Produces a term that represents the conversion of a bit-vector term \c bv to a
        floating-point term of sort \c s.

        \param c logical context
        \param bv a bit-vector term
        \param s floating-point sort

        \c s must be a FloatingPoint sort, \c t must be of bit-vector sort, and the bit-vector
        size of \c bv must be equal to \ccode{ebits+sbits} of \c s. The format of the bit-vector is
        as defined by the IEEE 754-2008 interchange format.

        def_API('Z3_mk_fpa_to_fp_bv', AST, (_in(CONTEXT),_in(AST),_in(SORT)))
    */
    Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s);

    /**
        \brief Conversion of a FloatingPoint term into another term of different FloatingPoint sort.

        Produces a term that represents the conversion of a floating-point term \c t to a
        floating-point term of sort \c s. If necessary, the result will be rounded according
        to rounding mode \c rm.

        \param c logical context
        \param rm term of RoundingMode sort
        \param t term of FloatingPoint sort
        \param s floating-point sort

        \c s must be a FloatingPoint sort, \c rm must be of RoundingMode sort, \c t must be of floating-point sort.

        def_API('Z3_mk_fpa_to_fp_float', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
    */
    Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);

    /**
        \brief Conversion of a term of real sort into a term of FloatingPoint sort.

        Produces a term that represents the conversion of term \c t of real sort into a
        floating-point term of sort \c s. If necessary, the result will be rounded according
        to rounding mode \c rm.

        \param c logical context
        \param rm term of RoundingMode sort
        \param t term of Real sort
        \param s floating-point sort

        \c s must be a FloatingPoint sort, \c rm must be of RoundingMode sort, \c t must be of real sort.

        def_API('Z3_mk_fpa_to_fp_real', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
    */
    Z3_ast Z3_API Z3_mk_fpa_to_fp_real(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);

    /**
        \brief Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.

        Produces a term that represents the conversion of the bit-vector term \c t into a
        floating-point term of sort \c s. The bit-vector \c t is taken to be in signed
        2's complement format. If necessary, the result will be rounded according
        to rounding mode \c rm.

        \param c logical context
        \param rm term of RoundingMode sort
        \param t term of bit-vector sort
        \param s floating-point sort

        \c s must be a FloatingPoint sort, \c rm must be of RoundingMode sort, \c t must be of bit-vector sort.

        def_API('Z3_mk_fpa_to_fp_signed', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
    */
    Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);

    /**
        \brief Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.

        Produces a term that represents the conversion of the bit-vector term \c t into a
        floating-point term of sort \c s. The bit-vector \c t is taken to be in unsigned
        2's complement format. If necessary, the result will be rounded according
        to rounding mode \c rm.

        \param c logical context
        \param rm term of RoundingMode sort
        \param t term of bit-vector sort
        \param s floating-point sort

        \c s must be a FloatingPoint sort, \c rm must be of RoundingMode sort, \c t must be of bit-vector sort.

        def_API('Z3_mk_fpa_to_fp_unsigned', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
    */
    Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);

    /**
        \brief Conversion of a floating-point term into an unsigned bit-vector.

        Produces a term that represents the conversion of the floating-point term \c t into a
        bit-vector term of size \c sz in unsigned 2's complement format. If necessary, the result
        will be rounded according to rounding mode \c rm.

        \param c logical context
        \param rm term of RoundingMode sort
        \param t term of FloatingPoint sort
        \param sz size of the resulting bit-vector

        def_API('Z3_mk_fpa_to_ubv', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(UINT)))
    */
    Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz);

    /**
        \brief Conversion of a floating-point term into a signed bit-vector.

        Produces a term that represents the conversion of the floating-point term \c t into a
        bit-vector term of size \c sz in signed 2's complement format. If necessary, the result
        will be rounded according to rounding mode \c rm.

        \param c logical context
        \param rm term of RoundingMode sort
        \param t term of FloatingPoint sort
        \param sz size of the resulting bit-vector

        def_API('Z3_mk_fpa_to_sbv', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(UINT)))
    */
    Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz);

    /**
        \brief Conversion of a floating-point term into a real-numbered term.

        Produces a term that represents the conversion of the floating-point term \c t into a
        real number. Note that this type of conversion will often result in non-linear
        constraints over real terms.

        \param c logical context
        \param t term of FloatingPoint sort

        def_API('Z3_mk_fpa_to_real', AST, (_in(CONTEXT),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_to_real(Z3_context c, Z3_ast t);


    /** @name Z3-specific floating-point extensions */
    /*@{*/
    /**
        \brief Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.

        \param c logical context
        \param s FloatingPoint sort

        def_API('Z3_fpa_get_ebits', UINT, (_in(CONTEXT),_in(SORT)))
    */
    unsigned Z3_API Z3_fpa_get_ebits(Z3_context c, Z3_sort s);

    /**
        \brief Retrieves the number of bits reserved for the significand in a FloatingPoint sort.

        \param c logical context
        \param s FloatingPoint sort

        def_API('Z3_fpa_get_sbits', UINT, (_in(CONTEXT),_in(SORT)))
    */
    unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s);

    /**
        \brief Checks whether a given floating-point numeral is a NaN.

        \param c logical context
        \param t a floating-point numeral

        def_API('Z3_fpa_is_numeral_nan', BOOL, (_in(CONTEXT), _in(AST)))
    */
    bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t);

    /**
        \brief Checks whether a given floating-point numeral is a +oo or -oo.

        \param c logical context
        \param t a floating-point numeral

        def_API('Z3_fpa_is_numeral_inf', BOOL, (_in(CONTEXT), _in(AST)))
    */
    bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t);

    /**
        \brief Checks whether a given floating-point numeral is +zero or -zero.

        \param c logical context
        \param t a floating-point numeral

        def_API('Z3_fpa_is_numeral_zero', BOOL, (_in(CONTEXT), _in(AST)))
    */
    bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t);

    /**
        \brief Checks whether a given floating-point numeral is normal.

        \param c logical context
        \param t a floating-point numeral

        def_API('Z3_fpa_is_numeral_normal', BOOL, (_in(CONTEXT), _in(AST)))
    */
    bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t);

    /**
        \brief Checks whether a given floating-point numeral is subnormal.

        \param c logical context
        \param t a floating-point numeral

        def_API('Z3_fpa_is_numeral_subnormal', BOOL, (_in(CONTEXT), _in(AST)))
    */
    bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t);

    /**
        \brief Checks whether a given floating-point numeral is positive.

        \param c logical context
        \param t a floating-point numeral

        def_API('Z3_fpa_is_numeral_positive', BOOL, (_in(CONTEXT), _in(AST)))
    */
    bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t);

    /**
        \brief Checks whether a given floating-point numeral is negative.

        \param c logical context
        \param t a floating-point numeral

        def_API('Z3_fpa_is_numeral_negative', BOOL, (_in(CONTEXT), _in(AST)))
    */
    bool Z3_API Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t);

    /**
        \brief Retrieves the sign of a floating-point literal as a bit-vector expression.

        \param c logical context
        \param t a floating-point numeral

        Remarks: NaN is an invalid argument.

        def_API('Z3_fpa_get_numeral_sign_bv', AST, (_in(CONTEXT), _in(AST)))
    */
    Z3_ast Z3_API Z3_fpa_get_numeral_sign_bv(Z3_context c, Z3_ast t);

    /**
        \brief Retrieves the significand of a floating-point literal as a bit-vector expression.

        \param c logical context
        \param t a floating-point numeral

        Remarks: NaN is an invalid argument.

        def_API('Z3_fpa_get_numeral_significand_bv', AST, (_in(CONTEXT), _in(AST)))
    */
    Z3_ast Z3_API Z3_fpa_get_numeral_significand_bv(Z3_context c, Z3_ast t);

    /**
        \brief Retrieves the sign of a floating-point literal.

        \param c logical context
        \param t a floating-point numeral
        \param sgn sign

        Remarks: sets \c sgn to 0 if `t' is positive and to 1 otherwise, except for
        NaN, which is an invalid argument.

        def_API('Z3_fpa_get_numeral_sign', BOOL, (_in(CONTEXT), _in(AST), _out(INT)))
    */
    bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, int * sgn);

    /**
        \brief Return the significand value of a floating-point numeral as a string.

        \param c logical context
        \param t a floating-point numeral

        Remarks: The significand \c s is always \ccode{0.0 <= s < 2.0}; the resulting string is long
        enough to represent the real significand precisely.

        def_API('Z3_fpa_get_numeral_significand_string', STRING, (_in(CONTEXT), _in(AST)))
    */
    Z3_string Z3_API Z3_fpa_get_numeral_significand_string(Z3_context c, Z3_ast t);

    /**
        \brief Return the significand value of a floating-point numeral as a uint64.

        \param c logical context
        \param t a floating-point numeral
        \param n pointer to output uint64

        Remarks: This function extracts the significand bits in `t`, without the
        hidden bit or normalization. Sets the \c Z3_INVALID_ARG error code if the
        significand does not fit into a \c uint64. NaN is an invalid argument.

        def_API('Z3_fpa_get_numeral_significand_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64)))
    */
    bool Z3_API Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, uint64_t * n);

    /**
        \brief Return the exponent value of a floating-point numeral as a string.

        \param c logical context
        \param t a floating-point numeral
        \param biased flag to indicate whether the result is in biased representation

        Remarks: This function extracts the exponent in `t`, without normalization.
        NaN is an invalid argument.

    def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST), _in(BOOL)))
    */
    Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t, bool biased);

    /**
        \brief Return the exponent value of a floating-point numeral as a signed 64-bit integer

        \param c logical context
        \param t a floating-point numeral
        \param n exponent
        \param biased flag to indicate whether the result is in biased representation

        Remarks: This function extracts the exponent in `t`, without normalization.
        NaN is an invalid argument.

        def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _in(BOOL)))
    */
    bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, int64_t * n, bool biased);

    /**
        \brief Retrieves the exponent of a floating-point literal as a bit-vector expression.

        \param c logical context
        \param t a floating-point numeral
        \param biased flag to indicate whether the result is in biased representation

        Remarks: This function extracts the exponent in `t`, without normalization.
        NaN is an invalid arguments.

        def_API('Z3_fpa_get_numeral_exponent_bv', AST, (_in(CONTEXT), _in(AST), _in(BOOL)))
    */
    Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t, bool biased);

    /**
        \brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.

        \param c logical context
        \param t term of FloatingPoint sort

        \c t must have FloatingPoint sort. The size of the resulting bit-vector is automatically
        determined.

        Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
        knows only one NaN and it will always produce the same bit-vector representation of
        that NaN.

        def_API('Z3_mk_fpa_to_ieee_bv', AST, (_in(CONTEXT),_in(AST)))
    */
    Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t);

    /**
        \brief Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.

        Produces a term that represents the conversion of \ccode{sig * 2^exp} into a
        floating-point term of sort \c s. If necessary, the result will be rounded
        according to rounding mode \c rm.

        \param c logical context
        \param rm term of RoundingMode sort
        \param exp exponent term of Int sort
        \param sig significand term of Real sort
        \param s FloatingPoint sort

        \c s must be a FloatingPoint sort, \c rm must be of RoundingMode sort, \c exp must be of int sort, \c sig must be of real sort.

        def_API('Z3_mk_fpa_to_fp_int_real', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(SORT)))
    */
    Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real(Z3_context c, Z3_ast rm, Z3_ast exp, Z3_ast sig, Z3_sort s);
    /*@}*/
    /*@}*/
    /*@}*/

#ifdef __cplusplus
}
#endif // __cplusplus

#endif