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)
def	py_value (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	kind (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)
def	py_value (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 2059 of file z3py.py.

Member Function Documentation

def __getitem__	(		self,
			arg
	)

Return the Z3 expression `self[arg]`.

Definition at line 2116 of file z3py.py.

    def __getitem__(self, arg):
        """Return the Z3 expression `self[arg]`.
        """
        if z3_debug():
            _z3_assert(self.is_lambda(), "quantifier should be a lambda expression")
        return _array_select(self, arg)

def as_ast

(

self

)

Definition at line 2062 of file z3py.py.

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

Referenced by QuantifierRef.children().

    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
        """
        return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx)

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 2242 of file z3py.py.

    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]
        """
        return [self.body()]

def get_id

(

self

)

Definition at line 2065 of file z3py.py.

    def get_id(self):
        return Z3_get_ast_id(self.ctx_ref(), self.as_ast())

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 2088 of file z3py.py.

    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
        """
        return Z3_is_quantifier_exists(self.ctx_ref(), self.ast)

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 2074 of file z3py.py.

    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
        """
        return Z3_is_quantifier_forall(self.ctx_ref(), self.ast)

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 2102 of file z3py.py.

Referenced by QuantifierRef.__getitem__().

    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
        """
        return Z3_is_lambda(self.ctx_ref(), self.ast)

def no_pattern	(		self,
			idx
	)

Return a no-pattern.

Definition at line 2181 of file z3py.py.

    def no_pattern(self, idx):
        """Return a no-pattern."""
        if z3_debug():
            _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
        return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)

def num_no_patterns

(

self

)

Return the number of no-patterns.

Definition at line 2177 of file z3py.py.

Referenced by QuantifierRef.no_pattern().

    def num_no_patterns(self):
        """Return the number of no-patterns."""
        return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast)

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 2147 of file z3py.py.

    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
        """
        return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast))

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 2198 of file z3py.py.

    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
        """
        return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast))

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 2159 of file z3py.py.

    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))
        """
        if z3_debug():
            _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
        return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)

def qid

(

self

)

Return the quantifier id of `self`.

Definition at line 2142 of file z3py.py.

    def qid(self):
        """Return the quantifier id of `self`.
        """
        return _symbol2py(self.ctx, Z3_get_quantifier_id(self.ctx_ref(), self.ast))

def skolem_id

(

self

)

Return the skolem id of `self`.

Definition at line 2137 of file z3py.py.

    def skolem_id(self):
        """Return the skolem id of `self`.
        """
        return _symbol2py(self.ctx, Z3_get_quantifier_skolem_id(self.ctx_ref(), self.ast))

def sort

(

self

)

Return the Boolean sort or sort of Lambda.

Definition at line 2068 of file z3py.py.

    def sort(self):
        """Return the Boolean sort or sort of Lambda."""
        if self.is_lambda():
            return _sort(self.ctx, self.as_ast())
        return BoolSort(self.ctx)

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 2210 of file z3py.py.

    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'
        """
        if z3_debug():
            _z3_assert(idx < self.num_vars(), "Invalid variable idx")
        return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx))

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 2226 of file z3py.py.

    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
        """
        if z3_debug():
            _z3_assert(idx < self.num_vars(), "Invalid variable idx")
        return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)

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 2123 of file z3py.py.

    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
        """
        return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))