Read a machine integer as an integer

[daniel-larraz]

Kind 2 has two surface syntaxes for machine integers: the keywords uint8
through int64, and uint<N> and
sint<N>
for a width of any size. Its JSON output names every one of them in the
general form, the eight that have a keyword included, so the

      case "int8":
      case "uint8":
      …

arms of Type.getType never match anything Kind 2 prints. A machine integer
falls through to the default of that switch, which treats a name it does not
recognise as an enumeration:

  i  kind2 type=uint<8>  ->  Enum / EnumValue    (a name, not a number)
  j  kind2 type=sint<8>  ->  Enum / EnumValue

So a consumer reading a counterexample over machine integers gets the name of
an enumeration constant where it wanted a number: no IntValue, no
BigInteger, nothing to do arithmetic with.

What changes

One more pattern in the default branch, beside the subrange […] of int and
array of fallbacks already there, reading the general form as an integer:

        if (typeString.matches("(u|s)int<[1-9][0-9]*>"))
        {
          return new Int();
        }

  i  kind2 type=int  ->  Int / IntValue    (arithmetic available)
  j  kind2 type=int  ->  Int / IntValue

Like the eight keyword cases, it gives the width up rather than carrying it,
so a stream reports as an integer and nothing more. Reporting the width would
mean a type of its own, which is a larger change and not what those cases do
today. The keyword cases are left in place: Kind 2's JSON does not produce
them, but getType is public and cheap to keep permissive.

A width that has no keyword of its own, uint<24> say, now reads like any
other rather than as a name.

Tests

machineIntegerCounterExample in Kind2ResultTests reads a counterexample
holding a uint<8>, a sint<8> and a uint<24>, and checks each is an
Int, that the values come back as BigInteger, and that a negative one
(-128) survives. Without the change it fails with

i should be an integer, not uint<8> ==> expected: <true> but was: <false>

The existing 32 result tests and 10 pretty printer tests still pass,
javadoc -Xdoclint:all is clean over the main sources, and it compiles at
the Java 8 language level that CI builds with.

Compatibility

This is independent of kind2-mc/kind2#1550 and can merge before or after it:
the uint<N> spelling is what Kind 2's JSON has always written, and that PR
does not change it — it widens the schema to admit it.

Checked by reading the output of every model in the Kind 2 regression tree
(639) through Result.analyzeJsonResult, both as Kind 2 prints it today and
with isCandidate put back to the quoted form releases before #1550 wrote.
One model fails in both runs, test-div-by-zero.lus, for the unrelated
reason recorded in #25: Kind 2 reports a real produced by a division by zero
as {"num": 1, "den": 0} and RealValue divides by that denominator.

Worth knowing

The XML output names the four widths it knows as uint8 and int8, so the
two formats disagree for the same model, and pp_print_type raises on any
other width rather than printing it. That is Kind 2's to settle, and is
written up in kind2-mc/kind2#1550.

🤖 Generated with Claude Code