Module EqOnly.UBVInvGen

Graph of unsigned bitvectors.

Parameters

module IS : sig ... end

Signature

val main : Numeral.t option -> bool -> bool -> bool -> 'a InputSystem.t -> Analysis.param -> TransSys.t -> (TransSys.t * Term.TermSet.t * Term.TermSet.t) list

Runs the invariant generator.

main max_depth top_only modular two_state input_sys aparam sys:

  • max_depth: length of the invariant generation run
  • top_only: run on top level only
  • modular: triggers modular MINING
  • two_state: generate two-state invariants
  • the rest should be obvious.
val exit : 'a -> unit

Clean exit for the invariant generator.