ArithSortRef Class Reference

Arithmetic. More...

Inheritance diagram for ArithSortRef:

Public Member Functions
def	is_real (self)
def	is_int (self)
def	is_bool (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)
def	__gt__ (self, other)
def	__hash__ (self)
Public Member Functions inherited from AstRef
def	__init__
def	__del__ (self)
def	__deepcopy__
def	__str__ (self)
def	__repr__ (self)
def	__eq__ (self, other)
def	__hash__ (self)
def	__nonzero__ (self)
def	__bool__ (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	__copy__ (self)
def	hash (self)
def	py_value (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 2431 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 2469 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 z3_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 z3_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 z3_debug():
                msg = "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s"
                _z3_assert(False, msg % self)

def is_bool

(

self

)

Definition at line 2462 of file z3py.py.

    def is_bool(self):
        return False

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 2448 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 2434 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 2465 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()

Field Documentation

ctx

Definition at line 2485 of file z3py.py.

Referenced by Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Simplifier.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Simplifier.add(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Optimize.assert_and_track(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), ParserContext.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Optimize.model(), Optimize.objectives(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Simplifier.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.query(), Fixedpoint.set(), Optimize.set(), Optimize.set_on_model(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Optimize.unsat_core(), Fixedpoint.update_rule(), and Simplifier.using_params().