🐛 Describe the bug

In an early version of #126905 I attempted to add asserts to our sympy functions. Specifically, for sympy functions that expected to receive integer inputs (like IntTrueDiv), I asserted that the inputs is_integer. Because our fragment of Sympy reasoning follows Python int/float promotion rules (and in particular, there is no data dependence about it), in principle it should be possible to always accurately tell if any given expression is integral or not.

However, there are some cases where we end up generating rational expressions in reasoning. The easiest way to end up with rationals is when you use builtin Sympy division, which aggressively distributes division across addition:

>>> import sympy
>>> from sympy.abc import x, y
>>> (x + y) / 2
x/2 + y/2

When simplifications involving rationals happen, it is easy to lose track that a larger quantity is_integer (and sympy's assumption system is rather weak, so it only does superficial reasoning). In the example above, if x + y is divisible by 2, then x/2 + y/2 is integral, but Sympy would never be able to tell you this.

I always thought rationals were an unexpected and unwelcome style of simplification that I was happy to obliterate from Sympy. And I have mostly eliminated it in #126905 However, the offline solver makes use of sympy's inequality solver, which does not support custom functions (sympy/sympy#26632), and so the offline solver rewrites FloorDiv into sympy division so that it can make use of it. This means rationals can show up, and in particular, means that I can't really do any is_integer asserts.

This issue is to track what we should do about this. We appear to be internally split about it. @lezcano strongly favors stringent invariants, but @avikchaudhuri says:

Hmm, seems hard to do reasoning on ints without allowing rationals. Feels like rationals are to ints what complex numbers are to reals...

Is there a flag we could turn off to temporarily avoid these assertions, understanding that we might allow intermediate rationals to show up, and later check that the solutions would be integers?

One possibility is certainly to have some sort of context manager that turns off the assertions in some context, and enable this context manager in the offline solver. I'm not sure if anyone has better ideas.

Versions

main