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 skolem_id (self)
 
def qid (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 __add__ (self, other)
 
def __radd__ (self, other)
 
def __rmul__ (self, other)
 
def __mul__ (self, other)
 
def __and__ (self, other)
 
def __or__ (self, other)
 
def __xor__ (self, other)
 
def __invert__ (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 __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 2028 of file z3py.py.

Member Function Documentation

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

Definition at line 2085 of file z3py.py.

2085  def __getitem__(self, arg):
2086  """Return the Z3 expression `self[arg]`.
2087  """
2088  if z3_debug():
2089  _z3_assert(self.is_lambda(), "quantifier should be a lambda expression")
2090  return _array_select(self, arg)
2091 
def is_lambda(self)
Definition: z3py.py:2071
def __getitem__(self, arg)
Definition: z3py.py:2085
def z3_debug()
Definition: z3py.py:62
def as_ast (   self)

Definition at line 2031 of file z3py.py.

2031  def as_ast(self):
2032  return self.ast
2033 
def as_ast(self)
Definition: z3py.py:2031
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 2156 of file z3py.py.

Referenced by QuantifierRef.children().

2156  def body(self):
2157  """Return the expression being quantified.
2158 
2159  >>> f = Function('f', IntSort(), IntSort())
2160  >>> x = Int('x')
2161  >>> q = ForAll(x, f(x) == 0)
2162  >>> q.body()
2163  f(Var(0)) == 0
2164  """
2165  return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx)
2166 
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:2156
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 2211 of file z3py.py.

2211  def children(self):
2212  """Return a list containing a single element self.body()
2213 
2214  >>> f = Function('f', IntSort(), IntSort())
2215  >>> x = Int('x')
2216  >>> q = ForAll(x, f(x) == 0)
2217  >>> q.children()
2218  [f(Var(0)) == 0]
2219  """
2220  return [self.body()]
2221 
2222 
def children(self)
Definition: z3py.py:2211
def body(self)
Definition: z3py.py:2156
def get_id (   self)

Definition at line 2034 of file z3py.py.

2034  def get_id(self):
2035  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
2036 
def get_id(self)
Definition: z3py.py:2034
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 2057 of file z3py.py.

2057  def is_exists(self):
2058  """Return `True` if `self` is an existential quantifier.
2059 
2060  >>> f = Function('f', IntSort(), IntSort())
2061  >>> x = Int('x')
2062  >>> q = ForAll(x, f(x) == 0)
2063  >>> q.is_exists()
2064  False
2065  >>> q = Exists(x, f(x) != 0)
2066  >>> q.is_exists()
2067  True
2068  """
2069  return Z3_is_quantifier_exists(self.ctx_ref(), self.ast)
2070 
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:2057
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 2043 of file z3py.py.

2043  def is_forall(self):
2044  """Return `True` if `self` is a universal quantifier.
2045 
2046  >>> f = Function('f', IntSort(), IntSort())
2047  >>> x = Int('x')
2048  >>> q = ForAll(x, f(x) == 0)
2049  >>> q.is_forall()
2050  True
2051  >>> q = Exists(x, f(x) != 0)
2052  >>> q.is_forall()
2053  False
2054  """
2055  return Z3_is_quantifier_forall(self.ctx_ref(), self.ast)
2056 
def is_forall(self)
Definition: z3py.py:2043
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 2071 of file z3py.py.

Referenced by QuantifierRef.__getitem__().

2071  def is_lambda(self):
2072  """Return `True` if `self` is a lambda expression.
2073 
2074  >>> f = Function('f', IntSort(), IntSort())
2075  >>> x = Int('x')
2076  >>> q = Lambda(x, f(x))
2077  >>> q.is_lambda()
2078  True
2079  >>> q = Exists(x, f(x) != 0)
2080  >>> q.is_lambda()
2081  False
2082  """
2083  return Z3_is_lambda(self.ctx_ref(), self.ast)
2084 
def is_lambda(self)
Definition: z3py.py:2071
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 2150 of file z3py.py.

2150  def no_pattern(self, idx):
2151  """Return a no-pattern."""
2152  if z3_debug():
2153  _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
2154  return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
2155 
def num_no_patterns(self)
Definition: z3py.py:2146
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:2150
def num_no_patterns (   self)
Return the number of no-patterns.

Definition at line 2146 of file z3py.py.

Referenced by QuantifierRef.no_pattern().

2146  def num_no_patterns(self):
2147  """Return the number of no-patterns."""
2148  return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast)
2149 
def num_no_patterns(self)
Definition: z3py.py:2146
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 2116 of file z3py.py.

