sirius/solver/
mod.rs

1//! Some symbolic computation utilities based on the [`Poly`] abstraction.
2//!
3//! All operations are exact. Coefficients are stored as `i128`s and panic on overflow.
4
5pub mod count;
6pub mod poly;
7
8pub mod t0;
9pub mod t1;
10pub mod t2;
11
12use js_sys::Function;
13use std::fmt;
14use std::path::PathBuf;
15
16use crate::parser::lexer::ArithCmpOp;
17use poly::{Poly, Var};
18
19use t1::{Linearized, Z3};
20
21/// Obligation vocabulary.
22#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
23pub enum Cmp {
24    Eq,
25    Ne,
26    Le,
27    Lt,
28    Ge,
29    Gt,
30}
31
32impl Cmp {
33    pub fn negate(self) -> Cmp {
34        match self {
35            Cmp::Eq => Cmp::Ne,
36            Cmp::Ne => Cmp::Eq,
37            Cmp::Le => Cmp::Gt,
38            Cmp::Lt => Cmp::Ge,
39            Cmp::Ge => Cmp::Lt,
40            Cmp::Gt => Cmp::Le,
41        }
42    }
43
44    fn smt(self) -> &'static str {
45        match self {
46            Cmp::Eq => "=",
47            Cmp::Ne => "distinct",
48            Cmp::Le => "<=",
49            Cmp::Lt => "<",
50            Cmp::Ge => ">=",
51            Cmp::Gt => ">",
52        }
53    }
54
55    pub fn from_lex(op: &ArithCmpOp) -> Self {
56        match op {
57            ArithCmpOp::Greater => Cmp::Gt,
58            ArithCmpOp::GreaterOrEq => Cmp::Ge,
59            ArithCmpOp::Less => Cmp::Lt,
60            ArithCmpOp::LessOrEq => Cmp::Le,
61            ArithCmpOp::Eq => Cmp::Eq,
62            ArithCmpOp::NotEq => Cmp::Ne,
63        }
64    }
65}
66
67impl fmt::Display for Cmp {
68    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
69        f.write_str(match self {
70            Cmp::Eq => "==",
71            Cmp::Ne => "!=",
72            Cmp::Le => "<=",
73            Cmp::Lt => "<",
74            Cmp::Ge => ">=",
75            Cmp::Gt => ">",
76        })
77    }
78}
79
80/// Format for facts and goals, e.g. `X > 2*Y`.
81#[derive(Clone, PartialEq, Eq, Debug)]
82pub struct Constraint {
83    pub lhs: Poly,
84    pub cmp: Cmp,
85    pub rhs: Poly,
86}
87
88impl Constraint {
89    pub fn new(lhs: Poly, cmp: Cmp, rhs: Poly) -> Self {
90        Self { lhs, cmp, rhs }
91    }
92
93    pub fn display_with(&self, names: &[&str]) -> String {
94        format!(
95            "{} {} {}",
96            self.lhs.display_with(Some(names)),
97            self.cmp,
98            self.rhs.display_with(Some(names))
99        )
100    }
101
102    pub fn negate(&self) -> Self {
103        Self {
104            lhs: self.lhs.clone(),
105            cmp: self.cmp.negate(),
106            rhs: self.rhs.clone(),
107        }
108    }
109}
110
111pub type Point = Vec<(Var, i128)>;
112
113/// Solver response.
114/// [`t0`] refutations provide a trivial `!goal` given non-negative variables;
115/// [`t1`] refutations provide a counterexample point;
116/// [`t2`] is best-effort and cannot refute.
117#[derive(Clone, PartialEq, Eq, Debug)]
118pub enum Verdict {
119    Proved,
120    RefutedBy(Constraint),
121    RefutedAt(Point),
122    Unknown,
123}
124
125/// A consolidated [`t0`] -> [`t1`] -> [`t2`] solving pipeline.
126pub struct Solver {
127    pub z3: Z3,
128}
129
130impl Solver {
131    /// Expect the z3 command to be available in the environment.
132    /// Optionally provide a filesystem cache for model output.
133    pub fn new_cli(cache_dir: Option<PathBuf>) -> Option<Self> {
134        Some(Self {
135            z3: Z3::new_cli(cache_dir)?,
136        })
137    }
138
139    /// Pass a javascript callback `string->string` for smt2 input.
140    pub fn new_wasm(callback: Function) -> Self {
141        Self {
142            z3: Z3::new_wasm(callback),
143        }
144    }
145
146    pub fn prove(
147        &mut self,
148        facts: &[Constraint],
149        goal: &Constraint,
150        names: &[String],
151        nonneg: &[Var],
152    ) -> Verdict {
153        let lin = Linearized::new(facts, goal, names, &|v| nonneg.contains(&v));
154
155        let verdict = {
156            if facts.contains(goal)
157                || t0::prove(goal.cmp, &goal.lhs, &goal.rhs, &|v| nonneg.contains(&v))
158            {
159                Verdict::Proved
160            } else {
161                if facts.contains(&goal.negate())
162                    || t0::prove(goal.cmp.negate(), &goal.lhs, &goal.rhs, &|v| {
163                        nonneg.contains(&v)
164                    })
165                {
166                    return Verdict::RefutedBy(goal.negate());
167                }
168
169                let lin_names: Vec<&str> = lin.names.iter().map(String::as_str).collect();
170
171                let z3_lia_verdict =
172                    self.z3
173                        .entails_lia(&lin.facts, &lin.goal, &lin.nonneg, &lin_names);
174
175                match (z3_lia_verdict, lin.pure_linear) {
176                    (Verdict::Proved, _) => Verdict::Proved,
177                    (Verdict::RefutedAt(p), true) => Verdict::RefutedAt(p),
178                    _ => Verdict::Unknown,
179                }
180            }
181        };
182
183        // atom abstraction discards how the atoms relate to their factors, so a nonlinear goal it
184        // could not settle gets one more chance at a positivity certificate
185        if verdict != Verdict::Proved
186            && !lin.pure_linear
187            && t2::prove(&mut self.z3, facts, goal, nonneg)
188        {
189            return Verdict::Proved;
190        }
191
192        verdict
193    }
194}
sirius/solver/mod.rs

sirius/solver/
mod.rs
