smtlib_lowlevel/
lexicon.rs

1use crate::parse::{ParseError, Parser, Token};
2
3/// **Numerals.** A `<numeral>` is the digit `0 or a non-empty sequence of
4/// digits not starting with `0`.
5#[derive(Clone, Copy, PartialEq, Eq, Hash)]
6#[cfg_attr(feature = "serde", derive(serde::Serialize))]
7pub struct Numeral<'st> {
8    repr: NumeralRepr<'st>,
9}
10#[derive(Clone, Copy, PartialEq, Eq, Hash)]
11#[cfg_attr(feature = "serde", derive(serde::Serialize))]
12enum NumeralRepr<'st> {
13    Number(u128),
14    String(&'st str),
15}
16impl std::fmt::Debug for Numeral<'_> {
17    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
18        match self.repr {
19            NumeralRepr::Number(n) => f.debug_tuple("Numeral").field(&n).finish(),
20            NumeralRepr::String(s) => f.debug_tuple("Numeral").field(&s).finish(),
21        }
22    }
23}
24#[derive(Debug, thiserror::Error, Clone)]
25pub enum NumeralError {
26    #[error("invalid numeral")]
27    Invalid,
28}
29impl Numeral<'_> {
30    pub const fn from_u128(n: u128) -> Numeral<'static> {
31        Numeral {
32            repr: NumeralRepr::Number(n),
33        }
34    }
35    pub const fn from_usize(n: usize) -> Numeral<'static> {
36        Numeral {
37            repr: NumeralRepr::Number(n as _),
38        }
39    }
40}
41impl<'st> Numeral<'st> {
42    pub fn try_from_str(s: &'st str) -> Result<Numeral<'st>, NumeralError> {
43        if s == "0" {
44            Ok(Numeral {
45                repr: NumeralRepr::Number(0),
46            })
47        } else if s.chars().all(|c| c.is_ascii_digit()) {
48            Ok(Self::from_validated_str(s))
49        } else {
50            Err(NumeralError::Invalid)
51        }
52    }
53    fn from_validated_str(s: &'st str) -> Self {
54        match s.parse() {
55            Ok(n) => Self {
56                repr: NumeralRepr::Number(n),
57            },
58            Err(_) => Self {
59                repr: NumeralRepr::String(s),
60            },
61        }
62    }
63    pub fn into_u128(self) -> Result<u128, &'st str> {
64        match self.repr {
65            NumeralRepr::Number(n) => Ok(n),
66            NumeralRepr::String(s) => Err(s),
67        }
68    }
69}
70
71impl std::fmt::Display for Numeral<'_> {
72    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
73        match self.repr {
74            NumeralRepr::Number(n) => write!(f, "{}", n),
75            NumeralRepr::String(s) => write!(f, "{}", s),
76        }
77    }
78}
79impl<'st> SmtlibParse<'st> for Numeral<'st> {
80    type Output = Self;
81    fn is_start_of(offset: usize, tokens: &mut Parser<'st, '_>) -> bool {
82        tokens.nth(offset) == Token::Numeral
83    }
84    fn parse(tokens: &mut Parser<'st, '_>) -> Result<Self, ParseError> {
85        let token = tokens.expect_st(Token::Numeral)?;
86        Ok(Numeral::from_validated_str(token))
87    }
88}
89impl From<u128> for Numeral<'_> {
90    fn from(value: u128) -> Self {
91        Numeral::from_u128(value)
92    }
93}
94#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
95#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
96pub struct Decimal<'st>(pub &'st str);
97impl std::fmt::Display for Decimal<'_> {
98    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
99        write!(f, "{}", self.0)
100    }
101}
102impl<'st> SmtlibParse<'st> for Decimal<'st> {
103    type Output = Self;
104    fn is_start_of(offset: usize, tokens: &mut Parser<'st, '_>) -> bool {
105        tokens.nth(offset) == Token::Decimal
106    }
107    fn parse(tokens: &mut Parser<'st, '_>) -> Result<Self, ParseError> {
108        Ok(Self(tokens.expect_st(Token::Decimal)?))
109    }
110}
111#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
112#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
113pub struct Symbol<'st>(pub &'st str);
114impl std::fmt::Display for Symbol<'_> {
115    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
116        write!(f, "{}", self.0)
117    }
118}
119impl<'st> SmtlibParse<'st> for Symbol<'st> {
120    type Output = Self;
121    fn is_start_of(offset: usize, tokens: &mut Parser<'st, '_>) -> bool {
122        tokens.nth(offset) == Token::Symbol
123    }
124    fn parse(tokens: &mut Parser<'st, '_>) -> Result<Self, ParseError> {
125        Ok(Self(tokens.expect_st(Token::Symbol)?))
126    }
127}
128#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
129#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
130pub struct Hexadecimal<'st>(pub &'st str);
131impl std::fmt::Display for Hexadecimal<'_> {
132    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
133        write!(f, "{}", self.0)
134    }
135}
136impl<'st> SmtlibParse<'st> for Hexadecimal<'st> {
137    type Output = Self;
138    fn is_start_of(offset: usize, tokens: &mut Parser<'st, '_>) -> bool {
139        tokens.nth(offset) == Token::Hexadecimal
140    }
141    fn parse(tokens: &mut Parser<'st, '_>) -> Result<Self, ParseError> {
142        Ok(Self(tokens.expect_st(Token::Hexadecimal)?))
143    }
144}
145impl Hexadecimal<'_> {
146    pub fn parse(&self) -> Result<i64, std::num::ParseIntError> {
147        i64::from_str_radix(&self.0[2..], 16)
148    }
149}
150#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
151#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
152pub struct Binary<'st>(pub &'st str);
153impl std::fmt::Display for Binary<'_> {
154    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
155        write!(f, "{}", self.0)
156    }
157}
158impl<'st> SmtlibParse<'st> for Binary<'st> {
159    type Output = Self;
160    fn is_start_of(offset: usize, tokens: &mut Parser<'st, '_>) -> bool {
161        tokens.nth(offset) == Token::Binary
162    }
163    fn parse(tokens: &mut Parser<'st, '_>) -> Result<Self, ParseError> {
164        Ok(Self(tokens.expect_st(Token::Binary)?))
165    }
166}
167impl Binary<'_> {
168    pub fn parse(&self) -> Result<i64, std::num::ParseIntError> {
169        i64::from_str_radix(&self.0[2..], 2)
170    }
171}
172#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
173#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
174pub struct Reserved<'st>(pub &'st str);
175impl std::fmt::Display for Reserved<'_> {
176    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
177        write!(f, "{}", self.0)
178    }
179}
180impl<'st> SmtlibParse<'st> for Reserved<'st> {
181    type Output = Self;
182    fn is_start_of(offset: usize, tokens: &mut Parser<'st, '_>) -> bool {
183        tokens.nth(offset) == Token::Reserved
184    }
185    fn parse(tokens: &mut Parser<'st, '_>) -> Result<Self, ParseError> {
186        Ok(Self(tokens.expect_st(Token::Reserved)?))
187    }
188}
189#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
190#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
191pub struct Keyword<'st>(pub &'st str);
192impl std::fmt::Display for Keyword<'_> {
193    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
194        write!(f, "{}", self.0)
195    }
196}
197impl<'st> SmtlibParse<'st> for Keyword<'st> {
198    type Output = Self;
199    fn is_start_of(offset: usize, tokens: &mut Parser<'st, '_>) -> bool {
200        tokens.nth(offset) == Token::Keyword
201    }
202    fn parse(tokens: &mut Parser<'st, '_>) -> Result<Self, ParseError> {
203        Ok(Self(tokens.expect_st(Token::Keyword)?))
204    }
205}
206
207pub type BValue = bool;
208
209pub(crate) trait SmtlibParse<'st>: Sized {
210    type Output: Clone;
211
212    fn is_start_of(offset: usize, tokens: &mut Parser<'st, '_>) -> bool;
213    fn parse(tokens: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError>;
214}
215
216impl<'st> SmtlibParse<'st> for String {
217    type Output = &'st str;
218    fn is_start_of(offset: usize, tokens: &mut Parser<'st, '_>) -> bool {
219        tokens.nth(offset) == Token::String
220    }
221    fn parse(tokens: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
222        tokens.expect_st(Token::String)
223    }
224}
225impl<'st> SmtlibParse<'st> for &'st str {
226    type Output = Self;
227    fn is_start_of(offset: usize, tokens: &mut Parser<'st, '_>) -> bool {
228        tokens.nth(offset) == Token::String
229    }
230
231    fn parse(tokens: &mut Parser<'st, '_>) -> Result<Self, ParseError> {
232        tokens.expect_st(Token::String)
233    }
234}
235impl<'st> SmtlibParse<'st> for bool {
236    type Output = Self;
237    fn is_start_of(_offset: usize, _tokens: &mut Parser<'st, '_>) -> bool {
238        todo!()
239    }
240
241    fn parse(_tokens: &mut Parser<'st, '_>) -> Result<Self, ParseError> {
242        todo!()
243    }
244}
smtlib_lowlevel/lexicon.rs

smtlib_lowlevel/
lexicon.rs
