smt_scope/parsers/z3/
inst.rs

1#[cfg(feature = "mem_dbg")]
2use mem_dbg::{MemDbg, MemSize};
3
4use crate::{
5    items::{ENodeIdx, Fingerprint, InstIdx, Instantiation, Match, MatchIdx, TermIdx},
6    parsers::z3::stack::Stack,
7    Error, FxHashMap, Result, TiVec,
8};
9
10use super::bugs::InstanceBody;
11
12#[derive(Debug)]
13pub struct InstData<'a> {
14    pub iidx: InstIdx,
15    pub inst: &'a Instantiation,
16    pub midx: MatchIdx,
17    pub match_: &'a Match,
18}
19
20#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
21#[derive(Debug, Default)]
22pub struct Insts {
23    // `theory-solving` fingerprints are always 0, others rarely repeat.
24    fingerprint_to_match: FxHashMap<Fingerprint, (MatchIdx, Option<InstIdx>)>,
25    pub(crate) matches: TiVec<MatchIdx, Match>,
26    pub(crate) insts: TiVec<InstIdx, Instantiation>,
27
28    inst_stack: Vec<ActiveInst>,
29
30    has_theory_solving_inst: bool,
31}
32
33impl Insts {
34    pub(super) fn new_match(
35        &mut self,
36        fingerprint: Fingerprint,
37        match_: Match,
38    ) -> Result<MatchIdx> {
39        self.has_theory_solving_inst |= match_.kind.quant_idx().is_none();
40
41        self.matches.raw.try_reserve(1)?;
42        let idx = self.matches.push_and_get_key(match_);
43        // Can remove a duplicate fingerprint if that one was never instantiated.
44        self.fingerprint_to_match.try_reserve(1)?;
45        self.fingerprint_to_match.insert(fingerprint, (idx, None));
46        Ok(idx)
47    }
48
49    pub fn get_match(&self, fingerprint: Fingerprint) -> Option<MatchIdx> {
50        self.fingerprint_to_match
51            .get(&fingerprint)
52            .map(|(idx, _)| *idx)
53    }
54    pub(super) fn new_inst(
55        &mut self,
56        fingerprint: Fingerprint,
57        inst: Instantiation,
58        body: Option<InstanceBody>,
59        stack: &Stack,
60        can_duplicate: bool,
61    ) -> Result<InstIdx> {
62        let (match_idx, inst_idx) = self
63            .fingerprint_to_match
64            .get_mut(&fingerprint)
65            .unwrap_or_else(|| panic!("{:x}", fingerprint.0));
66        let midx = *match_idx;
67        self.insts.raw.try_reserve(1)?;
68        let iidx = self.insts.push_and_get_key(inst);
69        // I have on very rare occasions seen an `[instance]` repeated twice
70        // with the same fingerprint (without an intermediate `[new-match]`).
71        debug_assert!(
72            stack.is_alive(self.matches[midx].frame)
73                && (can_duplicate
74                    || !inst_idx.is_some_and(|i| stack.is_alive(self.insts[i].frame))),
75            "duplicate instantiation of fingerprint {fingerprint}",
76        );
77        *inst_idx = Some(iidx);
78
79        self.inst_stack.try_reserve(1)?;
80        self.inst_stack.push(ActiveInst::new(iidx, body));
81        Ok(iidx)
82    }
83    pub fn end_inst(&mut self) -> Result<()> {
84        let active = self.inst_stack.pop().ok_or(Error::UnmatchedEndOfInstance)?;
85        self[active.idx].yields_terms = active.yields.into();
86        Ok(())
87    }
88
89    pub(super) fn active_inst(&mut self) -> Option<&mut ActiveInst> {
90        self.inst_stack.last_mut()
91    }
92
93    pub fn has_theory_solving_inst(&self) -> bool {
94        self.has_theory_solving_inst
95    }
96
97    pub fn instantiations(&self) -> impl Iterator<Item = InstData<'_>> {
98        self.insts
99            .iter_enumerated()
100            .map(move |(iidx, inst)| self.get_inst_inner(iidx, inst))
101    }
102
103    pub fn get_inst(&self, iidx: InstIdx) -> InstData<'_> {
104        let inst = &self.insts[iidx];
105        self.get_inst_inner(iidx, inst)
106    }
107
108    fn get_inst_inner<'a>(&'a self, iidx: InstIdx, inst: &'a Instantiation) -> InstData<'a> {
109        let match_ = &self.matches[inst.match_];
110        InstData {
111            iidx,
112            inst,
113            midx: inst.match_,
114            match_,
115        }
116    }
117}
118
119#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
120#[derive(Debug)]
121pub(super) struct ActiveInst {
122    pub(super) idx: InstIdx,
123    pub(super) body: Option<InstanceBody>,
124    pub(super) yields: Vec<ENodeIdx>,
125}
126
127impl ActiveInst {
128    fn new(idx: InstIdx, body: Option<InstanceBody>) -> Self {
129        Self {
130            idx,
131            body,
132            yields: Vec::new(),
133        }
134    }
135
136    pub(super) fn req_eqs(&self, term: TermIdx) -> impl Iterator<Item = (ENodeIdx, ENodeIdx)> + '_ {
137        self.body
138            .iter()
139            .flat_map(move |body| {
140                body.req_eqs
141                    .get(&term)
142                    .into_iter()
143                    .flat_map(|eqs| eqs.iter())
144            })
145            .copied()
146    }
147}
148
149impl std::ops::Index<InstIdx> for Insts {
150    type Output = Instantiation;
151    fn index(&self, idx: InstIdx) -> &Self::Output {
152        &self.insts[idx]
153    }
154}
155impl std::ops::IndexMut<InstIdx> for Insts {
156    fn index_mut(&mut self, idx: InstIdx) -> &mut Self::Output {
157        &mut self.insts[idx]
158    }
159}
160
161impl std::ops::Index<MatchIdx> for Insts {
162    type Output = Match;
163    fn index(&self, idx: MatchIdx) -> &Self::Output {
164        &self.matches[idx]
165    }
166}
smt_scope/parsers/z3/inst.rs

smt_scope/parsers/z3/
inst.rs
