Module Types.Term (.ml)

module Term: sig .. end

Module interface for terms

type t = Types.term

val compare : t -> t -> int

val equal : t -> t -> bool

val hash : t -> int

val subst : Variable.subst -> t -> t

Apply the substitution given in argument to the term

val htrue : Hstring.t

val hfalse : Hstring.t

val variables : t -> Variable.Set.t

returns the existential variables of the given term

val variables_proc : t -> Variable.Set.t

same as variables but only return skolemized variables of the form #i

val type_of : t -> Smt.Type.t

returns the type of the term as it is known by the SMT solver

val print : Format.formatter -> t -> unit

prints a term

module Set: Set.S  with type elt = t

set of terms