Quantifiers.
Universally and Existentially quantified formulas.
Definition at line 1686 of file z3py.py.
Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
>>> f = Function('f', IntSort(), IntSort())
>>> g = Function('g', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
>>> q.num_patterns()
2
Definition at line 1727 of file z3py.py.
1727 def num_patterns(self):
1728 """Return the number of patterns (i.e., quantifier instantiation hints) in `self`. 1730 >>> f = Function('f', IntSort(), IntSort()) 1731 >>> g = Function('g', IntSort(), IntSort()) 1733 >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ]) 1734 >>> q.num_patterns() unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a)
Return number of patterns used in quantifier.
Return the number of variables bounded by this quantifier.
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> x = Int('x')
>>> y = Int('y')
>>> q = ForAll([x, y], f(x, y) >= x)
>>> q.num_vars()
2
Definition at line 1778 of file z3py.py.
1779 """Return the number of variables bounded by this quantifier. 1781 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 1784 >>> q = ForAll([x, y], f(x, y) >= x) unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a)
Return number of bound variables of quantifier.
def pattern |
( |
|
self, |
|
|
|
idx |
|
) |
| |
Return a pattern (i.e., quantifier instantiation hints) in `self`.
>>> f = Function('f', IntSort(), IntSort())
>>> g = Function('g', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
>>> q.num_patterns()
2
>>> q.pattern(0)
f(Var(0))
>>> q.pattern(1)
g(Var(0))
Definition at line 1739 of file z3py.py.
1739 def pattern(self, idx):
1740 """Return a pattern (i.e., quantifier instantiation hints) in `self`. 1742 >>> f = Function('f', IntSort(), IntSort()) 1743 >>> g = Function('g', IntSort(), IntSort()) 1745 >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ]) 1746 >>> q.num_patterns() 1754 _z3_assert(idx < self.num_patterns(),
"Invalid pattern idx")
Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th pattern.
def var_name |
( |
|
self, |
|
|
|
idx |
|
) |
| |
Return a string representing a name used when displaying the quantifier.
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> x = Int('x')
>>> y = Int('y')
>>> q = ForAll([x, y], f(x, y) >= x)
>>> q.var_name(0)
'x'
>>> q.var_name(1)
'y'
Definition at line 1790 of file z3py.py.
1790 def var_name(self, idx):
1791 """Return a string representing a name used when displaying the quantifier. 1793 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 1796 >>> q = ForAll([x, y], f(x, y) >= x) 1803 _z3_assert(idx < self.num_vars(),
"Invalid variable idx")
Z3_symbol Z3_API Z3_get_quantifier_bound_name(Z3_context c, Z3_ast a, unsigned i)
Return symbol of the i'th bound variable.
def var_sort |
( |
|
self, |
|
|
|
idx |
|
) |
| |
Return the sort of a bound variable.
>>> f = Function('f', IntSort(), RealSort(), IntSort())
>>> x = Int('x')
>>> y = Real('y')
>>> q = ForAll([x, y], f(x, y) >= x)
>>> q.var_sort(0)
Int
>>> q.var_sort(1)
Real
Definition at line 1806 of file z3py.py.
1806 def var_sort(self, idx):
1807 """Return the sort of a bound variable. 1809 >>> f = Function('f', IntSort(), RealSort(), IntSort()) 1812 >>> q = ForAll([x, y], f(x, y) >= x) 1819 _z3_assert(idx < self.num_vars(),
"Invalid variable idx")
Z3_sort Z3_API Z3_get_quantifier_bound_sort(Z3_context c, Z3_ast a, unsigned i)
Return sort of the i'th bound variable.