|
| 1 | +// SPDX-License-Identifier: MPL-2.0 |
| 2 | +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | + |
| 4 | +//! SMT solver backends (Z3, CVC5) — the first `Solver`-kind backends. |
| 5 | +//! |
| 6 | +//! The other half of the backend taxonomy: where an assistant typechecks a |
| 7 | +//! file (exit code is the verdict), a *solver* is fed an SMT-LIB2 query and |
| 8 | +//! answers `sat`/`unsat`/`unknown` on stdout. Ground-truthed against Z3 |
| 9 | +//! 4.8.12 and CVC5 1.2.0: `<solver> <file.smt2>` prints one result token per |
| 10 | +//! `(check-sat)` and exits 0; a malformed file prints `(error …)` and exits |
| 11 | +//! non-zero. |
| 12 | +//! |
| 13 | +//! Verdict mapping (the documented convention — the query author frames their |
| 14 | +//! problem to suit it): |
| 15 | +//! * `unsat` → [`Verdict::Proven`] — the assertion set is unsatisfiable (a |
| 16 | +//! verification condition is discharged: `¬P` has no model, so `P` holds). |
| 17 | +//! * `sat` → [`Verdict::Refuted`] — a model/counterexample exists. |
| 18 | +//! * `unknown` / timeout → [`Verdict::Unknown`]. |
| 19 | +//! * a solver error / non-zero exit → [`Verdict::Error`]. |
| 20 | +//! * the binary absent → [`Verdict::Unavailable`]. |
| 21 | +//! |
| 22 | +//! The verdict is derived from the solver's ACTUAL output, never from a |
| 23 | +//! bare exit code (both `sat` and `unsat` exit 0). Over multiple |
| 24 | +//! `(check-sat)`s: any `sat` ⇒ Refuted; else any `unknown` ⇒ Unknown; else |
| 25 | +//! all `unsat` ⇒ Proven. |
| 26 | +//! |
| 27 | +//! SMT files are standalone queries: there is no import graph |
| 28 | +//! ([`Backend::direct_imports`] is empty → isolated DAG nodes, which is |
| 29 | +//! valid) and no root convention ([`Backend::discover_roots`] is empty, so |
| 30 | +//! `wired` is not meaningful for solver nodes). |
| 31 | +
|
| 32 | +use super::{Backend, BackendKind, Outcome, Verdict}; |
| 33 | +use crate::graph; |
| 34 | +use crate::lint::{LintRule, RuleConfig}; |
| 35 | +use anyhow::Result; |
| 36 | +use std::path::{Path, PathBuf}; |
| 37 | +use std::process::Command; |
| 38 | + |
| 39 | +const TAIL_LINES: usize = 40; |
| 40 | + |
| 41 | +/// An SMT-LIB2 solver backend, parameterised by its binary. |
| 42 | +#[derive(Clone, Copy, Debug)] |
| 43 | +pub struct Smt { |
| 44 | + name: &'static str, |
| 45 | + cmd: &'static str, |
| 46 | +} |
| 47 | + |
| 48 | +impl Smt { |
| 49 | + /// The Z3 solver. |
| 50 | + pub fn z3() -> Self { |
| 51 | + Self { |
| 52 | + name: "z3", |
| 53 | + cmd: "z3", |
| 54 | + } |
| 55 | + } |
| 56 | + |
| 57 | + /// The CVC5 solver. |
| 58 | + pub fn cvc5() -> Self { |
| 59 | + Self { |
| 60 | + name: "cvc5", |
| 61 | + cmd: "cvc5", |
| 62 | + } |
| 63 | + } |
| 64 | +} |
| 65 | + |
| 66 | +impl Backend for Smt { |
| 67 | + fn name(&self) -> &'static str { |
| 68 | + self.name |
| 69 | + } |
| 70 | + |
| 71 | + fn kind(&self) -> BackendKind { |
| 72 | + BackendKind::Solver |
| 73 | + } |
| 74 | + |
| 75 | + fn extensions(&self) -> &'static [&'static str] { |
| 76 | + &["smt2"] |
| 77 | + } |
| 78 | + |
| 79 | + fn check_file(&self, file: &Path, _include_root: &Path) -> Result<Outcome> { |
| 80 | + // Solvers read the query file directly; no include-root search path. |
| 81 | + let output = Command::new(self.cmd).arg(file).output(); |
| 82 | + match output { |
| 83 | + Ok(out) => { |
| 84 | + let mut combined = String::from_utf8_lossy(&out.stdout).into_owned(); |
| 85 | + combined.push_str(&String::from_utf8_lossy(&out.stderr)); |
| 86 | + let verdict = parse_verdict(&combined, out.status.success()); |
| 87 | + Ok(Outcome { |
| 88 | + available: true, |
| 89 | + exit_code: out.status.code(), |
| 90 | + // For a solver "ok" = the goal was discharged (unsat). |
| 91 | + ok: verdict == Verdict::Proven, |
| 92 | + output_tail: tail(&combined, TAIL_LINES), |
| 93 | + kind: BackendKind::Solver, |
| 94 | + verdict, |
| 95 | + }) |
| 96 | + } |
| 97 | + Err(e) if e.kind() == std::io::ErrorKind::NotFound => { |
| 98 | + Ok(Outcome::unavailable(BackendKind::Solver)) |
| 99 | + } |
| 100 | + Err(e) => Err(e.into()), |
| 101 | + } |
| 102 | + } |
| 103 | + |
| 104 | + fn module_name_of(&self, file: &Path, include_root: &Path) -> Option<String> { |
| 105 | + // No true module names; use the relative path as a stable node id. |
| 106 | + graph::module_name_of(file, include_root) |
| 107 | + } |
| 108 | + |
| 109 | + fn module_to_path(&self, module: &str, include_root: &Path) -> PathBuf { |
| 110 | + let mut p = include_root.to_path_buf(); |
| 111 | + for part in module.split('.') { |
| 112 | + p.push(part); |
| 113 | + } |
| 114 | + p.set_extension("smt2"); |
| 115 | + p |
| 116 | + } |
| 117 | + |
| 118 | + fn direct_imports(&self, _file: &Path) -> Result<Vec<String>> { |
| 119 | + // SMT queries are standalone: no dependency edges. |
| 120 | + Ok(Vec::new()) |
| 121 | + } |
| 122 | + |
| 123 | + fn discover_roots(&self, _include_root: &Path) -> Vec<PathBuf> { |
| 124 | + // No `All.agda`/`Main.idr`-style root convention for SMT. |
| 125 | + Vec::new() |
| 126 | + } |
| 127 | + |
| 128 | + fn lint_rules(&self, _cfg: &RuleConfig) -> Result<Vec<Box<dyn LintRule>>> { |
| 129 | + // No source-level escape-hatch class for SMT-LIB2. |
| 130 | + Ok(Vec::new()) |
| 131 | + } |
| 132 | +} |
| 133 | + |
| 134 | +/// Map solver output + exit status to a [`Verdict`]. Parses the actual |
| 135 | +/// `sat`/`unsat`/`unknown` result tokens; never trusts the bare exit code |
| 136 | +/// (both `sat` and `unsat` exit 0). |
| 137 | +fn parse_verdict(output: &str, exit_ok: bool) -> Verdict { |
| 138 | + if !exit_ok || output.contains("(error") { |
| 139 | + return Verdict::Error; |
| 140 | + } |
| 141 | + let mut saw_unsat = false; |
| 142 | + let mut saw_unknown = false; |
| 143 | + for tok in output.split_whitespace() { |
| 144 | + match tok { |
| 145 | + "sat" => return Verdict::Refuted, // any model ⇒ refuted |
| 146 | + "unsat" => saw_unsat = true, |
| 147 | + "unknown" => saw_unknown = true, |
| 148 | + _ => {} |
| 149 | + } |
| 150 | + } |
| 151 | + if saw_unknown { |
| 152 | + Verdict::Unknown |
| 153 | + } else if saw_unsat { |
| 154 | + Verdict::Proven |
| 155 | + } else { |
| 156 | + // Ran cleanly but produced no result token — treat as an error, not |
| 157 | + // a silent pass. |
| 158 | + Verdict::Error |
| 159 | + } |
| 160 | +} |
| 161 | + |
| 162 | +fn tail(s: &str, n: usize) -> String { |
| 163 | + let lines: Vec<&str> = s.lines().collect(); |
| 164 | + let start = lines.len().saturating_sub(n); |
| 165 | + lines[start..].join("\n") |
| 166 | +} |
| 167 | + |
| 168 | +#[cfg(test)] |
| 169 | +mod tests { |
| 170 | + use super::*; |
| 171 | + |
| 172 | + #[test] |
| 173 | + fn solver_identity() { |
| 174 | + assert_eq!(Smt::z3().name(), "z3"); |
| 175 | + assert_eq!(Smt::cvc5().name(), "cvc5"); |
| 176 | + assert_eq!(Smt::z3().kind(), BackendKind::Solver); |
| 177 | + assert_eq!(Smt::z3().extensions(), &["smt2"]); |
| 178 | + } |
| 179 | + |
| 180 | + #[test] |
| 181 | + fn module_to_path_uses_smt2_extension() { |
| 182 | + assert_eq!( |
| 183 | + Smt::z3().module_to_path("queries.overflow", Path::new("/r")), |
| 184 | + PathBuf::from("/r/queries/overflow.smt2") |
| 185 | + ); |
| 186 | + } |
| 187 | + |
| 188 | + #[test] |
| 189 | + fn solvers_have_no_edges_or_roots() { |
| 190 | + let tmp = tempfile::tempdir().unwrap(); |
| 191 | + let f = tmp.path().join("q.smt2"); |
| 192 | + std::fs::write(&f, "(check-sat)\n").unwrap(); |
| 193 | + assert!(Smt::z3().direct_imports(&f).unwrap().is_empty()); |
| 194 | + assert!(Smt::z3().discover_roots(tmp.path()).is_empty()); |
| 195 | + } |
| 196 | + |
| 197 | + #[test] |
| 198 | + fn verdict_mapping_is_honest() { |
| 199 | + // unsat ⇒ Proven (VC discharged), sat ⇒ Refuted, unknown ⇒ Unknown. |
| 200 | + assert_eq!(parse_verdict("unsat\n", true), Verdict::Proven); |
| 201 | + assert_eq!(parse_verdict("sat\n", true), Verdict::Refuted); |
| 202 | + assert_eq!(parse_verdict("unknown\n", true), Verdict::Unknown); |
| 203 | + // "sat" is a substring of "unsat" but a distinct token — no confusion. |
| 204 | + assert_eq!(parse_verdict("unsat\nunsat\n", true), Verdict::Proven); |
| 205 | + // Any sat among several checks ⇒ Refuted; any unknown (no sat) ⇒ Unknown. |
| 206 | + assert_eq!(parse_verdict("unsat\nsat\n", true), Verdict::Refuted); |
| 207 | + assert_eq!(parse_verdict("unsat\nunknown\n", true), Verdict::Unknown); |
| 208 | + // Errors / non-zero exit / no result ⇒ Error, never a silent pass. |
| 209 | + assert_eq!( |
| 210 | + parse_verdict("(error \"parse error\")", false), |
| 211 | + Verdict::Error |
| 212 | + ); |
| 213 | + assert_eq!(parse_verdict("(error \"x\")", true), Verdict::Error); |
| 214 | + assert_eq!(parse_verdict("", true), Verdict::Error); |
| 215 | + } |
| 216 | + |
| 217 | + #[test] |
| 218 | + fn check_file_is_honest_about_availability() { |
| 219 | + let tmp = tempfile::tempdir().unwrap(); |
| 220 | + let f = tmp.path().join("q.smt2"); |
| 221 | + std::fs::write( |
| 222 | + &f, |
| 223 | + "(declare-const x Int)\n(assert (and (> x 2) (< x 1)))\n(check-sat)\n", |
| 224 | + ) |
| 225 | + .unwrap(); |
| 226 | + let out = Smt::z3().check_file(&f, tmp.path()).unwrap(); |
| 227 | + assert_eq!(out.kind, BackendKind::Solver); |
| 228 | + if out.available { |
| 229 | + // If z3 is present this query is unsat ⇒ Proven; either way the |
| 230 | + // verdict is derived from real output, not fabricated. |
| 231 | + assert!(matches!( |
| 232 | + out.verdict, |
| 233 | + Verdict::Proven | Verdict::Refuted | Verdict::Unknown | Verdict::Error |
| 234 | + )); |
| 235 | + assert_eq!(out.ok, out.verdict == Verdict::Proven); |
| 236 | + } else { |
| 237 | + assert_eq!(out.verdict, Verdict::Unavailable); |
| 238 | + } |
| 239 | + } |
| 240 | +} |
0 commit comments