Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Data Fields
ArithSortRef Class Reference

Arithmetic. More...

+ Inheritance diagram for ArithSortRef:

Public Member Functions

def is_real
def is_int
def subsort
def cast

Data Fields

 ctx

Detailed Description

Arithmetic.

Real and Integer sorts.

Definition at line 1835 of file z3py.py.


Member Function Documentation

def cast (   self,
  val 
)
Try to cast `val` as an Integer or Real.

>>> IntSort().cast(10)
10
>>> is_int(IntSort().cast(10))
True
>>> is_int(10)
False
>>> RealSort().cast(10)
10
>>> is_real(RealSort().cast(10))
True

Reimplemented from SortRef.

Definition at line 1870 of file z3py.py.

01870 
01871     def cast(self, val):
01872         """Try to cast `val` as an Integer or Real.
01873         
01874         >>> IntSort().cast(10)
01875         10
01876         >>> is_int(IntSort().cast(10))
01877         True
01878         >>> is_int(10)
01879         False
01880         >>> RealSort().cast(10)
01881         10
01882         >>> is_real(RealSort().cast(10))
01883         True
01884         """
01885         if is_expr(val):
01886             if __debug__:
01887                 _z3_assert(self.ctx == val.ctx, "Context mismatch")
01888             val_s = val.sort()
01889             if self.eq(val_s):
01890                 return val
01891             if val_s.is_int() and self.is_real():
01892                 return ToReal(val)
01893             if __debug__:
01894                 _z3_assert(False, "Z3 Integer/Real expression expected" )
01895         else:
01896             if self.is_int():
01897                 return IntVal(val, self.ctx)
01898             if self.is_real():
01899                 return RealVal(val, self.ctx)
01900             if __debug__:
01901                 _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected")

def is_int (   self)
Return `True` if `self` is of the sort Integer.

>>> x = Int('x')
>>> x.is_int()
True
>>> (x + 1).is_int()
True
>>> x = Real('x')
>>> x.is_int()
False

Definition at line 1852 of file z3py.py.

Referenced by ArithSortRef.cast().

01852 
01853     def is_int(self):
01854         """Return `True` if `self` is of the sort Integer.
01855         
01856         >>> x = Int('x')
01857         >>> x.is_int()
01858         True
01859         >>> (x + 1).is_int()
01860         True
01861         >>> x = Real('x')
01862         >>> x.is_int()
01863         False
01864         """
01865         return self.kind() == Z3_INT_SORT

def is_real (   self)
Return `True` if `self` is of the sort Real.

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

Definition at line 1838 of file z3py.py.

Referenced by ArithSortRef.cast().

01838 
01839     def is_real(self):
01840         """Return `True` if `self` is of the sort Real.
01841         
01842         >>> x = Real('x')
01843         >>> x.is_real()
01844         True
01845         >>> (x + 1).is_real()
01846         True
01847         >>> x = Int('x')
01848         >>> x.is_real()
01849         False
01850         """
01851         return self.kind() == Z3_REAL_SORT

def subsort (   self,
  other 
)
Return `True` if `self` is a subsort of `other`.

Reimplemented from SortRef.

Definition at line 1866 of file z3py.py.

01866 
01867     def subsort(self, other):
01868         """Return `True` if `self` is a subsort of `other`."""
01869         return self.is_int() and is_arith_sort(other) and other.is_real()


Field Documentation

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