InvGen (kind2dev@731decdf5fb1.InvGen)

val main_bool : 
  bool ->
  'a InputSystem.t ->
  Analysis.param ->
  TransSys.t ->
  unit

Temporary entry point for boolean invariant generation.

val main_int : bool -> 'a InputSystem.t -> Analysis.param -> TransSys.t -> unit

Temporary entry point for integer invariant generation.

val main_bv : 
  bool ->
  int ->
  'a InputSystem.t ->
  Analysis.param ->
  TransSys.t ->
  unit

Temporary entry point for bitvector invariant generation.

val main_ubv : 
  bool ->
  int ->
  'a InputSystem.t ->
  Analysis.param ->
  TransSys.t ->
  unit

Temporary entry point for unsigned bitvector invariant generation.

val main_real : 
  bool ->
  'a InputSystem.t ->
  Analysis.param ->
  TransSys.t ->
  unit

Temporary entry point for real invariant generation.

val exit : 'a -> unit

Temporary exit point for boolean invariant generation.

module type Out = sig ... end

Signature of the module returned by the Make invariant generation functor when given a module with signature In.

module BoolInvGen : Out

Boolean invariant generation module.

module IntInvGen : Out

Int invariant generation module.

module RealInvGen : Out

Real invariant generation module.

module EqOnly : sig ... end

Graph modules for equivalence-only invgen.