Module Flags.Invgen

module Invgen: sig .. end

Invgen flags



val prune_trivial : unit -> bool
InvGen will remove trivial invariants, i.e. invariants implied by the transition relation.
val set_max_depth : int option -> unit
Sets the max depth for invariant generation.

Gets the max depth for invariant generation.

val max_depth : unit -> int option
val max_succ : unit -> int
Number of unrollings invariant generation should perform between switching to a different systems.
val lift_candidates : unit -> bool
InvGen will lift candidate terms from subsystems. *
val top_only : unit -> bool
InvGen will generate invariants only for top level. *
val all_out : unit -> bool
Forces invgen to consider a huge number of candidates.
val mine_trans : unit -> bool
InvGen will look for candidate terms in the transition predicate.
val two_state : unit -> bool
InvGen will run in two state mode.
val bool_eq_only : unit -> bool
Forces bool invgen to look for equalities only.
val arith_eq_only : unit -> bool
Forces arith invgen to look for equalities only.
val renice : unit -> int
Renice invariant generation process.