Z3-based SQL data generation: memoization, explicit outcomes, statistics & fixes

client-java/sql/src/main/java/org/evomaster/client/java/sql/heuristic/SqlHeuristicsCalculator.java

@@ -124,7 +124,8 @@ public SqlDistanceWithMetrics computeDistance(String sqlCommand) {
             double distanceToTrue = 1.0d - t.getOfTrue();
             return new SqlDistanceWithMetrics(distanceToTrue, 0, false);
         } catch (Exception ex) {
-            SimpleLogger.uniqueWarn("Failed to compute complete SQL heuristics for: " + sqlCommand);
+            SimpleLogger.uniqueWarn("Failed to compute complete SQL heuristics for: " + sqlCommand
+                    + " | cause: " + ex.getClass().getName() + ": " + ex.getMessage());
             return new SqlDistanceWithMetrics(Double.MAX_VALUE, 0, true);
         }
     }

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

@@ -13,6 +13,10 @@
 import net.sf.jsqlparser.statement.select.Select;
 import org.evomaster.dbconstraint.ast.*;
 
+import java.math.BigInteger;
+import java.sql.Timestamp;
+import java.time.ZoneOffset;
+import java.time.format.DateTimeFormatter;
 import java.util.ArrayDeque;
 import java.util.ArrayList;
 import java.util.Deque;
