tvm_tirx.sym.Analyzer

class tvm_tirx.sym.Analyzer

Bases: Object

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.

set_z3_default_fallback(enabled)

Set whether DEFAULT-strength queries try Z3 after native analysis fails.

Enabled by default. This setting is local to this analyzer and preserved by clone(). Stronger proof queries and Z3-specific APIs are unaffected. Changing it does not clear accepted premises or existing solver state. Z3 must also be available in the native build.

Parameters:

enabled (bool) – Whether to allow the DEFAULT-strength Z3 fallback.

Return type:

None

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=None)

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.

Return type:

str

set_z3_timeout_ms(timeout_ms)

Set Z3 timeout in milliseconds.

Raises:

RuntimeError – If TVM was built without Z3 (USE_Z3=OFF).

Parameters:

timeout_ms (int) – The timeout in milliseconds.

Return type:

None

set_z3_rlimit(rlimit)

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.

Return type:

None

get_z3_stats()

Get Z3 solver statistics.

Raises:

RuntimeError – If TVM was built without Z3 (USE_Z3=OFF).

Returns:

stats (str) – The Z3 statistics.

Return type:

str

const_int_bound(expr)

Find constant integer bound for expr.

Parameters:

expr (Expr) – The expression.

Returns:

bound (ConstIntBound) – The result bound

Return type:

ConstIntBound

const_int_bound_is_bound(var)

Check if a variable is bound to a range.

Parameters:

var (tvm_tirx.ir.Var) – The variable.

Returns:

result (bool) – Whether the variable is bound to a range.

Return type:

bool

modular_set(expr)

Find a modular set that expr belongs to.

Parameters:

expr (Expr) – The expression.

Returns:

result (ModularSet) – The result.

Return type:

ModularSet

simplify(expr, steps=2)

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 (Expr) – The result.

Return type:

Expr

clone()

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 (Analyzer) – A new analyzer holding an independent copy of the facts.

Return type:

Analyzer

rewrite_simplify(expr)

Simplify expression via rewriting rules.

Parameters:

expr (Expr) – The expression.

Returns:

result (Expr) – The result.

Return type:

Expr

property rewrite_simplify_stats

reset_rewrite_simplify_stats()

canonical_simplify(expr)

Simplify expression via canonicalization.

Parameters:

expr (Expr) – The expression.

Returns:

result (Expr) – The result.

Return type:

Expr

int_set(expr, dom_map=None)

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 (IntSet) – The result.

Return type:

IntSet

can_prove(expr, strength=ProofStrength.DEFAULT)

Check whether we can prove expr to be true.

Parameters:

• expr (Expr) – The expression.

• strength (ProofStrength) – The proof strength. SYMBOLIC_BOUND additionally enables symbolic bound analysis. When built with Z3 (TVM_TIRX_USE_Z3=ON), explicit stronger queries try Z3 after native analysis fails to prove the predicate. DEFAULT queries also try Z3 by default; this can be disabled with set_z3_default_fallback(). The existing Z3 timeout and resource limits apply; an unknown solver result means the predicate cannot be proved.

Returns:

result (bool) – Whether the predicate can be proved.

Return type:

bool

set_maximum_rewrite_steps(maximum)

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.

Return type:

None

sync_constraint_context(context)

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.

Return type:

None

can_prove_equal(lhs, rhs)

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 (bool) – Whether we can prove that lhs == rhs

Return type:

bool

try_compare(lhs, rhs)

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 (CompareResult) – The most specific result that can be proven about the comparison. Returns CompareResult.UNKNOWN when nothing can be proven.

Return type:

CompareResult