Encode string literals compared with DATE or TIMESTAMP columns

[agusaldasoro]

Stacked on #1846.

Problem

DATE and TIMESTAMP columns are encoded as epoch seconds (an SMT Int). A typed literal such as TIMESTAMP '2024-01-01 10:00:00' or, with #1846, DATE '2024-01-01' is converted to epoch seconds by the condition parser. A plain string literal is not: WHERE d > '2024-01-01' was written as (> (D ev__1) "2024-01-01"). Z3 rejects the formula for comparing an Int with a String, so the query gets no data. The same happened for TIMESTAMP columns (ts > '2024-01-01 10:00:00') and for IN lists.

Plain string literals are the common case: SQL written by hand, and the bound parameters of ORM queries, rarely use the typed form.

Fix

• JSqlVisitor.toEpochSeconds(String) (dbconstraint) is now public. It is the existing conversion used for typed TIMESTAMP literals, extracted unchanged. It accepts the same layouts (T or space separator, optional seconds and fraction, offsets), and reads a bare date as midnight UTC.
• SMTConditionVisitor: when one side of a comparison is a DATE or TIMESTAMP column of the schema and the other is a string literal, the literal is encoded with toEpochSeconds, on either side. The same applies to the string literals of an IN list on such a column.
  • A date before 1970 is written as (- n), since SMT-LIB has no negative numerals.
  • A string that is not a date or timestamp throws a DateTimeParseException. Only that conjunct is dropped and counted as a partial translation, like any other untranslatable condition.

Tests

• DateColumnSolvingTest (end to end against Z3 and H2) gets four more queries: d > '2024-01-01', '2024-03-05' = d, d IN ('2024-03-05', '2024-03-06') and ts > '2024-01-01 10:00:00'. Each checks that the generated row is inserted and returned by the query. All four fail on Encode DATE columns like TIMESTAMP ones #1846 (no actions).
• New TemporalStringLiteralTranslationTest, on the generated SMT-LIB. It checks the epoch encoding, the negated numeral for a date before 1970, and that a non-date string drops only its own conjunct. All three fail on Encode DATE columns like TIMESTAMP ones #1846.

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