detect more forms of modulo expressions when extracting a function

detect more forms of modulo expressions when extracting a function

This is similar to the modulo expression that is already being detected
but instead of starting out from an equality constraint

	f(x) + t m i + m n h(y) = 0

the pattern detected by the code in this commit starts out from
an integer division

	e = (f(x) + t m i)//(m n)

along with an inequality constraint of the form

	f(x) + t m i - m n e + c >= 0

with c <= -(n - 1) m that imply that

	f(x)//m + t i - (n - 1)

is equal to some multiple of n.

If, furthermore, the range of i is smaller than or equal to n,
in particular, if a pair of constraints

	-g(x) + i >= 0
	 g(x) - i + d >= 0

can be found with d < n, then a fixed expression for i can be extracted.

Signed-off-by: Sven Verdoolaege <sven@cerebras.net>