Encode DATE columns like TIMESTAMP ones

core-extra/dbconstraint/src/main/java/org/evomaster/dbconstraint/parser/jsql/JSqlVisitor.java

@@ -20,6 +20,7 @@
 import java.time.format.DateTimeFormatterBuilder;
 import java.time.temporal.ChronoField;
 import java.time.temporal.TemporalAccessor;
+import java.time.LocalDate;
 import java.time.LocalDateTime;
 import java.time.OffsetDateTime;
 import java.util.ArrayDeque;
@@ -173,8 +174,8 @@ public void visit(HexValue hexValue) {
 
     @Override
     public void visit(DateValue dateValue) {
-        // TODO This translation should be implemented
-        throw new RuntimeException("Extraction of condition not yet implemented");
+        // JDBC escape {d 'yyyy-MM-dd'}: the same encoding as DATE 'yyyy-MM-dd'
+        pushDate(dateValue.getValue().toLocalDate());
     }
 
     @Override
@@ -749,9 +750,27 @@ public void visit(DateTimeLiteralExpression dateTimeLiteralExpression) {
             stack.push(new SqlBigIntegerLiteralValue(BigInteger.valueOf(epochSeconds)));
             return;
         }
+        if (dateTimeLiteralExpression.getType() == DateTimeLiteralExpression.DateTime.DATE) {
+            String value = dateTimeLiteralExpression.getValue();
+            if (value.startsWith(SINGLE_QUOTE_CHAR) && value.endsWith(SINGLE_QUOTE_CHAR)) {
+                value = value.substring(1, value.length() - 1);
+            }
+            pushDate(LocalDate.parse(value));
+            return;
+        }
         throw new RuntimeException("Extraction of condition not yet implemented");
     }
 
