Domain (kind2dev@731decdf5fb1.InvGenGraph.Graph.Domain)

val name : string

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

type t

Type of the values of the candidate terms.

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

Value formatter.

val eq : t -> t -> bool

Equality over values.

val cmp : t -> t -> bool

Ordering relation.

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

Creates the term corresponding to the equality of two terms.

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

Creates the term corresponding to the ordering of two terms.

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

Evaluates a term.

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

Mines a transition system for candidate terms.

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.

val is_bot : Term.t -> bool

Returns true iff the input term is bottom.

val is_top : Term.t -> bool

Returns true iff the input term is top.

val is_os_running : unit -> bool

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