2383 def cast(self, val):
2384 """Try to cast `val` as an Integer or Real.
2385
2386 >>> IntSort().cast(10)
2387 10
2388 >>> is_int(IntSort().cast(10))
2389 True
2390 >>> is_int(10)
2391 False
2392 >>> RealSort().cast(10)
2393 10
2394 >>> is_real(RealSort().cast(10))
2395 True
2396 """
2397 if is_expr(val):
2398 if z3_debug():
2399 _z3_assert(self.ctx == val.ctx, "Context mismatch")
2400 val_s = val.sort()
2401 if self.eq(val_s):
2402 return val
2403 if val_s.is_int() and self.is_real():
2404 return ToReal(val)
2405 if val_s.is_bool() and self.is_int():
2406 return If(val, 1, 0)
2407 if val_s.is_bool() and self.is_real():
2408 return ToReal(If(val, 1, 0))
2409 if z3_debug():
2410 _z3_assert(False, "Z3 Integer/Real expression expected")
2411 else:
2412 if self.is_int():
2413 return IntVal(val, self.ctx)
2414 if self.is_real():
2415 return RealVal(val, self.ctx)
2416 if z3_debug():
2417 msg = "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s"
2418 _z3_assert(False, msg % self)
2419
2420