Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules 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 is_exists
 
def is_lambda
 
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
 
def __rmul__
 
def __mul__
 
- Public Member Functions inherited from ExprRef
def as_ast
 
def get_id
 
def sort
 
def sort_kind
 
def __eq__
 
def __hash__
 
def __ne__
 
def params
 
def decl
 
def num_args
 
def arg
 
def children
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__
 
def __deepcopy__
 
def __str__
 
def __repr__
 
def __eq__
 
def __hash__
 
def __nonzero__
 
def __bool__
 
def sexpr
 
def as_ast
 
def get_id
 
def ctx_ref
 
def eq
 
def translate
 
def __copy__
 
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 1803 of file z3py.py.

Member Function Documentation

def as_ast (   self)

Definition at line 1806 of file z3py.py.

1807  def as_ast(self):
1808  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 1914 of file z3py.py.

Referenced by QuantifierRef.children().

1915  def body(self):
1916  """Return the expression being quantified.
1917 
1918  >>> f = Function('f', IntSort(), IntSort())
1919  >>> x = Int('x')
1920  >>> q = ForAll(x, f(x) == 0)
1921  >>> q.body()
1922  f(Var(0)) == 0
1923  """
1924  return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx)
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
def ctx_ref
Definition: z3py.py:352
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 1969 of file z3py.py.

1970  def children(self):
1971  """Return a list containing a single element self.body()
1972 
1973  >>> f = Function('f', IntSort(), IntSort())
1974  >>> x = Int('x')
1975  >>> q = ForAll(x, f(x) == 0)
1976  >>> q.children()
1977  [f(Var(0)) == 0]
1978  """
1979  return [ self.body() ]
def get_id (   self)

Definition at line 1809 of file z3py.py.

1810  def get_id(self):
1811  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
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 as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
def is_exists (   self)
Return `True` if `self` is an existential quantifier.

>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0)
>>> q.is_exists()
False
>>> q = Exists(x, f(x) != 0)
>>> q.is_exists()
True

Definition at line 1832 of file z3py.py.

1833  def is_exists(self):
1834  """Return `True` if `self` is an existential quantifier.
1835 
1836  >>> f = Function('f', IntSort(), IntSort())
1837  >>> x = Int('x')
1838  >>> q = ForAll(x, f(x) == 0)
1839  >>> q.is_exists()
1840  False
1841  >>> q = Exists(x, f(x) != 0)
1842  >>> q.is_exists()
1843  True
1844  """
1845  return Z3_is_quantifier_exists(self.ctx_ref(), self.ast)
bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)
Determine if ast is an existential quantifier.
def ctx_ref
Definition: z3py.py:352
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 1818 of file z3py.py.

1819  def is_forall(self):
1820  """Return `True` if `self` is a universal quantifier.
1821 
1822  >>> f = Function('f', IntSort(), IntSort())
1823  >>> x = Int('x')
1824  >>> q = ForAll(x, f(x) == 0)
1825  >>> q.is_forall()
1826  True
1827  >>> q = Exists(x, f(x) != 0)
1828  >>> q.is_forall()
1829  False
1830  """
1831  return Z3_is_quantifier_forall(self.ctx_ref(), self.ast)
bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if an ast is a universal quantifier.
def ctx_ref
Definition: z3py.py:352
def is_lambda (   self)
Return `True` if `self` is a lambda expression.

>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = Lambda(x, f(x))
>>> q.is_lambda()
True
>>> q = Exists(x, f(x) != 0)
>>> q.is_lambda()
False

Definition at line 1846 of file z3py.py.

1847  def is_lambda(self):
1848  """Return `True` if `self` is a lambda expression.
1849 
1850  >>> f = Function('f', IntSort(), IntSort())
1851  >>> x = Int('x')
1852  >>> q = Lambda(x, f(x))
1853  >>> q.is_lambda()
1854  True
1855  >>> q = Exists(x, f(x) != 0)
1856  >>> q.is_lambda()
1857  False
1858  """
1859  return Z3_is_lambda(self.ctx_ref(), self.ast)
def ctx_ref
Definition: z3py.py:352
bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.
def no_pattern (   self,
  idx 
)
Return a no-pattern.

Definition at line 1908 of file z3py.py.

1909  def no_pattern(self, idx):
1910  """Return a no-pattern."""
1911  if z3_debug():
1912  _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
1913  return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th no_pattern.
def num_no_patterns
Definition: z3py.py:1904
def z3_debug
Definition: z3py.py:58
def ctx_ref
Definition: z3py.py:352
def num_no_patterns (   self)
Return the number of no-patterns.

