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

[llvmlistbot at llvm.org]

Hatsunespica wrote:

Hi! This is Yuyou. Thanks for the great PR!

I carefully checked operations in SMTBitVectors.
I found we have custom verifiers for ExtractOp and RepeatOp. I checked them with verifiers in the comb dialect and they look good.

Do you think we should have a verifier for ConcatOp as well? To make sure that the result width is equal to the sum of all input widths. 
Here is the verifier from the comb dialect, and the ConcatOp in the comd dialect also has "inferReturnTypes" as we did.
https://github.com/llvm/circt/blob/main/lib/Dialect/Comb/CombOps.cpp#L300


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