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

Referenced by BoolRef.sort().

01604 
01605     def as_ast(self):
01606         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 1682 of file z3py.py.

Referenced by QuantifierRef.children().

01682 
01683     def body(self):
01684         """Return the expression being quantified.
01685 
01686         >>> f = Function('f', IntSort(), IntSort())
01687         >>> x = Int('x')
01688         >>> q = ForAll(x, f(x) == 0)
01689         >>> q.body()
01690         f(Var(0)) == 0
01691         """
01692         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 1737 of file z3py.py.

01737 
01738     def children(self):
01739         """Return a list containing a single element self.body()
01740 
01741         >>> f = Function('f', IntSort(), IntSort())
01742         >>> x = Int('x')
01743         >>> q = ForAll(x, f(x) == 0)
01744         >>> q.children()
01745         [f(Var(0)) == 0]
01746         """
01747         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 1607 of file z3py.py.

01607 
01608     def get_id(self):
01609         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 1614 of file z3py.py.

01614 
01615     def is_forall(self):
01616         """Return `True` if `self` is a universal quantifier.
01617         
01618         >>> f = Function('f', IntSort(), IntSort())
01619         >>> x = Int('x')
01620         >>> q = ForAll(x, f(x) == 0)
01621         >>> q.is_forall()
01622         True
01623         >>> q = Exists(x, f(x) != 0)
01624         >>> q.is_forall()
01625         False
01626         """
01627         return Z3_is_quantifier_forall(self.ctx_ref(), self.ast)

def no_pattern	(	self,
		idx
	)

Return a no-pattern.

Definition at line 1676 of file z3py.py.

01676 
01677     def no_pattern(self, idx):
01678         """Return a no-pattern."""
01679         if __debug__:
01680             _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
01681         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 1672 of file z3py.py.

Referenced by QuantifierRef.no_pattern().

01672 
01673     def num_no_patterns(self):
01674         """Return the number of no-patterns."""
01675         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 1642 of file z3py.py.

01642 
01643     def num_patterns(self):
01644         """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
01645 
01646         >>> f = Function('f', IntSort(), IntSort())
01647         >>> g = Function('g', IntSort(), IntSort())
01648         >>> x = Int('x')
01649         >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
01650         >>> q.num_patterns()
01651         2
01652         """
01653         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 1693 of file z3py.py.

01693 
01694     def num_vars(self):
01695         """Return the number of variables bounded by this quantifier. 
01696         
01697         >>> f = Function('f', IntSort(), IntSort(), IntSort())
01698         >>> x = Int('x')
01699         >>> y = Int('y')
01700         >>> q = ForAll([x, y], f(x, y) >= x)
01701         >>> q.num_vars() 
01702         2
01703         """
01704         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 1654 of file z3py.py.

01654 
01655     def pattern(self, idx):
01656         """Return a pattern (i.e., quantifier instantiation hints) in `self`.
01657 
01658         >>> f = Function('f', IntSort(), IntSort())
01659         >>> g = Function('g', IntSort(), IntSort())
01660         >>> x = Int('x')
01661         >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
01662         >>> q.num_patterns()
01663         2
01664         >>> q.pattern(0)
01665         f(Var(0))
01666         >>> q.pattern(1)
01667         g(Var(0))
01668         """
01669         if __debug__:
01670             _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
01671         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 1610 of file z3py.py.

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

01610 
01611     def sort(self):
01612         """Return the Boolean sort."""
01613         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 1705 of file z3py.py.

01705 
01706     def var_name(self, idx):
01707         """Return a string representing a name used when displaying the quantifier. 
01708         
01709         >>> f = Function('f', IntSort(), IntSort(), IntSort())
01710         >>> x = Int('x')
01711         >>> y = Int('y')
01712         >>> q = ForAll([x, y], f(x, y) >= x)
01713         >>> q.var_name(0)
01714         'x'
01715         >>> q.var_name(1)
01716         'y'
01717         """
01718         if __debug__:
01719             _z3_assert(idx < self.num_vars(), "Invalid variable idx")
01720         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 1721 of file z3py.py.

01721 
01722     def var_sort(self, idx):
01723         """Return the sort of a bound variable.
01724 
01725         >>> f = Function('f', IntSort(), RealSort(), IntSort())
01726         >>> x = Int('x')
01727         >>> y = Real('y')
01728         >>> q = ForAll([x, y], f(x, y) >= x)
01729         >>> q.var_sort(0)
01730         Int
01731         >>> q.var_sort(1)
01732         Real
01733         """
01734         if __debug__:
01735             _z3_assert(idx < self.num_vars(), "Invalid variable idx")
01736         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 1628 of file z3py.py.

01628 
01629     def weight(self):
01630         """Return the weight annotation of `self`.
01631 
01632         >>> f = Function('f', IntSort(), IntSort())
01633         >>> x = Int('x')
01634         >>> q = ForAll(x, f(x) == 0)
01635         >>> q.weight()
01636         1
01637         >>> q = ForAll(x, f(x) == 0, weight=10)
01638         >>> q.weight()
01639         10
01640         """
01641         return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))

Public Member Functions

Detailed Description

Member Function Documentation