tvm_tirx.sym

Symbolic analysis: integer bounds, simplification and pattern detection.

Classes

Constraint()	A symbolic binding, range, or predicate, with collector-defined lifetime.
ConstraintContext([parent, parent_local_prefix])	Tracks the constraints relevant to each point in a traversal.
BindingConstraint(var, value)	The primitive value captured when var is bound.
RangeConstraint(var, domain)	A variable contained in a half-open range, without stride information.
PredicateConstraint(condition[, assume_always])	A boolean condition whose validity is supplied by its collector.
IntSet(*args, **kwargs)	Represent a set of integer in one dimension.
IntervalSet(min_value, max_value)	Represent set of continuous interval [min_value, max_value]
ModularSet(coeff, base)	Represent range of (coeff * x + base) for x in Z
ConstIntBound(min_value, max_value)	Represent constant integer bound
Analyzer()	Integer arithmetic analyzer
ProofStrength(*values)	Proof strength of the analysis
CompareResult(*values)	Result of a transitive comparison.
IterMapExpr(*args, **kwargs)	Base class of all IterMap expressions.
IterMark(source, extent)	Mark the source as an iterator in [0, extent).
IterSplitExpr(source, lower_factor, extent, ...)	Split of an iterator.
IterSumExpr(args, base)	Fuse multiple iterators by summing them with scaling.

Functions

estimate_region_lower_bound(region, var_dom, ...)	Analyze the region with affine map, given the domain of variables and their predicate Some subregion may be discarded during the lower-bound analysis.
estimate_region_strict_bound(region, ...[, ...])	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.
estimate_region_upper_bound(region, var_dom, ...)	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.
allow_uint_as_index()	Opt-in no-overflow domain for unsigned index arithmetic.
deduce_bound(var, cond, hint_map, relax_map)	Deduce the bound of the target variable in the cond.
detect_iter_map(indices, input_iters[, ...])	Detect if indices can be written as mapped iters from input iters
iter_map_simplify(indices, input_iters[, ...])	Simplify the indices using iter map detection.
normalize_iter_map_to_expr(expr)	Given an IterMapExpr, transform it to normal Expr
normalize_to_iter_sum(index, input_iters[, ...])	Normalize expr to iter sum.
subspace_divide(bindings, input_iters, sub_iters)	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]
inverse_affine_iter_map(iter_map, outputs)	Apply the inverse of the affine transformation to the outputs.

Supporting classes

IterMapResult(indices, errors, padding_predicate)	Result of iter map detection.
IterMapLevel(*values)	Possible kinds of iter mapping check level.

Supporting functions

pos_inf()	Returns the symbolic positive infinity
neg_inf()	Returns the symbolic negative infinity
union_lower_bound(sets)	Create a lower-bound of union set, where some of the segments may be dropped