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 is_exists (self)
 
def is_lambda (self)
 
def __getitem__ (self, arg)
 
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)
 
def from_string (self, s)
 
def serialize (self)
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__ (self)
 
def __deepcopy__
 
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 __copy__ (self)
 
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 1984 of file z3py.py.

Member Function Documentation

def __getitem__ (   self,
  arg 
)
Return the Z3 expression `self[arg]`.

Definition at line 2041 of file z3py.py.

2041  def __getitem__(self, arg):
2042  """Return the Z3 expression `self[arg]`.
2043  """
2044  if z3_debug():
2045  _z3_assert(self.is_lambda(), "quantifier should be a lambda expression")
2046  return _array_select(self, arg)
2047 
def is_lambda(self)
Definition: z3py.py:2027
def __getitem__(self, arg)
Definition: z3py.py:2041
def z3_debug()
Definition: z3py.py:62
def as_ast (   self)

Definition at line 1987 of file z3py.py.

1987  def as_ast(self):
1988  return self.ast
1989 
def as_ast(self)
Definition: z3py.py:1987
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 2102 of file z3py.py.

Referenced by QuantifierRef.children().

2102  def body(self):
2103  """Return the expression being quantified.
2104 
2105  >>> f = Function('f', IntSort(), IntSort())
2106  >>> x = Int('x')
2107  >>> q = ForAll(x, f(x) == 0)
2108  >>> q.body()
2109  f(Var(0)) == 0
2110  """
2111  return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx)
2112 
def ctx_ref(self)
Definition: z3py.py:400
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
def body(self)
Definition: z3py.py:2102
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 2157 of file z3py.py.

2157  def children(self):
2158  """Return a list containing a single element self.body()
2159 
2160  >>> f = Function('f', IntSort(), IntSort())
2161  >>> x = Int('x')
2162  >>> q = ForAll(x, f(x) == 0)
2163  >>> q.children()
2164  [f(Var(0)) == 0]
2165  """
2166  return [self.body()]
2167 
2168 
def children(self)
Definition: z3py.py:2157
def body(self)
Definition: z3py.py:2102
def get_id (   self)

Definition at line 1990 of file z3py.py.

1990  def get_id(self):
1991  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
1992 
def get_id(self)
Definition: z3py.py:1990
def as_ast(self)
Definition: z3py.py:392
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:400
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 2013 of file z3py.py.

2013  def is_exists(self):
2014  """Return `True` if `self` is an existential quantifier.
2015 
2016  >>> f = Function('f', IntSort(), IntSort())
2017  >>> x = Int('x')
2018  >>> q = ForAll(x, f(x) == 0)
2019  >>> q.is_exists()
2020  False
2021  >>> q = Exists(x, f(x) != 0)
2022  >>> q.is_exists()
2023  True
2024  """
2025  return Z3_is_quantifier_exists(self.ctx_ref(), self.ast)
2026 
bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)
Determine if ast is an existential quantifier.
def is_exists(self)
Definition: z3py.py:2013
def ctx_ref(self)
Definition: z3py.py:400
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 1999 of file z3py.py.

1999  def is_forall(self):
2000  """Return `True` if `self` is a universal quantifier.
2001 
2002  >>> f = Function('f', IntSort(), IntSort())
2003  >>> x = Int('x')
2004  >>> q = ForAll(x, f(x) == 0)
2005  >>> q.is_forall()
2006  True
2007  >>> q = Exists(x, f(x) != 0)
2008  >>> q.is_forall()
2009  False
2010  """
2011  return Z3_is_quantifier_forall(self.ctx_ref(), self.ast)
2012 
def is_forall(self)
Definition: z3py.py:1999
def ctx_ref(self)
Definition: z3py.py:400
bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if an ast is a universal quantifier.
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 2027 of file z3py.py.

Referenced by QuantifierRef.__getitem__().

2027  def is_lambda(self):
2028  """Return `True` if `self` is a lambda expression.
2029 
2030  >>> f = Function('f', IntSort(), IntSort())
2031  >>> x = Int('x')
2032  >>> q = Lambda(x, f(x))
2033  >>> q.is_lambda()
2034  True
2035  >>> q = Exists(x, f(x) != 0)
2036  >>> q.is_lambda()
2037  False
2038  """
2039  return Z3_is_lambda(self.ctx_ref(), self.ast)
2040 
def is_lambda(self)
Definition: z3py.py:2027
def ctx_ref(self)
Definition: z3py.py:400
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 2096 of file z3py.py.

2096  def no_pattern(self, idx):
2097  """Return a no-pattern."""
2098  if z3_debug():
2099  _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
2100  return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
2101 
def num_no_patterns(self)
Definition: z3py.py:2092
Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th no_pattern.
def z3_debug()
Definition: z3py.py:62
def ctx_ref(self)
Definition: z3py.py:400
def no_pattern(self, idx)
Definition: z3py.py:2096
def num_no_patterns (   self)
Return the number of no-patterns.

