Module `Flags.IVC`

Inductive Validity Cores

type minimize_mode = [ | `DO_NOT_MINIMIZE | `VALID_LUSTRE | `CONCISE ]
type ivc_element = [ | `NODE_CALL | `CONTRACT_ITEM | `EQUATION | `ASSERTION | `ANNOTATIONS ]

val compute_ivc : unit -> bool: Enable computation of Inductive Validity Cores

val ivc_all : unit -> bool
val ivc_category : unit -> ivc_element list: Specify on which elements we want to minimize

val print_ivc : unit -> bool: Print the model elements of the computed IVC

val print_ivc_compl : unit -> bool: Print the model elements NOT in the computed IVC

val ivc_approximate : unit -> bool: If true, compute an approximation of a MIVC

val ivc_must_set : unit -> bool: If true, compute the MUST set first and compute the IVCs starting from it

val ivc_smallest_first : unit -> bool: If true, compute a smallest IVC first

val ivc_only_main_node : unit -> bool: If true, compute IVC over elements of the main node only

val ivc_precomputed_mcs : unit -> int: Parameter k of the UMIVC algorithm. Correspond to the parameter 'k' of the implementation UMIVC. In particular, the value 0 implements the MARCO algorithm, and the value -1 (infinity) implements the CAMUS algorithm.

val ivc_per_property : unit -> bool: If true, IVCs will be computed for each properties separately

val minimize_program : unit -> minimize_mode: Generate a minimize lustre program

val minimized_program_dir : unit -> string: The directory where minimized programs should be saved

val ivc_uc_timeout : unit -> int: Timeout for unsat core computation