Encode DATE columns like TIMESTAMP ones

[agusaldasoro]

Problem

DATE was mapped to an SMT Int in TYPE_MAP, like TIMESTAMP, but none of the TIMESTAMP handling applied to it:

• No bounds. Z3 could give it any integer.
• No conversion back. SMTLibZ3DbConstraintSolver built a plain LongGene, so the INSERT carried the bare integer, e.g. INSERT INTO EV (D, …) VALUES (2, …). H2 rejects it with Data conversion error.
• No literals. DATE '2024-01-01' threw "Extraction of condition not yet implemented" in the condition parser, so the whole WHERE clause was dropped.

As a result, no row of a table with a DATE column was ever inserted, whatever the query. The failure is silent, because SqlScriptRunner.execInsert logs a failed insertion and carries on.

Fix

DATE now shares the TIMESTAMP encoding: epoch seconds, at midnight UTC.

• SmtLibGenerator: a DATE column gets the same epoch bounds as a TIMESTAMP one, plus (= (mod col 86400) 0) so the value is a whole day. DATE_TYPE is a constant next to TIMESTAMP_TYPE.
• SMTLibZ3DbConstraintSolver: a DATE value is rebuilt as 'yyyy-MM-dd', the same way a TIMESTAMP value is rebuilt as 'yyyy-MM-dd HH:mm:ss'.
• JSqlVisitor (dbconstraint): DATE 'yyyy-MM-dd' and the JDBC escape {d 'yyyy-MM-dd'} become the epoch seconds of that midnight, UTC.

Sharing the unit with TIMESTAMP also makes a comparison between a DATE column and a TIMESTAMP literal work.

Tests

• New DateColumnSolvingTest, end to end against Z3 and H2. For id = 1, d = DATE '2024-03-05', d > DATE '2024-01-01' and d > TIMESTAMP '2024-01-01 10:00:00', it solves the query, checks that the generated row is inserted (via executionResults, since failures are not thrown), and checks that the query returns it. All four fail on master with expected: <[true]> but was: <[false]>.
• WhereClauseTranslationLimitsTest: a new case checks that DATE '…' and {d '…'} encode as the epoch of their midnight.

All tests in core-extra/dbconstraint and under org.evomaster.core.database.sql.solver pass.

Out of scope

A quoted string compared against a DATE or TIMESTAMP column, e.g. d > '2024-01-01', still compares an Int with a String and gets no data. That is a separate follow-up.