package dolmen

  1. Overview
  2. Docs
package dolmen
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module type Dolmen_smtlib2_v6_script.TermSource

Sourcetype t

The type of terms.

Sourcetype id

The type of identifiers for constants.

Sourcetype location

The type of locations.

Sourceval 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.

Sourceval str : ?loc:location -> string -> t

Quoted strings. According to the smtlib manual, these can be interpreted as either string literals (when the String theory is used), or simply constants

Sourceval int : ?loc:location -> string -> t
Sourceval real : ?loc:location -> string -> t
Sourceval hexa : ?loc:location -> string -> t
Sourceval 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.

Sourceval colon : ?loc:location -> t -> t -> t

Juxtaposition of terms, used to annotate terms with their type.

Sourceval apply : ?loc:location -> t -> t list -> t

Application.

Sourceval letand : ?loc:location -> t list -> t -> t

Local parrallel bindings. The bindings are a list of terms built using the colon function.

Sourceval forall : ?loc:location -> t list -> t -> t

Universal quantification.

Sourceval exists : ?loc:location -> t list -> t -> t

Existencial quantification.

Sourceval match_ : ?loc:location -> t -> (t * t) list -> t

Pattern matching. The first term is the term to match, and each tuple in the list is a match case, which is a pair of a pattern and a match branch.

Sourceval sexpr : ?loc:location -> t list -> t

S-expressions. Used in smtlib's annotations,

Sourceval 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"