Skip to content

Commit 9bee480

Browse files
agusaldasoroagusaldasoro
committed
Add constants
1 parent 127bf4c commit 9bee480

5 files changed

Lines changed: 84 additions & 56 deletions

File tree

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

Lines changed: 10 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
package org.evomaster.solver;
22

3+
import org.evomaster.solver.smtlib.CheckSatResponse;
34
import org.evomaster.solver.smtlib.SMTResultParser;
45
import org.testcontainers.containers.BindMode;
56
import org.testcontainers.containers.Container;
@@ -20,10 +21,10 @@ public class Z3DockerExecutor implements AutoCloseable {
2021
// The Docker entrypoint that keeps it running indefinitely
2122
public static final String ENTRYPOINT = "while :; do sleep 1000 ; done";
2223

23-
// SMT-LIB (check-sat) response tokens returned by Z3
24-
private static final String SAT = "sat";
25-
private static final String UNSAT = "unsat";
26-
private static final String UNKNOWN = "unknown";
24+
// Z3 CLI invocation
25+
private static final String Z3_COMMAND = "z3";
26+
// Soft per-query timeout flag: "-t:<ms>" makes (check-sat) return 'unknown' on expiry
27+
private static final String TIMEOUT_FLAG_PREFIX = "-t:";
2728
private final String containerPath = "/smt2-resources/";
2829
private final GenericContainer<?> z3Prover;
2930

@@ -77,8 +78,8 @@ public Z3Result solveFromFile(String fileName) {
7778
public Z3Result solveFromFile(String fileName, long timeoutMs) {
7879
try {
7980
Container.ExecResult result = timeoutMs > 0
80-
? z3Prover.execInContainer("z3", "-t:" + timeoutMs, containerPath + fileName)
81-
: z3Prover.execInContainer("z3", containerPath + fileName);
81+
? z3Prover.execInContainer(Z3_COMMAND, TIMEOUT_FLAG_PREFIX + timeoutMs, containerPath + fileName)
82+
: z3Prover.execInContainer(Z3_COMMAND, containerPath + fileName);
8283

8384
if (result.getExitCode() != 0) {
8485
return Z3Result.error("Z3 exited with code " + result.getExitCode()
@@ -92,16 +93,16 @@ public Z3Result solveFromFile(String fileName, long timeoutMs) {
9293
}
9394

9495
String trimmed = stdout.trim();
95-
if (trimmed.startsWith(UNSAT)) {
96+
if (trimmed.startsWith(CheckSatResponse.UNSAT)) {
9697
return Z3Result.unsat();
9798
}
9899
// "unknown" means Z3 could not decide (e.g. incomplete theory or timeout).
99100
// It must be handled explicitly: otherwise it would fall through and be parsed
100101
// as an empty model, silently masquerading as SAT.
101-
if (trimmed.startsWith(UNKNOWN)) {
102+
if (trimmed.startsWith(CheckSatResponse.UNKNOWN)) {
102103
return Z3Result.unknown();
103104
}
104-
if (!trimmed.startsWith(SAT)) {
105+
if (!trimmed.startsWith(CheckSatResponse.SAT)) {
105106
return Z3Result.error("Unexpected Z3 output for file " + fileName + ": " + stdout);
106107
}
107108

‎core-extra/solver/src/main/java/org/evomaster/solver/smtlib/CheckSatResponse.java‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
package org.evomaster.solver.smtlib;
2+
3+
/**
4+
* The textual response tokens produced by SMT-LIB's {@code (check-sat)} command, as returned by Z3.
5+
* Shared between {@code Z3DockerExecutor} (which classifies the raw output) and {@link SMTResultParser}
6+
* so the tokens are defined in a single place.
7+
*/
8+
public final class CheckSatResponse {
9+
10+
private CheckSatResponse() {
11+
}
12+
13+
public static final String SAT = "sat";
14+
public static final String UNSAT = "unsat";
15+
public static final String UNKNOWN = "unknown";
16+
}

‎core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -53,14 +53,14 @@ public static Z3Solution parseZ3Response(String z3Response) {
5353
// Defensive: Z3DockerExecutor already classifies 'unsat'/'unknown' before invoking this
5454
// parser, so in practice only 'sat' models reach here. This guard is kept as a safety net
5555
// in case the parser is ever called directly with an unsat response.
56-
if (line.startsWith("unsat")) {
56+
if (line.startsWith(CheckSatResponse.UNSAT)) {
5757
throw new RuntimeException("Unsatisfiable problem");
5858
}
5959
if (line.trim().isEmpty()) {
6060
continue; // Skip empty lines
6161
}
6262

63-
if (line.startsWith("sat")) {
63+
if (line.startsWith(CheckSatResponse.SAT)) {
6464
buffer.setLength(0); // Reset buffer if a new result starts
6565
continue;
6666
}

‎core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -303,14 +303,14 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
303303
var gene: Gene = IntegerGene(dbColumnName, 0)
304304
when (val columnValue = columns.getField(smtColumn)) {
305305
is StringValue -> {
306-
gene = if (hasColumnType(schemaDto, table, dbColumnName, "BOOLEAN")) {
306+
gene = if (hasColumnType(schemaDto, table, dbColumnName, SmtLibGenerator.BOOLEAN_TYPE)) {
307307
BooleanGene(dbColumnName, toBoolean(columnValue.value))
308308
} else {
309309
StringGene(dbColumnName, columnValue.value)
310310
}
311311
}
312312
is LongValue -> {
313-
gene = if (hasColumnType(schemaDto, table, dbColumnName, "TIMESTAMP")) {
313+
gene = if (hasColumnType(schemaDto, table, dbColumnName, SmtLibGenerator.TIMESTAMP_TYPE)) {
314314
val epochSeconds = columnValue.value.toLong()
315315
val localDateTime = LocalDateTime.ofInstant(
316316
Instant.ofEpochSecond(epochSeconds), ZoneOffset.UTC

‎core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt‎

Lines changed: 54 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -169,20 +169,15 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
169169
private fun appendBooleanConstraints(smt: SMTLib) {
170170
for (smtTable in smtTables) {
171171
for (column in smtTable.dto.columns) {
172-
if (column.type.equals("BOOLEAN", ignoreCase = true)) {
172+
if (column.type.equals(BOOLEAN_TYPE, ignoreCase = true)) {
173173
val columnName = smtTable.smtColumnName(column.name).uppercase()
174174
for (i in 1..numberOfRows) {
175175
smt.addNode(
176176
AssertSMTNode(
177177
OrAssertion(
178-
listOf(
179-
EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"true\"")),
180-
EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"True\"")),
181-
EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"TRUE\"")),
182-
EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"false\"")),
183-
EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"False\"")),
184-
EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"FALSE\""))
185-
)
178+
BOOLEAN_LITERALS.map { literal ->
179+
EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"$literal\""))
180+
}
186181
)
187182
)
188183
)
@@ -195,25 +190,23 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
195190
private fun appendTimestampConstraints(smt: SMTLib) {
196191
for (smtTable in smtTables) {
197192
for (column in smtTable.dto.columns) {
198-
if (column.type.equals("TIMESTAMP", ignoreCase = true)) {
193+
if (column.type.equals(TIMESTAMP_TYPE, ignoreCase = true)) {
199194
val columnName = smtTable.smtColumnName(column.name).uppercase()
200-
val lowerBound = 0 // Example for Unix epoch start
201-
val upperBound = 32503680000 // Example for year 3000 in seconds
202195

203196
for (i in 1..numberOfRows) {
204197
smt.addNode(
205198
AssertSMTNode(
206199
GreaterThanOrEqualsAssertion(
207200
"($columnName ${smtTable.smtName}$i)",
208-
lowerBound.toString()
201+
TIMESTAMP_EPOCH_LOWER_BOUND.toString()
209202
)
210203
)
211204
)
212205
smt.addNode(
213206
AssertSMTNode(
214207
LessThanOrEqualsAssertion(
215208
"($columnName ${smtTable.smtName}$i)",
216-
upperBound.toString()
209+
TIMESTAMP_EPOCH_UPPER_BOUND.toString()
217210
)
218211
)
219212
)
@@ -604,44 +597,62 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
604597

605598
companion object {
606599

600+
// Bounds for TIMESTAMP columns, encoded as epoch seconds (SMT Int).
601+
private const val TIMESTAMP_EPOCH_LOWER_BOUND = 0L // Unix epoch start
602+
private const val TIMESTAMP_EPOCH_UPPER_BOUND = 32503680000L // ~year 3000, in seconds
603+
604+
// SMT-LIB sorts used as TYPE_MAP targets.
605+
private const val SMT_INT = "Int"
606+
private const val SMT_REAL = "Real"
607+
private const val SMT_STRING = "String"
608+
609+
// SQL type names that need special interpretation beyond their SMT sort: BOOLEAN is encoded as an
610+
// SMT String and TIMESTAMP as an SMT Int, so gene reconstruction must consult the original type.
611+
// Shared with the comparison sites in this class and referenced by SMTLibZ3DbConstraintSolver.
612+
const val BOOLEAN_TYPE = "BOOLEAN"
613+
const val TIMESTAMP_TYPE = "TIMESTAMP"
614+
615+
// The string values a BOOLEAN column may take (BOOLEAN is encoded as an SMT String).
616+
private val BOOLEAN_LITERALS = listOf("true", "True", "TRUE", "false", "False", "FALSE")
617+
607618
// Maps database column types to SMT-LIB types.
608619
// FUTURE WORK: this is one of three independent type vocabularies interpreting ColumnDto.type
609620
// (the others are SMTLibZ3DbConstraintSolver.getColumnDataType and .hasColumnType). They can
610621
// silently disagree when a backend reports a variant spelling; consolidating them into a single
611622
// source of truth is future work (see the note on SMTLibZ3DbConstraintSolver.hasColumnType).
612623
private val TYPE_MAP = mapOf(
613-
"BIGINT" to "Int",
614-
"BIT" to "Int",
615-
"INTEGER" to "Int",
616-
"INT" to "Int",
617-
"INT2" to "Int",
618-
"INT4" to "Int",
619-
"INT8" to "Int",
620-
"TINYINT" to "Int",
621-
"SMALLINT" to "Int",
624+
"BIGINT" to SMT_INT,
625+
"BIT" to SMT_INT,
626+
"INTEGER" to SMT_INT,
627+
"INT" to SMT_INT,
628+
"INT2" to SMT_INT,
629+
"INT4" to SMT_INT,
630+
"INT8" to SMT_INT,
631+
"TINYINT" to SMT_INT,
632+
"SMALLINT" to SMT_INT,
622633
// KNOWN LIMITATION: NUMERIC is mapped to Int, so any fractional part is truncated. This is
623634
// inconsistent with DECIMAL (mapped to Real). Mapping NUMERIC to Real (to preserve decimals)
624635
// is future work.
625-
"NUMERIC" to "Int",
626-
"SERIAL" to "Int",
627-
"SMALLSERIAL" to "Int",
628-
"BIGSERIAL" to "Int",
629-
"TIMESTAMP" to "Int",
630-
"DATE" to "Int",
631-
"FLOAT" to "Real",
632-
"DOUBLE" to "Real",
633-
"DECIMAL" to "Real",
634-
"REAL" to "Real",
635-
"CHARACTER VARYING" to "String",
636-
"CHAR" to "String",
637-
"VARCHAR" to "String",
638-
"TEXT" to "String",
639-
"CHARACTER LARGE OBJECT" to "String",
640-
"BOOLEAN" to "String",
641-
"BOOL" to "String",
642-
"UUID" to "String",
643-
"JSONB" to "String",
644-
"BYTEA" to "String",
636+
"NUMERIC" to SMT_INT,
637+
"SERIAL" to SMT_INT,
638+
"SMALLSERIAL" to SMT_INT,
639+
"BIGSERIAL" to SMT_INT,
640+
TIMESTAMP_TYPE to SMT_INT,
641+
"DATE" to SMT_INT,
642+
"FLOAT" to SMT_REAL,
643+
"DOUBLE" to SMT_REAL,
644+
"DECIMAL" to SMT_REAL,
645+
"REAL" to SMT_REAL,
646+
"CHARACTER VARYING" to SMT_STRING,
647+
"CHAR" to SMT_STRING,
648+
"VARCHAR" to SMT_STRING,
649+
"TEXT" to SMT_STRING,
650+
"CHARACTER LARGE OBJECT" to SMT_STRING,
651+
BOOLEAN_TYPE to SMT_STRING,
652+
"BOOL" to SMT_STRING,
653+
"UUID" to SMT_STRING,
654+
"JSONB" to SMT_STRING,
655+
"BYTEA" to SMT_STRING,
645656
)
646657
}
647658
}

0 commit comments

Comments
 (0)