Module type `InvGenDomain.Domain`

Signature of the modules describing an order relation over some values.

val name : string

Short string description of the values, used in the logging prefix.

Type of the values of the candidate terms.

type t

Type of the values of the candidate terms.

Value formatter.

val fmt : Stdlib.Format.formatter -> t -> unit

Value formatter.

Equality over values.

val eq : t -> t -> bool

Equality over values.

Ordering relation.

val cmp : t -> t -> bool

Ordering relation.

Creates the term corresponding to the equality of two terms.

val mk_eq : Term.t -> Term.t -> Term.t

Creates the term corresponding to the equality of two terms.

Creates the term corresponding to the ordering of two terms.

val mk_cmp : Term.t -> Term.t -> Term.t

Creates the term corresponding to the ordering of two terms.

Evaluates a term.

val eval : TransSys.t -> Model.t -> Term.t -> t

Evaluates a term.

Mines a transition system for candidate terms.

val mine : bool -> bool -> Analysis.param -> TransSys.t -> (TransSys.t * Term.TermSet.t) list

Mines a transition system for candidate terms.

Representative of the first equivalence class.

False for bool, a random term in the set for arith.

val first_rep_of : Term.TermSet.t -> Term.t * Term.TermSet.t

Representative of the first equivalence class.

False for bool, a random term in the set for arith.

Returns true iff the input term is bottom.

val is_bot : Term.t -> bool

Returns true iff the input term is bottom.

Returns true iff the input term is top.

val is_top : Term.t -> bool

Returns true iff the input term is top.

Returns true iff the one state invgen technique for this domain is running.

val is_os_running : unit -> bool: Returns true iff the one state invgen technique for this domain is running.