Z3
Public Member Functions
QuantifierRef Class Reference

Quantifiers. More...

+ Inheritance diagram for QuantifierRef:

Public Member Functions

def as_ast (self)
 
def get_id (self)
 
def sort (self)
 
def is_forall (self)
 
def is_exists (self)
 
def is_lambda (self)
 
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)
 
- Public Member Functions inherited from BoolRef
def sort (self)
 
def __rmul__ (self, other)
 
def __mul__ (self, other)
 
- Public Member Functions inherited from ExprRef
def as_ast (self)
 
def get_id (self)
 
def sort (self)
 
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 children (self)
 
- Public Member Functions inherited from AstRef
def __init__ (self, ast, ctx=None)
 
def __del__ (self)
 
def __deepcopy__ (self, memo={})
 
def __str__ (self)
 
def __repr__ (self)
 
def __eq__ (self, other)
 
def __hash__ (self)
 
def __nonzero__ (self)
 
def __bool__ (self)
 
def sexpr (self)
 
def as_ast (self)
 
def get_id (self)
 
def ctx_ref (self)
 
def eq (self, other)
 
def translate (self, target)
 
def __copy__ (self)
 
def hash (self)
 
- Public Member Functions inherited from Z3PPObject
def use_pp (self)
 

Additional Inherited Members

- Data Fields inherited from AstRef
 ast
 
 ctx
 

Detailed Description

Quantifiers.

Universally and Existentially quantified formulas.

Definition at line 1786 of file z3py.py.

Member Function Documentation

◆ as_ast()

def as_ast (   self)

Definition at line 1789 of file z3py.py.

1789  def as_ast(self):
1790  return self.ast
1791 

◆ body()

def body (   self)
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 1897 of file z3py.py.

Referenced by QuantifierRef.children().

1897  def body(self):
1898  """Return the expression being quantified.
1899 
1900  >>> f = Function('f', IntSort(), IntSort())
1901  >>> x = Int('x')
1902  >>> q = ForAll(x, f(x) == 0)
1903  >>> q.body()
1904  f(Var(0)) == 0
1905  """
1906  return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx)
1907 
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.

◆ children()

def children (   self)
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]

Definition at line 1952 of file z3py.py.

1952  def children(self):
1953  """Return a list containing a single element self.body()
1954 
1955  >>> f = Function('f', IntSort(), IntSort())
1956  >>> x = Int('x')
1957  >>> q = ForAll(x, f(x) == 0)
1958  >>> q.children()
1959  [f(Var(0)) == 0]
1960  """
1961  return [ self.body() ]
1962 

◆ get_id()

def get_id (   self)

Definition at line 1792 of file z3py.py.

1792  def get_id(self):
1793  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
1794 
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. Thus, two ast nodes created by the same context and having the same children and same function symbols have the same identifiers. Ast nodes created in the same context, but having different children or different functions have different identifiers. Variables and quantifiers are also assigned different identifiers according to their structure.

◆ is_exists()

def is_exists (   self)
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 1815 of file z3py.py.

1815  def is_exists(self):
1816  """Return `True` if `self` is an existential quantifier.
1817 
1818  >>> f = Function('f', IntSort(), IntSort())
1819  >>> x = Int('x')
1820  >>> q = ForAll(x, f(x) == 0)
1821  >>> q.is_exists()
1822  False
1823  >>> q = Exists(x, f(x) != 0)
1824  >>> q.is_exists()
1825  True
1826  """
1827  return Z3_is_quantifier_exists(self.ctx_ref(), self.ast)
1828 
Z3_bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)
Determine if ast is an existential quantifier.

◆ is_forall()

def is_forall (   self)
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 1801 of file z3py.py.

1801  def is_forall(self):
1802  """Return `True` if `self` is a universal quantifier.
1803 
1804  >>> f = Function('f', IntSort(), IntSort())
1805  >>> x = Int('x')
1806  >>> q = ForAll(x, f(x) == 0)
1807  >>> q.is_forall()
1808  True
1809  >>> q = Exists(x, f(x) != 0)
1810  >>> q.is_forall()
1811  False
1812  """
1813  return Z3_is_quantifier_forall(self.ctx_ref(), self.ast)
1814 
Z3_bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if an ast is a universal quantifier.

◆ is_lambda()

def is_lambda (   self)
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 1829 of file z3py.py.

1829  def is_lambda(self):
1830  """Return `True` if `self` is a lambda expression.
1831 
1832  >>> f = Function('f', IntSort(), IntSort())
1833  >>> x = Int('x')
1834  >>> q = Lambda(x, f(x))
1835  >>> q.is_lambda()
1836  True
1837  >>> q = Exists(x, f(x) != 0)
1838  >>> q.is_lambda()
1839  False
1840  """
1841  return Z3_is_lambda(self.ctx_ref(), self.ast)
1842 
Z3_bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.

