| 69 | |
| 70 | |
| 71 | def test_simplify_symbolic_comparison(): |
| 72 | ana = tvm.arith.Analyzer() |
| 73 | |
| 74 | i0 = tirx.Var("i0", "int64") |
| 75 | i1 = tirx.Var("i1", "int64") |
| 76 | n, m = tvm.tirx.SizeVar("n", "int64"), tvm.tirx.SizeVar("m", "int64") |
| 77 | outer = (n + 31) // 32 |
| 78 | ana.bind(i0, tvm.ir.Range(0, outer)) |
| 79 | ana.bind(i1, tvm.ir.Range(0, 32)) |
| 80 | PS = tvm.arith.ProofStrength |
| 81 | |
| 82 | assert not ana.can_prove(i0 * 32 + i1 < (n + 31) // 32 * 32, PS.DEFAULT) |
| 83 | assert ana.can_prove(i0 * 32 + i1 < (n + 31) // 32 * 32, PS.SYMBOLIC_BOUND) |
| 84 | assert ana.can_prove(i0 * 32 + i1 < (n + 31) // 32 * 32 + m, PS.SYMBOLIC_BOUND) |
| 85 | assert ana.can_prove(i0 * 32 + i1 + 1 <= (n + 31) // 32 * 32, PS.SYMBOLIC_BOUND) |
| 86 | assert ana.can_prove((n + 31) // 32 * 32 >= i0 * 32 + i1 + 1, PS.SYMBOLIC_BOUND) |
| 87 | assert ana.can_prove((n + 31) // 32 * 32 >= i0 * 32 + i1, PS.SYMBOLIC_BOUND) |
| 88 | |
| 89 | |
| 90 | # These tests exercised arith::CanProve's substitution-based proof loop for |