z3 4.11.2 · OCaml Package

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

package z3