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)
 
- 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 __ne__ (self, other)
 
def decl (self)
 
def num_args (self)
 
def arg (self, idx)
 
def children (self)
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__ (self)
 
def __str__ (self)
 
def __repr__ (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 1612 of file z3py.py.

Member Function Documentation

def as_ast (   self)

Definition at line 1615 of file z3py.py.

1615  def as_ast(self):
1616  return self.ast
1617 
def as_ast(self)
Definition: z3py.py:1615
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 1693 of file z3py.py.

Referenced by QuantifierRef.children().

1693  def body(self):
1694  """Return the expression being quantified.
1695 
1696  >>> f = Function('f', IntSort(), IntSort())
1697  >>> x = Int('x')
1698  >>> q = ForAll(x, f(x) == 0)
1699  >>> q.body()
1700  f(Var(0)) == 0
1701  """
1702  return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx)
1703 
Z3_ast Z3_API Z3_get_quantifier_body(__in Z3_context c, __in Z3_ast a)
Return body of quantifier.
def ctx_ref(self)
Definition: z3py.py:305
def body(self)
Definition: z3py.py:1693
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 1748 of file z3py.py.

1748  def children(self):
1749  """Return a list containing a single element self.body()
1750 
1751  >>> f = Function('f', IntSort(), IntSort())
1752  >>> x = Int('x')
1753  >>> q = ForAll(x, f(x) == 0)
1754  >>> q.children()
1755  [f(Var(0)) == 0]
1756  """
1757  return [ self.body() ]
1758 
def children(self)
Definition: z3py.py:1748
def body(self)
Definition: z3py.py:1693
def get_id (   self)

Definition at line 1618 of file z3py.py.

1618  def get_id(self):
1619  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
1620 
def get_id(self)
Definition: z3py.py:1618
def as_ast(self)
Definition: z3py.py:296
unsigned Z3_API Z3_get_ast_id(__in 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.
def ctx_ref(self)
Definition: z3py.py:305
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 1625 of file z3py.py.

1625  def is_forall(self):
1626  """Return `True` if `self` is a universal quantifier.
1627 
1628  >>> f = Function('f', IntSort(), IntSort())
1629  >>> x = Int('x')
1630  >>> q = ForAll(x, f(x) == 0)
1631  >>> q.is_forall()
1632  True
1633  >>> q = Exists(x, f(x) != 0)
1634  >>> q.is_forall()
1635  False
1636  """
1637  return Z3_is_quantifier_forall(self.ctx_ref(), self.ast)
1638 
def is_forall(self)
Definition: z3py.py:1625
def ctx_ref(self)
Definition: z3py.py:305
Z3_bool Z3_API Z3_is_quantifier_forall(__in Z3_context c, __in Z3_ast a)
Determine if quantifier is universal.
def no_pattern (   self,
  idx 
)
Return a no-pattern.

Definition at line 1687 of file z3py.py.

1687  def no_pattern(self, idx):
1688  """Return a no-pattern."""
1689  if __debug__:
1690  _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
1691  return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
1692 
Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(__in Z3_context c, __in Z3_ast a, unsigned i)
Return i'th no_pattern.
def num_no_patterns(self)
Definition: z3py.py:1683
def ctx_ref(self)
Definition: z3py.py:305
def no_pattern(self, idx)
Definition: z3py.py:1687
def num_no_patterns (   self)
Return the number of no-patterns.

Definition at line 1683 of file z3py.py.

Referenced by QuantifierRef.no_pattern().

1683  def num_no_patterns(self):
1684  """Return the number of no-patterns."""
1685  return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast)
1686 
def num_no_patterns(self)
Definition: z3py.py:1683
def ctx_ref(self)
Definition: z3py.py:305
unsigned Z3_API Z3_get_quantifier_num_no_patterns(__in Z3_context c, __in Z3_ast a)
Return number of no_patterns used in quantifier.
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 1653 of file z3py.py.

1653  def num_patterns(self):
1654  """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
1655 
1656  >>> f = Function('f', IntSort(), IntSort())
1657  >>> g = Function('g', IntSort(), IntSort())
1658  >>> x = Int('x')
1659  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1660  >>> q.num_patterns()
1661  2
1662  """
1663  return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast))
1664 
unsigned Z3_API Z3_get_quantifier_num_patterns(__in Z3_context c, __in Z3_ast a)
Return number of patterns used in quantifier.
def num_patterns(self)
Definition: z3py.py:1653
def ctx_ref(self)
Definition: z3py.py:305
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 1704 of file z3py.py.

