| 1347 | |
| 1348 | |
| 1349 | def If(c: BoolRef, t: ExprRef, e: ExprRef) -> ExprRef: |
| 1350 | merged: frozenset[tuple[str, ASTSort]] = frozenset().union(c._vars, t._vars, e._vars) |
| 1351 | ast = IteNode(c._ast, t._ast, e._ast) |
| 1352 | sort = t._sort |
| 1353 | # Return the appropriate subclass so arithmetic/comparison ops work |
| 1354 | if isinstance(t, ArithRef): |
| 1355 | return ArithRef(ast, sort, merged) # type: ignore[arg-type] |
| 1356 | if isinstance(t, BitVecRef): |
| 1357 | return BitVecRef(ast, sort, merged) # type: ignore[arg-type] |
| 1358 | if isinstance(t, BoolRef): |
| 1359 | return BoolRef(ast, merged) |
| 1360 | return ExprRef(ast, sort, merged) |
| 1361 | |
| 1362 | |
| 1363 | def Distinct(*args: ExprRef) -> BoolRef: |