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 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 __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)
 
- 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 2338 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 2376 of file z3py.py.

2376  def cast(self, val):
2377  """Try to cast `val` as an Integer or Real.
2378 
2379  >>> IntSort().cast(10)
2380  10
2381  >>> is_int(IntSort().cast(10))
2382  True
2383  >>> is_int(10)
2384  False
2385  >>> RealSort().cast(10)
2386  10
2387  >>> is_real(RealSort().cast(10))
2388  True
2389  """
2390  if is_expr(val):
2391  if z3_debug():
2392  _z3_assert(self.ctx == val.ctx, "Context mismatch")
2393  val_s = val.sort()
2394  if self.eq(val_s):
2395  return val
2396  if val_s.is_int() and self.is_real():
2397  return ToReal(val)
2398  if val_s.is_bool() and self.is_int():
2399  return If(val, 1, 0)
2400  if val_s.is_bool() and self.is_real():
2401  return ToReal(If(val, 1, 0))
2402  if z3_debug():
2403  _z3_assert(False, "Z3 Integer/Real expression expected")
2404  else:
2405  if self.is_int():
2406  return IntVal(val, self.ctx)
2407  if self.is_real():
2408  return RealVal(val, self.ctx)
2409  if z3_debug():
2410  msg = "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s"
2411  _z3_assert(False, msg % self)
2412 
2413 
def is_int(self)
Definition: z3py.py:2355
def If
Definition: z3py.py:1399
def is_real(self)
Definition: z3py.py:2341
def eq(self, other)
Definition: z3py.py:404
def ToReal(a)
Definition: z3py.py:3404
def z3_debug()
Definition: z3py.py:62
def cast(self, val)
Definition: z3py.py:2376
def RealVal
Definition: z3py.py:3246
def is_expr(a)
Definition: z3py.py:1260
def IntVal
Definition: z3py.py:3234
def is_bool (   self)

Definition at line 2369 of file z3py.py.

2369  def is_bool(self):
2370  return False
2371 
def is_bool(self)
Definition: z3py.py:2369
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 2355 of file z3py.py.

Referenced by ArithSortRef.cast().

2355  def is_int(self):
2356  """Return `True` if `self` is of the sort Integer.
2357 
2358  >>> x = Int('x')
2359  >>> x.is_int()
2360  True
2361  >>> (x + 1).is_int()
2362  True
2363  >>> x = Real('x')
2364  >>> x.is_int()
2365  False
2366  """
2367  return self.kind() == Z3_INT_SORT
2368 
def is_int(self)
Definition: z3py.py:2355
def kind(self)
Definition: z3py.py:568
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 2341 of file z3py.py.

Referenced by ArithSortRef.cast().

2341  def is_real(self):
2342  """Return `True` if `self` is of the sort Real.
2343 
2344  >>> x = Real('x')
2345  >>> x.is_real()
2346  True
2347  >>> (x + 1).is_real()
2348  True
2349  >>> x = Int('x')
2350  >>> x.is_real()
2351  False
2352  """
2353  return self.kind() == Z3_REAL_SORT
2354 
def is_real(self)
Definition: z3py.py:2341
def kind(self)
Definition: z3py.py:568
def subsort (   self,
  other 
)
Return `True` if `self` is a subsort of `other`.

Definition at line 2372 of file z3py.py.

2372  def subsort(self, other):
2373  """Return `True` if `self` is a subsort of `other`."""
2374  return self.is_int() and is_arith_sort(other) and other.is_real()
2375 
def is_arith_sort(s)
Definition: z3py.py:2414
def is_int(self)
Definition: z3py.py:2355
def subsort(self, other)
Definition: z3py.py:2372

Field Documentation

ctx