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