Module CooperQE

module CooperQE: sig .. end

Cooper quantifier elimination
Author(s): Ruoyu Zhang

val pp_print_model : Format.formatter -> (Var.t * Term.t) list -> unit

Print a model

val eliminate : Model.t -> Var.t list -> Poly.cformula -> Poly.cformula

Eliminate quantifiers of a list of variables in a formula