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 | as_ast |
def | get_id |
def | sort |
def | sort_kind |
def | __eq__ |
def | __hash__ |
def | __ne__ |
def | params |
def | decl |
def | num_args |
def | arg |
def | children |
![]() | |
def | __init__ |
def | __del__ |
def | __deepcopy__ |
def | __str__ |
def | __repr__ |
def | __eq__ |
def | __hash__ |
def | __nonzero__ |
def | __bool__ |
def | sexpr |
def | as_ast |
def | get_id |
def | ctx_ref |
def | eq |
def | translate |
def | __copy__ |
def | hash |
![]() | |
def | use_pp |
Additional Inherited Members | |
![]() | |
ast | |
ctx | |
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 2214 of file z3py.py.
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 2313 of file z3py.py.
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 2447 of file z3py.py.
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 2434 of file z3py.py.
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 2408 of file z3py.py.
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 2421 of file z3py.py.
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 2361 of file z3py.py.
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 2237 of file z3py.py.
def __neg__ | ( | self | ) |
Return an expression representing `-self`. >>> x = Int('x') >>> -x -x >>> simplify(-(-x)) x
Definition at line 2388 of file z3py.py.
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 2285 of file z3py.py.
def __radd__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other + self`. >>> x = Int('x') >>> 10 + x 10 + x
Definition at line 2227 of file z3py.py.
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 2340 of file z3py.py.
def __rmod__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other%self`. >>> x = Int('x') >>> 10 % x 10%x
Definition at line 2376 of file z3py.py.
def __rmul__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other * self`. >>> x = Real('x') >>> 10 * x 10*x
Definition at line 2252 of file z3py.py.
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 2299 of file z3py.py.
def __rsub__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other - self`. >>> x = Int('x') >>> 10 - x 10 - x
Definition at line 2275 of file z3py.py.
def __rtruediv__ | ( | self, | |
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 2262 of file z3py.py.
def __truediv__ | ( | self, | |
other | |||
) |
def is_int | ( | self | ) |
def is_real | ( | self | ) |
def sort | ( | self | ) |
Return the sort (type) of the arithmetical expression `self`. >>> Int('x').sort() Int >>> (Real('x') + 1).sort() Real
Definition at line 2179 of file z3py.py.
Referenced by ArithRef.__add__(), ArithRef.__div__(), ArithRef.__mul__(), ArithRef.__pow__(), ArithRef.__rpow__(), and ArithRef.__sub__().