Module Smt_sig.S.Term

module Term: sig .. end

type t

The type of terms

type operator =

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_sig.S.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 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