Cache deterministic Z3 errors

[agusaldasoro]

Problem

SMTLibZ3DbConstraintSolver never cached an ERROR result, on the grounds that it might be a transient Docker failure. Many errors are not transient, though:

• Z3 rejects the formula, e.g. because a generated literal is malformed. It prints (error "...") and exits with code 1.
• Z3's output cannot be parsed by SMTResultParser.

The same query produces the same formula and the same output every time. The search keeps producing such queries, so each reappearance paid for SMT-LIB generation, a temporary file and a full round-trip to the Z3 container, only to fail again. Each repeat was also counted as a new Z3 error in the statistics.

Fix

• Z3Result gets an isDeterministicError() flag and a deterministicError(message) factory. error(message) keeps its meaning: an error that may be transient.

• Z3DockerExecutor reports two cases as deterministic:

  • a non-zero exit whose stdout starts with (error, i.e. Z3 rejected the formula;
  • an exception thrown while parsing a sat model.

  Everything else stays a plain error: I/O or interruption, other exit codes, empty output, and other runtime exceptions while running the container. Their message no longer claims a parsing failure.

• SMTLibZ3DbConstraintSolver caches an ERROR only when it is deterministic. A cached error is served like a cached UNSAT: a cache hit that returns no actions. UNKNOWN and transient errors are still never cached.

Tests

Z3DockerExecutorTest, against the Z3 image:

• whenSolvingInvalidFileItReturnsError now also checks that the error is deterministic.
• New whenFormulaIsRejectedTheErrorIsDeterministic: a formula with an unescaped quote in a string literal, which Z3 rejects partway through the file.
• whenSolvingEmptyFileItReturnsError checks that empty output is not treated as deterministic.

All tests in core-extra/solver and under org.evomaster.core.database.sql.solver pass. The comments that said errors are never cached have been updated.

The caching itself is a single guarded line in the solver. It has no end-to-end test, because every query that currently makes Z3 fail is a bug fixed in another open PR (#1836, #1838), and such a test would break once those are merged.