From 67b43416f2d8ee3a78fc14af16bff705392b9889 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Thu, 12 Feb 2026 10:34:24 -0300 Subject: [PATCH] Add more types in schema z3 solver support --- .../core/problem/api/service/ApiWsStructureMutator.kt | 1 - .../main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt | 4 +++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/core/src/main/kotlin/org/evomaster/core/problem/api/service/ApiWsStructureMutator.kt b/core/src/main/kotlin/org/evomaster/core/problem/api/service/ApiWsStructureMutator.kt index c90654717b..e2085301bf 100644 --- a/core/src/main/kotlin/org/evomaster/core/problem/api/service/ApiWsStructureMutator.kt +++ b/core/src/main/kotlin/org/evomaster/core/problem/api/service/ApiWsStructureMutator.kt @@ -399,7 +399,6 @@ abstract class ApiWsStructureMutator : StructureMutator() { } private fun handleDSE(ind: T, sampler: ApiWsSampler, failedWhereQueries: List): MutableList> { - /* TODO: DSE should be plugged in here */ val schemaDto = sampler.sqlInsertBuilder?.schemaDto ?: throw IllegalStateException("No DB schema is available") diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt index ef732b3ecd..5f5e856805 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt @@ -523,9 +523,10 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I // Maps database column types to SMT-LIB types private val TYPE_MAP = mapOf( "BIGINT" to "Int", + "BIT" to "Int", "INTEGER" to "Int", "TINYINT" to "Int", - "TIMESTAMP" to "Int", + "TIMESTAMP" to "Int ", "DATE" to "Int", "FLOAT" to "Real", "DOUBLE" to "Real", @@ -534,6 +535,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I "CHARACTER VARYING" to "String", "CHAR" to "String", "VARCHAR" to "String", + "TEXT" to "String", "CHARACTER LARGE OBJECT" to "String", "BOOLEAN" to "String", // TODO: Check this )