Parse rational and negative real values in SMT-LIB models

[agusaldasoro]

Stacked on #1836.

Problem

Z3 prints a Real that is not an integer as a division, and a negative Real as a negation:

((p__1 (id-price 0 (/ 1999.0 100.0))))        ; PRICE = 19.99
((t__1 (id-price 0 (- (/ 7.0 2.0)))))         ; PRICE < -2.5
((t__1 (id-price 0 (- 20.0))))                ; PRICE = -20.0

SMTResultParser.parseValue only understood plain literals and the integer negation (- 6). On master these values break the struct split and throw ArrayIndexOutOfBoundsException, so the query gets an ERROR. With #1836 the split works, but the value comes back as the StringValue "/ 1999.0 100.0". SMTLibZ3DbConstraintSolver then builds a StringGene for a DECIMAL/REAL column, which gives an invalid INSERT. The problem hits any query that constrains a decimal column to a non-integer value (e.g. WHERE price > 10.5) or to a negative value.

Fix

parseValue first tries the new parseNumericTerm. It evaluates the numeric terms Z3 uses in models:

• integer and decimal literals;
• negation: (- x), plus (-x) as the existing line sanitizer rewrites it;
• division of two literals: (/ a b).

These can be nested, as in (- (/ 7.0 2.0)).

• Integers still become LongValue. An integer too large for a Long becomes a RealValue, as before.
• Divisions and decimals become RealValue.
• Anything else returns null and falls through to the existing string handling, so nothing else changes.

Tests

The new cases in SMTResultParserTest use the exact output of the Z3 image the solver runs:

• testParseComposedTypeWithRationalValue: (/ 1999.0 100.0) → 19.99
• testParseComposedTypeWithNegativeRealValues: (- (/ 7.0 2.0)) → -3.5 and (- 20.0) → -20.0

Both fail on #1836 (StringValue instead of RealValue) and pass with this change. All tests in core-extra/solver pass, including the Z3 Docker ones.