package dolmen

You can search for identifiers within the package.

in-package search v0.2.0

A parser library for automated deduction

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (11)

Authors

G

Guillaume Bury <guillaume.bury@gmail.com>

Maintainers

G

Guillaume Bury <guillaume.bury@gmail.com>

Sources

dolmen-0.8.1.tbz

sha256=80fc33ae81817a79c6e6b2f6c01c4cfcc0af02bfe4d2d1b87cf70b84cdde3928

sha512=3a44a99bce871161bc70cf909c813e9e6c91c590873cbc163c69b2ec90ab5be65bf0bf45430bc8d00d85d75cf0af004b06b8f5f1c9d4d47c8a30ab9f28762c04

doc/dolmen_smtlib2_poly/Dolmen_smtlib2_poly/Make/argument-3-T/index.html

Parameter `Make.T`

type t

The type of terms.

val const : ?loc:L.t -> I.t -> t

Constants, i.e non predefined symbols. This includes both constants defined by theories, defined locally in a problem, and also quantified variables.

val str : ?loc:L.t -> 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

val int : ?loc:L.t -> string -> t

val real : ?loc:L.t -> string -> t

val hexa : ?loc:L.t -> string -> t

val binary : ?loc:L.t -> 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:L.t -> t -> t -> t

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

val apply : ?loc:L.t -> t -> t list -> t

Application.

val letand : ?loc:L.t -> t list -> t -> t

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

val par : ?loc:L.t -> t list -> t -> t

universal quantification by type variables.

val forall : ?loc:L.t -> t list -> t -> t

Universal quantification.

val exists : ?loc:L.t -> t list -> t -> t

Existencial quantification.

val match_ : ?loc:L.t -> 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.

val sexpr : ?loc:L.t -> t list -> t

S-expressions. Used in smtlib's annotations,

val annot : ?loc:L.t -> 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"