rucc_verify/
solver.rs

1//! Running the solver.
2//!
3//! The solver is a program found on PATH, not a crate. A bitvector solver taken as a dependency
4//! would be the largest thing in the tree by a wide margin, it would have to hold the 1.85
5//! minimum the workspace holds, and `spec/18-package-layout.md` section 18.3 asks for a reason
6//! before anything is added at all. Shelling out costs a process per rule, which is nothing
7//! against the solving, and it means the version in use is the version CI installed and can say.
8
9use std::io::Write;
10use std::process::{Command, Stdio};
11
12/// A solver that was found.
13#[derive(Debug, Clone)]
14pub struct Solver {
15    program: String,
16    seconds: u32,
17}
18
19/// What the solver said about one query.
20#[derive(Debug, Clone, PartialEq, Eq)]
21pub enum Answer {
22    /// No model exists, which is the answer a discharged rule gets: nothing makes the claim
23    /// false.
24    Unsat,
25    /// A model exists, and here is what the solver printed of it. The rule is wrong.
26    Sat(String),
27    /// The solver gave up, usually on time. Not a failure of the rule and not a pass either.
28    Unknown,
29}
30
31impl Solver {
32    /// Look for a solver on PATH.
33    ///
34    /// Returns nothing when there is none, which is what lets the tests skip rather than fail on
35    /// a machine that has not got one. CI has one, and that is where the answer matters.
36    #[must_use]
37    pub fn find() -> Option<Solver> {
38        for program in ["z3", "cvc5"] {
39            let found = Command::new(program).arg("--version").output();
40            if found.is_ok_and(|out| out.status.success()) {
41                return Some(Solver { program: program.to_owned(), seconds: 10 });
42            }
43        }
44        None
45    }
46
47    /// How long a single query may take before the answer is [`Answer::Unknown`].
48    #[must_use]
49    pub fn within(self, seconds: u32) -> Solver {
50        Solver { seconds, ..self }
51    }
52
53    /// What the solver is called, for a report that has to name it.
54    #[must_use]
55    pub fn name(&self) -> &str {
56        &self.program
57    }
58
59    /// Ask one question.
60    ///
61    /// # Errors
62    ///
63    /// Anything that stops the solver from running or from being talked to.
64    pub fn ask(&self, query: &str) -> std::io::Result<Answer> {
65        let timeout = match self.program.as_str() {
66            "cvc5" => format!("--tlimit={}", self.seconds * 1000),
67            _ => format!("-T:{}", self.seconds),
68        };
69        let stdin = if self.program == "cvc5" { "-" } else { "-in" };
70
71        let mut child = Command::new(&self.program)
72            .arg(stdin)
73            .arg(timeout)
74            .stdin(Stdio::piped())
75            .stdout(Stdio::piped())
76            .stderr(Stdio::piped())
77            .spawn()?;
78        let Some(mut pipe) = child.stdin.take() else {
79            return Err(std::io::Error::other("the solver has no standard input"));
80        };
81        pipe.write_all(query.as_bytes())?;
82        drop(pipe);
83        let out = child.wait_with_output()?;
84        let said = String::from_utf8_lossy(&out.stdout);
85
86        // The first line is the verdict and anything after it is the model, which is only asked
87        // for when the verdict is `sat` and is the whole value of a refutation.
88        let mut lines = said.lines();
89        Ok(match lines.next().map(str::trim) {
90            Some("unsat") => Answer::Unsat,
91            Some("sat") => Answer::Sat(lines.collect::<Vec<_>>().join("\n")),
92            _ => Answer::Unknown,
93        })
94    }
95}
rucc_verify/solver.rs

rucc_verify/
solver.rs
