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-Bruijn 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_lambda_const : context -> Expr.expr list -> Expr.expr -> quantifier

Create a lambda binding.

val mk_lambda : context ->
       (Symbol.symbol * Sort.sort) list ->
       Expr.expr -> quantifier

Create a lambda binding where bound variables are given by symbols and sorts

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

Create a 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

Create a Quantifier.

val to_string : quantifier -> string

A string representation of the quantifier.