Module Flags.IC3

module IC3: sig .. end

IC3 flags

type qe = [ `Cooper | `Z3 | `Z3_impl | `Z3_impl2 ] 
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 = [ `IA | `None ] 
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.