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