Module Z3.Arithmetic

module Integer : sig ... end
module Real : sig ... end
val is_int : Expr.expr -> bool
val is_arithmetic_numeral : Expr.expr -> bool
val is_le : Expr.expr -> bool
val is_ge : Expr.expr -> bool
val is_lt : Expr.expr -> bool
val is_gt : Expr.expr -> bool
val is_add : Expr.expr -> bool
val is_sub : Expr.expr -> bool
val is_uminus : Expr.expr -> bool
val is_mul : Expr.expr -> bool
val is_div : Expr.expr -> bool
val is_idiv : Expr.expr -> bool
val is_remainder : Expr.expr -> bool
val is_modulus : Expr.expr -> bool
val is_int2real : Expr.expr -> bool
val is_real2int : Expr.expr -> bool
val is_real_is_int : Expr.expr -> bool
val is_real : Expr.expr -> bool
val is_int_numeral : Expr.expr -> bool
val is_rat_numeral : Expr.expr -> bool
val is_algebraic_number : Expr.expr -> bool
val mk_add : context -> Expr.expr list -> Expr.expr
val mk_mul : context -> Expr.expr list -> Expr.expr
val mk_sub : context -> Expr.expr list -> Expr.expr
val mk_unary_minus : context -> Expr.expr -> Expr.expr
val mk_div : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_power : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_lt : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_le : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_gt : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_ge : context -> Expr.expr -> Expr.expr -> Expr.expr