Definition at line 2092 of file z3py.py.

Referenced by QuantifierRef.no_pattern().

2092  def num_no_patterns(self):
2093  """Return the number of no-patterns."""
2094  return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast)
2095 
def num_no_patterns(self)
Definition: z3py.py:2092
def ctx_ref(self)
Definition: z3py.py:400
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 2062 of file z3py.py.

2062  def num_patterns(self):
2063  """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
2064 
2065  >>> f = Function('f', IntSort(), IntSort())
2066  >>> g = Function('g', IntSort(), IntSort())
2067  >>> x = Int('x')
2068  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
2069  >>> q.num_patterns()
2070  2
2071  """
2072  return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast))
2073 
def num_patterns(self)
Definition: z3py.py:2062
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:400
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 2113 of file z3py.py.

2113  def num_vars(self):
2114  """Return the number of variables bounded by this quantifier.
2115 
2116  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2117  >>> x = Int('x')
2118  >>> y = Int('y')
2119  >>> q = ForAll([x, y], f(x, y) >= x)
2120  >>> q.num_vars()
2121  2
2122  """
2123  return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast))
2124 
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:400
def num_vars(self)
Definition: z3py.py:2113
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 2074 of file z3py.py.

2074  def pattern(self, idx):
2075  """Return a pattern (i.e., quantifier instantiation hints) in `self`.
2076 
2077  >>> f = Function('f', IntSort(), IntSort())
2078  >>> g = Function('g', IntSort(), IntSort())
2079  >>> x = Int('x')
2080  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
2081  >>> q.num_patterns()
2082  2
2083  >>> q.pattern(0)
2084  f(Var(0))
2085  >>> q.pattern(1)
2086  g(Var(0))
2087  """
2088  if z3_debug():
2089  _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
2090  return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
2091 
Patterns.
Definition: z3py.py:1917
def num_patterns(self)
Definition: z3py.py:2062
Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th pattern.
def pattern(self, idx)
Definition: z3py.py:2074
def z3_debug()
Definition: z3py.py:62
def ctx_ref(self)
Definition: z3py.py:400
def sort (   self)
Return the Boolean sort or sort of Lambda.

Definition at line 1993 of file z3py.py.

1993  def sort(self):
1994  """Return the Boolean sort or sort of Lambda."""
1995  if self.is_lambda():
1996  return _sort(self.ctx, self.as_ast())
1997  return BoolSort(self.ctx)
1998 
def BoolSort
Definition: z3py.py:1687
def as_ast(self)
Definition: z3py.py:392
def sort(self)
Definition: z3py.py:1993
def is_lambda(self)
Definition: z3py.py:2027
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 2125 of file z3py.py.

2125  def var_name(self, idx):
2126  """Return a string representing a name used when displaying the quantifier.
2127 
2128  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2129  >>> x = Int('x')
2130  >>> y = Int('y')
2131  >>> q = ForAll([x, y], f(x, y) >= x)
2132  >>> q.var_name(0)
2133  'x'
2134  >>> q.var_name(1)
2135  'y'
2136  """
2137  if z3_debug():
2138  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
2139  return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx))
2140 
def var_name(self, idx)
Definition: z3py.py:2125
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:62
def ctx_ref(self)
Definition: z3py.py:400
def num_vars(self)
Definition: z3py.py:2113
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 2141 of file z3py.py.

2141  def var_sort(self, idx):
2142  """Return the sort of a bound variable.
2143 
2144  >>> f = Function('f', IntSort(), RealSort(), IntSort())
2145  >>> x = Int('x')
2146  >>> y = Real('y')
2147  >>> q = ForAll([x, y], f(x, y) >= x)
2148  >>> q.var_sort(0)
2149  Int
2150  >>> q.var_sort(1)
2151  Real
2152  """
2153  if z3_debug():
2154  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
2155  return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
2156 
def var_sort(self, idx)
Definition: z3py.py:2141
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:62
def ctx_ref(self)
Definition: z3py.py:400
def num_vars(self)
Definition: z3py.py:2113
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 2048 of file z3py.py.

2048  def weight(self):
2049  """Return the weight annotation of `self`.
2050 
2051  >>> f = Function('f', IntSort(), IntSort())
2052  >>> x = Int('x')
2053  >>> q = ForAll(x, f(x) == 0)
2054  >>> q.weight()
2055  1
2056  >>> q = ForAll(x, f(x) == 0, weight=10)
2057  >>> q.weight()
2058  10
2059  """
2060  return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))
2061 
unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a)
Obtain weight of quantifier.
def ctx_ref(self)
Definition: z3py.py:400
def weight(self)
Definition: z3py.py:2048