smt_scope/parsers/z3/
z3parser.rs

1use core::{fmt, ops::Index};
2
3#[cfg(feature = "mem_dbg")]
4use mem_dbg::{MemDbg, MemSize};
5use nonmax::NonMaxU64;
6use typed_index_collections::TiSlice;
7
8use crate::{
9    items::*, parsers::z3::VersionInfo, FxHashMap, IString, NonMaxU32, StringTable, TiVec,
10};
11
12use super::{
13    cdcl::Literals,
14    egraph::EGraph,
15    inst::{InstData, Insts},
16    inter_line::InterLine,
17    smt2::EventLog,
18    stack::{HasFrame, Stack},
19    synthetic::{AnyTerm, SynthIdx, SynthTerms},
20    terms::Terms,
21    // theory::TheorySolving,
22};
23
24/// A parser for Z3 log files. Use one of the various `Z3Parser::from_*` methods
25/// to construct this parser.
26#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
27#[derive(Debug)]
28pub struct Z3Parser {
29    pub(crate) version_info: VersionInfo,
30    /// How many times have we seen a `(push)`, determines if we are in incremental mode.
31    pub(crate) push_count: u32,
32    pub(crate) terms: Terms,
33    pub(crate) synth_terms: SynthTerms,
34
35    pub(crate) quantifiers: TiVec<QuantIdx, Quantifier>,
36
37    pub(crate) insts: Insts,
38
39    // pub(crate) ts: TheorySolving,
40    pub(crate) egraph: EGraph,
41    pub(crate) stack: Stack,
42
43    pub lits: Literals,
44
45    pub strings: StringTable,
46    pub events: EventLog,
47    pub(super) comm: InterLine,
48}
49
50pub type AstSize = core::result::Result<Option<NonMaxU64>, TermIdx>;
51
52#[derive(Default)]
53pub struct ParseErrors {
54    pub match_error_count: usize,
55    pub match_count: usize,
56
57    pub trans_error_count: usize,
58    pub trans_count: usize,
59}
60
61impl fmt::Display for ParseErrors {
62    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
63        if self.match_error_count == 0 && self.trans_error_count == 0 {
64            return Ok(());
65        }
66        write!(f, " Errors:")?;
67        if self.match_error_count != 0 {
68            write!(
69                f,
70                " {} match ({:.1}%)",
71                self.match_error_count,
72                100. * self.match_error_count as f64 / self.match_count as f64
73            )?;
74        }
75        if self.trans_error_count != 0 {
76            write!(
77                f,
78                " {} eq ({:.1}%)",
79                self.trans_error_count,
80                100. * self.trans_error_count as f64 / self.trans_count as f64
81            )?;
82        }
83        Ok(())
84    }
85}
86
87impl Z3Parser {
88    pub fn errors(&self) -> ParseErrors {
89        let mut errors = ParseErrors::default();
90        for match_ in self.insts.matches.iter() {
91            if match_.kind.pattern().is_none() {
92                continue;
93            }
94            debug_assert!(!match_.blamed.is_empty());
95            errors.match_count += 1;
96            if match_.blamed.iter().any(|b| !b.is_complete()) {
97                errors.match_error_count += 1;
98            }
99        }
100        errors.trans_count = self.egraph.equalities.transitive.len();
101        errors.trans_error_count = self
102            .egraph
103            .equalities
104            .transitive
105            .iter()
106            .filter(|eq| eq.error_from().is_some())
107            .count();
108        errors
109    }
110
111    pub fn meaning(&self, tidx: TermIdx) -> Option<&Meaning> {
112        self.terms.meaning(tidx)
113    }
114
115    pub fn from_to(&self, eq: EqTransIdx) -> (ENodeIdx, ENodeIdx) {
116        self.egraph.equalities.from_to(eq)
117    }
118
119    pub fn quant_count_incl_theory_solving(&self) -> (usize, bool) {
120        (self.quantifiers.len(), self.insts.has_theory_solving_inst())
121    }
122
123    pub fn quantifiers(&self) -> &TiSlice<QuantIdx, Quantifier> {
124        &self.quantifiers
125    }
126    pub fn instantiations(&self) -> &TiSlice<InstIdx, Instantiation> {
127        &self.insts.insts
128    }
129    pub fn instantiations_data(&self) -> impl Iterator<Item = InstData<'_>> + '_ {
130        self.insts.instantiations()
131    }
132    pub fn terms(&self) -> &TiSlice<TermIdx, Term> {
133        self.terms.app_terms.terms()
134    }
135    pub fn proofs(&self) -> &TiSlice<ProofIdx, ProofStep> {
136        self.terms.proof_terms.terms()
137    }
138    pub fn cdcls(&self) -> &TiSlice<CdclIdx, Cdcl> {
139        self.lits.cdcl.cdcls()
140    }
141
142    pub fn quantifier_body(&self, qidx: QuantIdx) -> Option<TermIdx> {
143        let children = &self[self[qidx].term].child_ids;
144        children.last().copied()
145    }
146
147    pub fn patterns(&self, q: QuantIdx) -> Option<&TiSlice<PatternIdx, TermIdx>> {
148        let child_ids = &self[self[q].term].child_ids;
149        child_ids
150            .len()
151            .checked_sub(1)
152            .map(|len| &child_ids[..len])
153            .map(TiSlice::from_ref)
154    }
155
156    pub fn get_inst(&self, iidx: InstIdx) -> InstData<'_> {
157        self.insts.get_inst(iidx)
158    }
159
160    pub fn get_instantiation_body(&self, iidx: InstIdx) -> Option<TermIdx> {
161        self.terms.get_instantiation_body(self[iidx].kind)
162    }
163
164    pub fn as_tidx(&self, sidx: SynthIdx) -> Option<TermIdx> {
165        self.synth_terms.as_tidx(sidx)
166    }
167
168    pub fn get_pattern(&self, qpat: QuantPat) -> Option<TermIdx> {
169        qpat.pat.map(|pat| self.patterns(qpat.quant).unwrap()[pat])
170    }
171
172    pub fn get_pattern_term(&self, qpat: QuantPat) -> Option<&Term> {
173        self.get_pattern(qpat).map(|tidx| &self[tidx])
174    }
175
176    pub fn get_frame(&self, idx: impl HasFrame) -> &StackFrame {
177        &self.stack[idx.frame(self)]
178    }
179
180    /// Does the proof step `pidx` prove `false`? This can may be under a
181    /// hypothesis so might not necessarily imply unsat.
182    pub fn proves_false(&self, pidx: ProofIdx) -> bool {
183        let result = &self[self[pidx].result];
184        result.child_ids.is_empty() && result.app_name().is_some_and(|name| &self[name] == "false")
185    }
186
187    /// Returns the size in AST nodes of the term `tidx`. Note that z3 eagerly
188    /// reduces terms such as `1 + 1` to `2` meaning that a matching loop can be
189    /// constant in this size metric!
190    pub fn ast_size(&self, tidx: TermIdx, cached: &mut FxHashMap<TermIdx, AstSize>) -> AstSize {
191        fn children(tidx: TermIdx, term: &Term) -> core::result::Result<&[TermIdx], TermIdx> {
192            match term.kind() {
193                TermKind::Var(_) => Err(tidx),
194                TermKind::App(_) => Ok(&*term.child_ids),
195                // TODO: decide if we want to return a size for quantifiers
196                TermKind::Quant(_) => {
197                    let body = term.child_ids.last().map(core::slice::from_ref);
198                    Ok(body.unwrap_or_default())
199                }
200            }
201        }
202        *self.terms.app_terms.ast_walk_cached(
203            tidx,
204            (),
205            cached,
206            |tidx, term, ()| (children(tidx, term).ok().unwrap_or_default(), ()),
207            |tidx, term, cached, ()| {
208                let children = children(tidx, term)?;
209                let mut size = NonMaxU64::ONE;
210                for child in children {
211                    let Some(child) = cached[child]? else {
212                        return Ok(None);
213                    };
214                    let child = NonMaxU64::new(size.get().saturating_add(child.get()));
215                    let Some(child) = child else {
216                        return Ok(None);
217                    };
218                    size = child;
219                }
220                Ok(Some(size))
221            },
222        )
223    }
224
225    pub fn inst_ast_size(
226        &self,
227        iidx: InstIdx,
228        cached: &mut FxHashMap<TermIdx, AstSize>,
229    ) -> std::option::Option<NonMaxU64> {
230        let bound_terms = self[self[iidx].match_]
231            .kind
232            .bound_terms(|e| self[e].owner, |t| t);
233        let mut sum = NonMaxU64::ZERO;
234        for bt in bound_terms {
235            let size = self.ast_size(bt, cached).unwrap();
236            let size = sum.get().saturating_add(size?.get());
237            sum = NonMaxU64::new(size)?;
238        }
239        Some(sum)
240    }
241
242    pub fn new_quant_pat_vec<T>(&self, f: impl Fn(QuantPat) -> T) -> QuantPatVec<T> {
243        QuantPatVec(
244            self.quantifiers()
245                .keys()
246                .map(|quant| {
247                    let mbqi = f(QuantPat { quant, pat: None });
248                    let pats = self.patterns(quant).into_iter().flat_map(|p| p.keys());
249                    let pats = pats
250                        .map(|pat| {
251                            f(QuantPat {
252                                quant,
253                                pat: Some(pat),
254                            })
255                        })
256                        .collect();
257                    PatVec { mbqi, pats }
258                })
259                .collect(),
260        )
261    }
262
263    pub(super) fn bound(&self, match_: &MatchKind, qvar: NonMaxU32) -> Option<TermIdx> {
264        match_.bound_term(|e| &self[e], qvar)
265    }
266}
267
268impl Index<TermIdx> for Z3Parser {
269    type Output = Term;
270    fn index(&self, idx: TermIdx) -> &Self::Output {
271        &self.terms[idx]
272    }
273}
274impl Index<SynthIdx> for Z3Parser {
275    type Output = AnyTerm;
276    fn index(&self, idx: SynthIdx) -> &Self::Output {
277        self.synth_terms.index(&self.terms, idx)
278    }
279}
280impl Index<ProofIdx> for Z3Parser {
281    type Output = ProofStep;
282    fn index(&self, idx: ProofIdx) -> &Self::Output {
283        &self.terms[idx]
284    }
285}
286impl Index<QuantIdx> for Z3Parser {
287    type Output = Quantifier;
288    fn index(&self, idx: QuantIdx) -> &Self::Output {
289        &self.quantifiers[idx]
290    }
291}
292impl Index<ENodeIdx> for Z3Parser {
293    type Output = ENode;
294    fn index(&self, idx: ENodeIdx) -> &Self::Output {
295        &self.egraph[idx]
296    }
297}
298impl Index<InstIdx> for Z3Parser {
299    type Output = Instantiation;
300    fn index(&self, idx: InstIdx) -> &Self::Output {
301        &self.insts[idx]
302    }
303}
304impl Index<MatchIdx> for Z3Parser {
305    type Output = Match;
306    fn index(&self, idx: MatchIdx) -> &Self::Output {
307        &self.insts[idx]
308    }
309}
310impl Index<EqGivenIdx> for Z3Parser {
311    type Output = EqualityExpl;
312    fn index(&self, idx: EqGivenIdx) -> &Self::Output {
313        &self.egraph.equalities.given[idx]
314    }
315}
316impl Index<EqTransIdx> for Z3Parser {
317    type Output = TransitiveExpl;
318    fn index(&self, idx: EqTransIdx) -> &Self::Output {
319        &self.egraph.equalities.transitive[idx]
320    }
321}
322impl Index<StackIdx> for Z3Parser {
323    type Output = StackFrame;
324    fn index(&self, idx: StackIdx) -> &Self::Output {
325        &self.stack[idx]
326    }
327}
328impl Index<LitIdx> for Z3Parser {
329    type Output = Literal;
330    fn index(&self, idx: LitIdx) -> &Self::Output {
331        &self.lits[idx]
332    }
333}
334impl Index<CdclIdx> for Z3Parser {
335    type Output = Cdcl;
336    fn index(&self, idx: CdclIdx) -> &Self::Output {
337        &self.lits.cdcl[idx]
338    }
339}
340impl Index<IString> for Z3Parser {
341    type Output = str;
342    fn index(&self, idx: IString) -> &Self::Output {
343        &self.strings[*idx]
344    }
345}
346
347#[test]
348fn ast_size() {
349    use rand::seq::SliceRandom;
350    use rand::SeedableRng;
351
352    let correct: TiVec<TermIdx, AstSize> =
353        serde_json::from_str(include_str!("../../../tests/data/ast_size.json")).unwrap();
354    let parser = crate::test_parser();
355    let mut idxs: Vec<_> = parser.terms().keys().collect();
356    for i in 0..10 {
357        let mut rng = rand::rngs::StdRng::seed_from_u64(i);
358        idxs.shuffle(&mut rng);
359        let mut cached = FxHashMap::default();
360        for &idx in &idxs {
361            let size = parser.ast_size(idx, &mut cached);
362            assert_eq!(size, correct[idx], "idx {idx}");
363        }
364    }
365}
smt_scope/parsers/z3/z3parser.rs

smt_scope/parsers/z3/
z3parser.rs
