lower-to-smt: Provide a better rewrite pattern mechanism

[math-fehr]

Currently, the OperationSemantics class has the following signature:

    @abstractmethod
    def get_semantics(
        self,
        operands: Sequence[SSAValue],
        results: Sequence[Attribute],
        attributes: Mapping[str, Attribute | SSAValue],
        effect_state: SSAValue | None,
        rewriter: PatternRewriter,
    ) -> tuple[Sequence[SSAValue], SSAValue | None]:
      ...

operands contains the new operands passed to the operation, meaning that the old operands type are now lost.

Instead, our signature sholud probably start with:

op: Operation:
new_operands: Sequence[SSAValue],
new_attributes: Mapping[str, Attribute | SSAValue],

so that all information remain.

Additionally, this would require to keep the old operations alive during the translation process.
This should be done similarly to the conversion patterns in MLIR.