Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Public Member Functions
QuantifierRef Class Reference

Quantifiers. More...

+ Inheritance diagram for QuantifierRef:

Public Member Functions

def as_ast
 
def get_id
 
def sort
 
def is_forall
 
def weight
 
def num_patterns
 
def pattern
 
def num_no_patterns
 
def no_pattern
 
def body
 
def num_vars
 
def var_name
 
def var_sort
 
def children
 
- Public Member Functions inherited from BoolRef
def sort
 
- Public Member Functions inherited from ExprRef
def as_ast
 
def get_id
 
def sort
 
def sort_kind
 
def __eq__
 
def __ne__
 
def decl
 
def num_args
 
def arg
 
def children
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__
 
def __str__
 
def __repr__
 
def sexpr
 
def as_ast
 
def get_id
 
def ctx_ref
 
def eq
 
def translate
 
def hash
 
- Public Member Functions inherited from Z3PPObject
def use_pp
 

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 
1626  def as_ast(self):
1627  return self.ast
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 
1704  def body(self):
1705  """Return the expression being quantified.
1706 
1707  >>> f = Function('f', IntSort(), IntSort())
1708  >>> x = Int('x')
1709  >>> q = ForAll(x, f(x) == 0)
1710  >>> q.body()
1711  f(Var(0)) == 0
1712  """
1713  return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx)
Z3_get_quantifier_body
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
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 
1759  def children(self):
1760  """Return a list containing a single element self.body()
1761 
1762  >>> f = Function('f', IntSort(), IntSort())
1763  >>> x = Int('x')
1764  >>> q = ForAll(x, f(x) == 0)
1765  >>> q.children()
1766  [f(Var(0)) == 0]
1767  """
1768  return [ self.body() ]
def get_id (   self)

Definition at line 1628 of file z3py.py.

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

Definition at line 1697 of file z3py.py.

1697 
1698  def no_pattern(self, idx):
1699  """Return a no-pattern."""
1700  if __debug__:
1701  _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
1702  return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
Z3_get_quantifier_no_pattern_ast
Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i&#39;th no_pattern.
z3py.QuantifierRef.num_no_patterns
def num_no_patterns
Definition: z3py.py:1693
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
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 
1694  def num_no_patterns(self):
1695  """Return the number of no-patterns."""
1696  return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast)
z3py.QuantifierRef.num_no_patterns
def num_no_patterns
Definition: z3py.py:1693
Z3_get_quantifier_num_no_patterns
unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a)
Return number of no_patterns used in quantifier.
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
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 
1664  def num_patterns(self):
1665  """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
1666 
1667  >>> f = Function('f', IntSort(), IntSort())
1668  >>> g = Function('g', IntSort(), IntSort())
1669  >>> x = Int('x')
1670  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1671  >>> q.num_patterns()
1672  2
1673  """
1674  return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast))
Z3_get_quantifier_num_patterns
unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a)
Return number of patterns used in quantifier.
z3py.AstRef.ctx_ref
def ctx_ref
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 
1715  def num_vars(self):
1716  """Return the number of variables bounded by this quantifier.
1717 
1718  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1719  >>> x = Int('x')
1720  >>> y = Int('y')
1721  >>> q = ForAll([x, y], f(x, y) >= x)
1722  >>> q.num_vars()
1723  2
1724  """
1725  return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast))
Z3_get_quantifier_num_bound
unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a)
Return number of bound variables of quantifier.
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
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 
1676  def pattern(self, idx):
1677  """Return a pattern (i.e., quantifier instantiation hints) in `self`.
1678 
1679  >>> f = Function('f', IntSort(), IntSort())
1680  >>> g = Function('g', IntSort(), IntSort())
1681  >>> x = Int('x')
1682  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1683  >>> q.num_patterns()
1684  2
1685  >>> q.pattern(0)
1686  f(Var(0))
1687  >>> q.pattern(1)
1688  g(Var(0))
1689  """
1690  if __debug__:
1691  _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
1692  return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
z3py.PatternRef
Patterns.
Definition: z3py.py:1555
Z3_get_quantifier_pattern_ast
Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i&#39;th pattern.
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
def sort (   self) 
Return the Boolean sort.

Definition at line 1631 of file z3py.py.

1631 
1632  def sort(self):
1633  """Return the Boolean sort."""
1634  return BoolSort(self.ctx)
z3py.BoolSort
def BoolSort
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 
1727  def var_name(self, idx):
1728  """Return a string representing a name used when displaying the quantifier.
1729 
1730  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1731  >>> x = Int('x')
1732  >>> y = Int('y')
1733  >>> q = ForAll([x, y], f(x, y) >= x)
1734  >>> q.var_name(0)
1735  'x'
1736  >>> q.var_name(1)
1737  'y'
1738  """
1739  if __debug__:
1740  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1741  return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx))
Z3_get_quantifier_bound_name
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.
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
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 
1743  def var_sort(self, idx):
1744  """Return the sort of a bound variable.
1745 
1746  >>> f = Function('f', IntSort(), RealSort(), IntSort())
1747  >>> x = Int('x')
1748  >>> y = Real('y')
1749  >>> q = ForAll([x, y], f(x, y) >= x)
1750  >>> q.var_sort(0)
1751  Int
1752  >>> q.var_sort(1)
1753  Real
1754  """
1755  if __debug__:
1756  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1757  return SortRef(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
Z3_get_quantifier_bound_sort
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.
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
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 
1650  def weight(self):
1651  """Return the weight annotation of `self`.
1652 
1653  >>> f = Function('f', IntSort(), IntSort())
1654  >>> x = Int('x')
1655  >>> q = ForAll(x, f(x) == 0)
1656  >>> q.weight()
1657  1
1658  >>> q = ForAll(x, f(x) == 0, weight=10)
1659  >>> q.weight()
1660  10
1661  """
1662  return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))
Z3_get_quantifier_weight
unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a)
Obtain weight of quantifier.
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
Generated on Fri Apr 12 2019 11:38:53 for Z3 by   doxygen 1.8.5