(self, other: object)
| 301 | return _ast_repr(self._ast) |
| 302 | |
| 303 | def __eq__(self, other: object) -> BoolRef: # type: ignore[override] |
| 304 | if isinstance(other, (int, float)): |
| 305 | other = _coerce_val(other, self._sort) |
| 306 | if not isinstance(other, ExprRef): |
| 307 | return NotImplemented |
| 308 | # Normalize: put non-literal args on the left. Python's reflected |
| 309 | # comparison protocol can swap self/other when one type is a subclass |
| 310 | # of the other (e.g. IntNumRef subclasses ArithRef), leading to |
| 311 | # "5 = x + 3" instead of "x + 3 = 5". We canonicalize by putting |
| 312 | # literal/value AST nodes on the RHS so tactics see the natural order. |
| 313 | lhs, rhs = self._ast, other._ast |
| 314 | if _is_literal(lhs) and not _is_literal(rhs): |
| 315 | lhs, rhs = rhs, lhs |
| 316 | return BoolRef( |
| 317 | BinOpNode(BinOp.EQ, lhs, rhs), |
| 318 | _merge(self._vars, other._vars), |
| 319 | ) |
| 320 | |
| 321 | def __ne__(self, other: object) -> BoolRef: # type: ignore[override] |
| 322 | if isinstance(other, (int, float)): |
nothing calls this directly
no test coverage detected