source

transform.smt.constrain_params ( mlir::transform::smt ::ConstrainParamsOp) ¶

Express contraints on params interpreted as symbolic values

Syntax:

operation ::= `transform.smt.constrain_params` `(` $params `)` attr-dict `:` type(operands) $body

Allows expressing constraints on params using the SMT dialect.

Each Transform dialect param provided as an operand has a corresponding argument of SMT-type in the region. The SMT-Dialect ops in the region use these arguments as operands.

The semantics of this op is that all the ops in the region together express a constraint on the params-interpreted-as-smt-vars. The op fails in case the expressed constraint is not satisfiable per SMTLIB semantics. Otherwise the op succeeds.

TODO: currently the operational semantics per the Transform interpreter is to always fail. The intention is build out support for hooking in your own operational semantics so you can invoke your favourite solver to determine satisfiability of the corresponding constraint problem.

Traits: NoTerminator

Interfaces: MemoryEffectOpInterface, TransformOpInterface

Operands: ¶