Add support for CHOOSE x \in i..j: P for large |j-i|

[konnov]

Consider the following example:

------------------------------- MODULE IntSqr ----------------------------
EXTENDS Integers

MAX_UINT64 == 2^32 - 1

VARIABLE
  \* @type: Int;
  n,
  \* @type: Int;
  r

IntSqr(m) ==
  CHOOSE x \in 0..MAX_UINT64:
    /\ x * x <= m
    /\ (x + 1) * (x + 1) > m \/ x + 1 >= MAX_UINT64

Init ==
  \E k \in 0..MAX_UINT64:
    /\ n = k
    /\ r = IntSqr(k)

Next ==
  UNCHANGED <<n, r>>

IntSqrTest1 ==
  n = 0 => r = 0

IntSqrTest2 ==
  n = 1 => r = 1

IntSqrTest3 ==  
  n = 7 => r = 2

IntSqrTest4 ==
  n = 3 => r = 1

IntSqrTest5 ==
  n = 4 => r = 2

IntSqrTest6 ==
  n = 17 => r = 4

IntSqrTest7 ==
  n = MAX_UINT64 => r * r <= MAX_UINT64 /\ (r + 1) * (r + 1) > MAX_UINT64

AllTests ==
  /\ IntSqrTest1
  /\ IntSqrTest2
  /\ IntSqrTest3
  /\ IntSqrTest4
  /\ IntSqrTest5
  /\ IntSqrTest6
  /\ IntSqrTest7

==========================================================================

Run the tests as follows:

$ apalache-mc check --write-intermediate=true --inv=AllTests IntSqr.tla

Apalache fails:

IntSqr.tla:18:3-20:20: rewriter error: Range bounds are too large to fit in scala.Int

If we change MAX_UINT64 to 2^8, the tests go through. The issue is that the bounded model checker is trying to expand the set 0..MAX_UINT64, which it should not expand in this case.

We should add a special rewriting rule for this case that simply introduces an integer constant and the related constraints over the constant. This case would be useful for abstracting functions over integers.