Module Z3.Quantifier

module Quantifier: sig .. end
Quantifier expressions

type quantifier 
val expr_of_quantifier : quantifier -> Expr.expr
val quantifier_of_expr : Expr.expr -> quantifier
module Pattern: sig .. end
Quantifier patterns
val get_index : Expr.expr -> int
The de-Burijn index of a bound variable.

Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain the meaning of de-Bruijn indices by indicating the compilation process from non-de-Bruijn formulas to de-Bruijn format. abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0) abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi)) abs1(x, x, n) = b_n abs1(y, x, n) = y abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n)) abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1)) The last line is significant: the index of a bound variable is different depending on the scope in which it appears. The deeper ( x : expr ) appears, the higher is its index.

val is_universal : quantifier -> bool
Indicates whether the quantifier is universal.
val is_existential : quantifier -> bool
Indicates whether the quantifier is existential.
val get_weight : quantifier -> int
The weight of the quantifier.
val get_num_patterns : quantifier -> int
The number of patterns.
val get_patterns : quantifier -> Pattern.pattern list
The patterns.
val get_num_no_patterns : quantifier -> int
The number of no-patterns.
val get_no_patterns : quantifier -> Pattern.pattern list
The no-patterns.
val get_num_bound : quantifier -> int
The number of bound variables.
val get_bound_variable_names : quantifier -> Symbol.symbol list
The symbols for the bound variables.
val get_bound_variable_sorts : quantifier -> Sort.sort list
The sorts of the bound variables.
val get_body : quantifier -> Expr.expr
The body of the quantifier.
val mk_bound : context -> int -> Sort.sort -> Expr.expr
Creates a new bound variable.
val mk_pattern : context -> Expr.expr list -> Pattern.pattern
Create a quantifier 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
Create a universal 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
Create a universal 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
Create an existential 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
Create an existential Quantifier.
val mk_quantifier : context ->
bool ->
Expr.expr list ->
Expr.expr ->
int option ->
Pattern.pattern list ->
Expr.expr list ->
Symbol.symbol option ->
Symbol.symbol option -> quantifier
Create a Quantifier.
val mk_quantifier : context ->
bool ->
Expr.expr list ->
Expr.expr ->
int option ->
Pattern.pattern list ->
Expr.expr list ->
Symbol.symbol option ->
Symbol.symbol option -> quantifier
Create a Quantifier.
val to_string : quantifier -> string
A string representation of the quantifier.