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

Member Function Documentation

◆ as_ast()

def as_ast (   self)

Definition at line 1795 of file z3py.py.

1795  def as_ast(self):
1796  return self.ast
1797 

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

Referenced by QuantifierRef.children().

1903  def body(self):
1904  """Return the expression being quantified.
1905 
1906  >>> f = Function('f', IntSort(), IntSort())
1907  >>> x = Int('x')
1908  >>> q = ForAll(x, f(x) == 0)
1909  >>> q.body()
1910  f(Var(0)) == 0
1911  """
1912  return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx)
1913 
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 1958 of file z3py.py.

1958  def children(self):
1959  """Return a list containing a single element self.body()
1960 
1961  >>> f = Function('f', IntSort(), IntSort())
1962  >>> x = Int('x')
1963  >>> q = ForAll(x, f(x) == 0)
1964  >>> q.children()
1965  [f(Var(0)) == 0]
1966  """
1967  return [ self.body() ]
1968 

◆ get_id()

def get_id (   self)

Definition at line 1798 of file z3py.py.

1798  def get_id(self):
1799  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
1800 
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 1821 of file z3py.py.

1821  def is_exists(self):
1822  """Return `True` if `self` is an existential quantifier.
1823 
1824  >>> f = Function('f', IntSort(), IntSort())
1825  >>> x = Int('x')
1826  >>> q = ForAll(x, f(x) == 0)
1827  >>> q.is_exists()
1828  False
1829  >>> q = Exists(x, f(x) != 0)
1830  >>> q.is_exists()
1831  True
1832  """
1833  return Z3_is_quantifier_exists(self.ctx_ref(), self.ast)
1834 
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 1807 of file z3py.py.

1807  def is_forall(self):
1808  """Return `True` if `self` is a universal quantifier.
1809 
1810  >>> f = Function('f', IntSort(), IntSort())
1811  >>> x = Int('x')
1812  >>> q = ForAll(x, f(x) == 0)
1813  >>> q.is_forall()
1814  True
1815  >>> q = Exists(x, f(x) != 0)
1816  >>> q.is_forall()
1817  False
1818  """
1819  return Z3_is_quantifier_forall(self.ctx_ref(), self.ast)
1820 
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 1835 of file z3py.py.

1835  def is_lambda(self):
1836  """Return `True` if `self` is a lambda expression.
1837 
1838  >>> f = Function('f', IntSort(), IntSort())
1839  >>> x = Int('x')
1840  >>> q = Lambda(x, f(x))
1841  >>> q.is_lambda()
1842  True
1843  >>> q = Exists(x, f(x) != 0)
1844  >>> q.is_lambda()
1845  False
1846  """
1847  return Z3_is_lambda(self.ctx_ref(), self.ast)
1848 
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 1897 of file z3py.py.

1897  def no_pattern(self, idx):
1898  """Return a no-pattern."""
1899  if __debug__:
1900  _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
1901  return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
1902 
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 1893 of file z3py.py.

1893  def num_no_patterns(self):
1894  """Return the number of no-patterns."""
1895  return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast)
1896 
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 1863 of file z3py.py.

1863  def num_patterns(self):
1864  """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
1865 
1866  >>> f = Function('f', IntSort(), IntSort())
1867  >>> g = Function('g', IntSort(), IntSort())
1868  >>> x = Int('x')
1869  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1870  >>> q.num_patterns()
1871  2
1872  """
1873  return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast))
1874 
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 1914 of file z3py.py.

1914  def num_vars(self):
1915  """Return the number of variables bounded by this quantifier.
1916 
1917  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1918  >>> x = Int('x')
1919  >>> y = Int('y')
1920  >>> q = ForAll([x, y], f(x, y) >= x)
1921  >>> q.num_vars()
1922  2
1923  """
1924  return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast))
1925 
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 1875 of file z3py.py.

1875  def pattern(self, idx):
1876  """Return a pattern (i.e., quantifier instantiation hints) in `self`.
1877 
1878  >>> f = Function('f', IntSort(), IntSort())
1879  >>> g = Function('g', IntSort(), IntSort())
1880  >>> x = Int('x')
1881  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1882  >>> q.num_patterns()
1883  2
1884  >>> q.pattern(0)
1885  f(Var(0))
1886  >>> q.pattern(1)
1887  g(Var(0))
1888  """
1889  if __debug__:
1890  _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
1891  return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
1892 
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 1801 of file z3py.py.

1801  def sort(self):
1802  """Return the Boolean sort or sort of Lambda."""
1803  if self.is_lambda():
1804  return _sort(self.ctx, self.as_ast())
1805  return BoolSort(self.ctx)
1806 
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 1926 of file z3py.py.

1926  def var_name(self, idx):
1927  """Return a string representing a name used when displaying the quantifier.
1928 
1929  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1930  >>> x = Int('x')
1931  >>> y = Int('y')
1932  >>> q = ForAll([x, y], f(x, y) >= x)
1933  >>> q.var_name(0)
1934  'x'
1935  >>> q.var_name(1)
1936  'y'
1937  """
1938  if __debug__:
1939  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1940  return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx))
1941 
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 1942 of file z3py.py.

1942  def var_sort(self, idx):
1943  """Return the sort of a bound variable.
1944 
1945  >>> f = Function('f', IntSort(), RealSort(), IntSort())
1946  >>> x = Int('x')
1947  >>> y = Real('y')
1948  >>> q = ForAll([x, y], f(x, y) >= x)
1949  >>> q.var_sort(0)
1950  Int
1951  >>> q.var_sort(1)
1952  Real
1953  """
1954  if __debug__:
1955  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1956  return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
1957 
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 1849 of file z3py.py.

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