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

.machine_readable/6a2/STATE.a2ml

@@ -45,7 +45,7 @@ milestones = [
   { name = "M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island)", completion = 0 },
   { name = "M3: Flying-Logic reasoning graph (src/reason: And|Or juncts, demote-only cycle-safe Verdict propagation, additive studio JSON)", completion = 100 },
   { name = "M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; escape-hatches)", completion = 90 },
-  { name = "M5: SMT solver backends (Z3, CVC5): SMT-LIB2 -> sat/unsat/unknown -> Verdict", completion = 0 },
+  { name = "M5: SMT solver backends (Z3, CVC5): SMT-LIB2 -> sat/unsat/unknown -> Verdict", completion = 100 },
   { name = "M6: Lean4 adapter (lake build + #print axioms audit)", completion = 0 },
   { name = "M7: Echidna dispatch seam (optional route to orchestrator :8090, same Outcome)", completion = 0 },
   { name = "M8: Coq/Rocq adapter (--heavy provisioning; Section-aware postulate classifier)", completion = 0 },
@@ -60,6 +60,21 @@ milestones = [
 # Remaining M0: `arghda doctor` Rust subcommand (interim: `just doctor` shells
 # the script's --verify-only table).
 #
+# M5 landed 2026-07-01: SMT solver backends (Z3, CVC5) — the FIRST Solver-kind
+# backends, exercising the other half of the taxonomy. src/prover/smt.rs: one
+# `Smt { name, cmd }` type with `Smt::z3()`/`Smt::cvc5()`. Kind=Solver, ext
+# .smt2. check_file runs `<solver> <file.smt2>` and PARSES stdout (never the
+# bare exit code — both sat and unsat exit 0): unsat→Proven (VC discharged),
+# sat→Refuted (model exists), unknown→Unknown, (error…)/nonzero→Error, absent→
+# Unavailable. Multi-check aggregate: any sat⇒Refuted; else any unknown⇒Unknown;
+# else all unsat⇒Proven; no token⇒Error (no silent pass). Solvers are standalone
+# queries: direct_imports=[] (isolated nodes — valid), discover_roots=[] (no
+# root convention → wired not meaningful), lint_rules=[]. Wired via --backend
+# z3|cvc5 (backend_for). Ground-truthed vs Z3 4.8.12 + CVC5 1.2.0. 100 tests
+# (75 lib + 25 integration; +5 smt unit +2 smt integration, hermetic). Dogfooded
+# REAL: `check --backend z3 unsat.smt2`→proven-eligible; `…sat.smt2`→rejected;
+# `reason --backend cvc5 --check`→sat=refuted/unsound, unsat=proven/sound.
+#
 # M4 landed 2026-07-01 (90%): the Idris2 backend — arghda is now genuinely
 # multi-backend. src/prover/idris2.rs: `idris2 --check --source-dir <root>
 # <file>` (ground-truthed vs Idris2 0.7.0), exit-code-only verdict; dotted
@@ -120,12 +135,12 @@ milestones = [
 
 [critical-next-actions]
 actions = [
-  "M1 (Backend trait) + M3 (reasoning graph) + M4 (Idris2) DONE. Next, all unblocked by the stable trait + --backend selector:",
-  "Flying-Logic epic M5: SMT solver backends (Z3, CVC5) — the FIRST Solver-kind backend; SMT-LIB2 -> unsat(Proven)/sat(Refuted)/unknown(Unknown). Both binaries provisioned. Exercises the Solver half of the taxonomy (no imports; isolated nodes).",
-  "Flying-Logic epic M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island; cross-flag import edges forbidden).",
-  "M4 follow-on (the missing 10%): .ipkg-declared roots; totality-hole (?name) + per-def `partial` lint.",
-  "M3 follow-on: feed real verdicts into `reason` from a workspace `proven/` state + wire staleness from the content-hash closure (proven.rs) so `arghda reason <workspace>` lights the cone without --check.",
-  "Finish M0: add the `arghda doctor` Rust subcommand and repoint `just doctor` at it (interim shells provision-provers.sh --verify-only).",
+  "M1 (Backend trait) + M3 (reasoning graph) + M4 (Idris2) + M5 (Z3/CVC5) DONE. Both interaction models (Assistant + Solver) now real. Next:",
+  "Flying-Logic epic M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island; cross-flag import edges forbidden). Small — extends the existing Agda backend.",
+  "Flying-Logic epic M6: Lean4 adapter (lake build + #print axioms audit → honest Unknown soundness when the audit is absent). Lean 4.13.0 provisioned.",
+  "Finish M0: add the `arghda doctor` Rust subcommand (report which backends are runnable — now agda/idris2/z3/cvc5) and repoint `just doctor` at it.",
+  "M4 follow-on: .ipkg-declared roots; totality-hole (?name) + per-def `partial` lint.",
+  "M3 follow-on: feed real verdicts into `reason` from a workspace `proven/` state + wire staleness from the content-hash closure (proven.rs).",
   "Serve /.well-known/groove for PanLL discovery (Groove protocol) — folds into M11.",
 ]
 
@@ -135,11 +150,9 @@ last-result = "pass"  # unknown | pass | warn | fail
 open-warnings = 0
 open-failures = 0
 # `just check` (fmt-check + clippy -D warnings + build + test + SPDX) green
-# post-M4: 70 lib + 23 integration = 93 tests pass. Dogfooded via real CLI
-# runs on BOTH backends: agda (`check`/`reason --check`) and idris2 (`check
-# --backend idris2` → proven-eligible; `reason --backend idris2 --check` →
-# live-typechecked cone). Dogfooded historically against echo-types +
-# agda-unused.
+# post-M5: 75 lib + 25 integration = 100 tests pass. Dogfooded via real CLI on
+# all four backends: agda + idris2 (Assistant), z3 + cvc5 (Solver). Dogfooded
+# historically against echo-types + agda-unused.
 
 [ecosystem]
 part-of = ["arghda"]

src/lib.rs

@@ -30,6 +30,6 @@ pub use diagnostic::{Diagnostic, LintReport, Severity};
 pub use event::{Event, EventKind};
 pub use graph::{build as build_graph, ImportGraph};
 pub use lint::{default_rules, rules_with_config, run_lints, LintRule, RuleConfig};
-pub use prover::{default_backend, Agda, Backend, BackendKind, Idris2, Outcome, Verdict};
+pub use prover::{default_backend, Agda, Backend, BackendKind, Idris2, Outcome, Smt, Verdict};
 pub use reason::{build as build_reason, Junct, ReasonDocument, ReasonEdge, ReasonNode};
 pub use workspace::{StaleEntry, State, Workspace};

src/main.rs

@@ -5,7 +5,7 @@ use anyhow::{Context, Result};
 use arghda_core::lint::LintContext;
 use arghda_core::{
     build_dag, build_reason, event, run_lints, unused, watcher, Agda, Backend, Idris2, LintRule,
-    RuleConfig, State, Workspace,
+    RuleConfig, Smt, State, Workspace,
 };
 use clap::{Parser, Subcommand};
 use std::path::{Path, PathBuf};
@@ -21,15 +21,17 @@ fn backend_for(name: &str) -> Result<Box<dyn Backend>> {
     match name {
         "agda" => Ok(Box::new(Agda)),
         "idris2" => Ok(Box::new(Idris2)),
-        other => anyhow::bail!("unknown backend `{other}` (known: agda, idris2)"),
+        "z3" => Ok(Box::new(Smt::z3())),
+        "cvc5" => Ok(Box::new(Smt::cvc5())),
+        other => anyhow::bail!("unknown backend `{other}` (known: agda, idris2, z3, cvc5)"),
     }
 }
 
 #[derive(Parser)]
 #[command(
     name = "arghda",
     version,
-    about = "Proof-workspace manager for provers/solvers (Agda, Idris2)"
+    about = "Proof-workspace manager for provers/solvers (Agda, Idris2, Z3, CVC5)"
 )]
 struct Cli {
     #[command(subcommand)]
@@ -56,7 +58,7 @@ enum Cmd {
         /// `<PATH>/.arghda/config.toml` if present.
         #[arg(long)]
         config: Option<PathBuf>,
-        /// Prover/solver backend to use: `agda` (default) or `idris2`.
+        /// Prover/solver backend: `agda` (default), `idris2`, `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
         /// Also run the external `agda-unused` analyser and re-emit its
@@ -75,7 +77,7 @@ enum Cmd {
         /// Include root (search path). Defaults to the file's directory.
         #[arg(long)]
         include_root: Option<PathBuf>,
-        /// Prover/solver backend to use: `agda` (default) or `idris2`.
+        /// Prover/solver backend: `agda` (default), `idris2`, `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
         /// Emit the report as JSON.
@@ -98,7 +100,7 @@ enum Cmd {
         /// `<PATH>/.arghda/config.toml` if present.
         #[arg(long)]
         config: Option<PathBuf>,
-        /// Prover/solver backend to use: `agda` (default) or `idris2`.
+        /// Prover/solver backend: `agda` (default), `idris2`, `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
     },
@@ -121,7 +123,7 @@ enum Cmd {
         /// `<PATH>/.arghda/config.toml` if present.
         #[arg(long)]
         config: Option<PathBuf>,
-        /// Prover/solver backend to use: `agda` (default) or `idris2`.
+        /// Prover/solver backend: `agda` (default), `idris2`, `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
         /// Run the backend on every node to populate REAL prover verdicts

src/prover/mod.rs

@@ -28,9 +28,11 @@ use std::path::{Path, PathBuf};
 
 pub mod agda;
 pub mod idris2;
+pub mod smt;
 
 pub use agda::Agda;
 pub use idris2::Idris2;
+pub use smt::Smt;
 
 /// The two backend interaction models.
 #[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize)]

src/prover/smt.rs

@@ -0,0 +1,240 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+//! SMT solver backends (Z3, CVC5) — the first `Solver`-kind backends.
+//!
+//! The other half of the backend taxonomy: where an assistant typechecks a
+//! file (exit code is the verdict), a *solver* is fed an SMT-LIB2 query and
+//! answers `sat`/`unsat`/`unknown` on stdout. Ground-truthed against Z3
+//! 4.8.12 and CVC5 1.2.0: `<solver> <file.smt2>` prints one result token per
+//! `(check-sat)` and exits 0; a malformed file prints `(error …)` and exits
+//! non-zero.
+//!
+//! Verdict mapping (the documented convention — the query author frames their
+//! problem to suit it):
+//! * `unsat` → [`Verdict::Proven`] — the assertion set is unsatisfiable (a
+//!   verification condition is discharged: `¬P` has no model, so `P` holds).
+//! * `sat` → [`Verdict::Refuted`] — a model/counterexample exists.
+//! * `unknown` / timeout → [`Verdict::Unknown`].
+//! * a solver error / non-zero exit → [`Verdict::Error`].
+//! * the binary absent → [`Verdict::Unavailable`].
+//!
+//! The verdict is derived from the solver's ACTUAL output, never from a
+//! bare exit code (both `sat` and `unsat` exit 0). Over multiple
+//! `(check-sat)`s: any `sat` ⇒ Refuted; else any `unknown` ⇒ Unknown; else
+//! all `unsat` ⇒ Proven.
+//!
+//! SMT files are standalone queries: there is no import graph
+//! ([`Backend::direct_imports`] is empty → isolated DAG nodes, which is
+//! valid) and no root convention ([`Backend::discover_roots`] is empty, so
+//! `wired` is not meaningful for solver nodes).
+
+use super::{Backend, BackendKind, Outcome, Verdict};
+use crate::graph;
+use crate::lint::{LintRule, RuleConfig};
+use anyhow::Result;
+use std::path::{Path, PathBuf};
+use std::process::Command;
+
+const TAIL_LINES: usize = 40;
+
+/// An SMT-LIB2 solver backend, parameterised by its binary.
+#[derive(Clone, Copy, Debug)]
+pub struct Smt {
+    name: &'static str,
+    cmd: &'static str,
+}
+
+impl Smt {
+    /// The Z3 solver.
+    pub fn z3() -> Self {
+        Self {
+            name: "z3",
+            cmd: "z3",
+        }
+    }
+
+    /// The CVC5 solver.
+    pub fn cvc5() -> Self {
+        Self {
+            name: "cvc5",
+            cmd: "cvc5",
+        }
+    }
+}
+
+impl Backend for Smt {
+    fn name(&self) -> &'static str {
+        self.name
+    }
+
+    fn kind(&self) -> BackendKind {
+        BackendKind::Solver
+    }
+
+    fn extensions(&self) -> &'static [&'static str] {
+        &["smt2"]
+    }
+
+    fn check_file(&self, file: &Path, _include_root: &Path) -> Result<Outcome> {
+        // Solvers read the query file directly; no include-root search path.
+        let output = Command::new(self.cmd).arg(file).output();
+        match output {
+            Ok(out) => {
+                let mut combined = String::from_utf8_lossy(&out.stdout).into_owned();
+                combined.push_str(&String::from_utf8_lossy(&out.stderr));
+                let verdict = parse_verdict(&combined, out.status.success());
+                Ok(Outcome {
+                    available: true,
+                    exit_code: out.status.code(),
+                    // For a solver "ok" = the goal was discharged (unsat).
+                    ok: verdict == Verdict::Proven,
+                    output_tail: tail(&combined, TAIL_LINES),
+                    kind: BackendKind::Solver,
+                    verdict,
+                })
+            }
+            Err(e) if e.kind() == std::io::ErrorKind::NotFound => {
+                Ok(Outcome::unavailable(BackendKind::Solver))
+            }
+            Err(e) => Err(e.into()),
+        }
+    }
+
+    fn module_name_of(&self, file: &Path, include_root: &Path) -> Option<String> {
+        // No true module names; use the relative path as a stable node id.
+        graph::module_name_of(file, include_root)
+    }
+
+    fn module_to_path(&self, module: &str, include_root: &Path) -> PathBuf {
+        let mut p = include_root.to_path_buf();
+        for part in module.split('.') {
+            p.push(part);
+        }
+        p.set_extension("smt2");
+        p
+    }
+
+    fn direct_imports(&self, _file: &Path) -> Result<Vec<String>> {
+        // SMT queries are standalone: no dependency edges.
+        Ok(Vec::new())
+    }
+
+    fn discover_roots(&self, _include_root: &Path) -> Vec<PathBuf> {
+        // No `All.agda`/`Main.idr`-style root convention for SMT.
+        Vec::new()
+    }
+
+    fn lint_rules(&self, _cfg: &RuleConfig) -> Result<Vec<Box<dyn LintRule>>> {
+        // No source-level escape-hatch class for SMT-LIB2.
+        Ok(Vec::new())
+    }
+}
+
+/// Map solver output + exit status to a [`Verdict`]. Parses the actual
+/// `sat`/`unsat`/`unknown` result tokens; never trusts the bare exit code
+/// (both `sat` and `unsat` exit 0).
+fn parse_verdict(output: &str, exit_ok: bool) -> Verdict {
+    if !exit_ok || output.contains("(error") {
+        return Verdict::Error;
+    }
+    let mut saw_unsat = false;
+    let mut saw_unknown = false;
+    for tok in output.split_whitespace() {
+        match tok {
+            "sat" => return Verdict::Refuted, // any model ⇒ refuted
+            "unsat" => saw_unsat = true,
+            "unknown" => saw_unknown = true,
+            _ => {}
+        }
+    }
+    if saw_unknown {
+        Verdict::Unknown
+    } else if saw_unsat {
+        Verdict::Proven
+    } else {
+        // Ran cleanly but produced no result token — treat as an error, not
+        // a silent pass.
+        Verdict::Error
+    }
+}
+
+fn tail(s: &str, n: usize) -> String {
+    let lines: Vec<&str> = s.lines().collect();
+    let start = lines.len().saturating_sub(n);
+    lines[start..].join("\n")
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn solver_identity() {
+        assert_eq!(Smt::z3().name(), "z3");
+        assert_eq!(Smt::cvc5().name(), "cvc5");
+        assert_eq!(Smt::z3().kind(), BackendKind::Solver);
+        assert_eq!(Smt::z3().extensions(), &["smt2"]);
+    }
+
+    #[test]
+    fn module_to_path_uses_smt2_extension() {
+        assert_eq!(
+            Smt::z3().module_to_path("queries.overflow", Path::new("/r")),
+            PathBuf::from("/r/queries/overflow.smt2")
+        );
+    }
+
+    #[test]
+    fn solvers_have_no_edges_or_roots() {
+        let tmp = tempfile::tempdir().unwrap();
+        let f = tmp.path().join("q.smt2");
+        std::fs::write(&f, "(check-sat)\n").unwrap();
+        assert!(Smt::z3().direct_imports(&f).unwrap().is_empty());
+        assert!(Smt::z3().discover_roots(tmp.path()).is_empty());
+    }
+
+    #[test]
+    fn verdict_mapping_is_honest() {
+        // unsat ⇒ Proven (VC discharged), sat ⇒ Refuted, unknown ⇒ Unknown.
+        assert_eq!(parse_verdict("unsat\n", true), Verdict::Proven);
+        assert_eq!(parse_verdict("sat\n", true), Verdict::Refuted);
+        assert_eq!(parse_verdict("unknown\n", true), Verdict::Unknown);
+        // "sat" is a substring of "unsat" but a distinct token — no confusion.
+        assert_eq!(parse_verdict("unsat\nunsat\n", true), Verdict::Proven);
+        // Any sat among several checks ⇒ Refuted; any unknown (no sat) ⇒ Unknown.
+        assert_eq!(parse_verdict("unsat\nsat\n", true), Verdict::Refuted);
+        assert_eq!(parse_verdict("unsat\nunknown\n", true), Verdict::Unknown);
+        // Errors / non-zero exit / no result ⇒ Error, never a silent pass.
+        assert_eq!(
+            parse_verdict("(error \"parse error\")", false),
+            Verdict::Error
+        );
+        assert_eq!(parse_verdict("(error \"x\")", true), Verdict::Error);
+        assert_eq!(parse_verdict("", true), Verdict::Error);
+    }
+
+    #[test]
+    fn check_file_is_honest_about_availability() {
+        let tmp = tempfile::tempdir().unwrap();
+        let f = tmp.path().join("q.smt2");
+        std::fs::write(
+            &f,
+            "(declare-const x Int)\n(assert (and (> x 2) (< x 1)))\n(check-sat)\n",
+        )
+        .unwrap();
+        let out = Smt::z3().check_file(&f, tmp.path()).unwrap();
+        assert_eq!(out.kind, BackendKind::Solver);
+        if out.available {
+            // If z3 is present this query is unsat ⇒ Proven; either way the
+            // verdict is derived from real output, not fabricated.
+            assert!(matches!(
+                out.verdict,
+                Verdict::Proven | Verdict::Refuted | Verdict::Unknown | Verdict::Error
+            ));
+            assert_eq!(out.ok, out.verdict == Verdict::Proven);
+        } else {
+            assert_eq!(out.verdict, Verdict::Unavailable);
+        }
+    }
+}

tests/fixtures/smt/sat.smt2

@@ -0,0 +1,6 @@
+; A satisfiable query: a model (counterexample) exists.
+; sat  =>  Refuted.
+(set-logic QF_LIA)
+(declare-const x Int)
+(assert (> x 2))
+(check-sat)