+    /**
+     * A DATE is encoded like a TIMESTAMP, in epoch seconds, at midnight UTC. Sharing the unit lets a
+     * DATE column be compared with a TIMESTAMP literal, and matches the decoder in
+     * SMTLibZ3DbConstraintSolver.
+     */
+    private void pushDate(LocalDate date) {
+        long epochSeconds = date.atStartOfDay().toEpochSecond(ZoneOffset.UTC);
+        stack.push(new SqlBigIntegerLiteralValue(BigInteger.valueOf(epochSeconds)));
+    }
+
     @Override
     public void visit(NotExpression notExpression) {
         // TODO This translation should be implemented

core/src/main/kotlin/org/evomaster/core/database/sql/solver/SmtLibGenerator.kt

@@ -98,6 +98,13 @@ class SmtLibGenerator(
         const val BOOLEAN_TYPE = "BOOLEAN"
         const val TIMESTAMP_TYPE = "TIMESTAMP"
 
+        /**
+         * Encoded like [TIMESTAMP_TYPE], in epoch seconds (SMT Int), constrained to midnight UTC. The
+         * shared unit lets a DATE column be compared with a TIMESTAMP literal.
+         */
+        const val DATE_TYPE = "DATE"
+        internal const val SECONDS_PER_DAY = 86400L
+
         /**
          * Encoded as SMT Strings with no constraint on their form, so the value Z3 assigns need not be
          * a valid UUID or JSON document; SMTLibZ3DbConstraintSolver turns it into one.
@@ -162,7 +169,7 @@ class SmtLibGenerator(
             "SMALLSERIAL" to SMT_INT,
             "BIGSERIAL" to SMT_INT,
             TIMESTAMP_TYPE to SMT_INT,
-            "DATE" to SMT_INT,
+            DATE_TYPE to SMT_INT,
             "FLOAT" to SMT_REAL,
             "DOUBLE" to SMT_REAL,
             "DECIMAL" to SMT_REAL,
@@ -417,7 +424,8 @@ class SmtLibGenerator(
     private fun appendTimestampConstraints(smt: SMTLib) {
         for (smtTable in smtTables) {
             for (column in smtTable.dto.columns) {
-                if (column.type.equals(TIMESTAMP_TYPE, ignoreCase = true)) {
+                val isDate = column.type.equals(DATE_TYPE, ignoreCase = true)
+                if (isDate || column.type.equals(TIMESTAMP_TYPE, ignoreCase = true)) {
                     val columnName = smtTable.smtColumnName(column.name).uppercase()
 
                     for (i in 1..numberOfRows) {
@@ -437,6 +445,15 @@ class SmtLibGenerator(
                                 )
                             )
                         )
+                        if (isDate) {
+                            smt.addNode(
+                                AssertSMTNode(
+                                    EqualsAssertion(
+                                        listOf("(mod ($columnName ${rowConstantName(smtTable.smtName, i)}) $SECONDS_PER_DAY)", "0")
+                                    )
+                                )
+                            )
+                        }
                     }
                 }
             }

core/src/main/kotlin/org/evomaster/core/database/sql/solver/service/SMTLibZ3DbConstraintSolver.kt

@@ -117,6 +117,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
         // reads a superset of the layouts a database may emit, of which this is one, so the value
         // round-trips: what is written here is read back to the same instant.
         private const val TIMESTAMP_FORMAT = "yyyy-MM-dd HH:mm:ss"
+        private const val DATE_FORMAT = "yyyy-MM-dd"
 
         private val UUID_PATTERN = Regex("[0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[0-9a-fA-F]{4}-[0-9a-fA-F]{4}-[0-9a-fA-F]{12}")
 
@@ -499,13 +500,20 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
                 }
             }
             is LongValue -> {
-                if (hasColumnType(schemaDto, table, dbColumnName, SmtLibGenerator.TIMESTAMP_TYPE)) {
+                val datePattern = when {
+                    hasColumnType(schemaDto, table, dbColumnName, SmtLibGenerator.TIMESTAMP_TYPE) -> TIMESTAMP_FORMAT
+                    // Without this a DATE column was inserted as a bare integer, which the
+                    // database rejects, so no row of its table was ever inserted
+                    hasColumnType(schemaDto, table, dbColumnName, SmtLibGenerator.DATE_TYPE) -> DATE_FORMAT
+                    else -> null
+                }
+                if (datePattern != null) {
                     val epochSeconds = columnValue.value.toLong()
                     val localDateTime = LocalDateTime.ofInstant(
                         Instant.ofEpochSecond(epochSeconds), ZoneOffset.UTC
                     )
                     val formatted = localDateTime.format(
-                        DateTimeFormatter.ofPattern(TIMESTAMP_FORMAT)
+                        DateTimeFormatter.ofPattern(datePattern)
                     )
                     ImmutableDataHolderGene(dbColumnName, formatted, inQuotes = true)
                 } else {
@@ -571,8 +579,8 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
      * compared case-insensitively as a raw string.
      *
      * CAVEAT: this relies on [ColumnDto.type] containing the exact spelling passed in (currently
-     * "BOOLEAN" and "TIMESTAMP"). It is needed because the SMT sort alone cannot recover these types
-     * (BOOLEAN is encoded as an SMT String, TIMESTAMP as an SMT Int), so gene reconstruction must
+     * "BOOLEAN", "TIMESTAMP" and "DATE"). It is needed because the SMT sort alone cannot recover these
+     * types (BOOLEAN is encoded as an SMT String, TIMESTAMP and DATE as an SMT Int), so gene reconstruction must
      * consult the original SQL type. The set of type spellings recognized here must stay consistent
      * with [SmtLibGenerator.TYPE_MAP]; if a backend reports a variant spelling (e.g. "BOOL" or
      * "TIMESTAMP WITHOUT TIME ZONE"), the special handling is silently skipped. Consolidating these

core/src/test/kotlin/org/evomaster/core/database/sql/solver/WhereClauseTranslationLimitsTest.kt

@@ -62,6 +62,16 @@ class WhereClauseTranslationLimitsTest {
         assertEpoch("T > TIMESTAMP '2026-08-18'", 1787011200)
     }
 
+    /**
+     * A DATE literal shares the TIMESTAMP encoding, at midnight UTC, so a DATE column can be compared
+     * with either. It used to be rejected, dropping the whole clause.
+     */
+    @Test
+    fun `date literals are encoded as the epoch of their midnight`() {
+        assertEpoch("D > DATE '2026-08-18'", 1787011200)
+        assertEpoch("D = {d '2026-08-18'}", 1787011200)
+    }
+
     /**
      * The layouts accepted are a set, not a prefix rule. A separator carries the time of day with it,
      * so a date followed by a dangling `T` or space is rejected rather than silently read as midnight,

core/src/test/kotlin/org/evomaster/core/database/sql/solver/service/DateColumnSolvingTest.kt

@@ -0,0 +1,73 @@
+package org.evomaster.core.database.sql.solver.service
+
+import org.evomaster.client.java.controller.api.dto.database.schema.DbInfoDto
+import org.evomaster.client.java.sql.DbInfoExtractor
+import org.evomaster.client.java.sql.SqlScriptRunner
+import org.evomaster.core.database.sql.SqlActionTransformer
+import org.junit.jupiter.api.AfterAll
+import org.junit.jupiter.api.Assertions.assertEquals
+import org.junit.jupiter.api.Assertions.assertFalse
+import org.junit.jupiter.api.BeforeAll
+import org.junit.jupiter.api.BeforeEach
+import org.junit.jupiter.params.ParameterizedTest
+import org.junit.jupiter.params.provider.ValueSource
+import java.sql.Connection
+import java.sql.DriverManager
+
+/**
+ * A DATE column is encoded, like a TIMESTAMP one, as epoch seconds, and must be inserted as a date.
+ *
+ * It used to be inserted as the bare integer Z3 assigned to it, which the database rejects, so no row
+ * of a table with a DATE column was ever inserted, whatever the query. The failure was silent:
+ * SqlScriptRunner.execInsert logs a failed insertion and carries on.
+ */
+class DateColumnSolvingTest {
+
+    companion object {
+        private lateinit var solver: SMTLibZ3DbConstraintSolver
+        private lateinit var connection: Connection
+        private lateinit var schemaDto: DbInfoDto
+
+        @JvmStatic
+        @BeforeAll
+        fun setup() {
+            connection = DriverManager.getConnection("jdbc:h2:mem:date_column_test", "sa", "")
+            SqlScriptRunner.execCommand(connection, "CREATE TABLE ev(id bigint primary key, d date);\n")
+            schemaDto = DbInfoExtractor.extract(connection)
+            solver = SMTLibZ3DbConstraintSolver()
+            solver.initializeExecutor()
+        }
+
+        @JvmStatic
+        @AfterAll
+        fun tearDown() {
+            connection.close()
+            if (this::solver.isInitialized) {
+                solver.close()
+            }
+        }
+    }
+
+    @BeforeEach
+    fun clean() {
+        SqlScriptRunner.execCommand(connection, "DELETE FROM ev;\n")
+    }
+
+    @ParameterizedTest
+    @ValueSource(strings = [
+        "SELECT * FROM ev WHERE id = 1",
+        "SELECT * FROM ev WHERE d = DATE '2024-03-05'",
+        "SELECT * FROM ev WHERE d > DATE '2024-01-01'",
+        "SELECT * FROM ev WHERE d > TIMESTAMP '2024-01-01 10:00:00'"
+    ])
+    fun generatedRowsAreInsertedAndSatisfyTheQuery(query: String) {
+        val actions = solver.solve(schemaDto, query, 1)
+        assertFalse(actions.isEmpty(), "Solver should return actions for a satisfiable query")
+
+        val results = SqlScriptRunner.execInsert(connection, SqlActionTransformer.transform(actions).insertions)
+        assertEquals(listOf(true), results.executionResults, "The generated row should be inserted")
+
+        val result = SqlScriptRunner.execCommand(connection, query)
+        assertFalse(result.isEmpty(), "Inserted rows should satisfy the original query")
+    }
+}