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    ) -> Vec<std::option::Option<NonMaxU64>> {
230        let bound_terms = self[self[iidx].match_]
231            .kind
232            .bound_terms(|e| self[e].owner, |t| t);
233        IntoIterator::into_iter(bound_terms)
234            .map(|bt| self.ast_size(bt, cached).unwrap())
235            .collect()
236    }
237
238    pub fn new_quant_pat_vec<T>(&self, f: impl Fn(QuantPat) -> T) -> QuantPatVec<T> {
239        QuantPatVec(
240            self.quantifiers()
241                .keys()
242                .map(|quant| {
243                    let mbqi = f(QuantPat { quant, pat: None });
244                    let pats = self.patterns(quant).into_iter().flat_map(|p| p.keys());
245                    let pats = pats
246                        .map(|pat| {
247                            f(QuantPat {
248                                quant,
249                                pat: Some(pat),
250                            })
251                        })
252                        .collect();
253                    PatVec { mbqi, pats }
254                })
255                .collect(),
256        )
257    }
258
259    pub(super) fn bound(&self, match_: &MatchKind, qvar: NonMaxU32) -> Option<TermIdx> {
260        match_.bound_term(|e| &self[e], qvar)
261    }
262
263    fn named_proofs(&self) -> &FxHashMap<ProofIdx, Option<ProofIdx>> {
264        &self.terms.named_asserts.named
265    }
266
267    /// See explanation at `NamedAsserts` struct. If `pidx` is a named assertion
268    /// then it was transformed into an implication, where the lhs is a named
269    /// variable. This returns the assertion corresponding to that variable.
270    pub fn named_assert_to_variable(&self, pidx: ProofIdx) -> Option<ProofIdx> {
271        self.named_proofs().get(&pidx).and_then(|opt| *opt)
272    }
273
274    /// See explanation at `NamedAsserts` struct. Returns true if `pidx` is a
275    /// named variable.
276    pub fn is_named_variable(&self, pidx: ProofIdx) -> bool {
277        self.named_proofs()
278            .get(&pidx)
279            .is_some_and(|opt| opt.is_none())
280    }
281}
282
283impl Index<TermIdx> for Z3Parser {
284    type Output = Term;
285    fn index(&self, idx: TermIdx) -> &Self::Output {
286        &self.terms[idx]
287    }
288}
289impl Index<SynthIdx> for Z3Parser {
290    type Output = AnyTerm;
291    fn index(&self, idx: SynthIdx) -> &Self::Output {
292        self.synth_terms.index(&self.terms, idx)
293    }
294}
295impl Index<ProofIdx> for Z3Parser {
296    type Output = ProofStep;
297    fn index(&self, idx: ProofIdx) -> &Self::Output {
298        &self.terms[idx]
299    }
300}
301impl Index<QuantIdx> for Z3Parser {
302    type Output = Quantifier;
303    fn index(&self, idx: QuantIdx) -> &Self::Output {
304        &self.quantifiers[idx]
305    }
306}
307impl Index<ENodeIdx> for Z3Parser {
308    type Output = ENode;
309    fn index(&self, idx: ENodeIdx) -> &Self::Output {
310        &self.egraph[idx]
311    }
312}
313impl Index<InstIdx> for Z3Parser {
314    type Output = Instantiation;
315    fn index(&self, idx: InstIdx) -> &Self::Output {
316        &self.insts[idx]
317    }
318}
319impl Index<MatchIdx> for Z3Parser {
320    type Output = Match;
321    fn index(&self, idx: MatchIdx) -> &Self::Output {
322        &self.insts[idx]
323    }
324}
325impl Index<EqGivenIdx> for Z3Parser {
326    type Output = EqualityExpl;
327    fn index(&self, idx: EqGivenIdx) -> &Self::Output {
328        &self.egraph.equalities.given[idx]
329    }
330}
331impl Index<EqTransIdx> for Z3Parser {
332    type Output = TransitiveExpl;
333    fn index(&self, idx: EqTransIdx) -> &Self::Output {
334        &self.egraph.equalities.transitive[idx]
335    }
336}
337impl Index<StackIdx> for Z3Parser {
338    type Output = StackFrame;
339    fn index(&self, idx: StackIdx) -> &Self::Output {
340        &self.stack[idx]
341    }
342}
343impl Index<LitIdx> for Z3Parser {
344    type Output = Literal;
345    fn index(&self, idx: LitIdx) -> &Self::Output {
346        &self.lits[idx]
347    }
348}
349impl Index<CdclIdx> for Z3Parser {
350    type Output = Cdcl;
351    fn index(&self, idx: CdclIdx) -> &Self::Output {
352        &self.lits.cdcl[idx]
353    }
354}
355impl Index<IString> for Z3Parser {
356    type Output = str;
357    fn index(&self, idx: IString) -> &Self::Output {
358        &self.strings[*idx]
359    }
360}
361
362#[test]
363fn ast_size() {
364    use rand::seq::SliceRandom;
365    use rand::SeedableRng;
366
367    let correct: TiVec<TermIdx, AstSize> =
368        serde_json::from_str(include_str!("../../../tests/data/ast_size.json")).unwrap();
369    let parser = crate::test_parser();
370    let mut idxs: Vec<_> = parser.terms().keys().collect();
371    for i in 0..10 {
372        let mut rng = rand::rngs::StdRng::seed_from_u64(i);
373        idxs.shuffle(&mut rng);
374        let mut cached = FxHashMap::default();
375        for &idx in &idxs {
376            let size = parser.ast_size(idx, &mut cached);
377            assert_eq!(size, correct[idx], "idx {idx}");
378        }
379    }
380}
smt_scope/parsers/z3/z3parser.rs

smt_scope/parsers/z3/
z3parser.rs
