Module Z3.Arithmetic.Real

module Real: sig .. end

Real Arithmetic

val mk_sort : context -> Sort.sort

Create a real sort.

val get_numerator : Expr.expr -> Expr.expr

The numerator of a rational numeral.

val get_denominator : Expr.expr -> Expr.expr

The denominator of a rational numeral.

val get_ratio : Expr.expr -> Q.t

Get a ratio from a real numeral

val to_decimal_string : Expr.expr -> int -> string

Returns a string representation in decimal notation. The result has at most as many decimal places as indicated by the int argument.

val numeral_to_string : Expr.expr -> string

Returns a string representation of a numeral.

val mk_const : context -> Symbol.symbol -> Expr.expr

Creates a real constant.

val mk_const_s : context -> string -> Expr.expr

Creates a real constant.

val mk_numeral_nd : context -> int -> int -> Expr.expr

Create a real numeral from a fraction.

Returns A Term with rational value and sort Real Arithmetic.Real.mk_numeral_s

val mk_numeral_s : context -> string -> Expr.expr

Create a real numeral.

val mk_numeral_i : context -> int -> Expr.expr

Create a real numeral.

val mk_is_integer : context -> Expr.expr -> Expr.expr

Creates an expression that checks whether a real number is an integer.

val mk_real2int : context -> Expr.expr -> Expr.expr

Coerce a real to an integer.

The semantics of this function follows the SMT-LIB standard for the function to_int. The argument must be of real sort.

module AlgebraicNumber: sig .. end

Algebraic Numbers