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	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	__rmul__ (self, other)
def	__mul__ (self, other)
Public Member Functions inherited from ExprRef
def	sort_kind (self)
def	__eq__ (self, other)
def	__hash__ (self)
def	__ne__ (self, other)
def	decl (self)
def	num_args (self)
def	arg (self, idx)
Public Member Functions inherited from AstRef
def	__init__ (self, ast, ctx=None)
def	__del__ (self)
def	__str__ (self)
def	__repr__ (self)
def	__nonzero__ (self)
def	__bool__ (self)
def	sexpr (self)
def	ctx_ref (self)
def	eq (self, other)
def	translate (self, target)
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 1686 of file z3py.py.

Member Function Documentation

as_ast()

def as_ast

(

self

)

Return a pointer to the corresponding C Z3_ast object.

Reimplemented from ExprRef.

Definition at line 1689 of file z3py.py.

    def as_ast(self):
        return self.ast

body()

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

    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)

Referenced by QuantifierRef.children().

children()

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]

Reimplemented from ExprRef.

Definition at line 1822 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() ]

get_id()

def get_id

(

self

)

Return unique identifier for object. It can be used for hash-tables and maps.

Reimplemented from ExprRef.

Definition at line 1692 of file z3py.py.

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

is_forall()

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 1699 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)

no_pattern()

def no_pattern	(		self,
			idx
	)

Return a no-pattern.

Definition at line 1761 of file z3py.py.

    def no_pattern(self, idx):
        """Return a no-pattern."""
        if __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)

num_no_patterns()

def num_no_patterns

(

self

)

Return the number of no-patterns.

Definition at line 1757 of file z3py.py.

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

Referenced by QuantifierRef.no_pattern().

num_patterns()

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 1727 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))

Referenced by QuantifierRef.pattern().

num_vars()

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 1778 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))

Referenced by QuantifierRef.var_name(), and QuantifierRef.var_sort().

pattern()

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 1739 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 __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)

sort()

def sort

(

self

)

Return the Boolean sort.

Reimplemented from BoolRef.

Definition at line 1695 of file z3py.py.

    def sort(self):
        """Return the Boolean sort."""
        return BoolSort(self.ctx)

var_name()

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 1790 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 __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))

var_sort()

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 1806 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 __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)

weight()

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 1713 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))