ArghDA M5: SMT solver backends (Z3, CVC5) — the Solver kind goes live

[hyperpolymath]

What & why

The first Solver-kind backends, on the M1 trait — arghda now spans both interaction models: assistants (typecheck a file → exit code) and solvers (answer an SMT-LIB2 query → sat/unsat/unknown). Chosen at the CLI with --backend z3|cvc5.

Changes

• src/prover/smt.rs — one Smt { name, cmd } type with Smt::z3() / Smt::cvc5(). check_file runs <solver> <file.smt2> and parses stdout (never the bare exit code — both sat and unsat exit 0):
  • unsat → Proven (VC discharged: ¬P has no model, so P holds)
  • sat → Refuted (a model/counterexample exists)
  • unknown → Unknown; (error …) / non-zero → Error; absent → Unavailable
  • multi-(check-sat) aggregate: any sat ⇒ Refuted; else any unknown ⇒ Unknown; else all unsat ⇒ Proven; no result token ⇒ Error (never a silent pass)
  • solvers are standalone queries: no import edges (isolated nodes — valid), no root convention (so wired isn't meaningful), no lint pack.
  • ground-truthed against Z3 4.8.12 + CVC5 1.2.0.
• src/main.rs — --backend z3|cvc5 wired via backend_for; about/help updated (Agda, Idris2, Z3, CVC5).

Verified (ran, not inferred)

• cargo test → 100 passing, 0 failed (75 lib + 25 integration; +5 SMT unit incl. the verdict-mapping table and the sat⊂unsat token trap, +2 SMT integration — hermetic, no solver needed for the graph path).
• cargo clippy -D warnings clean · cargo fmt --check clean · check-spdx.sh OK.
• Dogfooded real Z3 + CVC5:
  • check --backend z3 unsat.smt2 → proven-eligible
  • check --backend z3 sat.smt2 → rejected (exit 0 but verdict Refuted — honest)
  • reason --backend cvc5 --check → sat=refuted/unsound, unsat=proven/sound

Milestone status

Both backend interaction models are now real. Engine spine + four backends (Agda, Idris2, Z3, CVC5) done. Next: M2 Cubical-Agda, M6 Lean4.

---

Generated by Claude Code