[ARITH] Scope interval constraints to mapped variables#19963
Conversation
Scoped domain constraints refine variables already present in the relaxation map; they do not turn free parameters into relaxation domains. Apply a scoped constraint only when the variable is explicitly mapped, remove the finite-bound restoration fallback, and cover loop-local escape through compact-buffer simplification.
![gemini-code-assist[bot]](https://avatars.githubusercontent.com/in/956858?s=60&v=4){kind=small}
There was a problem hiding this comment.
Code Review
This pull request simplifies the IntervalSetEvaluator in src/arith/int_set.cc by removing logic that preserved parametric bounds under one-sided constraints and by checking dom_map_ early when evaluating variable nodes. It also removes a related test case and adds a new test test_loop_var_does_not_escape_compacted_buffer_extent to verify that loop variables do not escape compacted buffer extents. The feedback suggests removing a redundant cast var.as_or_throw<PrimExpr>() since Var can be implicitly converted to PrimExpr.
Important
The consumer version of Gemini Code Assist on GitHub is being sunset. Starting June 18, 2026, new organization installations will be blocked, and all code review activity will officially cease on July 17, 2026.
For more details on the timeline and next steps, please review the Help Documentation.
Run the loop-variable escape case directly in the compact-buffer suite so its scope assertion stays at the pass that owns allocation extent compaction.
2 participants
Rationale
Analyzer constraint scopes continue to provide loop-positive facts to constant-bound and rewrite proofs. During IntSet relaxation, however, a scoped domain constraint is a refinement only for a variable explicitly present in the relaxation map. Applying it to an unmapped variable reinterprets a free parameter as a relaxation domain and can let a loop-local symbol survive recursive interval evaluation.
Changes