1704  def num_vars(self):
1705  """Return the number of variables bounded by this quantifier.
1706 
1707  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1708  >>> x = Int('x')
1709  >>> y = Int('y')
1710  >>> q = ForAll([x, y], f(x, y) >= x)
1711  >>> q.num_vars()
1712  2
1713  """
1714  return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast))
1715 
def ctx_ref(self)
Definition: z3py.py:305
def num_vars(self)
Definition: z3py.py:1704
unsigned Z3_API Z3_get_quantifier_num_bound(__in Z3_context c, __in Z3_ast a)
Return number of bound variables of quantifier.
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 1665 of file z3py.py.

1665  def pattern(self, idx):
1666  """Return a pattern (i.e., quantifier instantiation hints) in `self`.
1667 
1668  >>> f = Function('f', IntSort(), IntSort())
1669  >>> g = Function('g', IntSort(), IntSort())
1670  >>> x = Int('x')
1671  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1672  >>> q.num_patterns()
1673  2
1674  >>> q.pattern(0)
1675  f(Var(0))
1676  >>> q.pattern(1)
1677  g(Var(0))
1678  """
1679  if __debug__:
1680  _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
1681  return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
1682 
Patterns.
Definition: z3py.py:1545
def num_patterns(self)
Definition: z3py.py:1653
Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(__in Z3_context c, __in Z3_ast a, unsigned i)
Return i'th pattern.
def pattern(self, idx)
Definition: z3py.py:1665
def ctx_ref(self)
Definition: z3py.py:305
def sort (   self)
Return the Boolean sort.

Definition at line 1621 of file z3py.py.

1621  def sort(self):
1622  """Return the Boolean sort."""
1623  return BoolSort(self.ctx)
1624 
def BoolSort
Definition: z3py.py:1336
def sort(self)
Definition: z3py.py:1621
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 1716 of file z3py.py.

1716  def var_name(self, idx):
1717  """Return a string representing a name used when displaying the quantifier.
1718 
1719  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1720  >>> x = Int('x')
1721  >>> y = Int('y')
1722  >>> q = ForAll([x, y], f(x, y) >= x)
1723  >>> q.var_name(0)
1724  'x'
1725  >>> q.var_name(1)
1726  'y'
1727  """
1728  if __debug__:
1729  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1730  return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx))
1731 
def var_name(self, idx)
Definition: z3py.py:1716
Z3_symbol Z3_API Z3_get_quantifier_bound_name(__in Z3_context c, __in Z3_ast a, unsigned i)
Return symbol of the i'th bound variable.
def ctx_ref(self)
Definition: z3py.py:305
def num_vars(self)
Definition: z3py.py:1704
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 1732 of file z3py.py.

1732  def var_sort(self, idx):
1733  """Return the sort of a bound variable.
1734 
1735  >>> f = Function('f', IntSort(), RealSort(), IntSort())
1736  >>> x = Int('x')
1737  >>> y = Real('y')
1738  >>> q = ForAll([x, y], f(x, y) >= x)
1739  >>> q.var_sort(0)
1740  Int
1741  >>> q.var_sort(1)
1742  Real
1743  """
1744  if __debug__:
1745  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1746  return SortRef(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
1747 
def var_sort(self, idx)
Definition: z3py.py:1732
def ctx_ref(self)
Definition: z3py.py:305
Z3_sort Z3_API Z3_get_quantifier_bound_sort(__in Z3_context c, __in Z3_ast a, unsigned i)
Return sort of the i'th bound variable.
def num_vars(self)
Definition: z3py.py:1704
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 1639 of file z3py.py.

1639  def weight(self):
1640  """Return the weight annotation of `self`.
1641 
1642  >>> f = Function('f', IntSort(), IntSort())
1643  >>> x = Int('x')
1644  >>> q = ForAll(x, f(x) == 0)
1645  >>> q.weight()
1646  1
1647  >>> q = ForAll(x, f(x) == 0, weight=10)
1648  >>> q.weight()
1649  10
1650  """
1651  return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))
1652 
unsigned Z3_API Z3_get_quantifier_weight(__in Z3_context c, __in Z3_ast a)
Obtain weight of quantifier.
def ctx_ref(self)
Definition: z3py.py:305
def weight(self)
Definition: z3py.py:1639