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

Member Function Documentation

◆ as_ast()

def as_ast (   self)

Definition at line 1806 of file z3py.py.

1806  def as_ast(self):
1807  return self.ast
1808 

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

Referenced by QuantifierRef.children().

1914  def body(self):
1915  """Return the expression being quantified.
1916 
1917  >>> f = Function('f', IntSort(), IntSort())
1918  >>> x = Int('x')
1919  >>> q = ForAll(x, f(x) == 0)
1920  >>> q.body()
1921  f(Var(0)) == 0
1922  """
1923  return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx)
1924 
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 1969 of file z3py.py.

1969  def children(self):
1970  """Return a list containing a single element self.body()
1971 
1972  >>> f = Function('f', IntSort(), IntSort())
1973  >>> x = Int('x')
1974  >>> q = ForAll(x, f(x) == 0)
1975  >>> q.children()
1976  [f(Var(0)) == 0]
1977  """
1978  return [ self.body() ]
1979 

◆ get_id()

def get_id (   self)

Definition at line 1809 of file z3py.py.

1809  def get_id(self):
1810  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
1811 
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 1832 of file z3py.py.

1832  def is_exists(self):
1833  """Return `True` if `self` is an existential quantifier.
1834 
1835  >>> f = Function('f', IntSort(), IntSort())
1836  >>> x = Int('x')
1837  >>> q = ForAll(x, f(x) == 0)
1838  >>> q.is_exists()
1839  False
1840  >>> q = Exists(x, f(x) != 0)
1841  >>> q.is_exists()
1842  True
1843  """
1844  return Z3_is_quantifier_exists(self.ctx_ref(), self.ast)
1845 
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 1818 of file z3py.py.

1818  def is_forall(self):
1819  """Return `True` if `self` is a universal quantifier.
1820 
1821  >>> f = Function('f', IntSort(), IntSort())
1822  >>> x = Int('x')
1823  >>> q = ForAll(x, f(x) == 0)
1824  >>> q.is_forall()
1825  True
1826  >>> q = Exists(x, f(x) != 0)
1827  >>> q.is_forall()
1828  False
1829  """
1830  return Z3_is_quantifier_forall(self.ctx_ref(), self.ast)
1831 
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 1846 of file z3py.py.

1846  def is_lambda(self):
1847  """Return `True` if `self` is a lambda expression.
1848 
1849  >>> f = Function('f', IntSort(), IntSort())
1850  >>> x = Int('x')
1851  >>> q = Lambda(x, f(x))
1852  >>> q.is_lambda()
1853  True
1854  >>> q = Exists(x, f(x) != 0)
1855  >>> q.is_lambda()
1856  False
1857  """
1858  return Z3_is_lambda(self.ctx_ref(), self.ast)
1859 
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 1908 of file z3py.py.

1908  def no_pattern(self, idx):
1909  """Return a no-pattern."""
1910  if z3_debug():
1911  _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
1912  return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
1913 
Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i&#39;th no_pattern.
def z3_debug()
Definition: z3py.py:58

◆ num_no_patterns()

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

Definition at line 1904 of file z3py.py.

1904  def num_no_patterns(self):
1905  """Return the number of no-patterns."""
1906  return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast)
1907 
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 1874 of file z3py.py.

1874  def num_patterns(self):
1875  """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
1876 
1877  >>> f = Function('f', IntSort(), IntSort())
1878  >>> g = Function('g', IntSort(), IntSort())
1879  >>> x = Int('x')
1880  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1881  >>> q.num_patterns()
1882  2
1883  """
1884  return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast))
1885 
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 1925 of file z3py.py.

1925  def num_vars(self):
1926  """Return the number of variables bounded by this quantifier.
1927 
1928  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1929  >>> x = Int('x')
1930  >>> y = Int('y')
1931  >>> q = ForAll([x, y], f(x, y) >= x)
1932  >>> q.num_vars()
1933  2
1934  """
1935  return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast))
1936 
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 1886 of file z3py.py.

1886  def pattern(self, idx):
1887  """Return a pattern (i.e., quantifier instantiation hints) in `self`.
1888 
1889  >>> f = Function('f', IntSort(), IntSort())
1890  >>> g = Function('g', IntSort(), IntSort())
1891  >>> x = Int('x')
1892  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1893  >>> q.num_patterns()
1894  2
1895  >>> q.pattern(0)
1896  f(Var(0))
1897  >>> q.pattern(1)
1898  g(Var(0))
1899  """
1900  if z3_debug():
1901  _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
1902  return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
1903 
Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i&#39;th pattern.
def z3_debug()
Definition: z3py.py:58

◆ sort()

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

Definition at line 1812 of file z3py.py.

1812  def sort(self):
1813  """Return the Boolean sort or sort of Lambda."""
1814  if self.is_lambda():
1815  return _sort(self.ctx, self.as_ast())
1816  return BoolSort(self.ctx)
1817 
def BoolSort(ctx=None)
Definition: z3py.py:1523

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

1937  def var_name(self, idx):
1938  """Return a string representing a name used when displaying the quantifier.
1939 
1940  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1941  >>> x = Int('x')
1942  >>> y = Int('y')
1943  >>> q = ForAll([x, y], f(x, y) >= x)
1944  >>> q.var_name(0)
1945  'x'
1946  >>> q.var_name(1)
1947  'y'
1948  """
1949  if z3_debug():
1950  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1951  return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx))
1952 
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.
def z3_debug()
Definition: z3py.py:58

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

1953  def var_sort(self, idx):
1954  """Return the sort of a bound variable.
1955 
1956  >>> f = Function('f', IntSort(), RealSort(), IntSort())
1957  >>> x = Int('x')
1958  >>> y = Real('y')
1959  >>> q = ForAll([x, y], f(x, y) >= x)
1960  >>> q.var_sort(0)
1961  Int
1962  >>> q.var_sort(1)
1963  Real
1964  """
1965  if z3_debug():
1966  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1967  return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
1968 
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.
def z3_debug()
Definition: z3py.py:58

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

1860  def weight(self):
1861  """Return the weight annotation of `self`.
1862 
1863  >>> f = Function('f', IntSort(), IntSort())
1864  >>> x = Int('x')
1865  >>> q = ForAll(x, f(x) == 0)
1866  >>> q.weight()
1867  1
1868  >>> q = ForAll(x, f(x) == 0, weight=10)
1869  >>> q.weight()
1870  10
1871  """
1872  return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))
1873 
unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a)
Obtain weight of quantifier.