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/// How long one query gets before the answer is [`Answer::Unknown`], in seconds.
13///
14/// Five minutes, and the number is measured rather than picked. Of the 571 rules the gate is
15/// given, all but five are settled in well under a second each, and whole files of them come back
16/// in under a second together. Four of the five are in `crates/rucc-opt/rules/safety.rules` and
17/// ask about a walk over an object at sixty four bits: five seconds each for `swept` and
18/// `swept.sym`, twenty for `reached`, and fifty four for `swept.down.sym`, which is the largest
19/// claim in the tree. That is z3 5.1.0 on a laptop with nothing else running. The fifth is the
20/// multiply against division in `crates/rucc-codegen/rules/x86-64.rules`, which no budget settles
21/// and which carries a written reason for the bounded proof it gets instead.
22///
23/// The same solver on a six core Linux box, which is the class of machine CI runs on, costs
24/// twenty four seconds for `reached` and between seventy five and eighty three for the downward
25/// sweep. Eighty three against the ninety this used to be is not a budget, it is a race the
26/// slower machine sometimes loses, and losing it reads as a rule nobody has proved. That is how
27/// the same tree proved and failed to prove minutes apart. tamnd/rucc#949.
28///
29/// The cost of a limit this loose is paid only by a rule that is genuinely not going to settle,
30/// and that rule stops the build either way. The cost of one too tight is a rule that is fine
31/// being reported as unproved, which reads as a real problem and is not one.
32const DEFAULT: u32 = 300;
33
34/// A solver that was found.
35#[derive(Debug, Clone)]
36pub struct Solver {
37    program: String,
38    seconds: u32,
39}
40
41/// What the solver said about one query.
42#[derive(Debug, Clone, PartialEq, Eq)]
43pub enum Answer {
44    /// No model exists, which is the answer a discharged rule gets: nothing makes the claim
45    /// false.
46    Unsat,
47    /// A model exists, and here is what the solver printed of it. The rule is wrong.
48    Sat(String),
49    /// The solver gave up, usually on time. Not a failure of the rule and not a pass either.
50    Unknown,
51}
52
53impl Solver {
54    /// Look for a solver on PATH.
55    ///
56    /// Returns nothing when there is none, which is what lets the tests skip rather than fail on
57    /// a machine that has not got one. CI has one, and that is where the answer matters.
58    #[must_use]
59    pub fn find() -> Option<Solver> {
60        for program in ["z3", "cvc5"] {
61            let found = Command::new(program).arg("--version").output();
62            if found.is_ok_and(|out| out.status.success()) {
63                return Some(Solver { program: program.to_owned(), seconds: DEFAULT });
64            }
65        }
66        None
67    }
68
69    /// How long a single query may take before the answer is [`Answer::Unknown`].
70    #[must_use]
71    pub fn within(self, seconds: u32) -> Solver {
72        Solver { seconds, ..self }
73    }
74
75    /// What the solver is called, for a report that has to name it.
76    #[must_use]
77    pub fn name(&self) -> &str {
78        &self.program
79    }
80
81    /// How long a rule is being given, for the same report.
82    ///
83    /// A run that says what the budget was is a run whose shrug can be read. Without it, a rule
84    /// reported as unproved is either a rule that is false or a rule that ran out of a number
85    /// nobody printed, and telling those apart is the whole difficulty of tamnd/rucc#949.
86    #[must_use]
87    pub fn seconds(&self) -> u32 {
88        self.seconds
89    }
90
91    /// Ask one question.
92    ///
93    /// # Errors
94    ///
95    /// Anything that stops the solver from running or from being talked to.
96    pub fn ask(&self, query: &str) -> std::io::Result<Answer> {
97        let timeout = match self.program.as_str() {
98            "cvc5" => format!("--tlimit={}", self.seconds * 1000),
99            _ => format!("-T:{}", self.seconds),
100        };
101        let stdin = if self.program == "cvc5" { "-" } else { "-in" };
102
103        let mut child = Command::new(&self.program)
104            .arg(stdin)
105            .arg(timeout)
106            .stdin(Stdio::piped())
107            .stdout(Stdio::piped())
108            .stderr(Stdio::piped())
109            .spawn()?;
110        let Some(mut pipe) = child.stdin.take() else {
111            return Err(std::io::Error::other("the solver has no standard input"));
112        };
113        pipe.write_all(query.as_bytes())?;
114        drop(pipe);
115        let out = child.wait_with_output()?;
116        let said = String::from_utf8_lossy(&out.stdout);
117
118        // The first line is the verdict and anything after it is the model, which is only asked
119        // for when the verdict is `sat` and is the whole value of a refutation.
120        let mut lines = said.lines();
121        Ok(match lines.next().map(str::trim) {
122            Some("unsat") => Answer::Unsat,
123            Some("sat") => Answer::Sat(lines.collect::<Vec<_>>().join("\n")),
124            _ => Answer::Unknown,
125        })
126    }
127}
rucc_verify/solver.rs

rucc_verify/
solver.rs
