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

Member Function Documentation

__getitem__()

__getitem__	(		self,
			arg
	)

Return the Z3 expression `self[arg]`.

Definition at line 2184 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 2130 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 2255 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 2310 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 2133 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 2156 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 2142 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 2170 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 2249 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 2245 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 2215 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 2266 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 2227 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 2210 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 2205 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 2136 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 2278 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 2294 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 2191 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 2154 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 2139 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().