tvm_tirx.sym

tvm_tirx.sym#

Symbolic analysis: integer bounds, simplification and pattern detection.

class tvm_tirx.sym.IntSet(*args: Any, **kwargs: Any)#

Represent a set of integer in one dimension.

is_nothing()#: Whether the set represent nothing

is_everything()#: Whether the set represent everything

static vector(vec)#

Construct an integer set that covers the vector expr

Parameters:: vec (Expr) – The vector expression.
Returns:: rset – The result set.
Return type:: IntSet

static single_point(point)#

Construct a point set.

Parameters:: point (Expr) – The vector expression.
Returns:: rset – The result set.
Return type:: IntSet

class tvm_tirx.sym.IntervalSet(min_value, max_value)#

Represent set of continuous interval [min_value, max_value]

Parameters:

min_value (Expr) – The minimum value in the interval.
max_value (Expr) – The maximum value in the interval.

tvm_tirx.sym.deduce_bound(var, cond, hint_map, relax_map)#

Deduce the bound of the target variable in the cond.

Parameters:

var (tvm_tirx.ir.Var) – The target variable to be deduced.
cond (Expr) – The condition
hint_map (Map[tvm_tirx.ir.Var, IntSet]) – Domain of variables used to help deduction.
relax_map (Map[tvm_tirx.ir.Var, IntSet]) – The domain of the variables to be relaxed using the provided domain.

tvm_tirx.sym.estimate_region_lower_bound(region, var_dom, predicate, analyzer=None)#

Analyze the region with affine map, given the domain of variables and their predicate Some subregion may be discarded during the lower-bound analysis.

Parameters:

region (List[Range]) – The region to be analyzed.
var_dom (Dict[tvm_tirx.ir.Var, Range]) – The ranges of the variables
predicate (Expr) – The predicate for the affine map
analyzer (Optional[tvm_tirx.sym.Analyzer]) – The analyzer to use. When provided, its accumulated bindings and constraints are reused; otherwise a fresh analyzer is created.

Returns:

region_int_set – None if the detection fails, or an array of IntSets as the result of analysis

Return type:

Optional[List[IntSet]]

tvm_tirx.sym.estimate_region_strict_bound(region, var_dom, predicate, analyzer=None)#

Analyze the region with affine map, given the domain of variables and their predicate The result should be strict, i.e. no region is discarded or relaxed.

Parameters:

region (List[Range]) – The region to be analyzed.
var_dom (Dict[tvm_tirx.ir.Var, Range]) – The ranges of the variables
predicate (Expr) – The predicate for the affine map
analyzer (Optional[tvm_tirx.sym.Analyzer]) – The analyzer to use. When provided, its accumulated bindings and constraints are reused; otherwise a fresh analyzer is created.

Returns:

region_int_set – None if the detection fails, or an array of IntSets as the result of analysis

Return type:

Optional[List[IntSet]]

tvm_tirx.sym.estimate_region_upper_bound(region, var_dom, predicate, analyzer=None)#

Analyze the region with affine map, given the domain of variables and their predicate Relaxation of the region may be used in upper-bound analysis, i.e. some extra region may be added to the result.

Parameters:

region (List[Range]) – The region to be analyzed.
var_dom (Dict[tvm_tirx.ir.Var, Range]) – The ranges of the variables
predicate (Expr) – The predicate for the affine map
analyzer (Optional[tvm_tirx.sym.Analyzer]) – The analyzer to use. When provided, its accumulated bindings and constraints are reused; otherwise a fresh analyzer is created.

Returns:

region_int_set – an array of IntSets as the result of analysis

Return type:

List[IntSet]

class tvm_tirx.sym.ModularSet(coeff, base)#: Represent range of (coeff * x + base) for x in Z

class tvm_tirx.sym.ConstIntBound(min_value, max_value)#

Represent constant integer bound

Parameters:

min_value (int) – The minimum value of the bound.
max_value (int) – The maximum value of the bound.

class tvm_tirx.sym.Analyzer#

Integer arithmetic analyzer

This is a stateful analyzer class that can be used to perform various symbolic integer analysis. The same analyzer instance can be passed to FFI APIs to share accumulated facts across calls.

property is_z3_enabled: bool#

Whether this build includes the Z3 backend (USE_Z3=ON).

