[SMT] Add Z3 lowering for set_logic op

[TaoBi22]

Slightly more complicated than this would ideally be because Z3 handles different logics with a separate solver constructor rather than as a function to be called on the solver.

[uenoku]

Z3 with a separate solver constructor rather than as a function to be called on the solver.

I believe most solvers would treat set-logic in such as way. I'm curios if it makes sense to add optional logic attribute to smt.solver op 🤔

[TaoBi22]

I'm curios if it makes sense to add optional logic attribute to smt.solver op 🤔

We thought the same, but decided that we should probably use SMTLIB as the golden reference - agreed that most solvers probably only support it as a one-off, but it would be a shame not to support functionality that some solvers could have

[maerhart]

Should we add an integration test for Z3 set-logic?

[TaoBi22]

Should we add an integration test for Z3 set-logic?

Not sure what you mean, there's an integration test for the Z3 export added in integration_test/Dialect/SMT/basic.mlir?

[maerhart]

Not sure what you mean, there's an integration test for the Z3 export added in integration_test/Dialect/SMT/basic.mlir?

Oh sorry, I overlooked that one.

[maerhart]

LGTM!

[TaoBi22]

Thanks!