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

Member Function Documentation

§ as_ast()

def as_ast (   self)

Definition at line 1731 of file z3py.py.

1731  def as_ast(self):
1732  return self.ast
1733 

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

Referenced by QuantifierRef.children().

1809  def body(self):
1810  """Return the expression being quantified.
1811 
1812  >>> f = Function('f', IntSort(), IntSort())
1813  >>> x = Int('x')
1814  >>> q = ForAll(x, f(x) == 0)
1815  >>> q.body()
1816  f(Var(0)) == 0
1817  """
1818  return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx)
1819 
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 1864 of file z3py.py.

1864  def children(self):
1865  """Return a list containing a single element self.body()
1866 
1867  >>> f = Function('f', IntSort(), IntSort())
1868  >>> x = Int('x')
1869  >>> q = ForAll(x, f(x) == 0)
1870  >>> q.children()
1871  [f(Var(0)) == 0]
1872  """
1873  return [ self.body() ]
1874 

§ get_id()

def get_id (   self)

Definition at line 1734 of file z3py.py.

1734  def get_id(self):
1735  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
1736 
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_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 1741 of file z3py.py.

1741  def is_forall(self):
1742  """Return `True` if `self` is a universal quantifier.
1743 
1744  >>> f = Function('f', IntSort(), IntSort())
1745  >>> x = Int('x')
1746  >>> q = ForAll(x, f(x) == 0)
1747  >>> q.is_forall()
1748  True
1749  >>> q = Exists(x, f(x) != 0)
1750  >>> q.is_forall()
1751  False
1752  """
1753  return Z3_is_quantifier_forall(self.ctx_ref(), self.ast)
1754 
Z3_bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if quantifier is universal.

§ no_pattern()

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

Definition at line 1803 of file z3py.py.

1803  def no_pattern(self, idx):
1804  """Return a no-pattern."""
1805  if __debug__:
1806  _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
1807  return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
1808 
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 1799 of file z3py.py.

1799  def num_no_patterns(self):
1800  """Return the number of no-patterns."""
1801  return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast)
1802 
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 1769 of file z3py.py.

1769  def num_patterns(self):
1770  """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
1771 
1772  >>> f = Function('f', IntSort(), IntSort())
1773  >>> g = Function('g', IntSort(), IntSort())
1774  >>> x = Int('x')
1775  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1776  >>> q.num_patterns()
1777  2
1778  """
1779  return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast))
1780 
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 1820 of file z3py.py.

1820  def num_vars(self):
1821  """Return the number of variables bounded by this quantifier.
1822 
1823  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1824  >>> x = Int('x')
1825  >>> y = Int('y')
1826  >>> q = ForAll([x, y], f(x, y) >= x)
1827  >>> q.num_vars()
1828  2
1829  """
1830  return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast))
1831 
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 1781 of file z3py.py.

1781  def pattern(self, idx):
1782  """Return a pattern (i.e., quantifier instantiation hints) in `self`.
1783 
1784  >>> f = Function('f', IntSort(), IntSort())
1785  >>> g = Function('g', IntSort(), IntSort())
1786  >>> x = Int('x')
1787  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1788  >>> q.num_patterns()
1789  2
1790  >>> q.pattern(0)
1791  f(Var(0))
1792  >>> q.pattern(1)
1793  g(Var(0))
1794  """
1795  if __debug__:
1796  _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
1797  return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
1798 
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.

Definition at line 1737 of file z3py.py.

1737  def sort(self):
1738  """Return the Boolean sort."""
1739  return BoolSort(self.ctx)
1740 
def BoolSort(ctx=None)
Definition: z3py.py:1449

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

1832  def var_name(self, idx):
1833  """Return a string representing a name used when displaying the quantifier.
1834 
1835  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1836  >>> x = Int('x')
1837  >>> y = Int('y')
1838  >>> q = ForAll([x, y], f(x, y) >= x)
1839  >>> q.var_name(0)
1840  'x'
1841  >>> q.var_name(1)
1842  'y'
1843  """
1844  if __debug__:
1845  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1846  return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx))
1847 
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 1848 of file z3py.py.

1848  def var_sort(self, idx):
1849  """Return the sort of a bound variable.
1850 
1851  >>> f = Function('f', IntSort(), RealSort(), IntSort())
1852  >>> x = Int('x')
1853  >>> y = Real('y')
1854  >>> q = ForAll([x, y], f(x, y) >= x)
1855  >>> q.var_sort(0)
1856  Int
1857  >>> q.var_sort(1)
1858  Real
1859  """
1860  if __debug__:
1861  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1862  return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
1863 
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 1755 of file z3py.py.

1755  def weight(self):
1756  """Return the weight annotation of `self`.
1757 
1758  >>> f = Function('f', IntSort(), IntSort())
1759  >>> x = Int('x')
1760  >>> q = ForAll(x, f(x) == 0)
1761  >>> q.weight()
1762  1
1763  >>> q = ForAll(x, f(x) == 0, weight=10)
1764  >>> q.weight()
1765  10
1766  """
1767  return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))
1768 
unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a)
Obtain weight of quantifier.