package dolmen

You can search for identifiers within the package.

in-package search v0.2.0

A parser library

Install

Dune Dependency

github.com Readme Edit opam file Versions (11)

Authors

G

Guillaume Bury

Maintainers

G

guillaume.bury@gmail.com

Sources

dolmen-0.4.1.tar.gz

md5=55a97ff61dd8398e38570272ae7e3964

sha512=83f71037eb568d5449ff2d968cb50a0b105c9712e0bd29497d1f95683698f394860a11d4dee2a2a41163504e395ef068c3974901fca11894d671684fe438fc51

doc/dolmen.smtlib/Dolmen_smtlib/module-type-Term/index.html

Module type `Dolmen_smtlib.Term`Source

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 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 letin : ?loc:location -> t list -> t -> t

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