dolmen 0.7 · OCaml Package

type t

The type of terms.

val prop : ?loc:L.t -> unit -> t

val bool : ?loc:L.t -> unit -> t

val ty_unit : ?loc:L.t -> unit -> t

val ty_int : ?loc:L.t -> unit -> t

val ty_real : ?loc:L.t -> unit -> t

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

Builtin types.

val void : ?loc:L.t -> unit -> t

val true_ : ?loc:L.t -> unit -> t

val false_ : ?loc:L.t -> unit -> t

Builtin constants.

val not_ : ?loc:L.t -> t -> t

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

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

val xor : ?loc:L.t -> t -> t -> t

val imply : ?loc:L.t -> t -> t -> t

val equiv : ?loc:L.t -> t -> t -> t

Propositional builtins.

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

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

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

Numerical constant creation.

val uminus : ?loc:L.t -> t -> t

val add : ?loc:L.t -> t -> t -> t

val sub : ?loc:L.t -> t -> t -> t

val mult : ?loc:L.t -> t -> t -> t

val div : ?loc:L.t -> t -> t -> t

val mod_ : ?loc:L.t -> t -> t -> t

val int_pow : ?loc:L.t -> t -> t -> t

val real_pow : ?loc:L.t -> t -> t -> t

val lt : ?loc:L.t -> t -> t -> t

val leq : ?loc:L.t -> t -> t -> t

val gt : ?loc:L.t -> t -> t -> t

val geq : ?loc:L.t -> t -> t -> t

Arithmetic builtins.

val eq : ?loc:L.t -> t -> t -> t

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

Equality and disequality.

val array_get : ?loc:L.t -> t -> t -> t

val array_set : ?loc:L.t -> t -> t -> t -> t

Array primitives.

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

Bitvector litteral.

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

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

val bitv_concat : ?loc:L.t -> t -> t -> t

Bitvector concatenation.

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

val arrow : ?loc:L.t -> t -> t -> t

Create a function type.

val ite : ?loc:L.t -> t -> t -> t -> t

Conditional terms.

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

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

Universal and existential quantifications.

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

Let-binding.

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

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

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

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

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

Record access for the field given by the identifier.

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

Create a check agains the given adt constructor.

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

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

val check : ?loc:L.t -> t -> t

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

val cut : ?loc:L.t -> t -> t

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

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

Used in trigger creation.

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

Create a (multi) trigger.

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

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

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

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

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

Annotate a term with an id for tracking purposes.

package dolmen