package dolmen

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

Module type Dolmen_ae.TermSource

Sourcetype t

The type of terms.

Sourcetype id

The type of identifiers

Sourcetype location

The type of locations attached to terms.

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

Builtin types.

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

Builtin constants.

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

Propositional builtins.

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

Numerical constant creation.

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

Arithmetic builtins.

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

Equality and disequality.

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

Array primitives.

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

Bitvector litteral.

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

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

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

Bitvector concatenation.

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

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

Create a function type.

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

Conditional terms.

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

Universal and existential quantifications.

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

Let-binding.

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

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

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

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

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

Record access for the field given by the identifier.

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

Create a check agains the given adt constructor.

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

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

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

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

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

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

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

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

Used in trigger creation.

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

Create a (multi) trigger.

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

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

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

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

Sourceval 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