2398 def cast(self, val):
2399 """Try to cast `val` as an Integer or Real.
2400
2401 >>> IntSort().cast(10)
2402 10
2403 >>> is_int(IntSort().cast(10))
2404 True
2405 >>> is_int(10)
2406 False
2407 >>> RealSort().cast(10)
2408 10
2409 >>> is_real(RealSort().cast(10))
2410 True
2411 """
2412 if is_expr(val):
2413 if z3_debug():
2414 _z3_assert(self.ctx == val.ctx, "Context mismatch")
2415 val_s = val.sort()
2416 if self.eq(val_s):
2417 return val
2418 if val_s.is_int() and self.is_real():
2419 return ToReal(val)
2420 if val_s.is_bool() and self.is_int():
2421 return If(val, 1, 0)
2422 if val_s.is_bool() and self.is_real():
2423 return ToReal(If(val, 1, 0))
2424 if z3_debug():
2425 _z3_assert(False, "Z3 Integer/Real expression expected")
2426 else:
2427 if self.is_int():
2428 return IntVal(val, self.ctx)
2429 if self.is_real():
2430 return RealVal(val, self.ctx)
2431 if z3_debug():
2432 msg = "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s"
2433 _z3_assert(False, msg % self)
2434
2435