Module Z3.QE

module QE: sig .. end

Quantifier elimination and model-based projection.

val qe_lite : context -> AST.ASTVector.ast_vector -> Expr.expr -> Expr.expr

val model_project : Model.model -> Expr.expr list -> Expr.expr -> Expr.expr

val model_project_skolem : Model.model ->
       Expr.expr list -> Expr.expr -> AST.ASTMap.ast_map -> Expr.expr

val model_project_with_witness : Model.model ->
       Expr.expr list -> Expr.expr -> AST.ASTMap.ast_map -> Expr.expr