[snapshot-regression-fix] Restore terminal "giveup" detection in the parallel tactic (pqffd)

[levnach]

Summary

Fixes a regression in the parallel tactic where a benchmark that should report unknown in well under a second instead spins until the wall-clock timeout.

• Originating discussion: https://github.com/Z3Prover/bench/discussions/2733
• Benchmark: iss-2922/bug-1.smt2 (uses (check-sat-using pqffd))
• Kind: diff
• z3 under test: z3-4.17.0-x64-glibc-2.39 (Nightly)

Divergence

The recorded oracle (193 B) shows z3 giving up quickly with a reason, then unknown, then a get-model error. Current z3 instead produces only timeout (8 B):

--- bug-1.expected.out (expected)
+++ produced (current z3)
@@ -1,6 +1 @@
-(sat.giveup interpreted functions sent to SAT solver (declare-fun = (a a) Bool)
-(declare-fun is (a) Bool)
-(declare-fun is (a) Bool)
-)
-unknown
-(error "line 8 column 10: model is not available")
+timeout

Root cause

The parallel tactic rewrite in commit 612fab1c9 ("Parallel tactic (#9824) (#9825)", +1970/−673 on src/solver/parallel_tactical.cpp) dropped the old terminal giveup detection.

Before that commit, the worker explicitly inspected reason_unknown() and stopped the whole search when a sub-solver gave up for a fundamental reason:

bool giveup() {
    ...
    std::string r = get_solver().reason_unknown();
    inc = "(incomplete";  m_giveup |= r.compare(0, inc.size(), inc) == 0;
    inc = "(sat.giveup";  m_giveup |= r.compare(0, inc.size(), inc) == 0;
    if (m_giveup) IF_VERBOSE(0, verbose_stream() << r << "\n");
    return m_giveup;
}
...
if (s.giveup()) { report_undef(s, s.get_solver().reason_unknown()); return; }

The new worker::run() loop treats every l_undef as resource-limited: it raises the per-thread conflict budget and splits the search into more cubes. But when the finite-domain solver is handed interpreted functions it cannot bit-blast, it returns l_undef with reason (sat.giveup interpreted functions sent to SAT solver ...). No amount of splitting or extra conflicts can ever change that answer, so the portfolio keeps retrying identical sub-problems until the -T:20 budget elapses — producing timeout instead of a fast unknown.

Fix

Re-introduce giveup detection in the new architecture (src/solver/parallel_tactical.cpp, +50 lines, single file):

• A small is_giveup_reason() helper recognises the terminal (sat.giveup / (incomplete prefixes reported by inc_sat_solver.
• In the worker's l_undef case, before raising conflicts or splitting, read reason_unknown(); if it is a giveup reason, stop the whole portfolio via a new batch_manager::set_giveup().
• set_giveup() records the reason, prints it at verbosity 0 (matching the prior tactic, which the snapshot oracle captures), sets a new terminal is_giveup state, and cancels the background threads. It is guarded by the batch-manager mutex and the is_running check so exactly one worker prints once and a single terminal verdict wins.
• get_result() maps is_giveup to l_undef; the reason is propagated to the goal in parallel_tactic::operator() so check-sat-using surfaces unknown with the reason.

Validation

Built the patched checkout and re-ran the benchmark with the same options the snapshot capture uses:

• cd z3 && ./configure && make -C build -j8 → build succeeded (Z3 version 4.17.0 - 64 bit).
• z3 -T:20 inputs/issues/iss-2922/bug-1.smt2 now matches the recorded oracle byte-for-byte (193 B, identical sha256), and completes in ~0.5 s instead of timing out at 20 s.
• Sanity checks: a normal pqffd SAT instance still returns sat with a correct model; a genuine resource-limited l_undef (empty/other reason) still falls through to the existing split-and-retry logic — only terminal giveup reasons short-circuit.

Opened as a draft for human review.

Co-authored-by: Copilot 223556219+Copilot@users.noreply.github.com

Generated by Fix a Z3 snapshot-regression divergence · 3.5K AIC · ⌖ 114.2 AIC · ⊞ 41.2K · ◷