[Tuner][Codegen] Add iree_codegen.constraints op and supporting infra

[kuhar]

Today, the tuner has to know a lot about the IREE compiler and its compilation pipelines, including what inputs they can compile, their configuration space, their lowering_config format, etc. This is partially encoded directly as Python logic and partially exposed through Python bindings. We want to move this to the compiler instead.

The constraints op encodes pipeline constraints over one or more root ops and can later be lowered to SMT-LIB for solving by the tuner, or verified against the selected lowering_config after dispatch configuration. See the discussion for the full proposal: #23521

Key design decisions:

• The (bidirectional) mapping from root ops to their constraints is based on root op sets: [Tuner][Codegen] Add set identifier to root op attributes #23536 to allow for root ops that return zero or many values.
• The knobs dict structurally mirrors the lowering_config / translation_info attributes, with tunable leaves as #iree_codegen.int_knob<"name">. This makes it possible for the tuner to mechanically substitute solved knob values back into concrete attributes without understanding their structure.
• Problem dimensions come in as index operands (from tensor.dim / constants), so that static sizes get constant-folded into the SMT body and dynamic shapes remain symbolic.
• The body uses upstream SMT dialect ops, so that we can directly export to SMT-LIB without a custom lowering.
• Pipeline attr accepts both DispatchLoweringPassPipelineAttr and the new PipelineAttrInterface ([Codegen] Add PipelineAttrInterface and PassPipelineAttr #23590) to support custom pipelines.

Issue: #23535

[amd-eochoalo]

Is part of the implementation still missing? I know that none of these ops will be lowered, instead they are used by the tuner, but I'm a little bit curious where the tuner code that uses these knobs is. Is it on a different repo?

[kuhar]

Is part of the implementation still missing? I know that none of these ops will be lowered, instead they are used by the tuner, but I'm a little bit curious where the tuner code that uses these knobs is. Is it on a different repo?

I'm landing piecewise to limit the PR size. There are no consumers as of now. Check the discussion in the PR description for the e2e prototype.

[amd-eochoalo]

I still need a bit of time to review the overall design a bit more, but this PR looks good.

I was thinking about suggesting a different target that includes the SMT dialect (since it is only useful for the tuner), but I think keeping the build system simple where the cost is only linking against the SMT dialect is a good trade off.

[kuhar]

I was thinking about suggesting a different target that includes the SMT dialect (since it is only useful for the tuner),

The plan is to also use it for verification after the usual compilation path decides the lowering config. But even if we did move it to a new target, I'm not sure what the benefit would be since everything is statically linked anyway.