smt_scope/items/
term.rs

1#[cfg(feature = "mem_dbg")]
2use mem_dbg::{MemDbg, MemSize};
3
4use crate::{BoxSlice, Error, FxHashMap, IString, NonMaxU32, Result, StringTable};
5
6use super::{QuantIdx, TermIdx};
7
8/// A Z3 term and associated data.
9#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
10#[derive(Debug, Clone, PartialEq, Eq, Hash)]
11pub struct Term {
12    pub id: TermId,
13    kind: TermKindInner,
14    /// Takes up `2 * size_of::<usize>()` space and avoids heap allocation for
15    /// lens <= 1.
16    pub child_ids: BoxSlice<TermIdx>,
17}
18
19impl Term {
20    #[allow(clippy::no_effect)]
21    pub(crate) const CHECK_SIZE: bool = {
22        #[allow(dead_code)]
23        struct SmallTerm {
24            id: TermId,
25            kind: TermKind,
26            child_ids: BoxSlice<TermIdx>,
27        }
28        let sizeof_eq = core::mem::size_of::<Term>() == core::mem::size_of::<SmallTerm>();
29        [(); 1][!sizeof_eq as usize];
30        true
31    };
32
33    pub fn new<'a>(
34        id: TermId,
35        kind: TermKind,
36        child_ids: BoxSlice<TermIdx>,
37        t: impl Fn(TermIdx) -> &'a Term,
38    ) -> Self {
39        let _ = Self::CHECK_SIZE;
40        let kind = match kind {
41            TermKind::Var(var) => TermKindInner::Var(var),
42            TermKind::App(app) => {
43                fn get_has_var<'a>(
44                    children: &[TermIdx],
45                    t: impl Fn(TermIdx) -> &'a Term,
46                ) -> Option<bool> {
47                    let mut has_var = false;
48                    for &c in children.iter() {
49                        has_var |= t(c).has_var()?;
50                    }
51                    Some(has_var)
52                }
53                TermKindInner::App(get_has_var(&child_ids, t), app)
54            }
55            TermKind::Quant(quant) => TermKindInner::Quant(quant),
56        };
57        Self {
58            id,
59            kind,
60            child_ids,
61        }
62    }
63
64    pub fn kind(&self) -> TermKind {
65        use TermKindInner::*;
66        match self.kind {
67            Var(.., var) => TermKind::Var(var),
68            App(.., app) => TermKind::App(app),
69            Quant(.., quant) => TermKind::Quant(quant),
70        }
71    }
72
73    pub fn var_idx(&self) -> Option<NonMaxU32> {
74        self.kind().var()
75    }
76    pub fn app_name(&self) -> Option<IString> {
77        self.kind().app()
78    }
79    pub fn quant_idx(&self) -> Option<QuantIdx> {
80        self.kind().quant()
81    }
82
83    /// Does this term contain a free variable? Returns `None` if the term
84    /// contains a quantifier (which may or may not bind all the free vars).
85    pub fn has_var(&self) -> Option<bool> {
86        match self.kind {
87            TermKindInner::Var(_) => Some(true),
88            TermKindInner::App(has_var, _) => has_var,
89            TermKindInner::Quant(_) => None,
90        }
91    }
92
93    /// Checks if this term can match another term. That is, if they have the
94    /// same kind and the same number of children. The children may still be
95    /// different.
96    pub fn can_match(&self, other: &Self) -> bool {
97        if self.kind() != other.kind() {
98            return false;
99        }
100        if self.has_var().unwrap_or(true) || other.has_var().unwrap_or(true) {
101            self.child_ids.len() == other.child_ids.len()
102        } else {
103            self.child_ids == other.child_ids
104        }
105    }
106}
107
108#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
109#[cfg_attr(feature = "mem_dbg", copy_type)]
110#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
111#[repr(u8)]
112pub enum TermKindInner {
113    Var(NonMaxU32),
114    App(Option<bool>, IString),
115    Quant(QuantIdx),
116}
117
118#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
119#[cfg_attr(feature = "mem_dbg", copy_type)]
120#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
121#[repr(u8)]
122pub enum TermKind {
123    Var(NonMaxU32),
124    App(IString),
125    Quant(QuantIdx),
126}
127
128impl TermKind {
129    pub(crate) fn parse_var(value: &str) -> Result<TermKind> {
130        value
131            .parse::<NonMaxU32>()
132            .map(TermKind::Var)
133            .map_err(Error::InvalidVar)
134    }
135    fn var(&self) -> Option<NonMaxU32> {
136        match self {
137            Self::Var(var) => Some(*var),
138            _ => None,
139        }
140    }
141    fn app(&self) -> Option<IString> {
142        match self {
143            Self::App(name) => Some(*name),
144            _ => None,
145        }
146    }
147    fn quant(&self) -> Option<QuantIdx> {
148        match self {
149            Self::Quant(idx) => Some(*idx),
150            _ => None,
151        }
152    }
153}
154
155/// Represents an ID string of the form `name#id` or `name#`.
156#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
157#[cfg_attr(feature = "mem_dbg", copy_type)]
158#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
159#[derive(Debug, Clone, Copy, Default, Hash, PartialEq, Eq)]
160pub struct TermId {
161    pub namespace: Option<IString>,
162    pub id: Option<NonMaxU32>,
163}
164impl TermId {
165    /// Splits an ID string into namespace and ID number.
166    /// 0 is used for identifiers without a number
167    /// (usually for theory-solving 'quantifiers' such as "basic#", "arith#")
168    pub fn parse(strings: &mut StringTable, value: &str) -> Result<Self> {
169        let hash_idx = value.bytes().position(|b| b == b'#');
170        let hash_idx = hash_idx.ok_or_else(|| Error::InvalidIdHash(value.to_string()))?;
171        let (namespace, id) = value.split_at(hash_idx);
172        let id = match &id[1..] {
173            "" => None,
174            id => Some(id.parse::<NonMaxU32>().map_err(Error::InvalidIdNumber)?),
175        };
176        let namespace = (!namespace.is_empty()).then(|| IString(strings.get_or_intern(namespace)));
177        Ok(Self { namespace, id })
178    }
179    pub fn order(&self) -> u32 {
180        self.id.map(|id| id.get() + 1).unwrap_or_default()
181    }
182
183    pub fn to_string_components<'a>(
184        &self,
185        strings: &'a StringTable,
186    ) -> (&'a str, Option<NonMaxU32>) {
187        let namespace = self.namespace.map(|ns| &strings[*ns]).unwrap_or_default();
188        (namespace, self.id)
189    }
190    pub fn to_string(&self, strings: &StringTable) -> String {
191        let (namespace, id) = self.to_string_components(strings);
192        let id = id.map(|id| id.to_string()).unwrap_or_default();
193        format!("{namespace}#{id}")
194    }
195}
196
197/// Remapping from `TermId` to `TermIdx`. We want to have a single flat vector
198/// of terms but `TermId`s don't map to this nicely, additionally the `TermId`s
199/// may repeat and so we want to map to the latest current `TermIdx`. Has a
200/// special fast path for the common empty namespace case.
201#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
202#[derive(Debug)]
203pub struct TermIdToIdxMap<K: Copy> {
204    empty_namespace: Vec<Option<K>>,
205    namespace_map: FxHashMap<IString, Vec<Option<K>>>,
206}
207
208impl<K: Copy> Default for TermIdToIdxMap<K> {
209    fn default() -> Self {
210        Self {
211            empty_namespace: Vec::new(),
212            namespace_map: FxHashMap::default(),
213        }
214    }
215}
216
217impl<K: Copy> TermIdToIdxMap<K> {
218    fn get_vec_mut(&mut self, namespace: Option<IString>) -> Result<&mut Vec<Option<K>>> {
219        if let Some(namespace) = namespace {
220            self.namespace_map.try_reserve(1)?;
221            Ok(self.namespace_map.entry(namespace).or_default())
222        } else {
223            // Special handling of common case for empty namespace
224            Ok(&mut self.empty_namespace)
225        }
226    }
227    pub fn register_term(&mut self, id: TermId, idx: K) -> Result<Option<K>> {
228        let id_idx = id.order() as usize;
229        let vec = self.get_vec_mut(id.namespace)?;
230        if id_idx >= vec.len() {
231            let new_len = id_idx + 1;
232            vec.try_reserve(new_len - vec.len())?;
233            vec.resize(new_len, None);
234        }
235        // The `id` of two different terms may clash and so we may remove
236        // a `TermIdx` from the map. This is fine since we want future uses of
237        // `id` to refer to the new term and not the old one.
238        let old = vec[id_idx].replace(idx);
239        Ok(old)
240    }
241    fn get_vec(&self, namespace: Option<IString>) -> Option<&Vec<Option<K>>> {
242        if let Some(namespace) = namespace {
243            self.namespace_map.get(&namespace)
244        } else {
245            Some(&self.empty_namespace)
246        }
247    }
248    pub fn get_term(&self, id: &TermId) -> Option<K> {
249        self.get_vec(id.namespace)
250            .and_then(|vec| vec.get(id.order() as usize).and_then(|x| x.as_ref()))
251            .copied()
252    }
253}
smt_scope/items/term.rs

smt_scope/items/
term.rs
