Quantifiers.
More...
|
def | as_ast (self) |
|
def | get_id (self) |
|
def | sort (self) |
|
def | is_forall (self) |
|
def | is_exists (self) |
|
def | is_lambda (self) |
|
def | __getitem__ (self, arg) |
|
def | weight (self) |
|
def | num_patterns (self) |
|
def | pattern (self, idx) |
|
def | num_no_patterns (self) |
|
def | no_pattern (self, idx) |
|
def | body (self) |
|
def | num_vars (self) |
|
def | var_name (self, idx) |
|
def | var_sort (self, idx) |
|
def | children (self) |
|
def | __rmul__ (self, other) |
|
def | __mul__ (self, other) |
|
def | sort_kind (self) |
|
def | __eq__ (self, other) |
|
def | __hash__ (self) |
|
def | __ne__ (self, other) |
|
def | params (self) |
|
def | decl (self) |
|
def | num_args (self) |
|
def | arg (self, idx) |
|
def | __init__ (self, ast, ctx=None) |
|
def | __del__ (self) |
|
def | __deepcopy__ (self, memo={}) |
|
def | __str__ (self) |
|
def | __repr__ (self) |
|
def | __nonzero__ (self) |
|
def | __bool__ (self) |
|
def | sexpr (self) |
|
def | ctx_ref (self) |
|
def | eq (self, other) |
|
def | translate (self, target) |
|
def | __copy__ (self) |
|
def | hash (self) |
|
def | use_pp (self) |
|
Quantifiers.
Universally and Existentially quantified formulas.
Definition at line 1811 of file z3py.py.
◆ __getitem__()
def __getitem__ |
( |
|
self, |
|
|
|
arg |
|
) |
| |
Return the Z3 expression `self[arg]`.
Definition at line 1868 of file z3py.py.
1868 def __getitem__(self, arg):
1869 """Return the Z3 expression `self[arg]`.
1872 _z3_assert(self.is_lambda(),
"quantifier should be a lambda expression")
1873 arg = self.sort().domain().cast(arg)
1874 return _to_expr_ref(
Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx)
◆ as_ast()
Return a pointer to the corresponding C Z3_ast object.
Reimplemented from ExprRef.
Definition at line 1814 of file z3py.py.
◆ body()
Return the expression being quantified.
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0)
>>> q.body()
f(Var(0)) == 0
Definition at line 1931 of file z3py.py.
1932 """Return the expression being quantified.
1934 >>> f = Function('f', IntSort(), IntSort())
1936 >>> q = ForAll(x, f(x) == 0)
Referenced by QuantifierRef.children().
◆ children()
Return a list containing a single element self.body()
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0)
>>> q.children()
[f(Var(0)) == 0]
Reimplemented from ExprRef.
Definition at line 1986 of file z3py.py.
1987 """Return a list containing a single element self.body()
1989 >>> f = Function('f', IntSort(), IntSort())
1991 >>> q = ForAll(x, f(x) == 0)
1995 return [ self.body() ]
◆ get_id()
Return unique identifier for object. It can be used for hash-tables and maps.
Reimplemented from ExprRef.
Definition at line 1817 of file z3py.py.
◆ is_exists()
Return `True` if `self` is an existential quantifier.
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0)
>>> q.is_exists()
False
>>> q = Exists(x, f(x) != 0)
>>> q.is_exists()
True
Definition at line 1840 of file z3py.py.
1840 def is_exists(self):
1841 """Return `True` if `self` is an existential quantifier.
1843 >>> f = Function('f', IntSort(), IntSort())
1845 >>> q = ForAll(x, f(x) == 0)
1848 >>> q = Exists(x, f(x) != 0)
◆ is_forall()
Return `True` if `self` is a universal quantifier.
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0)
>>> q.is_forall()
True
>>> q = Exists(x, f(x) != 0)
>>> q.is_forall()
False
Definition at line 1826 of file z3py.py.
1826 def is_forall(self):
1827 """Return `True` if `self` is a universal quantifier.
1829 >>> f = Function('f', IntSort(), IntSort())
1831 >>> q = ForAll(x, f(x) == 0)
1834 >>> q = Exists(x, f(x) != 0)
◆ is_lambda()
Return `True` if `self` is a lambda expression.
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = Lambda(x, f(x))
>>> q.is_lambda()
True
>>> q = Exists(x, f(x) != 0)
>>> q.is_lambda()
False
Definition at line 1854 of file z3py.py.
1854 def is_lambda(self):
1855 """Return `True` if `self` is a lambda expression.
1857 >>> f = Function('f', IntSort(), IntSort())
1859 >>> q = Lambda(x, f(x))
1862 >>> q = Exists(x, f(x) != 0)
Referenced by QuantifierRef.__getitem__(), and QuantifierRef.sort().
◆ no_pattern()
def no_pattern |
( |
|
self, |
|
|
|
idx |
|
) |
| |
Return a no-pattern.
Definition at line 1925 of file z3py.py.
1925 def no_pattern(self, idx):
1926 """Return a no-pattern."""
1928 _z3_assert(idx < self.num_no_patterns(),
"Invalid no-pattern idx")
◆ num_no_patterns()
def num_no_patterns |
( |
|
self | ) |
|
Return the number of no-patterns.
Definition at line 1921 of file z3py.py.
1921 def num_no_patterns(self):
1922 """Return the number of no-patterns."""
Referenced by QuantifierRef.no_pattern().
◆ num_patterns()
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 1891 of file z3py.py.
1891 def num_patterns(self):
1892 """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
1894 >>> f = Function('f', IntSort(), IntSort())
1895 >>> g = Function('g', IntSort(), IntSort())
1897 >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1898 >>> q.num_patterns()
Referenced by QuantifierRef.pattern().
◆ num_vars()
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 1942 of file z3py.py.
1943 """Return the number of variables bounded by this quantifier.
1945 >>> f = Function('f', IntSort(), IntSort(), IntSort())
1948 >>> q = ForAll([x, y], f(x, y) >= x)
Referenced by QuantifierRef.var_name(), and QuantifierRef.var_sort().
◆ pattern()
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 1903 of file z3py.py.
1903 def pattern(self, idx):
1904 """Return a pattern (i.e., quantifier instantiation hints) in `self`.
1906 >>> f = Function('f', IntSort(), IntSort())
1907 >>> g = Function('g', IntSort(), IntSort())
1909 >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1910 >>> q.num_patterns()
1918 _z3_assert(idx < self.num_patterns(),
"Invalid pattern idx")
◆ sort()
Return the Boolean sort or sort of Lambda.
Reimplemented from BoolRef.
Definition at line 1820 of file z3py.py.
1821 """Return the Boolean sort or sort of Lambda."""
1822 if self.is_lambda():
1823 return _sort(self.ctx, self.as_ast())
◆ var_name()
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 1954 of file z3py.py.
1954 def var_name(self, idx):
1955 """Return a string representing a name used when displaying the quantifier.
1957 >>> f = Function('f', IntSort(), IntSort(), IntSort())
1960 >>> q = ForAll([x, y], f(x, y) >= x)
1967 _z3_assert(idx < self.num_vars(),
"Invalid variable idx")
◆ var_sort()
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 1970 of file z3py.py.
1970 def var_sort(self, idx):
1971 """Return the sort of a bound variable.
1973 >>> f = Function('f', IntSort(), RealSort(), IntSort())
1976 >>> q = ForAll([x, y], f(x, y) >= x)
1983 _z3_assert(idx < self.num_vars(),
"Invalid variable idx")
◆ weight()
Return the weight annotation of `self`.
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0)
>>> q.weight()
1
>>> q = ForAll(x, f(x) == 0, weight=10)
>>> q.weight()
10
Definition at line 1877 of file z3py.py.
1878 """Return the weight annotation of `self`.
1880 >>> f = Function('f', IntSort(), IntSort())
1882 >>> q = ForAll(x, f(x) == 0)
1885 >>> q = ForAll(x, f(x) == 0, weight=10)
Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i)
Array read. The argument a is the array and i is the index of the array that gets read.
Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th pattern.
unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a)
Return number of no_patterns used in quantifier.
unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a)
Return number of patterns used in quantifier.
bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if an ast is a universal quantifier.
unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a)
Obtain weight of quantifier.
bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)
Determine if ast is an existential quantifier.
unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t)
Return a unique identifier for t. The identifier is unique up to structural equality....
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.
Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th no_pattern.
bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.
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.
unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a)
Return number of bound variables of quantifier.
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.