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

smt_scope/items/
quant.rs
