module type Term = sig .. end
type
The type of terms.
type
The type of identifiers for constants.
type
The type of locations.
val const : ?loc:location -> id -> t
Constants, i.e non predefined symbols. This includes both constants
defined by theories, defined locally in a problem, and also quantified variables.
val int : ?loc:location -> string -> t
val real : ?loc:location -> string -> t
val hexa : ?loc:location -> string -> t
val binary : ?loc:location -> string -> t
Constants lexically recognised as numbers in different formats. According to the smtlib
manual, these should not always be interpreted as numbers since their interpretation
is actually dependent on the theory set by the problem.
val colon : ?loc:location ->
t -> t -> t
Juxtaposition of terms, used to annotate terms with their type.
val apply : ?loc:location ->
t -> t list -> t
Application.
val letin : ?loc:location ->
t list -> t -> t
Local bindings. The bindings are a list of terms built using the colon function.
val forall : ?loc:location ->
t list -> t -> t
Universal quantification.
val exists : ?loc:location ->
t list -> t -> t
Existencial quantification.
val sexpr : ?loc:location -> t list -> t
S-expressions. Used in smtlib's annotations,
val annot : ?loc:location ->
t -> t list -> t
Attach a list of attributes (also called annotations) to a term. As written
in the smtlib manual, "Term attributes have no logical meaning --
semantically, attr t l is equivalent to t"