Module Z3.Arithmetic

module Arithmetic: sig .. end

Functions to manipulate arithmetic expressions

module Integer: sig .. end

Integer Arithmetic

module Real: sig .. end

Real Arithmetic

val is_int : Expr.expr -> bool

Indicates whether the term is of integer sort.

val is_arithmetic_numeral : Expr.expr -> bool

Indicates whether the term is an arithmetic numeral.

val is_le : Expr.expr -> bool

Indicates whether the term is a less-than-or-equal

val is_ge : Expr.expr -> bool

Indicates whether the term is a greater-than-or-equal

val is_lt : Expr.expr -> bool

Indicates whether the term is a less-than

val is_gt : Expr.expr -> bool

Indicates whether the term is a greater-than

val is_add : Expr.expr -> bool

Indicates whether the term is addition (binary)

val is_sub : Expr.expr -> bool

Indicates whether the term is subtraction (binary)

val is_uminus : Expr.expr -> bool

Indicates whether the term is a unary minus

val is_mul : Expr.expr -> bool

Indicates whether the term is multiplication (binary)

val is_div : Expr.expr -> bool

Indicates whether the term is division (binary)

val is_idiv : Expr.expr -> bool

Indicates whether the term is integer division (binary)

val is_remainder : Expr.expr -> bool

Indicates whether the term is remainder (binary)

val is_modulus : Expr.expr -> bool

Indicates whether the term is modulus (binary)

val is_int2real : Expr.expr -> bool

Indicates whether the term is a coercion of integer to real (unary)

val is_real2int : Expr.expr -> bool

Indicates whether the term is a coercion of real to integer (unary)

val is_real_is_int : Expr.expr -> bool

Indicates whether the term is a check that tests whether a real is integral (unary)

val is_real : Expr.expr -> bool

Indicates whether the term is of sort real.

val is_int_numeral : Expr.expr -> bool

Indicates whether the term is an integer numeral.

val is_rat_numeral : Expr.expr -> bool

Indicates whether the term is a real numeral.

val is_algebraic_number : Expr.expr -> bool

Indicates whether the term is an algebraic number

val mk_add : context -> Expr.expr list -> Expr.expr

Create an expression representing t[0] + t[1] + ....

val mk_mul : context -> Expr.expr list -> Expr.expr

Create an expression representing t[0] * t[1] * ....

val mk_sub : context -> Expr.expr list -> Expr.expr

Create an expression representing t[0] - t[1] - ....

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

Create an expression representing -t.

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

Create an expression representing t1 / t2.

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

Create an expression representing t1 ^ t2.

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

Create an expression representing t1 < t2

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

Create an expression representing t1 <= t2

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

Create an expression representing t1 > t2

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

Create an expression representing t1 >= t2