Module InvGenMiner

module type CandGen = sig ... end

Module generating candidate terms for invariant generation.

module Bool : CandGen

Bool candidate term miner.

module Int : CandGen

Integer candidate term miner.

module BV (L : sig ... end) : CandGen

BV candidate term miner.

module UBV (L : sig ... end) : CandGen

UBV candidate term miner.

module Real : CandGen

Real candidate term miner.

val has_mineable_int_terms : TransSys.t -> bool

Is there anything for the integer candidate term miner to work on?

true when the system or one of its subsystems has a state variable, or a subterm of its init or transition predicate, of type int or integer range that is not a numeral. Enumerations do not count: they carry IA in the logic of the system, but the integer rules skip them.

val has_mineable_real_terms : TransSys.t -> bool

Is there anything for the real candidate term miner to work on?

As has_mineable_int_terms, for type real and decimals.