Z3
Public Member Functions | Data Fields
ArithSortRef Class Reference

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)
 
def __hash__ (self)
 
- Public Member Functions inherited from AstRef
def __init__ (self, ast, ctx=None)
 
def __del__ (self)
 
def __deepcopy__ (self, memo={})
 
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)
 
- 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 2090 of file z3py.py.

Member Function Documentation

◆ cast()

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 2125 of file z3py.py.

2125  def cast(self, val):
2126  """Try to cast `val` as an Integer or Real.
2127 
2128  >>> IntSort().cast(10)
2129  10
2130  >>> is_int(IntSort().cast(10))
2131  True
2132  >>> is_int(10)
2133  False
2134  >>> RealSort().cast(10)
2135  10
2136  >>> is_real(RealSort().cast(10))
2137  True
2138  """
2139  if is_expr(val):
2140  if z3_debug():
2141  _z3_assert(self.ctx == val.ctx, "Context mismatch")
2142  val_s = val.sort()
2143  if self.eq(val_s):
2144  return val
2145  if val_s.is_int() and self.is_real():
2146  return ToReal(val)
2147  if val_s.is_bool() and self.is_int():
2148  return If(val, 1, 0)
2149  if val_s.is_bool() and self.is_real():
2150  return ToReal(If(val, 1, 0))
2151  if z3_debug():
2152  _z3_assert(False, "Z3 Integer/Real expression expected" )
2153  else:
2154  if self.is_int():
2155  return IntVal(val, self.ctx)
2156  if self.is_real():
2157  return RealVal(val, self.ctx)
2158  if z3_debug():
2159  _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s" % self)
2160 
def IntVal(val, ctx=None)
Definition: z3py.py:2937
def If(a, b, c, ctx=None)
Definition: z3py.py:1238
def RealVal(val, ctx=None)
Definition: z3py.py:2948
def ToReal(a)
Definition: z3py.py:3093
def z3_debug()
Definition: z3py.py:58
def is_expr(a)
Definition: z3py.py:1105

◆ is_int()

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 2107 of file z3py.py.

Referenced by ArithSortRef.cast().

2107  def is_int(self):
2108  """Return `True` if `self` is of the sort Integer.
2109 
2110  >>> x = Int('x')
2111  >>> x.is_int()
2112  True
2113  >>> (x + 1).is_int()
2114  True
2115  >>> x = Real('x')
2116  >>> x.is_int()
2117  False
2118  """
2119  return self.kind() == Z3_INT_SORT
2120 
def is_int(a)
Definition: z3py.py:2480

◆ is_real()

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 2093 of file z3py.py.

Referenced by ArithSortRef.cast().

2093  def is_real(self):
2094  """Return `True` if `self` is of the sort Real.
2095 
2096  >>> x = Real('x')
2097  >>> x.is_real()
2098  True
2099  >>> (x + 1).is_real()
2100  True
2101  >>> x = Int('x')
2102  >>> x.is_real()
2103  False
2104  """
2105  return self.kind() == Z3_REAL_SORT
2106 
def is_real(a)
Definition: z3py.py:2498

◆ subsort()

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

Definition at line 2121 of file z3py.py.

2121  def subsort(self, other):
2122  """Return `True` if `self` is a subsort of `other`."""
2123  return self.is_int() and is_arith_sort(other) and other.is_real()
2124 
def is_arith_sort(s)
Definition: z3py.py:2161

Field Documentation

◆ ctx

ctx

Definition at line 2141 of file z3py.py.

Referenced by Probe.__call__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), ApplyResult.__len__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Optimize.assert_and_track(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), Optimize.check(), Optimize.from_file(), Optimize.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Optimize.maximize(), Optimize.minimize(), Optimize.model(), Optimize.objectives(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Optimize.pop(), Optimize.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), Fixedpoint.register_relation(), Fixedpoint.set(), Optimize.set(), Fixedpoint.set_predicate_representation(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.to_string(), Optimize.unsat_core(), and Fixedpoint.update_rule().