Quantifiers. More...

Inheritance diagram for QuantifierRef:

Public Member Functions
def	as_ast
def	get_id
def	sort
def	is_forall
def	weight
def	num_patterns
def	pattern
def	num_no_patterns
def	no_pattern
def	body
def	num_vars
def	var_name
def	var_sort
def	children

Detailed Description

Quantifiers.

Universally and Existentially quantified formulas.

Definition at line 1622 of file z3py.py.

Member Function Documentation

def as_ast ( self )

Return a pointer to the corresponding C Z3_ast object.

Reimplemented from ExprRef.

Definition at line 1625 of file z3py.py.

Referenced by BoolRef.sort().

01625 
01626     def as_ast(self):
01627         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 1703 of file z3py.py.

Referenced by QuantifierRef.children().

01703 
01704     def body(self):
01705         """Return the expression being quantified.
01706 
01707         >>> f = Function('f', IntSort(), IntSort())
01708         >>> x = Int('x')
01709         >>> q = ForAll(x, f(x) == 0)
01710         >>> q.body()
01711         f(Var(0)) == 0
01712         """
01713         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]

Reimplemented from ExprRef.

Definition at line 1758 of file z3py.py.

01758 
01759     def children(self):
01760         """Return a list containing a single element self.body()
01761 
01762         >>> f = Function('f', IntSort(), IntSort())
01763         >>> x = Int('x')
01764         >>> q = ForAll(x, f(x) == 0)
01765         >>> q.children()
01766         [f(Var(0)) == 0]
01767         """
01768         return [ self.body() ]

def get_id ( self )

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

Reimplemented from ExprRef.

Definition at line 1628 of file z3py.py.

01628 
01629     def get_id(self):
01630         return Z3_get_ast_id(self.ctx_ref(), self.as_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 1635 of file z3py.py.

01635 
01636     def is_forall(self):
01637         """Return `True` if `self` is a universal quantifier.
01638         
01639         >>> f = Function('f', IntSort(), IntSort())
01640         >>> x = Int('x')
01641         >>> q = ForAll(x, f(x) == 0)
01642         >>> q.is_forall()
01643         True
01644         >>> q = Exists(x, f(x) != 0)
01645         >>> q.is_forall()
01646         False
01647         """
01648         return Z3_is_quantifier_forall(self.ctx_ref(), self.ast)

def no_pattern	(	self,
		idx
	)

Return a no-pattern.

Definition at line 1697 of file z3py.py.

01697 
01698     def no_pattern(self, idx):
01699         """Return a no-pattern."""
01700         if __debug__:
01701             _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
01702         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 1693 of file z3py.py.

Referenced by QuantifierRef.no_pattern().

01693 
01694     def num_no_patterns(self):
01695         """Return the number of no-patterns."""
01696         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 1663 of file z3py.py.

01663 
01664     def num_patterns(self):
01665         """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
01666 
01667         >>> f = Function('f', IntSort(), IntSort())
01668         >>> g = Function('g', IntSort(), IntSort())
01669         >>> x = Int('x')
01670         >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
01671         >>> q.num_patterns()
01672         2
01673         """
01674         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 1714 of file z3py.py.

01714 
01715     def num_vars(self):
01716         """Return the number of variables bounded by this quantifier. 
01717         
01718         >>> f = Function('f', IntSort(), IntSort(), IntSort())
01719         >>> x = Int('x')
01720         >>> y = Int('y')
01721         >>> q = ForAll([x, y], f(x, y) >= x)
01722         >>> q.num_vars() 
01723         2
01724         """
01725         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 1675 of file z3py.py.

01675 
01676     def pattern(self, idx):
01677         """Return a pattern (i.e., quantifier instantiation hints) in `self`.
01678 
01679         >>> f = Function('f', IntSort(), IntSort())
01680         >>> g = Function('g', IntSort(), IntSort())
01681         >>> x = Int('x')
01682         >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
01683         >>> q.num_patterns()
01684         2
01685         >>> q.pattern(0)
01686         f(Var(0))
01687         >>> q.pattern(1)
01688         g(Var(0))
01689         """
01690         if __debug__:
01691             _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
01692         return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)

def sort ( self )

Return the Boolean sort.

Reimplemented from BoolRef.

Definition at line 1631 of file z3py.py.

Referenced by ArrayRef.domain(), and ArrayRef.range().

01631 
01632     def sort(self):
01633         """Return the Boolean sort."""
01634         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 1726 of file z3py.py.

01726 
01727     def var_name(self, idx):
01728         """Return a string representing a name used when displaying the quantifier. 
01729         
01730         >>> f = Function('f', IntSort(), IntSort(), IntSort())
01731         >>> x = Int('x')
01732         >>> y = Int('y')
01733         >>> q = ForAll([x, y], f(x, y) >= x)
01734         >>> q.var_name(0)
01735         'x'
01736         >>> q.var_name(1)
01737         'y'
01738         """
01739         if __debug__:
01740             _z3_assert(idx < self.num_vars(), "Invalid variable idx")
01741         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 1742 of file z3py.py.

01742 
01743     def var_sort(self, idx):
01744         """Return the sort of a bound variable.
01745 
01746         >>> f = Function('f', IntSort(), RealSort(), IntSort())
01747         >>> x = Int('x')
01748         >>> y = Real('y')
01749         >>> q = ForAll([x, y], f(x, y) >= x)
01750         >>> q.var_sort(0)
01751         Int
01752         >>> q.var_sort(1)
01753         Real
01754         """
01755         if __debug__:
01756             _z3_assert(idx < self.num_vars(), "Invalid variable idx")
01757         return SortRef(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 1649 of file z3py.py.

01649 
01650     def weight(self):
01651         """Return the weight annotation of `self`.
01652 
01653         >>> f = Function('f', IntSort(), IntSort())
01654         >>> x = Int('x')
01655         >>> q = ForAll(x, f(x) == 0)
01656         >>> q.weight()
01657         1
01658         >>> q = ForAll(x, f(x) == 0, weight=10)
01659         >>> q.weight()
01660         10
01661         """
01662         return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))

Public Member Functions

Detailed Description

Member Function Documentation