(constraints1, constraints2, varmap, backvarmap)
| 339 | vranges = {} |
| 340 | |
| 341 | def _check_forward(constraints1, constraints2, varmap, backvarmap): |
| 342 | ana = tvm.arith.Analyzer() |
| 343 | all_vranges = vranges.copy() |
| 344 | all_vranges.update({v: r for v, r in constraints1.ranges.items()}) |
| 345 | |
| 346 | # Check that the transformation is injective |
| 347 | cond_on_vars = tvm.tirx.const(1, "bool") |
| 348 | for v in constraints1.variables: |
| 349 | if v in varmap: |
| 350 | # variable mapping is consistent |
| 351 | v_back = ana.simplify(tvm.tirx.stmt_functor.substitute(varmap[v], backvarmap)) |
| 352 | cond_on_vars = tvm.te.all(cond_on_vars, v == v_back) |
| 353 | # Also we have to check that the new relations are true when old relations are true |
| 354 | cond_subst = tvm.tirx.stmt_functor.substitute( |
| 355 | tvm.te.all(tvm.tirx.const(1, "bool"), *constraints2.relations), backvarmap |
| 356 | ) |
| 357 | # We have to include relations from vranges too |
| 358 | for v in constraints2.variables: |
| 359 | if v in constraints2.ranges: |
| 360 | r = constraints2.ranges[v] |
| 361 | range_cond = tvm.te.all(v >= r.min, v < r.min + r.extent) |
| 362 | range_cond = tvm.tirx.stmt_functor.substitute(range_cond, backvarmap) |
| 363 | cond_subst = tvm.te.all(cond_subst, range_cond) |
| 364 | cond_subst = ana.simplify(cond_subst) |
| 365 | check_bool_expr_is_true( |
| 366 | tvm.te.all(cond_subst, cond_on_vars), |
| 367 | all_vranges, |
| 368 | cond=tvm.te.all(tvm.tirx.const(1, "bool"), *constraints1.relations), |
| 369 | ) |
| 370 | |
| 371 | _check_forward( |
| 372 | constraints_trans.src, |
no test coverage detected
searching dependent graphs…