The Z3-specific methods (get_smtlib2(), get_z3_stats(), set_z3_timeout_ms(), set_z3_rlimit()) only work when this is True.

get_smtlib2(expr: Expr | None = None) → str#

Get the current Z3 problem in SMT-LIB2 format.

Raises:: RuntimeError – If TVM was built without Z3 (USE_Z3=OFF), since there is no solver state to export. Use is_z3_enabled to check first.
Parameters:: expr (Optional[Expr]) – The expression to prove. If provided, its negation is added to the problem.

set_z3_timeout_ms(timeout_ms: int) → None#

Set Z3 timeout in milliseconds.

Raises:: RuntimeError – If TVM was built without Z3 (USE_Z3=OFF).
Parameters:: timeout_ms (int) – The timeout in milliseconds.

set_z3_rlimit(rlimit: int) → None#

Set Z3 resource limit.

The resource limit gives deterministic solver budgeting (unlike a wall clock timeout). A value of 0 disables the limit.

Raises:: RuntimeError – If TVM was built without Z3 (USE_Z3=OFF).
Parameters:: rlimit (int) – The resource limit.

get_z3_stats() → str#

Get Z3 solver statistics.

Raises:: RuntimeError – If TVM was built without Z3 (USE_Z3=OFF).
Returns:: stats – The Z3 statistics.
Return type:: str

const_int_bound(expr: Expr) → ConstIntBound#

Find constant integer bound for expr.

Parameters:: expr (Expr) – The expression.
Returns:: bound – The result bound
Return type:: ConstIntBound

const_int_bound_is_bound(var: Var) → bool#

Check if a variable is bound to a range.

Parameters:: var (tvm_tirx.ir.Var) – The variable.
Returns:: result – Whether the variable is bound to a range.
Return type:: bool

modular_set(expr: Expr) → ModularSet#

Find a modular set that expr belongs to.

Parameters:: expr (Expr) – The expression.
Returns:: result – The result.
Return type:: ModularSet

simplify(expr: Expr, steps: int = 2) → Expr#

Simplify expression via both rewrite and canonicalization.

Parameters:

expr (Expr) – The expression.
steps (The simplification runs in the order of) – rewrite_simplify (step 1) -> canonical_simplify (step 2) -> rewrite_simplify (step 3) -> canonical_simplify (step 4) -> … param steps controls how many steps to run. Default is 2, i.e., rewrite_simplify + canonical_simplify.

Returns:

result – The result.

Return type:

Expr

clone() → Analyzer#

Return a deep copy of this analyzer with independent state.

The returned analyzer carries the same accumulated facts (variable bounds, modular sets, bindings, integer-set domains, literal constraints and transitive comparisons) as this one, but owns its own state: synchronizing or simplifying either analyzer afterwards does not affect the other. Unlike copying the handle, this is a true deep copy.

Returns:: result – A new analyzer holding an independent copy of the facts.
Return type:: Analyzer

rewrite_simplify(expr: Expr) → Expr#

Simplify expression via rewriting rules.

Parameters:: expr (Expr) – The expression.
Returns:: result – The result.
Return type:: Expr

canonical_simplify(expr: Expr) → Expr#

Simplify expression via canonicalization.

Parameters:: expr (Expr) – The expression.
Returns:: result – The result.
Return type:: Expr

int_set(expr: Expr, dom_map: dict[Var, IntSet] | None = None) → IntSet#

Compute a symbolic IntSet that covers expr for all values in dom_map.

Parameters:

expr (Expr) – The expression.
dom_map (Optional[Dict[tvm_tirx.ir.Var, tvm_tirx.sym.IntSet]]) – The domain for variables to be relaxed. When omitted, the analyzer uses the domains of the variables already bound to it.

Returns:

result – The result.

Return type:

IntSet

can_prove(expr: Expr, strength: ProofStrength = ProofStrength.DEFAULT) → bool#

Check whether we can prove expr to be true.

Parameters:

expr (Expr) – The expression.
strength (ProofStrength) – The proof strength. When TVM is built with Z3 (USE_Z3=ON), the optional Z3 fallback is only consulted at SYMBOLIC_BOUND or higher, after the native analyzers fail to prove the predicate.

Returns:

result – The result.

Return type:

Expr

set_maximum_rewrite_steps(maximum: int) → None#