@@ -24,6 +28,13 @@ public class JSqlVisitor implements ExpressionVisitor {
     private static final String SIMILAR_ESCAPE = "similar_escape";
     private static final String SIMILAR_TO_ESCAPE = "similar_to_escape";
 
+    private static final String LOWER = "LOWER";
+    private static final String UPPER = "UPPER";
+
+    private static final String SINGLE_QUOTE_CHAR = "'";
+
+    private static final String TIMESTAMP_FORMAT = "yyyy-MM-dd HH:mm:ss";
+
     private final Deque<SqlCondition> stack = new ArrayDeque<>();
 
     @Override
@@ -45,7 +56,14 @@ public void visit(NullValue nullValue) {
 
     @Override
     public void visit(Function function) {
-        // TODO This translation should be implemented
+        String name = function.getName().toUpperCase();
+        if ((name.equals(LOWER) || name.equals(UPPER))
+                && function.getParameters() != null
+                && function.getParameters().size() == 1) {
+            // Treat LOWER(col)/UPPER(col) as the column itself (case-folding is dropped as an approximation)
+            function.getParameters().get(0).accept(this);
+            return;
+        }
         throw new RuntimeException("Extraction of condition not yet implemented");
     }
 
@@ -113,8 +131,10 @@ public void visit(TimeValue timeValue) {
 
     @Override
     public void visit(TimestampValue timestampValue) {
-        // TODO This translation should be implemented
-        throw new RuntimeException("Extraction of condition not yet implemented");
+        // Treat the timestamp string as UTC so the epoch round-trips consistently with the
+        // UTC-based decoder in SMTLibZ3DbConstraintSolver (LocalDateTime.ofInstant(..., UTC)).
+        long epochSeconds = timestampValue.getValue().toLocalDateTime().toEpochSecond(ZoneOffset.UTC);
+        stack.push(new SqlBigIntegerLiteralValue(BigInteger.valueOf(epochSeconds)));
     }
 
     @Override
@@ -127,7 +147,7 @@ public void visit(StringValue stringValue) {
         String notEscapedValue = stringValue.getNotExcapedValue();
 
         String notEscapedValueNoQuotes;
-        if (notEscapedValue.startsWith("'") && notEscapedValue.endsWith("'")) {
+        if (notEscapedValue.startsWith(SINGLE_QUOTE_CHAR) && notEscapedValue.endsWith(SINGLE_QUOTE_CHAR)) {
             notEscapedValueNoQuotes = notEscapedValue.substring(1, notEscapedValue.length() - 1);
         } else {
             notEscapedValueNoQuotes = notEscapedValue;
@@ -599,7 +619,19 @@ public void visit(TimeKeyExpression timeKeyExpression) {
 
     @Override
     public void visit(DateTimeLiteralExpression dateTimeLiteralExpression) {
-        // TODO This translation should be implemented
+        if (dateTimeLiteralExpression.getType() == DateTimeLiteralExpression.DateTime.TIMESTAMP) {
+            String value = dateTimeLiteralExpression.getValue();
+            if (value.startsWith(SINGLE_QUOTE_CHAR) && value.endsWith(SINGLE_QUOTE_CHAR)) {
+                value = value.substring(1, value.length() - 1);
+            }
+            // Treat the timestamp string as UTC to match the UTC-based decoder in
+            // SMTLibZ3DbConstraintSolver (LocalDateTime.ofInstant(..., UTC)).
+            long epochSeconds = java.time.LocalDateTime.parse(value,
+                    DateTimeFormatter.ofPattern(TIMESTAMP_FORMAT))
+                    .toEpochSecond(ZoneOffset.UTC);
+            stack.push(new SqlBigIntegerLiteralValue(BigInteger.valueOf(epochSeconds)));
+            return;
+        }
         throw new RuntimeException("Extraction of condition not yet implemented");
     }
 

core-extra/dbconstraint/src/test/java/org/evomaster/dbconstraint/parser/JSqlConditionParserTest.java

@@ -1,12 +1,12 @@
 package org.evomaster.dbconstraint.parser;
 
 import org.evomaster.dbconstraint.ConstraintDatabaseType;
-import org.evomaster.dbconstraint.ast.SqlCondition;
-import org.evomaster.dbconstraint.ast.SqlInCondition;
+import org.evomaster.dbconstraint.ast.*;
 import org.evomaster.dbconstraint.parser.jsql.JSqlConditionParser;
 import org.junit.jupiter.api.Test;
 
 import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertInstanceOf;
 import static org.junit.jupiter.api.Assertions.assertTrue;
 
 public class JSqlConditionParserTest {
@@ -104,4 +104,51 @@ public void testParseCastAsCharacterLargeObject() throws SqlConditionParserExcep
         assertEquals(expected, actual);
     }
 
+    @Test
+    public void testParseLowerFunction() throws SqlConditionParserException {
+        JSqlConditionParser parser = new JSqlConditionParser();
+        // LOWER(col) should be treated as col (case-folding dropped as approximation)
+        SqlCondition withLower = parser.parse("LOWER(commit_mgr_desc) != 'init'", ConstraintDatabaseType.H2);
+        SqlCondition withoutLower = parser.parse("commit_mgr_desc != 'init'", ConstraintDatabaseType.H2);
+        assertEquals(withoutLower, withLower);
+    }
+
+    @Test
+    public void testParseUpperFunction() throws SqlConditionParserException {
+        JSqlConditionParser parser = new JSqlConditionParser();
+        SqlCondition withUpper = parser.parse("UPPER(status) != 'ACTIVE'", ConstraintDatabaseType.H2);
+        SqlCondition withoutUpper = parser.parse("status != 'ACTIVE'", ConstraintDatabaseType.H2);
+        assertEquals(withoutUpper, withUpper);
+    }
+
+    @Test
+    public void testParseIsNotNullOrLower() throws SqlConditionParserException {
+        // Pattern seen in tracking-system: col IS NOT NULL OR LOWER(other_col) != 'init'
+        JSqlConditionParser parser = new JSqlConditionParser();
+        SqlCondition condition = parser.parse(
+                "commit_emp_desc IS NOT NULL OR LOWER(commit_mgr_desc) != 'init'",
+                ConstraintDatabaseType.H2);
+        assertInstanceOf(SqlOrCondition.class, condition);
+    }
+
+    @Test
+    public void testParseTimestampLiteral() throws SqlConditionParserException {
+        // Pattern seen in tracking-system: col = TIMESTAMP 'datetime-string'
+        JSqlConditionParser parser = new JSqlConditionParser();
+        SqlCondition condition = parser.parse(
+                "commit_date = TIMESTAMP '2020-11-26 10:49:41'",
+                ConstraintDatabaseType.H2);
+        assertInstanceOf(SqlComparisonCondition.class, condition);
+        SqlComparisonCondition cmp = (SqlComparisonCondition) condition;
+        assertInstanceOf(SqlBigIntegerLiteralValue.class, cmp.getRightOperand());
+        // The epoch value must be computed in UTC so that the round-trip in
+        // SMTLibZ3DbConstraintSolver (LocalDateTime.ofInstant(..., UTC)) preserves
+        // the original string representation regardless of JVM timezone.
+        SqlBigIntegerLiteralValue epoch = (SqlBigIntegerLiteralValue) cmp.getRightOperand();
+        long expected = java.time.LocalDateTime.parse("2020-11-26 10:49:41",
+                java.time.format.DateTimeFormatter.ofPattern("yyyy-MM-dd HH:mm:ss"))
+                .toEpochSecond(java.time.ZoneOffset.UTC);
+        assertEquals(java.math.BigInteger.valueOf(expected), epoch.getBigInteger());
+    }
+
 }

core-extra/solver/src/main/java/org/evomaster/solver/Z3DockerExecutor.java

@@ -1,14 +1,12 @@
 package org.evomaster.solver;
 
 import org.evomaster.solver.smtlib.SMTResultParser;
-import org.evomaster.solver.smtlib.value.SMTLibValue;
 import org.testcontainers.containers.BindMode;
 import org.testcontainers.containers.Container;
 import org.testcontainers.containers.GenericContainer;
 import org.testcontainers.images.builder.ImageFromDockerfile;
 
 import java.io.IOException;
-import java.util.Map;
 import java.util.Optional;
 
 /**
@@ -21,6 +19,11 @@ public class Z3DockerExecutor implements AutoCloseable {
     public static final String Z3_DOCKER_IMAGE = "ghcr.io/z3prover/z3:ubuntu-20.04-bare-z3-sha-ba8d8f0";
     // The Docker entrypoint that keeps it running indefinitely
     public static final String ENTRYPOINT = "while :; do sleep 1000 ; done";
+
+    // SMT-LIB (check-sat) response tokens returned by Z3
+    private static final String SAT = "sat";
+    private static final String UNSAT = "unsat";
+    private static final String UNKNOWN = "unknown";
     private final String containerPath = "/smt2-resources/";
     private final GenericContainer<?> z3Prover;
 
@@ -54,28 +57,60 @@ public Z3DockerExecutor(String resourcesFolder) {
      * The file must be in the directory specified by containerPath.
      *
      * @param fileName the name of the SMT-LIB file to read and solve
-     * @return the result of the Z3 solver as a map of variable names to their values, if the problem is satisfiable (sat)
-     *         or an empty Optional if the problem is unsatisfiable (unsat)
+     * @return a {@link Z3Result} with status SAT (and the solution), UNSAT, UNKNOWN, or ERROR
+     */
+    public Z3Result solveFromFile(String fileName) {
+        return solveFromFile(fileName, 0);
+    }
+
+    /**
+     * Executes the Z3 solver on an SMT-LIB file located in the container.
+     * The file must be in the directory specified by containerPath.
+     *
+     * @param fileName  the name of the SMT-LIB file to read and solve
+     * @param timeoutMs soft per-query timeout in milliseconds. When greater than 0, it is passed
+     *                  to Z3 as {@code -t:<ms>}; if exceeded, Z3 returns {@code unknown} for the
+     *                  query (mapped to {@link Z3Result.Status#UNKNOWN}) rather than running
+     *                  unbounded. A value {@code <= 0} disables the timeout.
+     * @return a {@link Z3Result} with status SAT (and the solution), UNSAT, UNKNOWN, or ERROR
      */
-    public Optional<Map<String, SMTLibValue>> solveFromFile(String fileName) {
+    public Z3Result solveFromFile(String fileName, long timeoutMs) {
         try {
-            // Execute the Z3 solver on the specified file in the container
-            Container.ExecResult result = z3Prover.execInContainer("z3", containerPath + fileName);
+            Container.ExecResult result = timeoutMs > 0
+                    ? z3Prover.execInContainer("z3", "-t:" + timeoutMs, containerPath + fileName)
+                    : z3Prover.execInContainer("z3", containerPath + fileName);
+
             if (result.getExitCode() != 0) {
-                throw new RuntimeException("Error executing Z3 solver: \n" + result.getStdout() + "\n" + result.getStderr());
+                return Z3Result.error("Z3 exited with code " + result.getExitCode()
+                        + ": " + result.getStdout() + result.getStderr());
             }
+
             String stdout = result.getStdout();
+            if (stdout == null || stdout.trim().isEmpty()) {
+                return Z3Result.error("Z3 produced no output for file: " + fileName
+                        + " stderr: " + result.getStderr());
+            }
 
-            // Check if the solver returned any output
-            if (stdout == null || stdout.isEmpty()) {
-                String stderr = result.getStderr();
-                throw new RuntimeException("No result after solving file " + stderr);
+            String trimmed = stdout.trim();
+            if (trimmed.startsWith(UNSAT)) {
+                return Z3Result.unsat();
             }
+            // "unknown" means Z3 could not decide (e.g. incomplete theory or timeout).
+            // It must be handled explicitly: otherwise it would fall through and be parsed
+            // as an empty model, silently masquerading as SAT.
+            if (trimmed.startsWith(UNKNOWN)) {
+                return Z3Result.unknown();
+            }
+            if (!trimmed.startsWith(SAT)) {
+                return Z3Result.error("Unexpected Z3 output for file " + fileName + ": " + stdout);
+            }
+
+            return Z3Result.sat(SMTResultParser.parseZ3Response(stdout));
 
-            // Parse the solver output and return the result
-            return Optional.of(SMTResultParser.parseZ3Response(stdout));
         } catch (IOException | InterruptedException e) {
-            return Optional.empty();
+            return Z3Result.error("I/O or interruption error running Z3 on " + fileName + ": " + e.getMessage());
+        } catch (RuntimeException e) {
+            return Z3Result.error("Unexpected error parsing Z3 output for " + fileName + ": " + e.getMessage());
         }
     }
 

core-extra/solver/src/main/java/org/evomaster/solver/Z3Result.java

@@ -0,0 +1,72 @@
+package org.evomaster.solver;
+
+/**
+ * Represents the outcome of a Z3 solver invocation.
+ * Distinguishes between four possible states: SAT (satisfiable with a solution),
+ * UNSAT (unsatisfiable), UNKNOWN (Z3 could not decide, e.g. an incomplete theory
+ * or a timeout), and ERROR (solver or parsing failure).
+ */
+public class Z3Result {
+
+    public enum Status {
+        /** Z3 found a satisfying assignment. The solution is available. */
+        SAT,
+        /** The problem is unsatisfiable. No solution exists. */
+        UNSAT,
+        /**
+         * Z3 returned {@code unknown}: it could neither prove SAT nor UNSAT.
+         * Typical causes are an incomplete theory (e.g. non-linear arithmetic,
+         * quantifiers, some string/regex constraints) or a timeout. This is distinct
+         * from ERROR: the solver ran correctly, it just could not decide.
+         */
+        UNKNOWN,
+        /** A solver, I/O, or parsing error occurred. */
+        ERROR
+    }
+
+    private final Status status;
+    /** Non-null only when status == SAT. */
+    private final Z3Solution solution;
+    /** Non-null only when status == ERROR. */
+    private final String errorMessage;
+
+    private Z3Result(Status status, Z3Solution solution, String errorMessage) {
+        this.status = status;
+        this.solution = solution;
+        this.errorMessage = errorMessage;
+    }
+
+    public Status getStatus() {
+        return status;
+    }
+
+    /**
+     * @return the satisfying solution; non-null only when {@link #getStatus()} is SAT.
+     */
+    public Z3Solution getSolution() {
+        return solution;
+    }
+
+    /**
+     * @return the error message; non-null only when {@link #getStatus()} is ERROR.
+     */
+    public String getErrorMessage() {
+        return errorMessage;
+    }
+
+    public static Z3Result sat(Z3Solution solution) {
+        return new Z3Result(Status.SAT, solution, null);
+    }
+
+    public static Z3Result unsat() {
+        return new Z3Result(Status.UNSAT, null, null);
+    }
+
+    public static Z3Result unknown() {
+        return new Z3Result(Status.UNKNOWN, null, null);
+    }
+
+    public static Z3Result error(String message) {
+        return new Z3Result(Status.ERROR, null, message);
+    }
+}

core-extra/solver/src/main/java/org/evomaster/solver/Z3Solution.java

@@ -0,0 +1,55 @@
+package org.evomaster.solver;
+
+import org.evomaster.solver.smtlib.value.SMTLibValue;
+
+import java.util.Map;
+
+/**
+ * Represents a satisfying solution produced by the Z3 solver: a mapping from
+ * SMT-LIB variable/constant names to the values Z3 assigned to them.
+ */
+public class Z3Solution {
+
+    private final Map<String, SMTLibValue> assignments;
+
+    public Z3Solution(Map<String, SMTLibValue> assignments) {
+        this.assignments = assignments;
+    }
+
+    /**
+     * @return the assignments of this solution, keyed by variable/constant name.
+     */
+    public Map<String, SMTLibValue> getAssignments() {
+        return assignments;
+    }
+
+    /**
+     * @param name the variable/constant name
+     * @return the value assigned to the given name, or {@code null} if absent.
+     */
+    public SMTLibValue get(String name) {
+        return assignments.get(name);
+    }
+
+    /**
+     * @param name the variable/constant name
+     * @return whether the given name has an assigned value in this solution.
+     */
+    public boolean containsKey(String name) {
+        return assignments.containsKey(name);
+    }
+
+    /**
+     * @return the number of assignments in this solution.
+     */
+    public int size() {
+        return assignments.size();
+    }
+
+    /**
+     * @return whether this solution has no assignments.
+     */
+    public boolean isEmpty() {
+        return assignments.isEmpty();
+    }
+}