package dolmen

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

The type of terms.

type id

The type of identifiers

type location

The type of locations attached to terms.

val prop : ?loc:location -> unit -> t
val bool : ?loc:location -> unit -> t
val ty_unit : ?loc:location -> unit -> t
val ty_int : ?loc:location -> unit -> t
val ty_real : ?loc:location -> unit -> t
val ty_bitv : ?loc:location -> int -> t

Builtin types.

val void : ?loc:location -> unit -> t
val true_ : ?loc:location -> unit -> t
val false_ : ?loc:location -> unit -> t

Builtin constants.

val not_ : ?loc:location -> t -> t
val and_ : ?loc:location -> t list -> t
val or_ : ?loc:location -> t list -> t
val xor : ?loc:location -> t -> t -> t
val imply : ?loc:location -> t -> t -> t
val equiv : ?loc:location -> t -> t -> t

Propositional builtins.

val int : ?loc:location -> string -> t
val real : ?loc:location -> string -> t
val hexa : ?loc:location -> string -> t

Numerical constant creation.

val uminus : ?loc:location -> t -> t
val add : ?loc:location -> t -> t -> t
val sub : ?loc:location -> t -> t -> t
val mult : ?loc:location -> t -> t -> t
val div : ?loc:location -> t -> t -> t
val mod_ : ?loc:location -> t -> t -> t
val int_pow : ?loc:location -> t -> t -> t
val real_pow : ?loc:location -> t -> t -> t
val lt : ?loc:location -> t -> t -> t
val leq : ?loc:location -> t -> t -> t
val gt : ?loc:location -> t -> t -> t
val geq : ?loc:location -> t -> t -> t

Arithmetic builtins.

val eq : ?loc:location -> t -> t -> t
val neq : ?loc:location -> t list -> t

Equality and disequality.

val array_get : ?loc:location -> t -> t -> t
val array_set : ?loc:location -> t -> t -> t -> t

Array primitives.

val bitv : ?loc:location -> string -> t

Bitvector litteral.

val bitv_extract : ?loc:location -> t -> int -> int -> t

Bitvoector extraction. TODO: document meaning of the itnegers indexes.

val bitv_concat : ?loc:location -> t -> t -> t

Bitvector concatenation.

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 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 of terms (as well as types).

val arrow : ?loc:location -> t -> t -> t

Create a function type.

val ite : ?loc:location -> t -> t -> t -> t

Conditional terms.

val forall : ?loc:location -> t list -> t -> t
val exists : ?loc:location -> t list -> t -> t

Universal and existential quantifications.

val letin : ?loc:location -> t list -> t -> t

Let-binding.

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

val record : ?loc:location -> t list -> t

Create a record expression, with a list of equalities of the form "label = expr".

val record_with : ?loc:location -> t -> t list -> t

Record update, of the form "s with label = expr, ...".

val record_access : ?loc:location -> t -> id -> t

Record access for the field given by the identifier.

val adt_check : ?loc:location -> t -> id -> t

Create a check agains the given adt constructor.

val adt_project : ?loc:location -> t -> id -> t

Create a projection for the given field of an adt constructor.

val check : ?loc:location -> t -> t

Create a term to "check" a formula. TODO: ask @iguernlala about this.

val cut : ?loc:location -> t -> t

Create a cut. TODO: ask @iguernlala about this.

val in_interval : ?loc:location -> t -> (t * bool) -> (t * bool) -> t

Create a trigger for the given term/variable being inside of a given interval, which is given as a lower bound, and an upper bound. Each bound contains an expression for the bound value, as well as a boolean indicating whether the bound is strict or not.

val maps_to : ?loc:location -> id -> t -> t

Used in trigger creation.

val trigger : ?loc:location -> t list -> t

Create a (multi) trigger.

val triggers : ?loc:location -> t -> t list -> t

Annotate a term (generally a quantified formula), with a list of triggers.

val filters : ?loc:location -> t -> t list -> t

Annotate a term (genrally a quantified formula) with a list of filters.

val tracked : ?loc:location -> id -> t -> t

Annotate a term with an id for tracking purposes.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct