Module Z3.Arithmetic.Integer

module Integer: sig .. end

Integer Arithmetic

val mk_sort : context -> Sort.sort

Create a new integer sort.

val get_int : Expr.expr -> int

Retrieve the int value.

val get_big_int : Expr.expr -> Big_int.big_int

Get a big_int from an integer numeral

val numeral_to_string : Expr.expr -> string

Returns a string representation of a numeral.

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

Creates an integer constant.

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

Creates an integer constant.

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

Create an expression representing t1 mod t2. The arguments must have int type.

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

Create an expression representing t1 rem t2. The arguments must have int type.

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

Create an integer numeral.

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

Create an integer numeral.
Returns A Term with the given value and sort Integer

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

Coerce an integer to a real.

There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard.

You can take the floor of a real by creating an auxiliary integer Term k and and asserting MakeInt2Real(k) <= t1 < MkInt2Real(k)+1. The argument must be of integer sort.

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

Create an n-bit bit-vector from an integer argument.

NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.

The argument must be of integer sort.