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__ (self, ast, ctx=None)
 
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 1622 of file z3py.py.

Member Function Documentation

def as_ast (   self)

Definition at line 1625 of file z3py.py.

1625  def as_ast(self):
1626  return self.ast
1627 
def as_ast(self)
Definition: z3py.py:1625
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 1703 of file z3py.py.

Referenced by QuantifierRef.children().

1703  def body(self):
1704  """Return the expression being quantified.
1705 
1706  >>> f = Function('f', IntSort(), IntSort())
1707  >>> x = Int('x')
1708  >>> q = ForAll(x, f(x) == 0)
1709  >>> q.body()
1710  f(Var(0)) == 0
1711  """
1712  return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx)
1713 
def ctx_ref(self)
Definition: z3py.py:304
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
def body(self)
Definition: z3py.py:1703
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 1758 of file z3py.py.

1758  def children(self):
1759  """Return a list containing a single element self.body()
1760 
1761  >>> f = Function('f', IntSort(), IntSort())
1762  >>> x = Int('x')
1763  >>> q = ForAll(x, f(x) == 0)
1764  >>> q.children()
1765  [f(Var(0)) == 0]
1766  """
1767  return [ self.body() ]
1768 
def children(self)
Definition: z3py.py:1758
def body(self)
Definition: z3py.py:1703
def get_id (   self)

Definition at line 1628 of file z3py.py.

1628  def get_id(self):
1629  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
1630 
def get_id(self)
Definition: z3py.py:1628
def as_ast(self)
Definition: z3py.py:296
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.
def ctx_ref(self)
Definition: z3py.py:304
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 1635 of file z3py.py.

1635  def is_forall(self):
1636  """Return `True` if `self` is a universal quantifier.
1637 
1638  >>> f = Function('f', IntSort(), IntSort())
1639  >>> x = Int('x')
1640  >>> q = ForAll(x, f(x) == 0)
1641  >>> q.is_forall()
1642  True
1643  >>> q = Exists(x, f(x) != 0)
1644  >>> q.is_forall()
1645  False
1646  """
1647  return Z3_is_quantifier_forall(self.ctx_ref(), self.ast)
1648 
def is_forall(self)
Definition: z3py.py:1635
Z3_bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if quantifier is universal.
def ctx_ref(self)
Definition: z3py.py:304
def no_pattern (   self,
  idx 
)
Return a no-pattern.

Definition at line 1697 of file z3py.py.

1697  def no_pattern(self, idx):
1698  """Return a no-pattern."""
1699  if __debug__:
1700  _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
1701  return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
1702 
def num_no_patterns(self)
Definition: z3py.py:1693
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 ctx_ref(self)
Definition: z3py.py:304
def no_pattern(self, idx)
Definition: z3py.py:1697
def num_no_patterns (   self)
Return the number of no-patterns.

Definition at line 1693 of file z3py.py.

Referenced by QuantifierRef.no_pattern().

1693  def num_no_patterns(self):
1694  """Return the number of no-patterns."""
1695  return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast)
1696 
def num_no_patterns(self)
Definition: z3py.py:1693
def ctx_ref(self)
Definition: z3py.py:304
unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, 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 1663 of file z3py.py.

1663  def num_patterns(self):
1664  """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
1665 
1666  >>> f = Function('f', IntSort(), IntSort())
1667  >>> g = Function('g', IntSort(), IntSort())
1668  >>> x = Int('x')
1669  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1670  >>> q.num_patterns()
1671  2
1672  """
1673  return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast))
1674 
def num_patterns(self)
Definition: z3py.py:1663
unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a)
Return number of patterns used in quantifier.
def ctx_ref(self)
Definition: z3py.py:304
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 1714 of file z3py.py.

1714  def num_vars(self):
1715  """Return the number of variables bounded by this quantifier.
1716 
1717  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1718  >>> x = Int('x')
1719  >>> y = Int('y')
1720  >>> q = ForAll([x, y], f(x, y) >= x)
1721  >>> q.num_vars()
1722  2
1723  """
1724  return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast))
1725 
unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a)
Return number of bound variables of quantifier.
def ctx_ref(self)
Definition: z3py.py:304
def num_vars(self)
Definition: z3py.py:1714
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 1675 of file z3py.py.

1675  def pattern(self, idx):
1676  """Return a pattern (i.e., quantifier instantiation hints) in `self`.
1677 
1678  >>> f = Function('f', IntSort(), IntSort())
1679  >>> g = Function('g', IntSort(), IntSort())
1680  >>> x = Int('x')
1681  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1682  >>> q.num_patterns()
1683  2
1684  >>> q.pattern(0)
1685  f(Var(0))
1686  >>> q.pattern(1)
1687  g(Var(0))
1688  """
1689  if __debug__:
1690  _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
1691  return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
1692 
Patterns.
Definition: z3py.py:1555
def num_patterns(self)
Definition: z3py.py:1663
Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i&#39;th pattern.
def pattern(self, idx)
Definition: z3py.py:1675
def ctx_ref(self)
Definition: z3py.py:304
def sort (   self)
Return the Boolean sort.

Definition at line 1631 of file z3py.py.

1631  def sort(self):
1632  """Return the Boolean sort."""
1633  return BoolSort(self.ctx)
1634 
def sort(self)
Definition: z3py.py:1631
def BoolSort(ctx=None)
Definition: z3py.py:1346
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 1726 of file z3py.py.

1726  def var_name(self, idx):
1727  """Return a string representing a name used when displaying the quantifier.
1728 
1729  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1730  >>> x = Int('x')
1731  >>> y = Int('y')
1732  >>> q = ForAll([x, y], f(x, y) >= x)
1733  >>> q.var_name(0)
1734  'x'
1735  >>> q.var_name(1)
1736  'y'
1737  """
1738  if __debug__:
1739  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1740  return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx))
1741 
def var_name(self, idx)
Definition: z3py.py:1726
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 ctx_ref(self)
Definition: z3py.py:304
def num_vars(self)
Definition: z3py.py:1714
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 1742 of file z3py.py.

1742  def var_sort(self, idx):
1743  """Return the sort of a bound variable.
1744 
1745  >>> f = Function('f', IntSort(), RealSort(), IntSort())
1746  >>> x = Int('x')
1747  >>> y = Real('y')
1748  >>> q = ForAll([x, y], f(x, y) >= x)
1749  >>> q.var_sort(0)
1750  Int
1751  >>> q.var_sort(1)
1752  Real
1753  """
1754  if __debug__:
1755  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1756  return SortRef(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
1757 
def var_sort(self, idx)
Definition: z3py.py:1742
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 ctx_ref(self)
Definition: z3py.py:304
def num_vars(self)
Definition: z3py.py:1714
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 1649 of file z3py.py.

1649  def weight(self):
1650  """Return the weight annotation of `self`.
1651 
1652  >>> f = Function('f', IntSort(), IntSort())
1653  >>> x = Int('x')
1654  >>> q = ForAll(x, f(x) == 0)
1655  >>> q.weight()
1656  1
1657  >>> q = ForAll(x, f(x) == 0, weight=10)
1658  >>> q.weight()
1659  10
1660  """
1661  return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))
1662 
unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a)
Obtain weight of quantifier.
def ctx_ref(self)
Definition: z3py.py:304
def weight(self)
Definition: z3py.py:1649