Arithmetic. More...

Inheritance diagram for ArithSortRef:

Public Member Functions
def	is_real (self)

def	is_int (self)

def	subsort (self, other)

def	cast (self, val)

Public Member Functions inherited from SortRef
def	as_ast (self)

def	get_id (self)

def	kind (self)

def	subsort (self, other)

def	cast (self, val)

def	name (self)

def	__eq__ (self, other)

def	__ne__ (self, other)

Public Member Functions inherited from AstRef
def	__init__

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)

Public Member Functions inherited from Z3PPObject
def	use_pp (self)

Data Fields
	ctx

Data Fields inherited from AstRef
	ast

	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

Definition at line 1870 of file z3py.py.

     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
         """
         if is_expr(val):
             if __debug__:
                 _z3_assert(self.ctx == val.ctx, "Context mismatch")
             val_s = val.sort()
             if self.eq(val_s):
                 return val
             if val_s.is_int() and self.is_real():
                 return ToReal(val)
             if __debug__:
                 _z3_assert(False, "Z3 Integer/Real expression expected" )
         else:
             if self.is_int():
                 return IntVal(val, self.ctx)
             if self.is_real():
                 return RealVal(val, self.ctx)
             if __debug__:
                 _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().

     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
         """
         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().

     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
         """
         return self.kind() == Z3_REAL_SORT
 

def subsort	(	self,
		other
	)

Return `True` if `self` is a subsort of `other`.

Definition at line 1866 of file z3py.py.

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

Public Member Functions

Data Fields

Detailed Description

Member Function Documentation

Field Documentation