logicaffeine_tv/
tensor.rs

1//! A rewrite of the one IR, proven: the obligation `tensor_graph::smt` prints for two graphs, discharged by Z3.
2//!
3//! A rewrite is proven when every lemma of its obligation holds: its premises are satisfiable — the facts it assumes hold
4//! of some input, so nothing follows from them vacuously — and its premises with its goal are not: no input and no
5//! meaning of the ops the IR leaves open makes the lemma's two terms differ, or a read of the rewritten graph stray out
6//! of range.
7
8use logicaffeine_compile::tensor_graph::smt::{Lemma, Obligation};
9use z3::{Params, SatResult, Solver};
10
11/// What Z3 says of one obligation.
12#[derive(Clone, Debug, PartialEq, Eq)]
13pub enum Verdict {
14    /// The rewrite keeps the meaning.
15    Proven,
16    /// A counterexample: the model Z3 found, an input and a meaning of the open ops under which the graphs differ.
17    Refuted(String),
18    /// The premises assume what no input satisfies, so the goal would follow from them whatever it says.
19    Vacuous,
20    /// Z3 gave no answer within the time, and why.
21    Unknown(String),
22}
23
24fn solver(text: &str, timeout_ms: u32) -> Solver {
25    let s = Solver::new();
26    let mut params = Params::new();
27    params.set_u32("timeout", timeout_ms);
28    s.set_params(&params);
29    s.from_string(text.to_string());
30    s
31}
32
33/// Discharge `o`: every lemma, each given up to `timeout_ms` for each of its two checks. The first lemma that is not
34/// proven gives the verdict.
35pub fn discharge(o: &Obligation, timeout_ms: u32) -> Verdict {
36    for lemma in &o.lemmas {
37        let verdict = lemma_verdict(lemma, timeout_ms);
38        if verdict != Verdict::Proven {
39            return verdict;
40        }
41    }
42    Verdict::Proven
43}
44
45fn lemma_verdict(lemma: &Lemma, timeout_ms: u32) -> Verdict {
46    let premises = solver(&lemma.premises, timeout_ms);
47    match premises.check() {
48        SatResult::Sat => {}
49        SatResult::Unsat => return Verdict::Vacuous,
50        SatResult::Unknown => return Verdict::Unknown(premises.get_reason_unknown().unwrap_or_default()),
51    }
52    let whole = solver(&lemma.text(), timeout_ms);
53    match whole.check() {
54        SatResult::Unsat => Verdict::Proven,
55        SatResult::Sat => Verdict::Refuted(whole.get_model().map(|m| m.to_string()).unwrap_or_default()),
56        SatResult::Unknown => Verdict::Unknown(whole.get_reason_unknown().unwrap_or_default()),
57    }
58}
logicaffeine_tv/tensor.rs

logicaffeine_tv/
tensor.rs
