module Term: sig .. end
type
The type of terms
type
| |
Plus |
| |
Minus |
| |
Mult |
| |
Div |
| |
Modulo |
The type of operators
val make_int : Num.num -> t
make_int n creates an integer constant of value n.
val make_real : Num.num -> t
make_real n creates an real constant of value n.
val make_app : Smt.Symbol.t -> t list -> t
make_app f l creates the application of function symbol f to a list
of terms l.
val make_arith : operator -> t -> t -> t
make_arith op t1 t2 creates the term t1 <op> t2.
val make_ite : Smt.Formula.t -> t -> t -> t
make_ite f t1 t2 creates the term if f then t1 else t2.
val is_int : t -> bool
is_int x is true if the term x has type int
val is_real : t -> bool
is_real x is true if the term x has type real
val t_true : t
t_true is the boolean term true
val t_false : t
t_false is the boolean term false