Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions
ArithRef Class Reference
+ Inheritance diagram for ArithRef:

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__

Detailed Description

Integer and Real expressions.

Definition at line 1917 of file z3py.py.


Member Function Documentation

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)
Return `self`.

>>> x = Int('x')
>>> +x
x

Definition at line 2138 of file z3py.py.

02138 
02139     def __pos__(self):
02140         """Return `self`.
02141         
02142         >>> x = Int('x')
02143         >>> +x
02144         x
02145         """
02146         return 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

Definition at line 1968 of file z3py.py.

01968 
01969     def __radd__(self, other):
01970         """Create the Z3 expression `other + self`.
01971         
01972         >>> x = Int('x')
01973         >>> 10 + x
01974         10 + x
01975         """
01976         a, b = _coerce_exprs(self, other)
01977         return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx)

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

Definition at line 1991 of file z3py.py.

01991 
01992     def __rmul__(self, other):
01993         """Create the Z3 expression `other * self`.
01994         
01995         >>> x = Real('x')
01996         >>> 10 * x
01997         10*x
01998         """
01999         a, b = _coerce_exprs(self, other)
02000         return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx)

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

Definition at line 2014 of file z3py.py.

02014 
02015     def __rsub__(self, other):
02016         """Create the Z3 expression `other - self`.
02017         
02018         >>> x = Int('x')
02019         >>> 10 - x
02020         10 - x
02021         """
02022         a, b = _coerce_exprs(self, other)
02023         return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx)

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

Definition at line 1930 of file z3py.py.

01930 
01931     def is_int(self):
01932         """Return `True` if `self` is an integer expression.
01933         
01934         >>> x = Int('x')
01935         >>> x.is_int()
01936         True
01937         >>> (x + 1).is_int()
01938         True
01939         >>> y = Real('y')
01940         >>> (x + y).is_int()
01941         False
01942         """
01943         return self.sort().is_int()

def is_real (   self)
Return `True` if `self` is an real expression.

>>> x = Real('x')
>>> x.is_real()
True
>>> (x + 1).is_real()
True

Definition at line 1944 of file z3py.py.

01944 
01945     def is_real(self):
01946         """Return `True` if `self` is an real expression.
01947         
01948         >>> x = Real('x')
01949         >>> x.is_real()
01950         True
01951         >>> (x + 1).is_real()
01952         True
01953         """
01954         return self.sort().is_real()

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)

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines