Module `Flags.IC3`

IC3 flags

type qe = [ | `Z3 | `Z3_impl | `Z3_impl2 | `Cooper ]: Algorithm usable for quantifier elimination in IC3.

val qe : unit -> qe: The QE algorithm IC3 should use.

val set_qe : qe -> unit: Sets qe.

val check_inductive : unit -> bool: Check inductiveness of blocking clauses.

val print_to_file : unit -> string option: File for inductive blocking clauses.

val inductively_generalize : unit -> int: Tighten blocking clauses to an unsatisfiable core.

val block_in_future : unit -> bool: Block counterexample in future frames.

val block_in_future_first : unit -> bool: Block counterexample in future frames first before returning to frame.

val fwd_prop_non_gen : unit -> bool: Also propagate clauses before generalization.

val fwd_prop_ind_gen : unit -> bool: Inductively generalize all clauses after forward propagation.

val fwd_prop_subsume : unit -> bool: Subsumption in forward propagation.

val use_invgen : unit -> bool: Use invariants from invariant generators.

type abstr = [ | `None | `IA ]: Legal abstraction mechanisms for in IC3.

val abstr : unit -> abstr: Abstraction mechanism IC3 should use.

type extract = [ | `First | `Vars ]: Legal heuristics for extraction of implicants in IC3.

val extract : unit -> extract: Heuristic for extraction of implicants in IC3.