2116  def num_patterns(self):
2117  """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
2118 
2119  >>> f = Function('f', IntSort(), IntSort())
2120  >>> g = Function('g', IntSort(), IntSort())
2121  >>> x = Int('x')
2122  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
2123  >>> q.num_patterns()
2124  2
2125  """
2126  return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast))
2127 
def num_patterns(self)
Definition: z3py.py:2116
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 2167 of file z3py.py.

2167  def num_vars(self):
2168  """Return the number of variables bounded by this quantifier.
2169 
2170  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2171  >>> x = Int('x')
2172  >>> y = Int('y')
2173  >>> q = ForAll([x, y], f(x, y) >= x)
2174  >>> q.num_vars()
2175  2
2176  """
2177  return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast))
2178 
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:2167
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 2128 of file z3py.py.

2128  def pattern(self, idx):
2129  """Return a pattern (i.e., quantifier instantiation hints) in `self`.
2130 
2131  >>> f = Function('f', IntSort(), IntSort())
2132  >>> g = Function('g', IntSort(), IntSort())
2133  >>> x = Int('x')
2134  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
2135  >>> q.num_patterns()
2136  2
2137  >>> q.pattern(0)
2138  f(Var(0))
2139  >>> q.pattern(1)
2140  g(Var(0))
2141  """
2142  if z3_debug():
2143  _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
2144  return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
2145 
Patterns.
Definition: z3py.py:1961
def num_patterns(self)
Definition: z3py.py:2116
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:2128
def z3_debug()
Definition: z3py.py:62
def ctx_ref(self)
Definition: z3py.py:400
def qid (   self)
Return the quantifier id of `self`.

Definition at line 2111 of file z3py.py.

2111  def qid(self):
2112  """Return the quantifier id of `self`.
2113  """
2114  return _symbol2py(self.ctx, Z3_get_quantifier_id(self.ctx_ref(), self.ast))
2115 
def qid(self)
Definition: z3py.py:2111
Z3_symbol Z3_API Z3_get_quantifier_id(Z3_context c, Z3_ast a)
Obtain id of quantifier.
def ctx_ref(self)
Definition: z3py.py:400
def skolem_id (   self)
Return the skolem id of `self`.

Definition at line 2106 of file z3py.py.

2106  def skolem_id(self):
2107  """Return the skolem id of `self`.
2108  """
2109  return _symbol2py(self.ctx, Z3_get_quantifier_skolem_id(self.ctx_ref(), self.ast))
2110 
Z3_symbol Z3_API Z3_get_quantifier_skolem_id(Z3_context c, Z3_ast a)
Obtain skolem id of quantifier.
def skolem_id(self)
Definition: z3py.py:2106
def ctx_ref(self)
Definition: z3py.py:400
def sort (   self)
Return the Boolean sort or sort of Lambda.

Definition at line 2037 of file z3py.py.

2037  def sort(self):
2038  """Return the Boolean sort or sort of Lambda."""
2039  if self.is_lambda():
2040  return _sort(self.ctx, self.as_ast())
2041  return BoolSort(self.ctx)
2042 
def BoolSort
Definition: z3py.py:1731
def as_ast(self)
Definition: z3py.py:392
def sort(self)
Definition: z3py.py:2037
def is_lambda(self)
Definition: z3py.py:2071
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 2179 of file z3py.py.

2179  def var_name(self, idx):
2180  """Return a string representing a name used when displaying the quantifier.
2181 
2182  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2183  >>> x = Int('x')
2184  >>> y = Int('y')
2185  >>> q = ForAll([x, y], f(x, y) >= x)
2186  >>> q.var_name(0)
2187  'x'
2188  >>> q.var_name(1)
2189  'y'
2190  """
2191  if z3_debug():
2192  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
2193  return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx))
2194 
def var_name(self, idx)
Definition: z3py.py:2179
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:2167
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 2195 of file z3py.py.

2195  def var_sort(self, idx):
2196  """Return the sort of a bound variable.
2197 
2198  >>> f = Function('f', IntSort(), RealSort(), IntSort())
2199  >>> x = Int('x')
2200  >>> y = Real('y')
2201  >>> q = ForAll([x, y], f(x, y) >= x)
2202  >>> q.var_sort(0)
2203  Int
2204  >>> q.var_sort(1)
2205  Real
2206  """
2207  if z3_debug():
2208  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
2209  return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
2210 
def var_sort(self, idx)
Definition: z3py.py:2195
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:2167
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 2092 of file z3py.py.

2092  def weight(self):
2093  """Return the weight annotation of `self`.
2094 
2095  >>> f = Function('f', IntSort(), IntSort())
2096  >>> x = Int('x')
2097  >>> q = ForAll(x, f(x) == 0)
2098  >>> q.weight()
2099  1
2100  >>> q = ForAll(x, f(x) == 0, weight=10)
2101  >>> q.weight()
2102  10
2103  """
2104  return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))
2105 
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:2092