sig
  type quantifier
  val expr_of_quantifier : Z3.Quantifier.quantifier -> Z3.Expr.expr
  val quantifier_of_expr : Z3.Expr.expr -> Z3.Quantifier.quantifier
  module Pattern :
    sig
      type pattern
      val get_num_terms : Z3.Quantifier.Pattern.pattern -> int
      val get_terms : Z3.Quantifier.Pattern.pattern -> Z3.Expr.expr list
      val to_string : Z3.Quantifier.Pattern.pattern -> string
    end
  val get_index : Z3.Expr.expr -> int
  val is_universal : Z3.Quantifier.quantifier -> bool
  val is_existential : Z3.Quantifier.quantifier -> bool
  val get_weight : Z3.Quantifier.quantifier -> int
  val get_num_patterns : Z3.Quantifier.quantifier -> int
  val get_patterns :
    Z3.Quantifier.quantifier -> Z3.Quantifier.Pattern.pattern list
  val get_num_no_patterns : Z3.Quantifier.quantifier -> int
  val get_no_patterns :
    Z3.Quantifier.quantifier -> Z3.Quantifier.Pattern.pattern list
  val get_num_bound : Z3.Quantifier.quantifier -> int
  val get_bound_variable_names :
    Z3.Quantifier.quantifier -> Z3.Symbol.symbol list
  val get_bound_variable_sorts :
    Z3.Quantifier.quantifier -> Z3.Sort.sort list
  val get_body : Z3.Quantifier.quantifier -> Z3.Expr.expr
  val mk_bound : Z3.context -> int -> Z3.Sort.sort -> Z3.Expr.expr
  val mk_pattern :
    Z3.context -> Z3.Expr.expr list -> Z3.Quantifier.Pattern.pattern
  val mk_forall :
    Z3.context ->
    Z3.Sort.sort list ->
    Z3.Symbol.symbol list ->
    Z3.Expr.expr ->
    int option ->
    Z3.Quantifier.Pattern.pattern list ->
    Z3.Expr.expr list ->
    Z3.Symbol.symbol option ->
    Z3.Symbol.symbol option -> Z3.Quantifier.quantifier
  val mk_forall_const :
    Z3.context ->
    Z3.Expr.expr list ->
    Z3.Expr.expr ->
    int option ->
    Z3.Quantifier.Pattern.pattern list ->
    Z3.Expr.expr list ->
    Z3.Symbol.symbol option ->
    Z3.Symbol.symbol option -> Z3.Quantifier.quantifier
  val mk_exists :
    Z3.context ->
    Z3.Sort.sort list ->
    Z3.Symbol.symbol list ->
    Z3.Expr.expr ->
    int option ->
    Z3.Quantifier.Pattern.pattern list ->
    Z3.Expr.expr list ->
    Z3.Symbol.symbol option ->
    Z3.Symbol.symbol option -> Z3.Quantifier.quantifier
  val mk_exists_const :
    Z3.context ->
    Z3.Expr.expr list ->
    Z3.Expr.expr ->
    int option ->
    Z3.Quantifier.Pattern.pattern list ->
    Z3.Expr.expr list ->
    Z3.Symbol.symbol option ->
    Z3.Symbol.symbol option -> Z3.Quantifier.quantifier
  val mk_lambda_const :
    Z3.context ->
    Z3.Expr.expr list -> Z3.Expr.expr -> Z3.Quantifier.quantifier
  val mk_lambda :
    Z3.context ->
    (Z3.Symbol.symbol * Z3.Sort.sort) list ->
    Z3.Expr.expr -> Z3.Quantifier.quantifier
  val mk_quantifier :
    Z3.context ->
    bool ->
    Z3.Sort.sort list ->
    Z3.Symbol.symbol list ->
    Z3.Expr.expr ->
    int option ->
    Z3.Quantifier.Pattern.pattern list ->
    Z3.Expr.expr list ->
    Z3.Symbol.symbol option ->
    Z3.Symbol.symbol option -> Z3.Quantifier.quantifier
  val mk_quantifier_const :
    Z3.context ->
    bool ->
    Z3.Expr.expr list ->
    Z3.Expr.expr ->
    int option ->
    Z3.Quantifier.Pattern.pattern list ->
    Z3.Expr.expr list ->
    Z3.Symbol.symbol option ->
    Z3.Symbol.symbol option -> Z3.Quantifier.quantifier
  val to_string : Z3.Quantifier.quantifier -> string
end