Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Public Member Functions | Data Fields
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__
 
def __hash__
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__
 
def __deepcopy__
 
def __str__
 
def __repr__
 
def __eq__
 
def __hash__
 
def __nonzero__
 
def __bool__
 
def sexpr
 
def as_ast
 
def get_id
 
def ctx_ref
 
def eq
 
def translate
 
def __copy__
 
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 2090 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 2125 of file z3py.py.

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

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

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

Definition at line 2121 of file z3py.py.

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

Field Documentation

ctx

Definition at line 2141 of file z3py.py.

Referenced by Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Optimize.assert_and_track(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), 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(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.query(), Fixedpoint.set(), Optimize.set(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Optimize.unsat_core(), and Fixedpoint.update_rule().