| 1141 | |
| 1142 | |
| 1143 | def RealVal(n: int | float | str) -> ArithRef: |
| 1144 | if isinstance(n, float): |
| 1145 | num, den = n.as_integer_ratio() |
| 1146 | return RatNumRef(num, den) |
| 1147 | if isinstance(n, str): |
| 1148 | if "/" in n: |
| 1149 | num_s, den_s = n.split("/", 1) |
| 1150 | return RatNumRef(int(num_s.strip()), int(den_s.strip())) |
| 1151 | coerced: int | float = float(n) if "." in n or "e" in n.lower() else int(n) |
| 1152 | return RealVal(coerced) |
| 1153 | return ArithRef(ToRealNode(IntLit(n)), RealSort()) |
| 1154 | |
| 1155 | |
| 1156 | def BoolVal(b: bool) -> BoolRef: |