Module Flags.QE

QE flags

type qe_method = [
  1. | `Precise
  2. | `Impl
  3. | `Impl2
  4. | `Cooper
]

Methods available for quantifier elimination.

val qe_method : unit -> qe_method

The QE method used.

val set_qe_method : qe_method -> unit

Set qe_method.

type extract = [
  1. | `First
  2. | `Vars
]

Supported heuristics for extraction of implicants.

val extract : unit -> extract

Heuristic for extraction of implicants.

val ae_val_use_ctx : unit -> bool

Use context (premises) in ae_val procedure

val order_var_by_elim : unit -> bool

Order variables in polynomials by order of elimination *

val general_lbound : unit -> bool

Choose lower bounds containing variables *