smt_scope/items/
enode.rs

1#[cfg(feature = "mem_dbg")]
2use mem_dbg::{MemDbg, MemSize};
3
4use crate::{FxHashMap, FxHashSet, NonMaxU32};
5
6use super::{ENodeIdx, EqGivenIdx, EqTransIdx, InstIdx, ProofIdx, StackIdx, TermIdx};
7
8#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
9#[derive(Debug)]
10pub struct ENode {
11    pub frame: StackIdx,
12    pub blame: ENodeBlame,
13    pub owner: TermIdx,
14    pub z3_generation: NonMaxU32,
15
16    pub(crate) equalities: Vec<Equality>,
17    /// This will never contain a `TransitiveExpl::to` pointing to itself. It
18    /// may contain `TransitiveExpl::given_len` of 0, but only when
19    /// `get_simple_path` fails but `can_mismatch` is true.
20    pub(crate) transitive: FxHashMap<ENodeIdx, EqTransIdx>,
21}
22
23#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
24#[derive(Debug, Clone)]
25pub enum ENodeBlame {
26    /// The `ENode` was created by an instantiation.
27    Inst((InstIdx, FxHashSet<EqTransIdx>)),
28    /// The `ENode` was created by a proof step.
29    Proof(ProofIdx),
30    /// The `ENode` represents either `#1` or `#2`.
31    BoolConst,
32    /// We don't know why the `ENode` was created.
33    Unknown,
34}
35
36impl ENodeBlame {
37    pub fn inst(&self) -> Option<InstIdx> {
38        match self {
39            Self::Inst((inst, _)) => Some(*inst),
40            _ => None,
41        }
42    }
43
44    pub fn proof(&self) -> Option<ProofIdx> {
45        match self {
46            Self::Proof(proof) => Some(*proof),
47            _ => None,
48        }
49    }
50}
51
52#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
53#[cfg_attr(feature = "mem_dbg", copy_type)]
54#[derive(Debug, Clone, Copy)]
55pub struct Equality {
56    pub(crate) _frame: StackIdx,
57    pub to: ENodeIdx,
58    pub expl: EqGivenIdx,
59}
smt_scope/items/enode.rs

smt_scope/items/
enode.rs
