Quantifiers. More...
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 |
Quantifiers.
Universally and Existentially quantified formulas.
def as_ast | ( | self | ) |
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.
def get_id | ( | self | ) |
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().
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))