Module InvGenDomain.Bool

module Bool: Domain 
Boolean domain with implication.

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

Type of the values of the candidate terms.

type t 
Value formatter.
val fmt : Format.formatter -> t -> unit
Equality over values.
val eq : t -> t -> bool
Ordering relation.
val cmp : t -> t -> bool
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 ordering of two terms.
val mk_cmp : Term.t -> Term.t -> Term.t
Evaluates a term.
val eval : TransSys.t -> Model.t -> Term.t -> t
Mines a transition system for candidate terms.
val mine : bool ->
bool -> Analysis.param -> TransSys.t -> (TransSys.t * Term.TermSet.t) list
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
Returns true iff the input term is bottom.
val is_bot : Term.t -> bool
Returns true iff the input term is top.
val is_top : Term.t -> bool
Returns true iff the one state invgen technique for this domain is running.
val is_os_running : unit -> bool