[Mlir-commits] [mlir] [mlir][SMT] upstream `SMT` dialect (PR #131480)

[Fehr Mathieu]

https://github.com/math-fehr approved this pull request.

Very nice! I don't have many comments, especially since was already used for a while in CIRCT.

My only real issue is that `declare_fun` is kind of both `declare-fun` and `declare-const`, in the sense that both `smt.declare_fun : smt.func<() -> int>` and `smt.declare_fun : int` represent the same SMT-LIB operation if I understand correctly? I am not sure if having an `smt.declare` operation that would contain both would be a better idea or not.

https://github.com/llvm/llvm-project/pull/131480