smt_scope/items/
inst.rs

1#[cfg(feature = "mem_dbg")]
2use mem_dbg::{MemDbg, MemSize};
3
4use crate::{BoxSlice, Error, NonMaxU32, Result};
5use std::fmt;
6
7use super::{
8    ENode, ENodeIdx, EqTransIdx, MatchIdx, PatternIdx, ProofIdx, QuantIdx, QuantPat, StackIdx,
9    TermId, TermIdx,
10};
11
12#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
13#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
14#[derive(Debug, Clone)]
15pub struct Match {
16    pub kind: MatchKind,
17    pub blamed: Box<[Blame]>,
18    pub frame: StackIdx,
19}
20
21impl Match {
22    /// A quantifier may have multiple possible patterns where each
23    /// instantiation will be due to matching exactly one. Each of these
24    /// patterns has a sequence of arbitrarily many terms which must all be
25    /// matched. This returns a sequence of `Blame` where each explains how the
26    /// corresponding term in the pattern was matched.
27    pub fn pattern_matches(&self) -> impl Iterator<Item = &Blame> {
28        self.blamed.iter()
29    }
30}
31
32#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
33#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
34#[derive(Debug, Clone, Hash, Eq, PartialEq)]
35pub enum MatchKind {
36    MBQI {
37        quant: QuantIdx,
38        bound_terms: BoxSlice<ENodeIdx>,
39    },
40    TheorySolving {
41        axiom_id: TermId,
42        bound_terms: BoxSlice<TermIdx>,
43        rewrite_of: Option<TermIdx>,
44    },
45    Axiom {
46        axiom: QuantIdx,
47        pattern: PatternIdx,
48        bound_terms: BoxSlice<TermIdx>,
49    },
50    Quantifier {
51        quant: QuantIdx,
52        pattern: PatternIdx,
53        bound_terms: BoxSlice<ENodeIdx>,
54    },
55}
56
57#[derive(Debug, Clone, Copy)]
58pub struct BoundVars<'a, T: Copy>(&'a [T]);
59impl<'a, T: Copy> BoundVars<'a, T> {
60    pub fn get(&self, idx: NonMaxU32) -> Option<T> {
61        self.0.get(idx.get() as usize).copied()
62    }
63}
64
65impl MatchKind {
66    pub fn quant_pat(&self) -> Option<QuantPat> {
67        self.quant_idx().map(|quant| QuantPat {
68            quant,
69            pat: self.pattern(),
70        })
71    }
72
73    pub fn quant_idx(&self) -> Option<QuantIdx> {
74        match self {
75            Self::MBQI { quant, .. }
76            | Self::Axiom { axiom: quant, .. }
77            | Self::Quantifier { quant, .. } => Some(*quant),
78            _ => None,
79        }
80    }
81    pub fn pattern(&self) -> Option<PatternIdx> {
82        match self {
83            Self::MBQI { .. } | Self::TheorySolving { .. } => None,
84            Self::Axiom { pattern, .. } | Self::Quantifier { pattern, .. } => Some(*pattern),
85        }
86    }
87
88    pub fn bound_terms<T>(
89        &self,
90        enode: impl Fn(ENodeIdx) -> T,
91        term: impl Fn(TermIdx) -> T,
92    ) -> Box<[T]> {
93        match self {
94            Self::MBQI { bound_terms, .. } | Self::Quantifier { bound_terms, .. } => {
95                bound_terms.iter().map(|&x| enode(x)).collect()
96            }
97            Self::TheorySolving { bound_terms, .. } | Self::Axiom { bound_terms, .. } => {
98                bound_terms.iter().map(|&x| term(x)).collect()
99            }
100        }
101    }
102    pub fn is_discovered(&self) -> bool {
103        self.quant_idx().is_none()
104    }
105    pub fn is_mbqi(&self) -> bool {
106        matches!(self, Self::MBQI { .. })
107    }
108    // TODO: this is currently unused
109    pub fn rewrite_of(&self) -> Option<TermIdx> {
110        match self {
111            Self::TheorySolving { rewrite_of, .. } => *rewrite_of,
112            _ => None,
113        }
114    }
115
116    pub fn bound_term<'a>(
117        &self,
118        to_tidx: impl Fn(ENodeIdx) -> &'a ENode,
119        qvar: NonMaxU32,
120    ) -> Option<TermIdx> {
121        match self {
122            Self::MBQI { bound_terms, .. } | Self::Quantifier { bound_terms, .. } => {
123                BoundVars(bound_terms)
124                    .get(qvar)
125                    .map(to_tidx)
126                    .map(|e| e.owner)
127            }
128            Self::TheorySolving { bound_terms, .. } | Self::Axiom { bound_terms, .. } => {
129                BoundVars(bound_terms).get(qvar)
130            }
131        }
132    }
133
134    pub fn quant_and_enodes(&self) -> Option<(QuantIdx, BoundVars<'_, ENodeIdx>)> {
135        match self {
136            Self::MBQI { quant, bound_terms }
137            | Self::Quantifier {
138                quant, bound_terms, ..
139            } => Some((*quant, BoundVars(bound_terms))),
140            Self::TheorySolving { .. } | Self::Axiom { .. } => None,
141        }
142    }
143}
144
145/// Explains how a term in a pattern was matched. It will always start with an
146/// enode and then have some sequence of equalities used to rewrite distinct
147/// subexpressions of the enode.
148#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
149#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
150#[derive(Debug, Clone, PartialEq, Eq, Hash)]
151pub struct Blame {
152    pub coupling: Coupling,
153    pub enode: ENodeIdx,
154    pub equalities: BoxSlice<EqTransIdx>,
155}
156
157#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
158#[cfg_attr(feature = "mem_dbg", copy_type)]
159#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
160#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
161pub enum Coupling {
162    /// The enode and equalities parsed from the logfile could be used exactly
163    /// to obtain the matched sub-pattern.
164    Exact,
165    /// The enode and equalities parsed from the logfile could be used exactly
166    /// to obtain the matched sub-pattern. Some of the equalities needed to be
167    /// flipped, reused or used in a different order.
168    SwappedEqs,
169    /// The enode required some unlogged equalities to be matched. These
170    /// equalities existed in the logfile but were not blamed.
171    MissingEqs,
172    /// The enode required some new equalities to be matched. These equalities
173    /// did not exist in the logfile.
174    AddedEqs,
175    /// The enode could not be rewritten to the matched sub-pattern. This should
176    /// not appear in the final `Blame`.
177    Error,
178}
179
180impl Blame {
181    pub fn is_complete(&self) -> bool {
182        matches!(
183            self.coupling,
184            Coupling::Exact | Coupling::SwappedEqs | Coupling::MissingEqs
185        )
186    }
187}
188
189/// An identifier for a Z3 quantifier instantiation (called "fingerprint" in the original Axiom Profiler).
190/// Represented as a 16-digit hexadecimal number in log files.
191#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
192#[cfg_attr(feature = "mem_dbg", copy_type)]
193#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
194#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
195pub struct Fingerprint(pub u64);
196impl Fingerprint {
197    pub fn parse(value: &str) -> Result<Self> {
198        u64::from_str_radix(value.strip_prefix("0x").unwrap_or(value), 16)
199            .map(Self)
200            .map_err(Error::InvalidFingerprint)
201    }
202    pub fn is_zero(&self) -> bool {
203        self.0 == 0
204    }
205}
206impl std::ops::Deref for Fingerprint {
207    type Target = u64;
208    fn deref(&self) -> &Self::Target {
209        &self.0
210    }
211}
212impl fmt::Display for Fingerprint {
213    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
214        write!(f, "{:x}", self.0)
215    }
216}
217
218/// A Z3 instantiation.
219#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
220#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
221#[derive(Debug, Clone)]
222pub struct Instantiation {
223    pub match_: MatchIdx,
224    pub kind: InstantiationKind,
225    /// The enodes that were yielded by the instantiation along with the
226    /// generalised terms for them (`MaybeSynthIdx::Parsed` if the yielded term
227    /// doesn't contain any quantified variables)
228    pub yields_terms: BoxSlice<ENodeIdx>,
229    pub frame: StackIdx,
230}
231
232#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
233#[cfg_attr(feature = "mem_dbg", copy_type)]
234#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
235#[derive(Debug, Clone, Copy)]
236pub enum InstantiationKind {
237    /// Axiom instantiations (i.e. those with `.fingerprint.is_zero()`) point to
238    /// a term regardless of whether proofs are enabled. These terms seem to
239    /// generally be an equality.
240    Axiom { body: TermIdx },
241    NonAxiom {
242        fingerprint: Fingerprint,
243        z3_generation: NonMaxU32,
244        proof: InstProofLink,
245    },
246}
247
248impl InstantiationKind {
249    pub fn fingerprint(&self) -> Fingerprint {
250        match self {
251            Self::NonAxiom { fingerprint, .. } => *fingerprint,
252            _ => Fingerprint(0),
253        }
254    }
255
256    pub fn z3_generation(&self) -> Option<NonMaxU32> {
257        match self {
258            Self::NonAxiom { z3_generation, .. } => Some(*z3_generation),
259            _ => None,
260        }
261    }
262
263    pub fn proof(&self) -> Option<ProofIdx> {
264        match self {
265            Self::NonAxiom {
266                proof: InstProofLink::HasProof(proof),
267                ..
268            } => Some(*proof),
269            _ => None,
270        }
271    }
272}
273
274/// A Z3 instantiation.
275#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
276#[cfg_attr(feature = "mem_dbg", copy_type)]
277#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
278#[derive(Debug, Clone, Copy)]
279pub enum InstProofLink {
280    /// When proofs are enabled (i.e. if z3 was run with `proof=true`) non-axiom
281    /// instantiations will include a pointer to the instantiation proof step.
282    HasProof(ProofIdx),
283    /// When proofs are disabled, non-axiom instantiations have no link to the
284    /// fact (i.e. their body) that was instantiated. However, we use a hack to
285    /// try and find the proof term nevertheless: the `[mk-app]` immediately
286    /// preceding the `[instantiation]` line is generally the term we just
287    /// proved.
288    ProofsDisabled(Option<TermIdx>),
289}
smt_scope/items/inst.rs

smt_scope/items/
inst.rs
