module Integer:sig
..end
val mk_sort : context -> Sort.sort
val get_int : Expr.expr -> int
val get_big_int : Expr.expr -> Big_int.big_int
val numeral_to_string : Expr.expr -> string
val mk_const : context -> Symbol.symbol -> Expr.expr
val mk_const_s : context -> string -> Expr.expr
val mk_mod : context -> Expr.expr -> Expr.expr -> Expr.expr
t1 mod t2
.
The arguments must have int type.val mk_rem : context -> Expr.expr -> Expr.expr -> Expr.expr
t1 rem t2
.
The arguments must have int type.val mk_numeral_s : context -> string -> Expr.expr
val mk_numeral_i : context -> int -> Expr.expr
val mk_int2real : context -> Expr.expr -> Expr.expr
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
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.