ArithSortRef Class Reference

Arithmetic. More...

Inheritance diagram for ArithSortRef:

Public Member Functions
def	is_real
def	is_int
def	subsort
def	cast
Public Member Functions inherited from SortRef
def	as_ast
def	get_id
def	kind
def	subsort
def	cast
def	name
def	__eq__
def	__ne__
Public Member Functions inherited from AstRef
def	__init__
def	__del__
def	__str__
def	__repr__
def	sexpr
def	as_ast
def	get_id
def	ctx_ref
def	eq
def	translate
def	hash
Public Member Functions inherited from Z3PPObject
def	use_pp

Data Fields
	ctx
Data Fields inherited from AstRef
	ast
	ctx

Detailed Description

Arithmetic.

Real and Integer sorts.

Definition at line 1856 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 1891 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 val_s.is_bool() and self.is_int():
                return If(val, 1, 0)
            if val_s.is_bool() and self.is_real():
                return ToReal(If(val, 1, 0))
            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")