package dolmen

  1. Overview
  2. Docs
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.