Add a fast pre-check for trivially unrealizable specs (inspired by ltlsynt's try_create_direct_strategy)

[gaperez64]

Context

When a spec contains a G(boolean) constraint that is only over inputs (or that the controller cannot help satisfy), the spec is unrealizable regardless of any strategy. acacia-bonsai currently doesn't recognize this structurally — it builds the BA, runs preprocessing, and grinds through the full K-bounded safety game until it gives up. ltlsynt has a fast path for exactly this case and returns UNREALIZABLE without ever building the arena.

Concrete example: selection-ltl-2025v2/selection-ltl-2025/Light_a50cadd7.tlsf (and Warnlight_a50cadd7.tlsf). One conjunct is G !(p0b0room29light29on <-> p0b0room29light29off) — both APs are inputs, so the controller has no influence. ltlsynt reports UNREALIZABLE in ~10ms; acacia-bonsai sweeps K = 2, 5, 8, ..., 98 on three search paths (real + unreal-x-formula + unreal-x-automaton) and reports UNKNOWN.

What ltlsynt does

subprojects/spot/spot/twaalgos/synthesis.cc:1223 — try_create_direct_strategy(f, output_aps, gi, want_strategy):

1. Decomposes f into G(α) ∧ G(β) ∧ … ∧ rest, with the boolean Gs gathered into f_g.
2. Builds the BDD of f_g and computes bdd_exist(g_bdd, output_bdd). This projects out the outputs, leaving the set of input valuations for which some output choice could satisfy the constraint.
3. If the result is not bddtrue, there is an input valuation no output can rescue → return UNREALIZABLE immediately.
4. Several other shortcuts for Equiv/G F/F G patterns (lines ~1319+).

subprojects/spot/bin/ltlsynt.cc:437-449 calls this before falling through to the full game-solving pipeline (gated by opt_bypass).

Proposed change

Add an analogous fast pre-check in src/solver/solver_invoker.hh::run_one_ltl::operator(), run before the formula is negated and translated:

• On the realizability path: if the pre-check says UNREALIZABLE, the realizability child returns false (UNKNOWN locally), but a sibling unreal child can short-circuit and report UNREAL. Even better: short-circuit at the run_ltl level and exit immediately with EXIT_CODE_UNREAL.
• On the unreal-x-* paths: the formula is the original (modulo X-pushing); the same UNREALIZABLE detection applies.

Two options for the implementation:

1. Reuse spot's API directly. Call spot::try_create_direct_strategy(spot_formula, output_aps, gi, /*want_strategy=*/false) once at the entry of the runner. If it returns realizability_code::UNREALIZABLE, declare UNREAL. Cheap, well-tested, but requires constructing a synthesis_info and threading it through (only because the spot API needs it for verbose / bv stats). For our use we'd pass a stub.
2. Implement the input-only-G check ourselves. A few lines: walk the top-level And for G(φ) with φ boolean, AND those into a single BDD over inputs∪outputs, project the outputs out, check != bddtrue. Avoids the dependency on the higher-level synthesis API.

Option (1) is simpler and inherits future improvements to the heuristic.

Where the current pipeline misses this

The empty-automaton bug (issue ##X — replace with the relevant PR/issue if filed) is a symptom of this: for the unreal-x-automaton path on Light/Warnlight, after X-pushing the formula's BA collapses to 0 states, which used to crash and now returns UNKNOWN after the recent guard patch in solver_invoker.hh. With the pre-check in place, we'd detect UNREAL before ever calling create_automaton on those subformulas.

Acceptance criteria

• A new pre-check in run_one_ltl::operator() (or higher up in run_ltl) that, for Light_a50cadd7, Warnlight_a50cadd7, and any spec with a G-boolean input-only constraint, returns UNREAL in <100 ms without entering the K loop.
• Regression: all currently-passing benchmarks still produce the same verdicts (the pre-check only ever short-circuits to UNREAL, never claims REAL).
• A few unit tests covering: pure G-boolean over inputs, mixed G + non-G, and a control case where outputs can satisfy the constraint.

Notes

• Worth checking whether the fast path should also live in the decomposition layer — for Light, the formula is decomposed into 2 subformulas (DECOMPOSE_SPEC=1); the input-only-G constraint is in just one of them, and any_of over the unreal paths means catching it on that subformula is enough.
• ltlsynt has additional shortcuts (Equiv, GF/FG patterns); worth scanning the rest of try_create_direct_strategy to see which others apply to our typical inputs.

[gaperez64]

Unclear if this should be done at tlsf level or within acacia...

[gaperez64]

Implemented in the preprocessor instead: gaperez64/tlsf-tools#14