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

Member Function Documentation

§ as_ast()

def as_ast (   self)

Definition at line 1717 of file z3py.py.

1717  def as_ast(self):
1718  return self.ast
1719 

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

Referenced by QuantifierRef.children().

1795  def body(self):
1796  """Return the expression being quantified.
1797 
1798  >>> f = Function('f', IntSort(), IntSort())
1799  >>> x = Int('x')
1800  >>> q = ForAll(x, f(x) == 0)
1801  >>> q.body()
1802  f(Var(0)) == 0
1803  """
1804  return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx)
1805 
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 1850 of file z3py.py.

1850  def children(self):
1851  """Return a list containing a single element self.body()
1852 
1853  >>> f = Function('f', IntSort(), IntSort())
1854  >>> x = Int('x')
1855  >>> q = ForAll(x, f(x) == 0)
1856  >>> q.children()
1857  [f(Var(0)) == 0]
1858  """
1859  return [ self.body() ]
1860 

§ get_id()

def get_id (   self)

Definition at line 1720 of file z3py.py.

1720  def get_id(self):
1721  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
1722 
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 1727 of file z3py.py.

1727  def is_forall(self):
1728  """Return `True` if `self` is a universal quantifier.
1729 
1730  >>> f = Function('f', IntSort(), IntSort())
1731  >>> x = Int('x')
1732  >>> q = ForAll(x, f(x) == 0)
1733  >>> q.is_forall()
1734  True
1735  >>> q = Exists(x, f(x) != 0)
1736  >>> q.is_forall()
1737  False
1738  """
1739  return Z3_is_quantifier_forall(self.ctx_ref(), self.ast)
1740 
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 1789 of file z3py.py.

1789  def no_pattern(self, idx):
1790  """Return a no-pattern."""
1791  if __debug__:
1792  _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
1793  return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
1794 
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 1785 of file z3py.py.

1785  def num_no_patterns(self):
1786  """Return the number of no-patterns."""
1787  return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast)
1788 
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 1755 of file z3py.py.

1755  def num_patterns(self):
1756  """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
1757 
1758  >>> f = Function('f', IntSort(), IntSort())
1759  >>> g = Function('g', IntSort(), IntSort())
1760  >>> x = Int('x')
1761  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1762  >>> q.num_patterns()
1763  2
1764  """
1765  return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast))
1766 
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 1806 of file z3py.py.

1806  def num_vars(self):
1807  """Return the number of variables bounded by this quantifier.
1808 
1809  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1810  >>> x = Int('x')
1811  >>> y = Int('y')
1812  >>> q = ForAll([x, y], f(x, y) >= x)
1813  >>> q.num_vars()
1814  2
1815  """
1816  return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast))
1817 
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 1767 of file z3py.py.

1767  def pattern(self, idx):
1768  """Return a pattern (i.e., quantifier instantiation hints) in `self`.
1769 
1770  >>> f = Function('f', IntSort(), IntSort())
1771  >>> g = Function('g', IntSort(), IntSort())
1772  >>> x = Int('x')
1773  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1774  >>> q.num_patterns()
1775  2
1776  >>> q.pattern(0)
1777  f(Var(0))
1778  >>> q.pattern(1)
1779  g(Var(0))
1780  """
1781  if __debug__:
1782  _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
1783  return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
1784 
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 1723 of file z3py.py.

1723  def sort(self):
1724  """Return the Boolean sort."""
1725  return BoolSort(self.ctx)
1726 
def BoolSort(ctx=None)
Definition: z3py.py:1435

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

1818  def var_name(self, idx):
1819  """Return a string representing a name used when displaying the quantifier.
1820 
1821  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1822  >>> x = Int('x')
1823  >>> y = Int('y')
1824  >>> q = ForAll([x, y], f(x, y) >= x)
1825  >>> q.var_name(0)
1826  'x'
1827  >>> q.var_name(1)
1828  'y'
1829  """
1830  if __debug__:
1831  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1832  return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx))
1833 
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 1834 of file z3py.py.

1834  def var_sort(self, idx):
1835  """Return the sort of a bound variable.
1836 
1837  >>> f = Function('f', IntSort(), RealSort(), IntSort())
1838  >>> x = Int('x')
1839  >>> y = Real('y')
1840  >>> q = ForAll([x, y], f(x, y) >= x)
1841  >>> q.var_sort(0)
1842  Int
1843  >>> q.var_sort(1)
1844  Real
1845  """
1846  if __debug__:
1847  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1848  return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
1849 
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 1741 of file z3py.py.

1741  def weight(self):
1742  """Return the weight annotation of `self`.
1743 
1744  >>> f = Function('f', IntSort(), IntSort())
1745  >>> x = Int('x')
1746  >>> q = ForAll(x, f(x) == 0)
1747  >>> q.weight()
1748  1
1749  >>> q = ForAll(x, f(x) == 0, weight=10)
1750  >>> q.weight()
1751  10
1752  """
1753  return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))
1754 
unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a)
Obtain weight of quantifier.