◆ no_pattern()

def no_pattern (   self,
  idx 
)
Return a no-pattern.

Definition at line 1891 of file z3py.py.

1891  def no_pattern(self, idx):
1892  """Return a no-pattern."""
1893  if __debug__:
1894  _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
1895  return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
1896 
Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i&#39;th no_pattern.

◆ num_no_patterns()

def num_no_patterns (   self)
Return the number of no-patterns.

Definition at line 1887 of file z3py.py.

1887  def num_no_patterns(self):
1888  """Return the number of no-patterns."""
1889  return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast)
1890 
unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a)
Return number of no_patterns used in quantifier.

◆ num_patterns()

def num_patterns (   self)
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 1857 of file z3py.py.

1857  def num_patterns(self):
1858  """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
1859 
1860  >>> f = Function('f', IntSort(), IntSort())
1861  >>> g = Function('g', IntSort(), IntSort())
1862  >>> x = Int('x')
1863  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1864  >>> q.num_patterns()
1865  2
1866  """
1867  return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast))
1868 
unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a)
Return number of patterns used in quantifier.

◆ num_vars()

def num_vars (   self)
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 1908 of file z3py.py.

1908  def num_vars(self):
1909  """Return the number of variables bounded by this quantifier.
1910 
1911  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1912  >>> x = Int('x')
1913  >>> y = Int('y')
1914  >>> q = ForAll([x, y], f(x, y) >= x)
1915  >>> q.num_vars()
1916  2
1917  """
1918  return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast))
1919 
unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a)
Return number of bound variables of quantifier.

◆ 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 1869 of file z3py.py.

1869  def pattern(self, idx):
1870  """Return a pattern (i.e., quantifier instantiation hints) in `self`.
1871 
1872  >>> f = Function('f', IntSort(), IntSort())
1873  >>> g = Function('g', IntSort(), IntSort())
1874  >>> x = Int('x')
1875  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1876  >>> q.num_patterns()
1877  2
1878  >>> q.pattern(0)
1879  f(Var(0))
1880  >>> q.pattern(1)
1881  g(Var(0))
1882  """
1883  if __debug__:
1884  _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
1885  return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
1886 
Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i&#39;th pattern.

◆ sort()

def sort (   self)
Return the Boolean sort or sort of Lambda.

Definition at line 1795 of file z3py.py.

1795  def sort(self):
1796  """Return the Boolean sort or sort of Lambda."""
1797  if self.is_lambda():
1798  return _sort(self.ctx, self.as_ast())
1799  return BoolSort(self.ctx)
1800 
def BoolSort(ctx=None)
Definition: z3py.py:1512

◆ 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 1920 of file z3py.py.

1920  def var_name(self, idx):
1921  """Return a string representing a name used when displaying the quantifier.
1922 
1923  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1924  >>> x = Int('x')
1925  >>> y = Int('y')
1926  >>> q = ForAll([x, y], f(x, y) >= x)
1927  >>> q.var_name(0)
1928  'x'
1929  >>> q.var_name(1)
1930  'y'
1931  """
1932  if __debug__:
1933  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1934  return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx))
1935 
Z3_symbol Z3_API Z3_get_quantifier_bound_name(Z3_context c, Z3_ast a, unsigned i)
Return symbol of the i&#39;th bound variable.

◆ 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 1936 of file z3py.py.

1936  def var_sort(self, idx):
1937  """Return the sort of a bound variable.
1938 
1939  >>> f = Function('f', IntSort(), RealSort(), IntSort())
1940  >>> x = Int('x')
1941  >>> y = Real('y')
1942  >>> q = ForAll([x, y], f(x, y) >= x)
1943  >>> q.var_sort(0)
1944  Int
1945  >>> q.var_sort(1)
1946  Real
1947  """
1948  if __debug__:
1949  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1950  return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
1951 
Z3_sort Z3_API Z3_get_quantifier_bound_sort(Z3_context c, Z3_ast a, unsigned i)
Return sort of the i&#39;th bound variable.

◆ weight()

def weight (   self)
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 1843 of file z3py.py.

1843  def weight(self):
1844  """Return the weight annotation of `self`.
1845 
1846  >>> f = Function('f', IntSort(), IntSort())
1847  >>> x = Int('x')
1848  >>> q = ForAll(x, f(x) == 0)
1849  >>> q.weight()
1850  1
1851  >>> q = ForAll(x, f(x) == 0, weight=10)
1852  >>> q.weight()
1853  10
1854  """
1855  return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))
1856 
unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a)
Obtain weight of quantifier.