smt_scope/items/
quant.rs

1use std::{
2    borrow::Cow,
3    ops::{Index, IndexMut},
4};
5
6#[cfg(feature = "mem_dbg")]
7use mem_dbg::{MemDbg, MemSize};
8
9use crate::{BoxSlice, IString, NonMaxU32, StringTable, TiVec};
10
11use super::{PatternIdx, ProofIdx, QuantIdx, TermIdx};
12
13/// A Z3 quantifier and associated data.
14#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
15#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
16#[derive(Debug)]
17pub struct Quantifier {
18    pub kind: QuantKind,
19    pub num_vars: NonMaxU32,
20    pub term: TermIdx,
21    pub vars: Option<VarNames>,
22}
23
24impl Quantifier {
25    pub fn is_lambda(&self) -> bool {
26        matches!(self.kind, QuantKind::Lambda(_))
27    }
28}
29
30/// Represents an ID string of the form `name!id`.
31#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
32#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
33#[derive(Debug, Clone, PartialEq, Eq, Hash)]
34pub enum QuantKind {
35    Lambda(BoxSlice<ProofIdx>),
36    NamedQuant(IString),
37    /// Represents a name string of the form `name!id`
38    UnnamedQuant {
39        name: IString,
40        id: usize,
41    },
42}
43
44impl QuantKind {
45    pub(crate) fn parse(strings: &mut StringTable, value: &str) -> Self {
46        match QuantKindParse::parse(value) {
47            QuantKindParse::Named(name) => Self::NamedQuant(IString(strings.get_or_intern(name))),
48            QuantKindParse::Unnamed { name, id } => Self::UnnamedQuant {
49                name: IString(strings.get_or_intern(name)),
50                id,
51            },
52        }
53    }
54
55    pub fn parse_existing(strings: &StringTable, value: &str) -> Option<Self> {
56        match QuantKindParse::parse(value) {
57            QuantKindParse::Named(name) => Some(Self::NamedQuant(IString(strings.get(name)?))),
58            QuantKindParse::Unnamed { name, id } => Some(Self::UnnamedQuant {
59                name: IString(strings.get(name)?),
60                id,
61            }),
62        }
63    }
64
65    pub fn user_name(&self) -> Option<IString> {
66        match self {
67            Self::NamedQuant(name) => Some(*name),
68            _ => None,
69        }
70    }
71
72    pub fn name<'a>(&self, strings: &'a StringTable) -> Option<Cow<'a, str>> {
73        match self {
74            Self::NamedQuant(name) => Some(Cow::Borrowed(&strings[**name])),
75            Self::UnnamedQuant { name, id } => {
76                Some(Cow::Owned(format!("{}!{id}", &strings[**name])))
77            }
78            Self::Lambda(_) => None,
79        }
80    }
81}
82
83enum QuantKindParse<'a> {
84    Named(&'a str),
85    Unnamed { name: &'a str, id: usize },
86}
87
88impl<'a> QuantKindParse<'a> {
89    /// Splits an ID string into name and ID number (if unnamed).
90    /// 0 is used for identifiers without a number
91    /// (usually for theory-solving 'quantifiers' such as "basic#", "arith#")
92    fn parse(value: &'a str) -> Self {
93        let mut split = value.split('!');
94        let name = split.next().expect(value);
95        split
96            .next()
97            .and_then(|id| id.parse::<usize>().ok())
98            .map_or(Self::Named(value), |id| Self::Unnamed { name, id })
99    }
100}
101
102#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
103#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
104#[derive(Debug)]
105pub enum VarNames {
106    TypeOnly(BoxSlice<IString>),
107    NameAndType(Box<[(IString, IString)]>),
108}
109impl VarNames {
110    pub fn get_type<'a>(
111        strings: &'a StringTable,
112        this: Option<&Self>,
113        idx: usize,
114    ) -> Option<&'a str> {
115        this.as_ref().map(|this| {
116            let ty = match this {
117                Self::TypeOnly(names) => names[idx],
118                Self::NameAndType(names) => names[idx].1,
119            };
120            &strings[*ty]
121        })
122    }
123
124    pub fn is_empty(&self) -> bool {
125        self.len() == 0
126    }
127    pub fn len(&self) -> usize {
128        match self {
129            Self::TypeOnly(names) => names.len(),
130            Self::NameAndType(names) => names.len(),
131        }
132    }
133}
134
135#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
136#[cfg_attr(feature = "mem_dbg", copy_type)]
137#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
138#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
139pub struct QuantPat {
140    pub quant: QuantIdx,
141    pub pat: Option<PatternIdx>,
142}
143
144#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
145#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
146#[derive(Debug, Clone)]
147pub struct QuantPatVec<T>(pub TiVec<QuantIdx, PatVec<T>>);
148
149#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
150#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
151#[derive(Debug, Clone)]
152pub struct PatVec<T> {
153    pub(crate) mbqi: T,
154    pub(crate) pats: TiVec<PatternIdx, T>,
155}
156
157impl<T> Index<QuantPat> for QuantPatVec<T> {
158    type Output = T;
159    fn index(&self, index: QuantPat) -> &Self::Output {
160        &self.0[index.quant][index.pat]
161    }
162}
163
164impl<T> IndexMut<QuantPat> for QuantPatVec<T> {
165    fn index_mut(&mut self, index: QuantPat) -> &mut Self::Output {
166        &mut self.0[index.quant][index.pat]
167    }
168}
169
170impl<T> QuantPatVec<T> {
171    pub fn iter_enumerated(&self) -> impl Iterator<Item = (QuantPat, &T)> {
172        let quants = self.0.iter_enumerated();
173        quants.flat_map(move |(quant, data)| {
174            data.iter_enumerated()
175                .map(move |(pat, data)| (QuantPat { quant, pat }, data))
176        })
177    }
178}
179
180impl<T> Index<Option<PatternIdx>> for PatVec<T> {
181    type Output = T;
182    fn index(&self, index: Option<PatternIdx>) -> &Self::Output {
183        if let Some(pattern) = index {
184            &self.pats[pattern]
185        } else {
186            &self.mbqi
187        }
188    }
189}
190
191impl<T> IndexMut<Option<PatternIdx>> for PatVec<T> {
192    fn index_mut(&mut self, index: Option<PatternIdx>) -> &mut Self::Output {
193        if let Some(pattern) = index {
194            &mut self.pats[pattern]
195        } else {
196            &mut self.mbqi
197        }
198    }
199}
200
201impl<T> PatVec<T> {
202    pub fn iter_enumerated(&self) -> impl Iterator<Item = (Option<PatternIdx>, &T)> {
203        let mbqi = core::iter::once((None, &self.mbqi));
204        let pats = self.pats.iter_enumerated();
205        let pats = pats.map(|(pat, data)| (Some(pat), data));
206        mbqi.chain(pats)
207    }
208}
smt_scope/items/quant.rs

smt_scope/items/
quant.rs
