Integrate Solver with ApiWsStructureMutator

.gitignore

@@ -123,6 +123,7 @@ Migrations/
 /e2e-tests/spring-rest-mysql-column-types/target/
 /e2e-tests/spring-rest-postgres-column-types/target/
 /e2e-tests/spring-rest-h2-column-types/target/
+/e2e-tests/spring-rest-h2-z3solver/target/
 /test-old-libraries/target/
 /e2e-tests/spring-web/target/
 /e2e-tests/spring-rest-mongo/target/
@@ -166,5 +167,7 @@ Migrations/
 /e2e-tests/spring-rest-bb/maven/target/
 /target/
 /wfc/target/
+
+*.DS_Store
 /e2e-tests/emb-json/target/
 /process_data/

client-java/sql-dto/src/main/java/org/evomaster/client/java/controller/api/dto/database/execution/SqlExecutionsDto.java

@@ -54,9 +54,9 @@ public class SqlExecutionsDto {
      * Every time there is a WHERE clause which "failed" (ie, resulted in false),
      * we keep track of which tables/columns where involved in determining the
      * result of the WHERE.
-     *
      * If there is no WHERE, but still no data was returned, we consider it
      * as a failed WHERE
+     * The key is the table name and the value is the set of columns involved in the WHERE
      */
     public Map<String, Set<String>> failedWhere = new HashMap<>();
 

core/src/main/kotlin/org/evomaster/core/BaseModule.kt

@@ -14,8 +14,7 @@ import org.evomaster.core.search.service.mutator.MutationWeightControl
 import org.evomaster.core.search.service.mutator.genemutation.ArchiveGeneMutator
 import org.evomaster.core.search.tracer.ArchiveMutationTrackService
 import org.evomaster.core.search.tracer.TrackService
-
-
+import org.evomaster.core.solver.SMTLibZ3DbConstraintSolver
 
 
 /**
@@ -87,6 +86,9 @@ class BaseModule(val args: Array<String>, val noTests: Boolean = false) : Abstra
         bind(ExecutionInfoReporter::class.java)
                 .asEagerSingleton()
 
+        bind(SMTLibZ3DbConstraintSolver::class.java)
+            .asEagerSingleton()
+
         //no longer needed if TestSuiteWriter is moved out?
 //        if(noTests){
 //            bind(TestCaseWriter::class.java)

core/src/main/kotlin/org/evomaster/core/Main.kt

@@ -12,8 +12,6 @@ import org.evomaster.core.AnsiColor.Companion.inRed
 import org.evomaster.core.AnsiColor.Companion.inYellow
 import org.evomaster.core.config.ConfigProblemException
 import org.evomaster.core.logging.LoggingUtil
-import org.evomaster.core.output.OutputFormat
-import org.evomaster.core.output.Termination
 import org.evomaster.core.output.TestSuiteSplitter
 import org.evomaster.core.output.clustering.SplitResult
 import org.evomaster.core.output.service.TestSuiteWriter

core/src/main/kotlin/org/evomaster/core/problem/api/service/ApiWsStructureMutator.kt

@@ -22,6 +22,7 @@ import org.evomaster.core.search.gene.sql.SqlPrimaryKeyGene
 import org.evomaster.core.search.impact.impactinfocollection.ImpactsOfIndividual
 import org.evomaster.core.search.service.mutator.MutatedGeneSpecification
 import org.evomaster.core.search.service.mutator.StructureMutator
+import org.evomaster.core.solver.SMTLibZ3DbConstraintSolver
 import org.evomaster.core.sql.SqlAction
 import org.evomaster.core.sql.SqlActionUtils
 import org.evomaster.core.sql.SqlInsertBuilder
@@ -46,6 +47,12 @@ abstract class ApiWsStructureMutator : StructureMutator() {
     @Inject
     protected lateinit var harvestResponseHandler: HarvestActualHttpWsResponseHandler
 
+    // TODO: This should only be initialized when config.generateSqlDataWithDSE is enabled
+    // TODO: Also, z3solver.close() should be invoked
+    // when the application is shutting down to stop the Docker container and clean the tmp folder
+    @Inject
+    protected lateinit var z3Solver: SMTLibZ3DbConstraintSolver
+
     override fun addAndHarvestExternalServiceActions(
         individual: EvaluatedIndividual<*>,
         /**
@@ -268,7 +275,8 @@ abstract class ApiWsStructureMutator : StructureMutator() {
 
         val oldSqlActions = mutableListOf<EnvironmentAction>().plus(ind.seeInitializingActions())
 
-        val addedSqlInsertions = handleFailedWhereSQL(ind, fw, mutatedGenes, sampler)
+        val failedWhereQueries = evaluatedIndividual.fitness.getViewOfAggregatedFailedWhereQueries()
+        val addedSqlInsertions = handleFailedWhereSQL(ind, fw, failedWhereQueries, mutatedGenes, sampler)
 
         ind.repairInitializationActions(randomness)
         // update impact based on added genes
@@ -289,6 +297,10 @@ abstract class ApiWsStructureMutator : StructureMutator() {
          * Map of FAILED WHERE clauses. from table name key to column name values
          */
         fw: Map<String, Set<String>>,
+        /**
+         * List queries with FAILED WHERE clauses
+         */
+        failedWhereQueries: List<String>,
         mutatedGenes: MutatedGeneSpecification?, sampler: ApiWsSampler<T>
     ): MutableList<List<SqlAction>>? {
 
@@ -297,7 +309,7 @@ abstract class ApiWsStructureMutator : StructureMutator() {
         }
 
         if (config.generateSqlDataWithDSE) {
-            return handleDSE(sampler, fw)
+            return handleDSE(ind, sampler, failedWhereQueries)
         }
 
         return mutableListOf()
@@ -385,9 +397,18 @@ abstract class ApiWsStructureMutator : StructureMutator() {
         return addedSqlInsertions
     }
 
-    private fun <T : ApiWsIndividual> handleDSE(sampler: ApiWsSampler<T>, fw: Map<String, Set<String>>): MutableList<List<SqlAction>> {
-        /* TODO: DSE should be plugged in here */
-        return mutableListOf()
+    private fun <T : ApiWsIndividual> handleDSE(ind: T, sampler: ApiWsSampler<T>, failedWhereQueries: List<String>): MutableList<List<SqlAction>> {
+        val schemaDto = sampler.sqlInsertBuilder?.schemaDto
+            ?: throw IllegalStateException("No DB schema is available")
+
+        val newActions = mutableListOf<List<SqlAction>>()
+        for (query in failedWhereQueries) {
+            val newActionsForQuery = z3Solver.solve(schemaDto, query)
+            newActions.addAll(mutableListOf(newActionsForQuery))
+            ind.addInitializingDbActions(actions = newActionsForQuery)
+        }
+
+        return newActions
     }
 
     private fun <T : ApiWsIndividual> handleFailedFind(

core/src/main/kotlin/org/evomaster/core/search/FitnessValue.kt

@@ -79,13 +79,19 @@ class FitnessValue(
 
     /**
      * When SUT does SQL commands using WHERE, keep track of when those "fails" (ie evaluate
-     * to false), in particular the tables and columns in them involved
+     * to false), in particular, the tables and columns in them involved
      */
     private val aggregatedFailedWhere: MutableMap<String, Set<String>> = mutableMapOf()
 
+    /**
+     * When SUT does SQL commands using WHERE, keep track of when those "fails" (ie evaluate
+     * to false), in particular, the sql query involved
+     */
+    private val aggregatedFailedWhereQueries: MutableList<String> = mutableListOf()
+
     /**
      * When SUT does MONGO commands using FIND, keep track of when those "fails" (ie evaluate
-     * to false), in particular the collection and fields in them involved
+     * to false), in particular, the collection and fields in them involved
      */
     private val aggregatedFailedFind: MutableList<MongoFailedQuery> = mutableListOf()
 
@@ -140,6 +146,11 @@ class FitnessValue(
                 databaseExecutions.values,
                 {x ->  x.failedWhere}
         ))
+
+        aggregatedFailedWhereQueries.clear()
+        aggregatedFailedWhereQueries.addAll(
+            databaseExecutions.values.flatMap { a -> a.executionInfo }.map{ b -> b.sqlCommand }
+        )
     }
     fun aggregateMongoDatabaseData(){
         aggregatedFailedFind.clear()
@@ -166,6 +177,8 @@ class FitnessValue(
 
     fun getViewOfAggregatedFailedWhere() = aggregatedFailedWhere
 
+    fun getViewOfAggregatedFailedWhereQueries() = aggregatedFailedWhereQueries
+
     fun getViewOfAggregatedFailedFind() = aggregatedFailedFind
 
     fun doesCover(target: Int): Boolean {

core/src/main/kotlin/org/evomaster/core/solver/DbConstraintSolver.kt

@@ -1,5 +1,6 @@
 package org.evomaster.core.solver
 
+import org.evomaster.client.java.controller.api.dto.database.schema.DbInfoDto
 import org.evomaster.core.sql.SqlAction
 
 /**
@@ -12,5 +13,5 @@ interface DbConstraintSolver : AutoCloseable {
      * Solves the given constraints and returns the Db Gene to insert in the database
      * @return a list of SQLAction with the inserts in the db for the given constraints
      */
-    fun solve(sqlQuery: String): List<SqlAction>
+    fun solve(schemaDto: DbInfoDto, sqlQuery: String, numberOfRows: Int = 1): List<SqlAction>
 }

core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt

@@ -91,9 +91,13 @@ class SMTConditionVisitor(
         return when {
             operand.contains(".") -> { // Handle column references with aliases
                 val parts = operand.split(".")
-                val tableName = tableAliases[parts[0]] ?: defaultTableName
-                val columnName = parts[parts.lastIndex]
-                getColumnReference(tableName, columnName)
+                if (tableAliases.containsKey(parts[0])) {
+                    val tableName = tableAliases[parts[0]] ?: defaultTableName
+                    val columnName = parts[parts.lastIndex]
+                    getColumnReference(tableName, columnName)
+                } else {
+                    operand
+                }
             }
             isAColumn(operand) -> { // Handle direct column references
                 getColumnReference(defaultTableName, operand)