Expressions. More...
Public Member Functions | |
def | as_ast |
def | get_id |
def | sort |
def | sort_kind |
def | __eq__ |
def | __ne__ |
def | decl |
def | num_args |
def | arg |
def | children |
Expressions.
Constraints, formulas and terms are expressions in Z3. Expressions are ASTs. Every expression has a sort. There are three main kinds of expressions: function applications, quantifiers and bounded variables. A constant is a function application with 0 arguments. For quantifier free problems, all expressions are function applications.
def __eq__ | ( | self, | |
other | |||
) |
Return a Z3 expression that represents the constraint `self == other`. If `other` is `None`, then this method simply returns `False`. >>> a = Int('a') >>> b = Int('b') >>> a == b a == b >>> a == None False
Definition at line 771 of file z3py.py.
Referenced by Probe.__ne__().
00771 00772 def __eq__(self, other): 00773 """Return a Z3 expression that represents the constraint `self == other`. 00774 00775 If `other` is `None`, then this method simply returns `False`. 00776 00777 >>> a = Int('a') 00778 >>> b = Int('b') 00779 >>> a == b 00780 a == b 00781 >>> a == None 00782 False 00783 """ 00784 if other == None: 00785 return False 00786 a, b = _coerce_exprs(self, other) 00787 return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __ne__ | ( | self, | |
other | |||
) |
Return a Z3 expression that represents the constraint `self != other`. If `other` is `None`, then this method simply returns `True`. >>> a = Int('a') >>> b = Int('b') >>> a != b a != b >>> a != None True
Definition at line 788 of file z3py.py.
00788 00789 def __ne__(self, other): 00790 """Return a Z3 expression that represents the constraint `self != other`. 00791 00792 If `other` is `None`, then this method simply returns `True`. 00793 00794 >>> a = Int('a') 00795 >>> b = Int('b') 00796 >>> a != b 00797 a != b 00798 >>> a != None 00799 True 00800 """ 00801 if other == None: 00802 return True 00803 a, b = _coerce_exprs(self, other) 00804 _args, sz = _to_ast_array((a, b)) 00805 return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)
def arg | ( | self, | |
idx | |||
) |
Return argument `idx` of the application `self`. This method assumes that `self` is a function application with at least `idx+1` arguments. >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.arg(0) a >>> t.arg(1) b >>> t.arg(2) 0
Definition at line 837 of file z3py.py.
Referenced by ExprRef.children().
00837 00838 def arg(self, idx): 00839 """Return argument `idx` of the application `self`. 00840 00841 This method assumes that `self` is a function application with at least `idx+1` arguments. 00842 00843 >>> a = Int('a') 00844 >>> b = Int('b') 00845 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 00846 >>> t = f(a, b, 0) 00847 >>> t.arg(0) 00848 a 00849 >>> t.arg(1) 00850 b 00851 >>> t.arg(2) 00852 0 00853 """ 00854 if __debug__: 00855 _z3_assert(is_app(self), "Z3 application expected") 00856 _z3_assert(idx < self.num_args(), "Invalid argument index") 00857 return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx)
def as_ast | ( | self | ) |
Return a pointer to the corresponding C Z3_ast object.
Reimplemented from AstRef.
Reimplemented in QuantifierRef, and PatternRef.
Definition at line 742 of file z3py.py.
Referenced by ExprRef.arg(), ExprRef.decl(), ExprRef.get_id(), ExprRef.num_args(), ExprRef.sort(), and BoolRef.sort().
def children | ( | self | ) |
Return a list containing the children of the given expression >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.children() [a, b, 0]
Reimplemented in QuantifierRef.
Definition at line 858 of file z3py.py.
00858 00859 def children(self): 00860 """Return a list containing the children of the given expression 00861 00862 >>> a = Int('a') 00863 >>> b = Int('b') 00864 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 00865 >>> t = f(a, b, 0) 00866 >>> t.children() 00867 [a, b, 0] 00868 """ 00869 if is_app(self): 00870 return [self.arg(i) for i in range(self.num_args())] 00871 else: 00872 return []
def decl | ( | self | ) |
Return the Z3 function declaration associated with a Z3 application. >>> f = Function('f', IntSort(), IntSort()) >>> a = Int('a') >>> t = f(a) >>> eq(t.decl(), f) True >>> (a + 1).decl() +
Definition at line 806 of file z3py.py.
00806 00807 def decl(self): 00808 """Return the Z3 function declaration associated with a Z3 application. 00809 00810 >>> f = Function('f', IntSort(), IntSort()) 00811 >>> a = Int('a') 00812 >>> t = f(a) 00813 >>> eq(t.decl(), f) 00814 True 00815 >>> (a + 1).decl() 00816 + 00817 """ 00818 if __debug__: 00819 _z3_assert(is_app(self), "Z3 application expected") 00820 return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx)
def get_id | ( | self | ) |
Return unique identifier for object. It can be used for hash-tables and maps.
Reimplemented from AstRef.
Reimplemented in QuantifierRef, and PatternRef.
Definition at line 745 of file z3py.py.
00745 00746 def get_id(self): 00747 return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
def num_args | ( | self | ) |
Return the number of arguments of a Z3 application. >>> a = Int('a') >>> b = Int('b') >>> (a + b).num_args() 2 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.num_args() 3
Definition at line 821 of file z3py.py.
Referenced by ExprRef.arg(), and ExprRef.children().
00821 00822 def num_args(self): 00823 """Return the number of arguments of a Z3 application. 00824 00825 >>> a = Int('a') 00826 >>> b = Int('b') 00827 >>> (a + b).num_args() 00828 2 00829 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 00830 >>> t = f(a, b, 0) 00831 >>> t.num_args() 00832 3 00833 """ 00834 if __debug__: 00835 _z3_assert(is_app(self), "Z3 application expected") 00836 return int(Z3_get_app_num_args(self.ctx_ref(), self.as_ast()))
def sort | ( | self | ) |
Return the sort of expression `self`. >>> x = Int('x') >>> (x + 1).sort() Int >>> y = Real('y') >>> (x + y).sort() Real
Reimplemented in DatatypeRef, ArrayRef, BitVecRef, ArithRef, QuantifierRef, and BoolRef.
Definition at line 748 of file z3py.py.
Referenced by ArrayRef.domain(), ArrayRef.range(), and ExprRef.sort_kind().
def sort_kind | ( | self | ) |
Shorthand for `self.sort().kind()`. >>> a = Array('a', IntSort(), IntSort()) >>> a.sort_kind() == Z3_ARRAY_SORT True >>> a.sort_kind() == Z3_INT_SORT False