Set the maximum allowed number of rewrite-simplify steps.

When a positive limit is set, the simplifier raises an exception once it exceeds that number of rewrite steps. This is useful for guarding against performance regressions in tests.

Parameters:: maximum (int) – The maximum number of rewrite steps, or a non-positive value to allow an unlimited number of steps.

sync_constraint_context(context: ConstraintContext) → None#

Synchronize this analyzer with the premises visible in context.

The analyzer captures the current context position. Later appends become visible only after another synchronization. Switching to a parent, sibling, or empty context removes facts no longer present there. Repeating this call for an unchanged context is inexpensive.

Parameters:: context (ConstraintContext) – Binding, range, and predicate premises for subsequent queries. Captured premises and their referenced expressions must not be modified through aliases.

can_prove_equal(lhs: Expr, rhs: Expr) → bool#

Whether we can prove that lhs == rhs

Parameters:

lhs (Expr) – The left-hand side of the comparison
rhs (Expr) – The right-hand side of the comparison

Returns:

result – Whether we can prove that lhs == rhs

Return type:

bool

try_compare(lhs: Expr, rhs: Expr) → CompareResult#

Compare lhs and rhs using directly known comparisons and constant offsets.

Parameters:

lhs (Expr) – The left-hand side of the comparison.
rhs (Expr) – The right-hand side of the comparison.

Returns:

result – The most specific result that can be proven about the comparison. Returns CompareResult.UNKNOWN when nothing can be proven.

Return type:

CompareResult

class tvm_tirx.sym.ProofStrength(value)#: Proof strength of the analysis

class tvm_tirx.sym.CompareResult(value)#

Result of a transitive comparison.

Values must match the C++ sym::CompareResult enum.

tvm_tirx.sym.allow_uint_as_index()#

Opt-in no-overflow domain for unsigned index arithmetic.

Within the scope, the analyzer treats uint32/uint64 scalars as index types: it assumes their values never approach the type limit (no wraparound), so the signed rewrite rule set (floordiv/floormod decomposition, modular analysis) applies to them. Every unsigned expression admitted under the assumption is logged once per process (WARNING) so the assumption stays auditable.

Off by default. Intended for compile-time layout proofs (offsets that provably stay small), NOT for runtime codegen semantics where unsigned wraparound is real behavior.

class tvm_tirx.sym.IterMapExpr(*args: Any, **kwargs: Any)#: Base class of all IterMap expressions.

class tvm_tirx.sym.IterMark(source, extent)#

Mark the source as an iterator in [0, extent).

Parameters:

source (Expr.) – The source expression.
extent (Expr) – The extent of the iterator.

class tvm_tirx.sym.IterSplitExpr(source, lower_factor, extent, scale)#

Split of an iterator.

result = floormod(floordiv(source, lower_factor), extent) * scale

Parameters:

source (IterMark) – The source marked iterator.
lower_factor (Expr) – The lower factor to split the domain.
extent (Expr) – The extent of the split.
scale (Expr) – Additional scale to the split.

class tvm_tirx.sym.IterSumExpr(args, base)#

Fuse multiple iterators by summing them with scaling.

result = sum(args) + base

Parameters:

args (List[IterSplitExpr]) – The input to the sum expression.
base (Expr) – The base offset.

tvm_tirx.sym.detect_iter_map(indices, input_iters, predicate=True, check_level=IterMapLevel.Surjective, analyzer=None, simplify_trivial_iterators=True)#

Detect if indices can be written as mapped iters from input iters

Parameters:

indices (List[Expr]) – The input indices
input_iters (Map[tvm_tirx.ir.Var, Range]) – The domain of each input iterators.
predicate (Expr) – The predicate constraints on the input iterators
check_level (Union[str, IterMapLevel]) – Checking level of iteration mapping
simplify_trivial_iterators (bool) – If true, iterators with extent of 1 will be replaced with a constant value.
analyzer (Optional[tvm_tirx.sym.Analyzer]) – The analyzer to use. When provided, its accumulated bindings and constraints are reused; otherwise a fresh analyzer is created.

Returns:

results – The iter map matching result. The result’s .indices is empty array if no match can be found.

Return type:

IterMapResult

tvm_tirx.sym.iter_map_simplify(indices, input_iters, predicate=True, check_level=IterMapLevel.Surjective, analyzer=None, simplify_trivial_iterators=True)#

