A dialect that models satisfiability modulo theories Operations smt.and (mlir::smt::AndOp) smt.apply_func (mlir::smt::ApplyFuncOp) smt.array.broadcast (mlir::smt::ArrayBroadcastOp) smt.array.select (mlir::smt::ArraySelectOp) smt.array.store (mlir::smt::ArrayStoreOp) smt.assert (mlir::smt::AssertOp) smt.bv.add (mlir::smt::BVAddOp) smt.bv.and (mlir::smt::BVAndOp) smt.bv.ashr (mlir::smt::BVAShrOp) smt.bv.cmp (mlir::smt::BVCmpOp) smt.bv.concat (mlir::smt::ConcatOp) smt.bv.constant (mlir::smt::BVC...