Arithmetic expression (Int, Nat, Real).
| 431 | |
| 432 | |
| 433 | class ArithRef(ExprRef): |
| 434 | """Arithmetic expression (Int, Nat, Real).""" |
| 435 | |
| 436 | __slots__ = () |
| 437 | |
| 438 | def __init__( |
| 439 | self, |
| 440 | ast: ASTNode, |
| 441 | sort: ArithSortRef, |
| 442 | vars: frozenset[tuple[str, ASTSort]] = frozenset(), |
| 443 | ) -> None: |
| 444 | super().__init__(ast, sort, vars) |
| 445 | |
| 446 | def _binop(self, op: str, other: ArithRef | int | float) -> ArithRef: |
| 447 | other = _coerce_arith(other, self._sort) |
| 448 | return ArithRef( |
| 449 | BinOpNode(op, self._ast, other._ast), |
| 450 | self._sort, # type: ignore[arg-type] |
| 451 | _merge(self._vars, other._vars), |
| 452 | ) |
| 453 | |
| 454 | def __add__(self, other: ArithRef | int | float) -> ArithRef: |
| 455 | return self._binop(BinOp.ADD, other) |
| 456 | |
| 457 | def __radd__(self, other: int | float) -> ArithRef: |
| 458 | return _coerce_arith(other, self._sort)._binop(BinOp.ADD, self) |
| 459 | |
| 460 | def __sub__(self, other: ArithRef | int | float) -> ArithRef: |
| 461 | return self._binop(BinOp.SUB, other) |
| 462 | |
| 463 | def __rsub__(self, other: int | float) -> ArithRef: |
| 464 | return _coerce_arith(other, self._sort)._binop(BinOp.SUB, self) |
| 465 | |
| 466 | def __mul__(self, other: ArithRef | int | float) -> ArithRef: |
| 467 | return self._binop(BinOp.MUL, other) |
| 468 | |
| 469 | def __rmul__(self, other: int | float) -> ArithRef: |
| 470 | return _coerce_arith(other, self._sort)._binop(BinOp.MUL, self) |
| 471 | |
| 472 | def __truediv__(self, other: ArithRef | int | float) -> ArithRef: |
| 473 | # Int uses Euclidean div (SMT-LIB), Real uses normal div |
| 474 | op = BinOp.EDIV if isinstance(self._sort._ast_sort, IntASTSort) else BinOp.DIV |
| 475 | return self._binop(op, other) |
| 476 | |
| 477 | def __mod__(self, other: ArithRef | int | float) -> ArithRef: |
| 478 | # Int uses Euclidean mod (SMT-LIB), Real uses normal mod |
| 479 | op = BinOp.EMOD if isinstance(self._sort._ast_sort, IntASTSort) else BinOp.MOD |
| 480 | return self._binop(op, other) |
| 481 | |
| 482 | def __rtruediv__(self, other: int | float) -> ArithRef: |
| 483 | op = BinOp.EDIV if isinstance(self._sort._ast_sort, IntASTSort) else BinOp.DIV |
| 484 | return _coerce_arith(other, self._sort)._binop(op, self) |
| 485 | |
| 486 | def __rmod__(self, other: int | float) -> ArithRef: |
| 487 | op = BinOp.EMOD if isinstance(self._sort._ast_sort, IntASTSort) else BinOp.MOD |
| 488 | return _coerce_arith(other, self._sort)._binop(op, self) |
| 489 | |
| 490 | def __pow__(self, other: ArithRef | int | float) -> ArithRef: |
no outgoing calls
no test coverage detected