Simplify the indices using iter map detection.

Parameters:

indices (List[Expr]) – The input indices
input_iters (Map[tvm_tirx.ir.Var, Range]) – The domain of each input iterators.
predicate (Expr) – The predicate constraints on the input iterators
check_level (Union[str, IterMapLevel]) – Checking level of iteration mapping
simplify_trivial_iterators (bool) – If true, iterators with extent of 1 will be replaced with a constant value.
analyzer (Optional[tvm_tirx.sym.Analyzer]) – The analyzer to use. When provided, its accumulated bindings and constraints are reused; otherwise a fresh analyzer is created.

Returns:

results – The simplified indices. The input indices are returned unchanged if no match can be found.

Return type:

List[Expr]

tvm_tirx.sym.normalize_iter_map_to_expr(expr)#

Given an IterMapExpr, transform it to normal Expr

Parameters:: expr (IterMapExpr) – the input IterMapExpr
Returns:: result – the corresponding normal Expr
Return type:: Expr

tvm_tirx.sym.normalize_to_iter_sum(index, input_iters, analyzer=None)#

Normalize expr to iter sum.

The normalized result ensures that each scale is in the form of (symbol_prod) * cscale It will also sort in desc order by cscale then len(symbol_prod).

Parameters:

index (Expr) – The input index
input_iters (Map[tvm_tirx.ir.Var, Range]) – The domain of each input iterators.
analyzer (Optional[tvm_tirx.sym.Analyzer]) – The analyzer to use. When provided, its accumulated bindings and constraints are reused; otherwise a fresh analyzer is created.

Returns:

iter_sum – The result iter sum

Return type:

IterSumExpr

Note

This function does best effort detection, so some undetected part can go into iter_sum.base

This function is useful to decide the stride multiplier and division factor in buffer access patterns.

tvm_tirx.sym.subspace_divide(bindings, input_iters, sub_iters, predicate=True, check_level=IterMapLevel.Surjective, analyzer=None, simplify_trivial_iterators=True)#

Detect if bindings can be written as [a_0*e_0 + b_0 + c_0, a_1*e_1 + b_1, ..., a_n*e_n + b_n]

where:

a = some-quasi-affine-iter-map(input_iters set_minus sub_iters)
b = some-quasi-affine-iter-map(sub_iters)
c is constant symbols
e is the extent of b

For example:

z*12 + y*3 + x + c = (z*4+y)*3 + x
bindings = [z*12 + y*3 + x + c]
input_iters = [z, y, x]
sub_iter = [x]
Then the result will be [a, b] where
a = [z*4 + y]
b = [x]

Parameters:

bindings (List[Expr]) – The input bindings
input_iters (Map[tvm_tirx.ir.Var, Range]) – The domain of input iterator, which is the basis of the whole space
sub_iters (Array[tvm_tirx.ir.Var]) – The subset of input_iters, which is the basis of the subspace
predicate (Expr) – The predicate constraints on the input iterators
check_level (Union[str, IterMapLevel]) – Checking level of iteration mapping
simplify_trivial_iterators (bool) – If true, iterators with extent of 1 will be replaced with a constant value.
analyzer (Optional[tvm_tirx.sym.Analyzer]) – The analyzer to use. When provided, its accumulated bindings and constraints are reused; otherwise a fresh analyzer is created.

Returns:

results – The result list has length len(bindings) + 1.

[0, len(bindings)): The iter map matching result. The inner list is of length 2. The first expr is the basis of the quotient space. The second expr is the basis of the subspace.
len(bindings): the predicate of outer space and inner space.
Empty array if no match can be found.

Return type:

List[List[Expr]]

tvm_tirx.sym.inverse_affine_iter_map(iter_map, outputs)#

Apply the inverse of the affine transformation to the outputs. Similar to the back-propagation, starting from the outputs, it visits the DAG of the expressions in reverse topology order and applies the inverse of the affine transformation until it reaches the input. The affine iter map is required to be bijective.

For example, iter_map = [l0 // 16, l0 % 16], outputs = [output_0, output_1], the affine transformation specified by iter_map will be applied to outputs and the result will be {l0: ((output_0*16) + output_1)}.

tvm_tirx.sym

Contents

tvm_tirx.sym#