Public Member Functions | |
def | sort |
def | is_int |
def | is_real |
def | __add__ |
def | __radd__ |
def | __mul__ |
def | __rmul__ |
def | __sub__ |
def | __rsub__ |
def | __pow__ |
def | __rpow__ |
def | __div__ |
def | __truediv__ |
def | __rdiv__ |
def | __rtruediv__ |
def | __mod__ |
def | __rmod__ |
def | __neg__ |
def | __pos__ |
def | __le__ |
def | __lt__ |
def | __gt__ |
def | __ge__ |
def __add__ | ( | self, | |
other | |||
) |
Create the Z3 expression `self + other`. >>> x = Int('x') >>> y = Int('y') >>> x + y x + y >>> (x + y).sort() Int
Definition at line 1955 of file z3py.py.
01955 01956 def __add__(self, other): 01957 """Create the Z3 expression `self + other`. 01958 01959 >>> x = Int('x') 01960 >>> y = Int('y') 01961 >>> x + y 01962 x + y 01963 >>> (x + y).sort() 01964 Int 01965 """ 01966 a, b = _coerce_exprs(self, other) 01967 return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx)
def __div__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other/self`. >>> x = Int('x') >>> y = Int('y') >>> x/y x/y >>> (x/y).sort() Int >>> (x/y).sexpr() '(div x y)' >>> x = Real('x') >>> y = Real('y') >>> x/y x/y >>> (x/y).sort() Real >>> (x/y).sexpr() '(/ x y)'
Definition at line 2052 of file z3py.py.
02052 02053 def __div__(self, other): 02054 """Create the Z3 expression `other/self`. 02055 02056 >>> x = Int('x') 02057 >>> y = Int('y') 02058 >>> x/y 02059 x/y 02060 >>> (x/y).sort() 02061 Int 02062 >>> (x/y).sexpr() 02063 '(div x y)' 02064 >>> x = Real('x') 02065 >>> y = Real('y') 02066 >>> x/y 02067 x/y 02068 >>> (x/y).sort() 02069 Real 02070 >>> (x/y).sexpr() 02071 '(/ x y)' 02072 """ 02073 a, b = _coerce_exprs(self, other) 02074 return ArithRef(Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __ge__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other >= self`. >>> x, y = Ints('x y') >>> x >= y x >= y >>> y = Real('y') >>> x >= y ToReal(x) >= y
Definition at line 2186 of file z3py.py.
02186 02187 def __ge__(self, other): 02188 """Create the Z3 expression `other >= self`. 02189 02190 >>> x, y = Ints('x y') 02191 >>> x >= y 02192 x >= y 02193 >>> y = Real('y') 02194 >>> x >= y 02195 ToReal(x) >= y 02196 """ 02197 a, b = _coerce_exprs(self, other) 02198 return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __gt__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other > self`. >>> x, y = Ints('x y') >>> x > y x > y >>> y = Real('y') >>> x > y ToReal(x) > y
Definition at line 2173 of file z3py.py.
02173 02174 def __gt__(self, other): 02175 """Create the Z3 expression `other > self`. 02176 02177 >>> x, y = Ints('x y') 02178 >>> x > y 02179 x > y 02180 >>> y = Real('y') 02181 >>> x > y 02182 ToReal(x) > y 02183 """ 02184 a, b = _coerce_exprs(self, other) 02185 return BoolRef(Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __le__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other <= self`. >>> x, y = Ints('x y') >>> x <= y x <= y >>> y = Real('y') >>> x <= y ToReal(x) <= y
Definition at line 2147 of file z3py.py.
02147 02148 def __le__(self, other): 02149 """Create the Z3 expression `other <= self`. 02150 02151 >>> x, y = Ints('x y') 02152 >>> x <= y 02153 x <= y 02154 >>> y = Real('y') 02155 >>> x <= y 02156 ToReal(x) <= y 02157 """ 02158 a, b = _coerce_exprs(self, other) 02159 return BoolRef(Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __lt__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other < self`. >>> x, y = Ints('x y') >>> x < y x < y >>> y = Real('y') >>> x < y ToReal(x) < y
Definition at line 2160 of file z3py.py.
02160 02161 def __lt__(self, other): 02162 """Create the Z3 expression `other < self`. 02163 02164 >>> x, y = Ints('x y') 02165 >>> x < y 02166 x < y 02167 >>> y = Real('y') 02168 >>> x < y 02169 ToReal(x) < y 02170 """ 02171 a, b = _coerce_exprs(self, other) 02172 return BoolRef(Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __mod__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other%self`. >>> x = Int('x') >>> y = Int('y') >>> x % y x%y >>> simplify(IntVal(10) % IntVal(3)) 1
Definition at line 2100 of file z3py.py.
02100 02101 def __mod__(self, other): 02102 """Create the Z3 expression `other%self`. 02103 02104 >>> x = Int('x') 02105 >>> y = Int('y') 02106 >>> x % y 02107 x%y 02108 >>> simplify(IntVal(10) % IntVal(3)) 02109 1 02110 """ 02111 a, b = _coerce_exprs(self, other) 02112 if __debug__: 02113 _z3_assert(a.is_int(), "Z3 integer expression expected") 02114 return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __mul__ | ( | self, | |
other | |||
) |
Create the Z3 expression `self * other`. >>> x = Real('x') >>> y = Real('y') >>> x * y x*y >>> (x * y).sort() Real
Definition at line 1978 of file z3py.py.
01978 01979 def __mul__(self, other): 01980 """Create the Z3 expression `self * other`. 01981 01982 >>> x = Real('x') 01983 >>> y = Real('y') 01984 >>> x * y 01985 x*y 01986 >>> (x * y).sort() 01987 Real 01988 """ 01989 a, b = _coerce_exprs(self, other) 01990 return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx)
def __neg__ | ( | self | ) |
Return an expression representing `-self`. >>> x = Int('x') >>> -x -x >>> simplify(-(-x)) x
Definition at line 2127 of file z3py.py.
02127 02128 def __neg__(self): 02129 """Return an expression representing `-self`. 02130 02131 >>> x = Int('x') 02132 >>> -x 02133 -x 02134 >>> simplify(-(-x)) 02135 x 02136 """ 02137 return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx)
def __pos__ | ( | self | ) |
def __pow__ | ( | self, | |
other | |||
) |
Create the Z3 expression `self**other` (** is the power operator). >>> x = Real('x') >>> x**3 x**3 >>> (x**3).sort() Real >>> simplify(IntVal(2)**8) 256
Definition at line 2024 of file z3py.py.
02024 02025 def __pow__(self, other): 02026 """Create the Z3 expression `self**other` (** is the power operator). 02027 02028 >>> x = Real('x') 02029 >>> x**3 02030 x**3 02031 >>> (x**3).sort() 02032 Real 02033 >>> simplify(IntVal(2)**8) 02034 256 02035 """ 02036 a, b = _coerce_exprs(self, other) 02037 return ArithRef(Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __radd__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other + self`. >>> x = Int('x') >>> 10 + x 10 + x
def __rdiv__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other/self`. >>> x = Int('x') >>> 10/x 10/x >>> (10/x).sexpr() '(div 10 x)' >>> x = Real('x') >>> 10/x 10/x >>> (10/x).sexpr() '(/ 10.0 x)'
Definition at line 2079 of file z3py.py.
02079 02080 def __rdiv__(self, other): 02081 """Create the Z3 expression `other/self`. 02082 02083 >>> x = Int('x') 02084 >>> 10/x 02085 10/x 02086 >>> (10/x).sexpr() 02087 '(div 10 x)' 02088 >>> x = Real('x') 02089 >>> 10/x 02090 10/x 02091 >>> (10/x).sexpr() 02092 '(/ 10.0 x)' 02093 """ 02094 a, b = _coerce_exprs(self, other) 02095 return ArithRef(Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __rmod__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other%self`. >>> x = Int('x') >>> 10 % x 10%x
Definition at line 2115 of file z3py.py.
02115 02116 def __rmod__(self, other): 02117 """Create the Z3 expression `other%self`. 02118 02119 >>> x = Int('x') 02120 >>> 10 % x 02121 10%x 02122 """ 02123 a, b = _coerce_exprs(self, other) 02124 if __debug__: 02125 _z3_assert(a.is_int(), "Z3 integer expression expected") 02126 return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __rmul__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other * self`. >>> x = Real('x') >>> 10 * x 10*x
def __rpow__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other**self` (** is the power operator). >>> x = Real('x') >>> 2**x 2**x >>> (2**x).sort() Real >>> simplify(2**IntVal(8)) 256
Definition at line 2038 of file z3py.py.
02038 02039 def __rpow__(self, other): 02040 """Create the Z3 expression `other**self` (** is the power operator). 02041 02042 >>> x = Real('x') 02043 >>> 2**x 02044 2**x 02045 >>> (2**x).sort() 02046 Real 02047 >>> simplify(2**IntVal(8)) 02048 256 02049 """ 02050 a, b = _coerce_exprs(self, other) 02051 return ArithRef(Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __rsub__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other - self`. >>> x = Int('x') >>> 10 - x 10 - x
def __rtruediv__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other/self`.
Definition at line 2096 of file z3py.py.
02096 02097 def __rtruediv__(self, other): 02098 """Create the Z3 expression `other/self`.""" 02099 return self.__rdiv__(other)
def __sub__ | ( | self, | |
other | |||
) |
Create the Z3 expression `self - other`. >>> x = Int('x') >>> y = Int('y') >>> x - y x - y >>> (x - y).sort() Int
Definition at line 2001 of file z3py.py.
02001 02002 def __sub__(self, other): 02003 """Create the Z3 expression `self - other`. 02004 02005 >>> x = Int('x') 02006 >>> y = Int('y') 02007 >>> x - y 02008 x - y 02009 >>> (x - y).sort() 02010 Int 02011 """ 02012 a, b = _coerce_exprs(self, other) 02013 return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx)
def __truediv__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other/self`.
Definition at line 2075 of file z3py.py.
02075 02076 def __truediv__(self, other): 02077 """Create the Z3 expression `other/self`.""" 02078 return self.__div__(other)
def is_int | ( | self | ) |
Return `True` if `self` is an integer expression. >>> x = Int('x') >>> x.is_int() True >>> (x + 1).is_int() True >>> y = Real('y') >>> (x + y).is_int() False
def is_real | ( | self | ) |
Return `True` if `self` is an real expression. >>> x = Real('x') >>> x.is_real() True >>> (x + 1).is_real() True
def sort | ( | self | ) |
Return the sort (type) of the arithmetical expression `self`. >>> Int('x').sort() Int >>> (Real('x') + 1).sort() Real
Reimplemented from ExprRef.
Definition at line 1920 of file z3py.py.
Referenced by ArithRef.__add__(), ArithRef.__div__(), ArithRef.__mul__(), ArithRef.__pow__(), ArithRef.__rpow__(), ArithRef.__sub__(), ArrayRef.domain(), ArithRef.is_int(), ArithRef.is_real(), and ArrayRef.range().
01920 01921 def sort(self): 01922 """Return the sort (type) of the arithmetical expression `self`. 01923 01924 >>> Int('x').sort() 01925 Int 01926 >>> (Real('x') + 1).sort() 01927 Real 01928 """ 01929 return ArithSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)