QuantifierRef Class Reference

Quantifiers. More...

Inheritance diagram for QuantifierRef:

Public Member Functions
	as_ast (self)
	get_id (self)
	sort (self)
	is_forall (self)
	is_exists (self)
	is_lambda (self)
	__getitem__ (self, arg)
	weight (self)
	skolem_id (self)
	qid (self)
	num_patterns (self)
	pattern (self, idx)
	num_no_patterns (self)
	no_pattern (self, idx)
	body (self)
	num_vars (self)
	var_name (self, idx)
	var_sort (self, idx)
	children (self)
Public Member Functions inherited from BoolRef
	__add__ (self, other)
	__radd__ (self, other)
	__rmul__ (self, other)
	__mul__ (self, other)
	__and__ (self, other)
	__or__ (self, other)
	__xor__ (self, other)
	__invert__ (self)
	py_value (self)
Public Member Functions inherited from ExprRef
	sort_kind (self)
	__eq__ (self, other)
	__hash__ (self)
	__ne__ (self, other)
	params (self)
	decl (self)
	kind (self)
	num_args (self)
	arg (self, idx)
	update (self, *args)
	from_string (self, s)
	serialize (self)
Public Member Functions inherited from AstRef
	__init__ (self, ast, ctx=None)
	__del__ (self)
	__deepcopy__ (self, memo={})
	__str__ (self)
	__repr__ (self)
	__nonzero__ (self)
	__bool__ (self)
	sexpr (self)
	ctx_ref (self)
	eq (self, other)
	translate (self, target)
	__copy__ (self)
	hash (self)
Public Member Functions inherited from Z3PPObject
	use_pp (self)

Data Fields
	ctx
	ast
Data Fields inherited from BoolRef
	ctx
Data Fields inherited from ExprRef
	ctx
	ast
Data Fields inherited from AstRef
	ast
	ctx

Additional Inherited Members
Protected Member Functions inherited from Z3PPObject
	_repr_html_ (self)

Detailed Description

Quantifiers.

Universally and Existentially quantified formulas.

Definition at line 2149 of file z3py.py.

Member Function Documentation

__getitem__()

__getitem__	(		self,
			arg
	)

Return the Z3 expression `self[arg]`.

Definition at line 2206 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)
 

as_ast()

as_ast

(

self

)

Return a pointer to the corresponding C Z3_ast object.

Reimplemented from ExprRef.

Definition at line 2152 of file z3py.py.

    def as_ast(self):
        return self.ast
 

Referenced by AstRef.__del__(), BitVecRef.__invert__(), ArithRef.__neg__(), BitVecRef.__neg__(), ExprRef.arg(), IntNumRef.as_binary_string(), BitVecNumRef.as_binary_string(), RatNumRef.as_decimal(), AlgebraicNumRef.as_decimal(), IntNumRef.as_string(), RatNumRef.as_string(), BitVecNumRef.as_string(), ExprRef.decl(), ArrayRef.default(), RatNumRef.denominator(), AstRef.eq(), AstRef.get_id(), SortRef.get_id(), FuncDeclRef.get_id(), ExprRef.get_id(), PatternRef.get_id(), QuantifierRef.get_id(), AstRef.hash(), AlgebraicNumRef.index(), ExprRef.num_args(), AlgebraicNumRef.poly(), RatNumRef.py_value(), AstRef.sexpr(), AstRef.translate(), ExprRef.update(), and DatatypeRef.update_field().

body()

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 2277 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()

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 2332 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()

get_id

(

self

)

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

Reimplemented from ExprRef.

Definition at line 2155 of file z3py.py.

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

is_exists()

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

is_forall()

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

is_lambda()

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

    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)
 

Referenced by QuantifierRef.__getitem__(), and QuantifierRef.sort().

no_pattern()

no_pattern	(		self,
			idx
	)

Return a no-pattern.

Definition at line 2271 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)
 

num_no_patterns()

num_no_patterns

(

self

)

Return the number of no-patterns.

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

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 2237 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()

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 2288 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()

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

qid()

qid

(

self

)

Return the quantifier id of `self`.

Definition at line 2232 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))
 

skolem_id()

skolem_id

(

self

)

Return the skolem id of `self`.

Definition at line 2227 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))
 

sort()

sort

(

self

)

Return the Boolean sort or sort of Lambda.

Reimplemented from BoolRef.

Definition at line 2158 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)
 

Referenced by ArrayRef.domain(), ArrayRef.domain_n(), ArithRef.is_int(), ArithRef.is_real(), ArrayRef.range(), BitVecRef.size(), and ExprRef.sort_kind().

var_name()

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

var_sort()

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

weight()

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

Field Documentation

ast

ast

Definition at line 2176 of file z3py.py.

Referenced by FuncDeclRef.__call__(), AstRef.__deepcopy__(), AstRef.__del__(), SortRef.__eq__(), SortRef.__ne__(), DatatypeSortRef.accessor(), FuncDeclRef.arity(), AstRef.as_ast(), ExprRef.as_ast(), QuantifierRef.as_ast(), FuncDeclRef.as_func_decl(), QuantifierRef.body(), FuncDeclRef.domain(), ArraySortRef.domain_n(), QuantifierRef.is_exists(), QuantifierRef.is_lambda(), FuncDeclRef.kind(), SortRef.name(), QuantifierRef.no_pattern(), QuantifierRef.num_no_patterns(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), FuncDeclRef.params(), QuantifierRef.pattern(), QuantifierRef.qid(), FuncDeclRef.range(), ArraySortRef.range(), DatatypeSortRef.recognizer(), QuantifierRef.skolem_id(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().

ctx

ctx

Definition at line 2161 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), AstMap.__contains__(), AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), AstRef.__deepcopy__(), Datatype.__deepcopy__(), ParamsRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), AstMap.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Statistics.__deepcopy__(), Context.__del__(), AstRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), ParamsRef.__del__(), ParamDescrsRef.__del__(), Goal.__del__(), AstVector.__del__(), AstMap.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), ModelRef.__del__(), Statistics.__del__(), Solver.__del__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), AstMap.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), BoolRef.__mul__(), ArithRef.__mul__(), BitVecRef.__mul__(), ExprRef.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), ParamsRef.__repr__(), ParamDescrsRef.__repr__(), AstMap.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), QuantifierRef.body(), FiniteSetSortRef.cast(), Solver.check(), Goal.convert_model(), AstRef.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), Goal.get(), ParamDescrsRef.get_documentation(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), ModelRef.get_sort(), ModelRef.get_universe(), Goal.inconsistent(), AstMap.keys(), Statistics.keys(), Solver.model(), SortRef.name(), QuantifierRef.no_pattern(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), FuncDeclRef.params(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Solver.pop(), Goal.prec(), ModelRef.project(), ModelRef.project_with_witness(), Solver.push(), AstVector.push(), QuantifierRef.qid(), FuncDeclRef.range(), ArraySortRef.range(), DatatypeSortRef.recognizer(), Context.ref(), AstMap.reset(), Solver.reset(), AstVector.resize(), Solver.set(), ParamsRef.set(), Goal.sexpr(), AstVector.sexpr(), ModelRef.sexpr(), ParamDescrsRef.size(), Goal.size(), QuantifierRef.skolem_id(), AstVector.translate(), AstRef.translate(), Goal.translate(), ModelRef.translate(), ExprRef.update(), DatatypeRef.update_field(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().