Definition at line 1904 of file z3py.py.

Referenced by QuantifierRef.no_pattern().

1905  def num_no_patterns(self):
1906  """Return the number of no-patterns."""
1907  return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast)
def num_no_patterns
Definition: z3py.py:1904
unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a)
Return number of no_patterns used in quantifier.
def ctx_ref
Definition: z3py.py:352
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 1874 of file z3py.py.

1875  def num_patterns(self):
1876  """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
1877 
1878  >>> f = Function('f', IntSort(), IntSort())
1879  >>> g = Function('g', IntSort(), IntSort())
1880  >>> x = Int('x')
1881  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1882  >>> q.num_patterns()
1883  2
1884  """
1885  return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast))
unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a)
Return number of patterns used in quantifier.
def ctx_ref
Definition: z3py.py:352
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 1925 of file z3py.py.

1926  def num_vars(self):
1927  """Return the number of variables bounded by this quantifier.
1928 
1929  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1930  >>> x = Int('x')
1931  >>> y = Int('y')
1932  >>> q = ForAll([x, y], f(x, y) >= x)
1933  >>> q.num_vars()
1934  2
1935  """
1936  return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast))
unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a)
Return number of bound variables of quantifier.
def ctx_ref
Definition: z3py.py:352
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 1886 of file z3py.py.

1887  def pattern(self, idx):
1888  """Return a pattern (i.e., quantifier instantiation hints) in `self`.
1889 
1890  >>> f = Function('f', IntSort(), IntSort())
1891  >>> g = Function('g', IntSort(), IntSort())
1892  >>> x = Int('x')
1893  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1894  >>> q.num_patterns()
1895  2
1896  >>> q.pattern(0)
1897  f(Var(0))
1898  >>> q.pattern(1)
1899  g(Var(0))
1900  """
1901  if z3_debug():
1902  _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
1903  return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
Patterns.
Definition: z3py.py:1741
Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th pattern.
def z3_debug
Definition: z3py.py:58
def ctx_ref
Definition: z3py.py:352
def sort (   self)
Return the Boolean sort or sort of Lambda.

Definition at line 1812 of file z3py.py.

1813  def sort(self):
1814  """Return the Boolean sort or sort of Lambda."""
1815  if self.is_lambda():
1816  return _sort(self.ctx, self.as_ast())
1817  return BoolSort(self.ctx)
def BoolSort
Definition: z3py.py:1523
def as_ast
Definition: z3py.py:344
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 1937 of file z3py.py.

1938  def var_name(self, idx):
1939  """Return a string representing a name used when displaying the quantifier.
1940 
1941  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1942  >>> x = Int('x')
1943  >>> y = Int('y')
1944  >>> q = ForAll([x, y], f(x, y) >= x)
1945  >>> q.var_name(0)
1946  'x'
1947  >>> q.var_name(1)
1948  'y'
1949  """
1950  if z3_debug():
1951  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1952  return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx))
Z3_symbol Z3_API Z3_get_quantifier_bound_name(Z3_context c, Z3_ast a, unsigned i)
Return symbol of the i'th bound variable.
def z3_debug
Definition: z3py.py:58
def ctx_ref
Definition: z3py.py:352
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 1953 of file z3py.py.

1954  def var_sort(self, idx):
1955  """Return the sort of a bound variable.
1956 
1957  >>> f = Function('f', IntSort(), RealSort(), IntSort())
1958  >>> x = Int('x')
1959  >>> y = Real('y')
1960  >>> q = ForAll([x, y], f(x, y) >= x)
1961  >>> q.var_sort(0)
1962  Int
1963  >>> q.var_sort(1)
1964  Real
1965  """
1966  if z3_debug():
1967  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1968  return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
Z3_sort Z3_API Z3_get_quantifier_bound_sort(Z3_context c, Z3_ast a, unsigned i)
Return sort of the i'th bound variable.
def z3_debug
Definition: z3py.py:58
def ctx_ref
Definition: z3py.py:352
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 1860 of file z3py.py.

1861  def weight(self):
1862  """Return the weight annotation of `self`.
1863 
1864  >>> f = Function('f', IntSort(), IntSort())
1865  >>> x = Int('x')
1866  >>> q = ForAll(x, f(x) == 0)
1867  >>> q.weight()
1868  1
1869  >>> q = ForAll(x, f(x) == 0, weight=10)
1870  >>> q.weight()
1871  10
1872  """
1873  return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))
unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a)
Obtain weight of quantifier.
def ctx_ref
Definition: z3py.py:352