smt_scope/parsers/z3/
bugs.rs

1use std::{borrow::Cow, collections::hash_map::Entry};
2
3#[cfg(feature = "mem_dbg")]
4use mem_dbg::{MemDbg, MemSize};
5
6use crate::{
7    items::{
8        Blame, BoundVars, ENodeIdx, EqTransIdx, InstIdx, MatchIdx, MatchKind, ProofIdx,
9        ProofStepKind, TermId, TermIdx, TermKind,
10    },
11    Error as E, FxHashMap, FxHashSet, IString, NonMaxU32, Result, StringTable,
12};
13
14use super::{
15    blame::{BasicEq, BlameFinder, BlamedEqsParse, ComplexEq, CustomEq, ForceEq},
16    terms::Terms,
17    Z3Parser,
18};
19
20// Z3 FIXED (v4.9.0+) https://github.com/Z3Prover/z3/issues/6081
21// This changes `null` to `<null>` and adds `|` around :qid with spaces.
22
23impl Z3Parser {
24    fn is_z3_6081_fixed(&self) -> bool {
25        self.version_info.is_ge_version(4, 9, 0)
26    }
27
28    pub(super) fn check_lambda_name(&self, lambda: &str) -> Result<()> {
29        let correct = if self.is_z3_6081_fixed() {
30            lambda == "<null>"
31        } else {
32            lambda == "null"
33        };
34        correct
35            .then_some(())
36            .ok_or_else(|| E::NonNullLambdaName(lambda.to_string()))
37    }
38
39    pub(super) fn parse_qid<'a>(
40        &self,
41        l: &mut impl Iterator<Item = &'a str>,
42    ) -> Result<(Cow<'a, str>, NonMaxU32)> {
43        let mut qid = Cow::Borrowed(l.next().ok_or(E::UnexpectedNewline)?);
44        let mut num_vars = l.next().ok_or(E::UnexpectedNewline)?;
45        if self.is_z3_6081_fixed() {
46            if qid.starts_with('|') && !qid.ends_with('|') {
47                qid += " ";
48                qid += num_vars;
49                while !num_vars.ends_with('|') {
50                    num_vars = l.next().ok_or(E::UnexpectedNewline)?;
51                    qid += " ";
52                    qid += num_vars;
53                }
54                num_vars = l.next().ok_or(E::UnexpectedNewline)?;
55            }
56            let nvs = num_vars.parse::<NonMaxU32>().map_err(E::InvalidVarNum)?;
57            return Ok((qid, nvs));
58        }
59
60        let mut nvs = num_vars.parse::<NonMaxU32>();
61        if nvs.is_err() {
62            qid = Cow::Owned(format!("|{qid}"));
63        }
64        while nvs.is_err() {
65            qid += " ";
66            qid += num_vars;
67            num_vars = l.next().ok_or(E::UnexpectedNewline)?;
68            nvs = num_vars.parse::<NonMaxU32>();
69        }
70        if matches!(qid, Cow::Owned(_)) {
71            qid += "|";
72        }
73        Ok((qid, nvs.unwrap()))
74    }
75}
76
77// Z3 ISSUE: https://github.com/viperproject/smt-scope/issues/106
78
79impl Z3Parser {
80    pub(super) fn parse_app_name<'a>(
81        &mut self,
82        l: &mut impl Iterator<Item = &'a str>,
83    ) -> Result<(Cow<'a, str>, Option<TermId>)> {
84        let mut name = Cow::Borrowed(l.next().ok_or(E::UnexpectedNewline)?);
85        let mut l = l.map(|id| (id, TermId::parse(&mut self.strings, id)));
86        let mut idp = l.next();
87
88        let post = |name: Cow<'a, str>| match name {
89            Cow::Borrowed(n) => Cow::Borrowed(n),
90            Cow::Owned(mut n) => {
91                n += "|";
92                Cow::Owned(n)
93            }
94        };
95        while let Some((ids, id)) = idp {
96            if let Ok(id) = id {
97                return Ok((post(name), Some(id)));
98            }
99            if let Cow::Borrowed(n) = name {
100                name = Cow::Owned(format!("|{n}"));
101            }
102            name += " ";
103            name += ids;
104            idp = l.next();
105        }
106        Ok((post(name), None))
107    }
108}
109
110impl Z3Parser {
111    /// Unused.
112    /// TODO: this could help us fix the egraph `can_mismatch` thing
113    pub fn check_eq(&self, from: ENodeIdx, to: ENodeIdx) -> bool {
114        self.egraph.check_eq(from, to, &self.stack)
115            || self.check_eq_if(from, to)
116            || self.check_eq_if(to, from)
117    }
118
119    fn check_eq_if(&self, from: ENodeIdx, to: ENodeIdx) -> bool {
120        let term = &self[self[from].owner];
121        if term.app_name().is_none_or(|n| &self[n] != "if") || term.child_ids.len() != 3 {
122            return false;
123        }
124        let Some(lit) = self.lits.get_assign(term.child_ids[0], &self.stack) else {
125            return false;
126        };
127        let from = if self[lit].term.value {
128            term.child_ids[1]
129        } else {
130            term.child_ids[2]
131        };
132        let Some(from) = self.egraph.get_enode_imm(from, &self.stack) else {
133            debug_assert!(false, "if child not in egraph");
134            return false;
135        };
136        self.check_eq(from, to)
137    }
138}
139
140// Z3 ISSUE: https://github.com/viperproject/smt-scope/issues/63
141
142#[derive(Debug, Clone, Copy)]
143pub struct TransEqAllowed {
144    pub can_mismatch_initial: bool,
145    pub can_mismatch_congr: bool,
146}
147
148impl Z3Parser {
149    pub(super) fn make_blamed(
150        &mut self,
151        match_: &MatchKind,
152        blamed: Vec<(usize, ENodeIdx, BlamedEqsParse)>,
153        pat: TermIdx,
154    ) -> Result<(bool, Box<[Blame]>)> {
155        let pattern = &self[pat];
156        if blamed.len() < pattern.child_ids.len() {
157            return Err(E::SubpatTooFewBlame(pattern.child_ids.len() - blamed.len()));
158        }
159
160        let mut finder = BlameFinder::new(self, match_, blamed, pat)?;
161        if let Some((correct_order, result)) = finder.find_blamed::<BasicEq>()? {
162            return Ok((correct_order, result));
163        }
164        if let Some((correct_order, result)) = finder.find_blamed::<ComplexEq>()? {
165            return Ok((correct_order, result));
166        }
167        if let Some((correct_order, result)) = finder.find_blamed::<CustomEq>()? {
168            return Ok((correct_order, result));
169        }
170        if let Some((correct_order, result)) = finder.find_blamed::<ForceEq>()? {
171            return Ok((correct_order, result));
172        }
173
174        let not_found = finder.not_found();
175        Err(E::SubpatNoBlame(not_found))
176    }
177}
178
179// Z3 ISSUE: https://github.com/viperproject/smt-scope/issues/100
180
181#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
182#[derive(Debug, Default)]
183pub(super) struct TermsBug {
184    /// Solve bug by switching to an artificial namespace after a "string" mk_app.
185    get_model: Option<IString>,
186    get_model_idx: u32,
187}
188
189impl Terms {
190    /// Normally one would use `app_terms.parse_existing_id`, but here we
191    /// implement the workaround for `get_model`.
192    pub fn parse_app_child_id(&self, mut term_id: TermId) -> Result<TermIdx> {
193        if let Some(namespace) = self.bug.get_model {
194            debug_assert!(term_id.namespace.is_none());
195            term_id.namespace = Some(namespace);
196        }
197        self.get_app_term_bug(term_id)
198    }
199
200    pub fn check_get_model(&mut self, id: &mut TermId, name: &str, strings: &mut StringTable) {
201        let bug = &mut self.bug;
202        let get_model = bug.get_model.take();
203        if id.namespace.is_some() {
204            return;
205        }
206        // See https://github.com/Z3Prover/z3/blob/z3-4.13.4/src/ast/format.cpp#L45-L52
207        let Some(get_model) = get_model else {
208            // Is a mk_app line with this term the start of a get-model command?
209            if name == "string" {
210                let namespace = format!("get-model-{}", bug.get_model_idx);
211                bug.get_model_idx += 1;
212                bug.get_model = Some(IString(strings.get_or_intern(namespace)));
213                id.namespace = bug.get_model;
214            }
215            return;
216        };
217        match name {
218            "string" | "cr" | "compose" | "indent" | "choice" => {
219                bug.get_model = Some(get_model);
220                id.namespace = Some(get_model);
221            }
222            _ => (),
223        }
224    }
225}
226
227// TODO (file issue): the produced body of an instantiation can be different than the
228// expected one with normal substitutions.
229
230#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
231#[derive(Debug, Default)]
232pub(super) struct InstanceBody {
233    pub req_eqs: FxHashMap<TermIdx, FxHashSet<(ENodeIdx, ENodeIdx)>>,
234}
235
236impl Z3Parser {
237    pub(super) fn instance_body(
238        &self,
239        proof: Option<ProofIdx>,
240        midx: MatchIdx,
241    ) -> Option<InstanceBody> {
242        let proof = &self[proof?];
243        // Can be Quantifier or MBQI kind here
244        let match_ = &self[midx];
245        let Some((qidx, bound)) = match_.kind.quant_and_enodes() else {
246            debug_assert!(false, "unexpected kind {match_:?}");
247            return None;
248        };
249        let body = match proof.kind {
250            ProofStepKind::PR_QUANT_INST => {
251                // Proved `¬quant ∨ body`
252                let result = &self[proof.result];
253                debug_assert_eq!(result.child_ids.len(), 2);
254                debug_assert!(result.app_name().is_some_and(|n| &self[n] == "or"));
255                debug_assert!({
256                    let not = &self[result.child_ids[0]];
257                    not.child_ids.len() == 1
258                        && not.app_name().is_some_and(|n| &self[n] == "not")
259                        && self[not.child_ids[0]]
260                            .quant_idx()
261                            .is_some_and(|q| q == qidx)
262                });
263                result.child_ids[1]
264            }
265            ProofStepKind::PR_TRANS => {
266                // Proved `body = true`, regardless of quant truth
267                let result = &self[proof.result];
268                debug_assert_eq!(result.child_ids.len(), 2);
269                debug_assert!(result.app_name().is_some_and(|n| &self[n] == "="));
270                debug_assert!({
271                    let true_ = &self[result.child_ids[1]];
272                    true_.child_ids.is_empty()
273                        && true_.app_name().is_some_and(|n| &self[n] == "true")
274                });
275                result.child_ids[0]
276            }
277            _ => {
278                debug_assert!(
279                    false,
280                    "unexpected kind {proof:?} / {:?}",
281                    self[proof.result].id
282                );
283                return None;
284            }
285        };
286        let Some(qbody) = self.quantifier_body(qidx) else {
287            debug_assert!(false, "quantifier {:?} has no body", self[qidx]);
288            return None;
289        };
290        let mut ib = InstanceBody::default();
291        self.mk_instance_body(bound, 0, qbody, body, &mut ib);
292        Some(ib)
293    }
294
295    fn mk_instance_body(
296        &self,
297        bound: BoundVars<ENodeIdx>,
298        // The number of quantified variables we have walked through from the
299        // top-level instantiated expr (which might have nested quants) to here?
300        mut inner_binds: u32,
301        qbody: TermIdx,
302        body: TermIdx,
303        ib: &mut InstanceBody,
304    ) -> bool {
305        let Entry::Vacant(v) = ib.req_eqs.entry(body) else {
306            return false;
307        };
308
309        let qb = &self[qbody];
310        if qb.has_var().is_some_and(|v| !v) {
311            debug_assert_eq!(qbody, body, "unexpected unequal no var body");
312            return qbody != body;
313        }
314
315        let b = match qb.kind() {
316            TermKind::Var(qvar) => {
317                if let Some(qvar) = qvar.get().checked_sub(inner_binds) {
318                    let Some(qb) = bound.get(NonMaxU32::new(qvar).unwrap()) else {
319                        debug_assert!(false, "error: {qvar:?} / {bound:?} ({inner_binds})");
320                        return true;
321                    };
322                    let qbody = self[qb].owner;
323                    if qbody != body {
324                        let Some(b) = self.egraph.get_enode_imm(body, &self.stack) else {
325                            debug_assert!(false, "body not in egraph");
326                            return true;
327                        };
328                        if !self.egraph.check_eq(qb, b, &self.stack) {
329                            // TODO: handle this case
330                            return true;
331                        }
332                        v.insert(Default::default()).insert((qb, b));
333                    }
334                    return false;
335                } else {
336                    let b = &self[body];
337                    let TermKind::Var(var) = b.kind() else {
338                        debug_assert!(false, "unexpected kind {b:?}");
339                        return true;
340                    };
341                    debug_assert_eq!(qvar, var, "unexpected var {qvar} / {var} / {bound:?}");
342                    return qvar != var;
343                }
344            }
345            TermKind::Quant(qinner) => {
346                let b = &self[body];
347                let TermKind::Quant(inner) = b.kind() else {
348                    debug_assert!(false, "unexpected kind {b:?}");
349                    return true;
350                };
351                let qinner = &self[qinner];
352                let inner = &self[inner];
353                if qinner.num_vars != inner.num_vars
354                    || qinner.kind != inner.kind
355                    || qb.child_ids.len() != b.child_ids.len()
356                {
357                    debug_assert!(
358                        false,
359                        "unexpected quant {qinner:?} / {inner:?} / {qb:?} / {b:?}"
360                    );
361                    return true;
362                }
363                let vars = qinner.num_vars.get();
364                inner_binds += vars;
365                b
366            }
367            TermKind::App(qname) => {
368                let b = &self[body];
369                debug_assert!(inner_binds > 0 || !b.has_var().is_some_and(|v| v));
370                let TermKind::App(name) = b.kind() else {
371                    debug_assert!(false, "unexpected kind {b:?}");
372                    return true;
373                };
374                if qname != name || qb.child_ids.len() != b.child_ids.len() {
375                    debug_assert!(false, "unexpected app body {qb:?} / {b:?}");
376                    return true;
377                }
378                b
379            }
380        };
381        let mut error = false;
382        for (q, b) in qb.child_ids.iter().zip(b.child_ids.iter()) {
383            error |= self.mk_instance_body(bound, inner_binds, *q, *b, ib);
384        }
385        let eqs = b.child_ids.iter();
386        let eqs: FxHashSet<_> = eqs
387            .flat_map(|b| {
388                let eqs = ib.req_eqs.get(b);
389                eqs.into_iter().flat_map(|e| e.iter().copied())
390            })
391            .collect();
392        let old = ib.req_eqs.insert(body, eqs);
393        debug_assert!(old.is_none(), "unexpected old eqs {old:?}");
394        error || old.is_some()
395    }
396
397    pub(super) fn active_inst(
398        &mut self,
399        idx: TermIdx,
400    ) -> Result<Option<(InstIdx, FxHashSet<EqTransIdx>)>> {
401        let created_by = self.insts.active_inst();
402        created_by
403            .as_ref()
404            .map(|a| {
405                let req_eqs = a.req_eqs(idx);
406                let mismatch = TransEqAllowed {
407                    can_mismatch_initial: false,
408                    can_mismatch_congr: false,
409                };
410                let req_eqs = req_eqs
411                    .map(|(from, to)| {
412                        self.egraph
413                            .new_trans_equality(from, to, &self.stack, mismatch)
414                            .map(|r| r.unwrap())
415                    })
416                    .collect::<Result<_>>()?;
417                Ok((a.idx, req_eqs))
418            })
419            .transpose()
420    }
421}