Module CooperQE

Cooper quantifier elimination

author
Ruoyu Zhang
val pp_print_model : Stdlib.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