module Quantifier:sig
..end
type
quantifier =
| |
Quantifier of |
val expr_of_quantifier : quantifier -> Expr.expr
val quantifier_of_expr : Expr.expr -> quantifier
module Pattern:sig
..end
val get_index : Expr.expr -> int
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
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_quantifier : context ->
bool ->
Expr.expr list ->
Expr.expr ->
int option ->
Pattern.pattern list ->
Expr.expr list ->
Symbol.symbol option ->
Symbol.symbol option -> 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
val to_string : quantifier -> string