Public Member Functions | |
def | sort (self) |
def | is_int (self) |
def | is_real (self) |
def | __add__ (self, other) |
def | __radd__ (self, other) |
def | __mul__ (self, other) |
def | __rmul__ (self, other) |
def | __sub__ (self, other) |
def | __rsub__ (self, other) |
def | __pow__ (self, other) |
def | __rpow__ (self, other) |
def | __div__ (self, other) |
def | __truediv__ (self, other) |
def | __rdiv__ (self, other) |
def | __rtruediv__ (self, other) |
def | __mod__ (self, other) |
def | __rmod__ (self, other) |
def | __neg__ (self) |
def | __pos__ (self) |
def | __le__ (self, other) |
def | __lt__ (self, other) |
def | __gt__ (self, other) |
def | __ge__ (self, other) |
![]() | |
def | as_ast (self) |
def | get_id (self) |
def | sort (self) |
def | sort_kind (self) |
def | __eq__ (self, other) |
def | __ne__ (self, other) |
def | decl (self) |
def | num_args (self) |
def | arg (self, idx) |
def | children (self) |
![]() | |
def | __init__ (self, ast, ctx=None) |
def | __del__ (self) |
def | __str__ (self) |
def | __repr__ (self) |
def | sexpr (self) |
def | as_ast (self) |
def | get_id (self) |
def | ctx_ref (self) |
def | eq (self, other) |
def | translate (self, target) |
def | hash (self) |
![]() | |
def | use_pp (self) |
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 1980 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 2077 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 2211 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 2198 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 2172 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 2185 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 2125 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 2003 of file z3py.py.
def __neg__ | ( | self | ) |
Return an expression representing `-self`. >>> x = Int('x') >>> -x -x >>> simplify(-(-x)) x
Definition at line 2152 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 2049 of file z3py.py.
def __radd__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other + self`. >>> x = Int('x') >>> 10 + x 10 + x
Definition at line 1993 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 2104 of file z3py.py.
def __rmod__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other%self`. >>> x = Int('x') >>> 10 % x 10%x
Definition at line 2140 of file z3py.py.
def __rmul__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other * self`. >>> x = Real('x') >>> 10 * x 10*x
Definition at line 2016 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 2063 of file z3py.py.
def __rsub__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other - self`. >>> x = Int('x') >>> 10 - x 10 - x
Definition at line 2039 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 2026 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 1945 of file z3py.py.
Referenced by ArithRef.__add__(), ArithRef.__div__(), ArithRef.__mul__(), ArithRef.__pow__(), ArithRef.__rpow__(), and ArithRef.__sub__().