Closed tqchen closed 1 month ago
cc @yzhliu
@tqchen is it resolved?
Ah, sorry, I mixed it with another arith issue, reopening.
Here is another one:
=================================== FAILURES ===================================
__________________________ test_solution_consistency ___________________________
def test_solution_consistency():
seed = random.randrange(sys.maxsize)
print(
"\nThis test is intentionally non-deterministic, "
"if it fails please report it in github issue together with this seed {}\n".format(seed)
)
random.seed(seed)
def _check(variables, formulas, coef=(-5, 5), bounds=(-20, 20)):
vs = [te.var("x" + str(i)) for i in range(variables)]
fs = []
for i in range(formulas):
s1 = sum([v * random.randint(coef[0], coef[1]) for v in vs])
s1 += random.randint(coef[0], coef[1])
s2 = sum([v * random.randint(coef[0], coef[1]) for v in vs])
s2 += random.randint(coef[0], coef[1])
op = random.choice([tir.expr.EQ, tir.expr.LE, tir.expr.LT, tir.expr.GE, tir.expr.GT])
fs.append(op(s1, s2))
vranges = {v: tvm.ir.expr.Range(bounds[0], bounds[1] + 1) for v in vs}
before = te.all(tir.const(1, "bool"), *fs)
after = arith._ffi_api.SolveInequalitiesAsCondition(vs, vranges, fs)
after = te.all(tir.const(1, "bool"), *after)
testing.check_bool_expr_is_true(before == after, vranges)
solution = arith.solve_linear_inequalities(fs, vs, vranges, deskew_range=True)
testing.check_int_constraints_trans_consistency(solution)
for i in range(3):
_check(1, 1)
for i in range(3):
_check(1, 2)
for i in range(3):
_check(2, 1)
for i in range(3):
_check(2, 2)
for i in range(3):
_check(2, 3)
# Somewhere here coefficients in the results become too large, leading to overflow,
# so we use smaller initial coefficients
for i in range(5):
_check(3, 3, coef=(-2, 2))
for i in range(5):
> _check(3, 4, coef=(-2, 2))
tests/python/unittest/test_arith_solve_linear_inequality.py:70:
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
tests/python/unittest/test_arith_solve_linear_inequality.py:51: in _check
testing.check_int_constraints_trans_consistency(solution)
python/tvm/testing.py:360: in check_int_constraints_trans_consistency
constraints_trans.src_to_dst,
python/tvm/testing.py:347: in _check_forward
cond=tvm.te.all(tvm.tir.const(1, "bool"), *constraints1.relations),
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
bool_expr = (!((((((0 - floordiv(((0 - x2.shifted) - 1), 2)) - (x2.shifted*2)) - 5) <= ((((floordiv((0 - floordiv(((0 - x2.shifted...2)), 2) + x0.shifted) - floordiv(((0 - floordiv(((0 - x2.shifted) - 3), 2)) - 1), 2))) && (x2.shifted == x2.shifted))))
vranges = {x2.shifted: range(min=0, ext=18), x0.shifted: range(min=0, ext=14)}
cond = ((((((0 - floordiv(((0 - x2.shifted) - 1), 2)) - (x2.shifted*2)) - 5) <= ((((floordiv((0 - floordiv(((0 - x2.shifted) ...(floordiv(((0 - x2.shifted) - 1), 2)*4)) - 6))) && ((floordiv(((0 - x2.shifted) - 1), 2)*2) == ((0 - x2.shifted) - 2)))
def check_bool_expr_is_true(bool_expr, vranges, cond=None):
"""Check that bool_expr holds given the condition cond
for every value of free variables from vranges.
for example, 2x > 4y solves to x > 2y given x in (0, 10) and y in (0, 10)
here bool_expr is x > 2y, vranges is {x: (0, 10), y: (0, 10)}, cond is 2x > 4y
We creates iterations to check,
for x in range(10):
for y in range(10):
assert !(2x > 4y) || (x > 2y)
Parameters
----------
bool_expr : tvm.ir.PrimExpr
Boolean expression to check
vranges: Dict[tvm.tir.expr.Var, tvm.ir.Range]
Free variables and their ranges
cond: tvm.ir.PrimExpr
extra conditions needs to be satisfied.
"""
if cond is not None:
bool_expr = tvm.te.any(tvm.tir.Not(cond), bool_expr)
def _run_expr(expr, vranges):
"""Evaluate expr for every value of free variables
given by vranges and return the tensor of results.
"""
def _compute_body(*us):
vmap = {v: u + r.min for (v, r), u in zip(vranges.items(), us)}
return tvm.tir.stmt_functor.substitute(expr, vmap)
A = tvm.te.compute([r.extent.value for v, r in vranges.items()], _compute_body)
args = [tvm.nd.empty(A.shape, A.dtype)]
sch = tvm.te.create_schedule(A.op)
mod = tvm.build(sch, [A])
mod(*args)
return args[0].asnumpy()
res = _run_expr(bool_expr, vranges)
if not np.all(res):
indices = list(np.argwhere(res == 0)[0])
counterex = [(str(v), i + r.min) for (v, r), i in zip(vranges.items(), indices)]
counterex = sorted(counterex, key=lambda x: x[0])
counterex = ", ".join([v + " = " + str(i) for v, i in counterex])
ana = tvm.arith.Analyzer()
raise AssertionError(
"Expression {}\nis not true on {}\n"
> "Counterexample: {}".format(ana.simplify(bool_expr), vranges, counterex)
)
E AssertionError: Expression ((((((((floordiv((0 - floordiv(((0 - x2.shifted: int32) - 1), 2)), 2)*2) + (x0.shifted: int32*2)) - (x2.shifted*2)) - 4) < (((0 - floordiv(((0 - x2.shifted) - 1), 2)) - (x2.shifted*2)) - 5)) || ((((0 - (x2.shifted*2)) - (floordiv(((0 - x2.shifted) - 1), 2)*4)) - 6) < ((((floordiv((0 - floordiv(((0 - x2.shifted) - 1), 2)), 2)*2) + (x0.shifted*2)) - (x2.shifted*2)) - 4))) || ((floordiv(((0 - x2.shifted) - 1), 2)*2) != ((0 - x2.shifted) - 2))) || (((((((((((0 - floordiv(((0 - x2.shifted) - 1), 2)) - floordiv(floormod(((0 - x2.shifted) - 1), -4), 2)) - (x0.shifted*2)) <= (((floordiv((0 - floordiv(((0 - x2.shifted) - 1), 2)), 2)*2) + (x0.shifted*2)) + 2)) && ((((floordiv(((0 - x2.shifted) - 1), 2) - floordiv(floormod(((0 - x2.shifted) - 1), -4), 2)) - (x0.shifted*2)) - 1) == (((((floordiv(((0 - x2.shifted) - 1), 2)*2) + x2.shifted) + 1) - (floordiv((0 - floordiv(((0 - x2.shifted) - 1), 2)), 2)*2)) - (x0.shifted*2)))) && (((0 - (x2.shifted*2)) - 6) < ((x2.shifted*2) + 6))) && ((((floordiv(((0 - x2.shifted) - 1), 2)*2) + floordiv((0 - floordiv(((0 - x2.shifted) - 1), 2)), 2)) + x0.shifted) < 0)) && ((-18 <= ((floordiv((0 - floordiv(((0 - x2.shifted) - 1), 2)), 2) + x0.shifted) - x2.shifted)) && (((floordiv((0 - floordiv(((0 - x2.shifted) - 1), 2)), 2) + x0.shifted) - x2.shifted) < 23))) && ((x2.shifted <= 39) && (-43 < x2.shifted))) && ((-23 <= x2.shifted) && (x2.shifted < 18))) && (x0.shifted == ((floordiv((0 - floordiv(((0 - x2.shifted) - 1), 2)), 2) + x0.shifted) - floordiv(((0 - floordiv(((0 - x2.shifted) - 3), 2)) - 1), 2)))))
E is not true on {x2.shifted: range(min=0, ext=18), x0.shifted: range(min=0, ext=14)}
E Counterexample: x0.shifted: int32 = 0, x2.shifted: int32 = 2
python/tvm/testing.py:303: AssertionError
----------------------------- Captured stdout call -----------------------------
This test is intentionally non-deterministic, if it fails please report it in github issue together with this seed 2078641736
http://ci.tvm.ai:8080/job/temp-ci-docker-staging/job/ci-stage2/12/execution/node/229/log/
cc @junrushao