mlir.dialects.transform.smt¶

Classes¶

`Type`
`Block`
`ConstrainParamsOp`	Allows expressing constraints on params using the SMT dialect.
`ConstrainParamsOpAdaptor`
`ConstrainParamsOp`	Allows expressing constraints on params using the SMT dialect.

Functions¶

`smt_constrain_params`(→ Union[_ods_ir, _ods_ir, ...)
`constrain_params`(results, params, arg_types[, loc, ip])

Module Contents¶

class mlir.dialects.transform.smt.Type(cast_from_type: Type)¶

property _CAPIPtr: object¶: Gets a capsule wrapping the MlirType.

static _CAPICreate(arg: object, /) → Type¶: Creates a Type from a capsule wrapping MlirType.

static parse(asm: str, context: Context | None = None) → Type¶

Parses the assembly form of a type.

Returns a Type object or raises an MLIRError if the type cannot be parsed.

property context: Context¶: Context that owns the Type.

__eq__(arg: Type, /) → bool¶
__eq__(other: object | None) → bool: Compares type with non-type object (always returns False).

__hash__() → int¶: Returns the hash value of the Type.

dump() → None¶: Dumps a debug representation of the object to stderr.

__str__() → str¶: Returns the assembly form of the Type.

__repr__() → str¶: Returns a string representation of the Type.

maybe_downcast() → Type¶: Downcasts the Type to a more specific Type if possible.

property typeid: TypeID¶: Returns the TypeID of the Type, or raises ValueError if Type has no TypeID.

class mlir.dialects.transform.smt.Block¶

property _CAPIPtr: object¶: Gets a capsule wrapping the MlirBlock.

property owner: OpView¶: Returns the owning operation of this block.

property region: Region¶: Returns the owning region of this block.

property arguments: BlockArgumentList¶: Returns a list of block arguments.

add_argument(type: Type, loc: Location) → BlockArgument¶

Appends an argument of the specified type to the block.

Parameters:

type – The type of the argument to add.
loc – The source location for the argument.

Returns:

The newly added block argument.

erase_argument(index: int) → None¶

Erases the argument at the specified index.

Parameters:: index – The index of the argument to erase.

property operations: OperationList¶: Returns a forward-optimized sequence of operations.

static create_at_start(parent: Region, arg_types: collections.abc.Sequence[Type] = [], arg_locs: collections.abc.Sequence[Location] | None = None) → Block¶: Creates and returns a new Block at the beginning of the given region (with given argument types and locations).

append_to(region: Region) → None¶

Appends this block to a region.

Transfers ownership if the block is currently owned by another region.

Parameters:: region – The region to append the block to.

create_before(*arg_types, arg_locs: collections.abc.Sequence[Location] | None = None) → Block¶: Creates and returns a new Block before this block (with given argument types and locations).

create_after(*arg_types, arg_locs: collections.abc.Sequence[Location] | None = None) → Block¶: Creates and returns a new Block after this block (with given argument types and locations).

__iter__() → OperationIterator¶: Iterates over operations in the block.

__eq__(arg: Block, /) → bool¶
__eq__(arg: object, /) → bool: Compares block with non-block object (always returns False).

__hash__() → int¶: Returns the hash value of the block.

__str__() → str¶: Returns the assembly form of the block.

append(operation: _OperationBase) → None¶

Appends an operation to this block.

If the operation is currently in another block, it will be moved.

Parameters:: operation – The operation to append to the block.

property successors: BlockSuccessors¶: Returns the list of Block successors.

property predecessors: BlockPredecessors¶: Returns the list of Block predecessors.

class mlir.dialects.transform.smt.ConstrainParamsOp(results_: Sequence[_ods_ir], params: Sequence[_ods_ir], *, loc: _ods_ir | None = None, ip: _ods_ir | None = None)¶

Bases: _ods_ir

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 params-as-SMT-vars as operands, thereby expressing relevant constraints on their allowed values.

Computations w.r.t. passed-in params can also be expressed through the region’s SMT-ops. Namely, the constraints express relationships to other SMT-variables which can then be yielded from the region (with smt.yield).

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 and any one satisfying assignment is used to map the SMT-variables yielded in the region to ``transform.param``s.

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.

OPERATION_NAME = 'transform.smt.constrain_params'¶

_ODS_REGIONS = (1, True)¶

params() → _ods_ir¶

results_() → _ods_ir¶

body() → _ods_ir¶

class mlir.dialects.transform.smt.ConstrainParamsOpAdaptor(operands: list[Value], attributes: OpAttributeMap)¶

class mlir.dialects.transform.smt.ConstrainParamsOpAdaptor(operands: list[Value], opview: OpView)

Bases: _ods_ir

OPERATION_NAME = 'transform.smt.constrain_params'¶

params() → _ods_ir¶

mlir.dialects.transform.smt.smt_constrain_params(results_: Sequence[_ods_ir], params: Sequence[_ods_ir], *, loc: _ods_ir | None = None, ip: _ods_ir | None = None) → _ods_ir | _ods_ir | ConstrainParamsOp¶

class mlir.dialects.transform.smt.ConstrainParamsOp(results: Sequence[mlir.ir.Type], params: Sequence[mlir.dialects.transform.AnyParamType], arg_types: Sequence[mlir.ir.Type], loc=None, ip=None)¶

Bases: ConstrainParamsOp

Allows expressing constraints on params using the SMT dialect.

property body: mlir.ir.Block¶

mlir.dialects.transform.smt.constrain_params(results: Sequence[mlir.ir.Type], params: Sequence[mlir.dialects.transform.AnyParamType], arg_types: Sequence[mlir.ir.Type], loc=None, ip=None)¶