Skip to main content

smtlib_lowlevel/
ast.rs

1//! Generated by `cargo xtask ast`, do not edit by hand.
2#![allow(clippy::uninlined_format_args)]
3
4use crate::parse::{Token, Parser, ParseError};
5use crate::storage::Storage;
6use itertools::Itertools;
7use crate::lexicon::*;
8#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
9#[cfg_attr(feature = "serde", derive(serde::Serialize))]
10pub enum Attribute<'st> {
11    /// `<keyword>`
12    Keyword(Keyword<'st>),
13    /// `<keyword> <attribute_value>`
14    WithValue(Keyword<'st>, AttributeValue<'st>),
15}
16impl std::fmt::Display for Attribute<'_> {
17    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
18        match self {
19            Self::Keyword(m0) => write!(f, "{}", m0),
20            Self::WithValue(m0, m1) => write!(f, "{} {}", m0, m1),
21        }
22    }
23}
24impl<'st> Attribute<'st> {
25    pub fn parse(st: &'st Storage, src: &str) -> Result<Attribute<'st>, ParseError> {
26        <Attribute<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
27    }
28}
29impl<'st> SmtlibParse<'st> for Attribute<'st> {
30    type Output = Attribute<'st>;
31    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
32        (Keyword::is_start_of(offset, p) && AttributeValue::is_start_of(offset + 1, p))
33            || (Keyword::is_start_of(offset, p))
34    }
35    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
36        let offset = 0;
37        if Keyword::is_start_of(offset, p) && AttributeValue::is_start_of(offset + 1, p)
38        {
39            let m0 = <Keyword<'st> as SmtlibParse<'st>>::parse(p)?;
40            let m1 = <AttributeValue<'st> as SmtlibParse<'st>>::parse(p)?;
41            #[allow(clippy::useless_conversion)]
42            return Ok(Self::WithValue(m0.into(), m1.into()));
43        }
44        if Keyword::is_start_of(offset, p) {
45            let m0 = <Keyword<'st> as SmtlibParse<'st>>::parse(p)?;
46            #[allow(clippy::useless_conversion)] return Ok(Self::Keyword(m0.into()));
47        }
48        Err(p.stuck("Attribute"))
49    }
50}
51#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
52#[cfg_attr(feature = "serde", derive(serde::Serialize))]
53pub enum AttributeValue<'st> {
54    /// `(<s_expr>)`
55    Expr(SExpr<'st>),
56    /// `<spec_constant>`
57    SpecConstant(SpecConstant<'st>),
58    /// `<symbol>`
59    Symbol(Symbol<'st>),
60}
61impl std::fmt::Display for AttributeValue<'_> {
62    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
63        match self {
64            Self::Expr(m0) => write!(f, "({})", m0),
65            Self::SpecConstant(m0) => write!(f, "{}", m0),
66            Self::Symbol(m0) => write!(f, "{}", m0),
67        }
68    }
69}
70impl<'st> AttributeValue<'st> {
71    pub fn parse(
72        st: &'st Storage,
73        src: &str,
74    ) -> Result<AttributeValue<'st>, ParseError> {
75        <AttributeValue<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
76    }
77}
78impl<'st> SmtlibParse<'st> for AttributeValue<'st> {
79    type Output = AttributeValue<'st>;
80    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
81        (p.nth(offset) == Token::LParen) || (Symbol::is_start_of(offset, p))
82            || (SpecConstant::is_start_of(offset, p))
83    }
84    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
85        let offset = 0;
86        if p.nth(offset) == Token::LParen {
87            p.expect(Token::LParen)?;
88            let m0 = <SExpr<'st> as SmtlibParse<'st>>::parse(p)?;
89            p.expect(Token::RParen)?;
90            #[allow(clippy::useless_conversion)] return Ok(Self::Expr(m0.into()));
91        }
92        if Symbol::is_start_of(offset, p) {
93            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
94            #[allow(clippy::useless_conversion)] return Ok(Self::Symbol(m0.into()));
95        }
96        if SpecConstant::is_start_of(offset, p) {
97            let m0 = <SpecConstant<'st> as SmtlibParse<'st>>::parse(p)?;
98            #[allow(clippy::useless_conversion)]
99            return Ok(Self::SpecConstant(m0.into()));
100        }
101        Err(p.stuck("AttributeValue"))
102    }
103}
104#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
105#[cfg_attr(feature = "serde", derive(serde::Serialize))]
106pub enum CheckSatResponse {
107    /// `sat`
108    Sat,
109    /// `unknown`
110    Unknown,
111    /// `unsat`
112    Unsat,
113}
114impl std::fmt::Display for CheckSatResponse {
115    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
116        match self {
117            Self::Sat => write!(f, "sat"),
118            Self::Unknown => write!(f, "unknown"),
119            Self::Unsat => write!(f, "unsat"),
120        }
121    }
122}
123impl<'st> CheckSatResponse {
124    pub fn parse(st: &'st Storage, src: &str) -> Result<CheckSatResponse, ParseError> {
125        <CheckSatResponse as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
126    }
127}
128impl<'st> SmtlibParse<'st> for CheckSatResponse {
129    type Output = CheckSatResponse;
130    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
131        (p.nth_matches(offset, Token::Symbol, "unsat"))
132            || (p.nth_matches(offset, Token::Symbol, "unknown"))
133            || (p.nth_matches(offset, Token::Symbol, "sat"))
134    }
135    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
136        let offset = 0;
137        if p.nth_matches(offset, Token::Symbol, "unsat") {
138            p.expect_matches(Token::Symbol, "unsat")?;
139            #[allow(clippy::useless_conversion)] return Ok(Self::Unsat);
140        }
141        if p.nth_matches(offset, Token::Symbol, "unknown") {
142            p.expect_matches(Token::Symbol, "unknown")?;
143            #[allow(clippy::useless_conversion)] return Ok(Self::Unknown);
144        }
145        if p.nth_matches(offset, Token::Symbol, "sat") {
146            p.expect_matches(Token::Symbol, "sat")?;
147            #[allow(clippy::useless_conversion)] return Ok(Self::Sat);
148        }
149        Err(p.stuck("CheckSatResponse"))
150    }
151}
152#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
153#[cfg_attr(feature = "serde", derive(serde::Serialize))]
154pub enum Command<'st> {
155    /// `(assert <term>)`
156    Assert(&'st Term<'st>),
157    /// `(assert-soft <term> <optimization_attribute>*)`
158    AssertSoft(&'st Term<'st>, &'st [OptimizationAttribute<'st>]),
159    /// `(check-sat)`
160    CheckSat,
161    /// `(check-sat-assuming (<prop_literal>*))`
162    CheckSatAssuming(&'st [PropLiteral<'st>]),
163    /// `(declare-const <symbol> <sort>)`
164    DeclareConst(Symbol<'st>, Sort<'st>),
165    /// `(declare-datatype <symbol> <datatype_dec>)`
166    DeclareDatatype(Symbol<'st>, DatatypeDec<'st>),
167    /// `(declare-datatypes (<sort_dec>n+1) (<datatype_dec>n+1))`
168    DeclareDatatypes(&'st [SortDec<'st>], &'st [DatatypeDec<'st>]),
169    /// `(declare-fun <symbol> (<sort>*) <sort>)`
170    DeclareFun(Symbol<'st>, &'st [Sort<'st>], Sort<'st>),
171    /// `(declare-sort <symbol> <numeral>)`
172    DeclareSort(Symbol<'st>, Numeral<'st>),
173    /// `(define-fun <function_def>)`
174    DefineFun(FunctionDef<'st>),
175    /// `(define-fun-rec <function_def>)`
176    DefineFunRec(FunctionDef<'st>),
177    /// `(define-funs-rec (<function_dec>n+1) (<term>n+1))`
178    DefineFunsRec(&'st [FunctionDec<'st>], &'st [&'st Term<'st>]),
179    /// `(define-sort <symbol> (<symbol>*) <sort>)`
180    DefineSort(Symbol<'st>, &'st [Symbol<'st>], Sort<'st>),
181    /// `(echo <string>)`
182    Echo(&'st str),
183    /// `(eval <term>)`
184    Eval(&'st Term<'st>),
185    /// `(exit)`
186    Exit,
187    /// `(get-assertions)`
188    GetAssertions,
189    /// `(get-assignment)`
190    GetAssignment,
191    /// `(get-info <info_flag>)`
192    GetInfo(InfoFlag<'st>),
193    /// `(get-model)`
194    GetModel,
195    /// `(get-option <keyword>)`
196    GetOption(Keyword<'st>),
197    /// `(get-proof)`
198    GetProof,
199    /// `(get-unsat-assumptions)`
200    GetUnsatAssumptions,
201    /// `(get-unsat-core)`
202    GetUnsatCore,
203    /// `(get-value (<term>+))`
204    GetValue(&'st [&'st Term<'st>]),
205    /// `(maximize <term>)`
206    Maximize(&'st Term<'st>),
207    /// `(minimize <term>)`
208    Minimize(&'st Term<'st>),
209    /// `(pop <numeral>)`
210    Pop(Numeral<'st>),
211    /// `(push <numeral>)`
212    Push(Numeral<'st>),
213    /// `(reset)`
214    Reset,
215    /// `(reset-assertions)`
216    ResetAssertions,
217    /// `(set-info <attribute>)`
218    SetInfo(Attribute<'st>),
219    /// `(set-logic <symbol>)`
220    SetLogic(Symbol<'st>),
221    /// `(set-option <option>)`
222    SetOption(Option<'st>),
223    /// `(simplify <term>)`
224    Simplify(&'st Term<'st>),
225}
226impl std::fmt::Display for Command<'_> {
227    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
228        match self {
229            Self::Assert(m0) => write!(f, "(assert {})", m0),
230            Self::AssertSoft(m0, m1) => {
231                write!(f, "(assert-soft {} {})", m0, m1.iter().format(" "))
232            }
233            Self::CheckSat => write!(f, "(check-sat)"),
234            Self::CheckSatAssuming(m0) => {
235                write!(f, "(check-sat-assuming ({}))", m0.iter().format(" "))
236            }
237            Self::DeclareConst(m0, m1) => write!(f, "(declare-const {} {})", m0, m1),
238            Self::DeclareDatatype(m0, m1) => {
239                write!(f, "(declare-datatype {} {})", m0, m1)
240            }
241            Self::DeclareDatatypes(m0, m1) => {
242                write!(
243                    f, "(declare-datatypes ({}) ({}))", m0.iter().format(" "), m1.iter()
244                    .format(" ")
245                )
246            }
247            Self::DeclareFun(m0, m1, m2) => {
248                write!(f, "(declare-fun {} ({}) {})", m0, m1.iter().format(" "), m2)
249            }
250            Self::DeclareSort(m0, m1) => write!(f, "(declare-sort {} {})", m0, m1),
251            Self::DefineFun(m0) => write!(f, "(define-fun {})", m0),
252            Self::DefineFunRec(m0) => write!(f, "(define-fun-rec {})", m0),
253            Self::DefineFunsRec(m0, m1) => {
254                write!(
255                    f, "(define-funs-rec ({}) ({}))", m0.iter().format(" "), m1.iter()
256                    .format(" ")
257                )
258            }
259            Self::DefineSort(m0, m1, m2) => {
260                write!(f, "(define-sort {} ({}) {})", m0, m1.iter().format(" "), m2)
261            }
262            Self::Echo(m0) => write!(f, "(echo {})", m0),
263            Self::Eval(m0) => write!(f, "(eval {})", m0),
264            Self::Exit => write!(f, "(exit)"),
265            Self::GetAssertions => write!(f, "(get-assertions)"),
266            Self::GetAssignment => write!(f, "(get-assignment)"),
267            Self::GetInfo(m0) => write!(f, "(get-info {})", m0),
268            Self::GetModel => write!(f, "(get-model)"),
269            Self::GetOption(m0) => write!(f, "(get-option {})", m0),
270            Self::GetProof => write!(f, "(get-proof)"),
271            Self::GetUnsatAssumptions => write!(f, "(get-unsat-assumptions)"),
272            Self::GetUnsatCore => write!(f, "(get-unsat-core)"),
273            Self::GetValue(m0) => write!(f, "(get-value ({}))", m0.iter().format(" ")),
274            Self::Maximize(m0) => write!(f, "(maximize {})", m0),
275            Self::Minimize(m0) => write!(f, "(minimize {})", m0),
276            Self::Pop(m0) => write!(f, "(pop {})", m0),
277            Self::Push(m0) => write!(f, "(push {})", m0),
278            Self::Reset => write!(f, "(reset)"),
279            Self::ResetAssertions => write!(f, "(reset-assertions)"),
280            Self::SetInfo(m0) => write!(f, "(set-info {})", m0),
281            Self::SetLogic(m0) => write!(f, "(set-logic {})", m0),
282            Self::SetOption(m0) => write!(f, "(set-option {})", m0),
283            Self::Simplify(m0) => write!(f, "(simplify {})", m0),
284        }
285    }
286}
287impl<'st> Command<'st> {
288    pub fn parse(st: &'st Storage, src: &str) -> Result<Command<'st>, ParseError> {
289        <Command<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
290    }
291}
292impl<'st> SmtlibParse<'st> for Command<'st> {
293    type Output = Command<'st>;
294    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
295        (p.nth(offset) == Token::LParen
296            && p.nth_matches(offset + 1, Token::Symbol, "define-funs-rec")
297            && p.nth(offset + 2) == Token::LParen)
298            || (p.nth(offset) == Token::LParen
299                && p.nth_matches(offset + 1, Token::Reserved, "declare-datatypes")
300                && p.nth(offset + 2) == Token::LParen)
301            || (p.nth(offset) == Token::LParen
302                && p.nth_matches(offset + 1, Token::Reserved, "get-value")
303                && p.nth(offset + 2) == Token::LParen)
304            || (p.nth(offset) == Token::LParen
305                && p.nth_matches(offset + 1, Token::Reserved, "define-sort"))
306            || (p.nth(offset) == Token::LParen
307                && p.nth_matches(offset + 1, Token::Reserved, "declare-fun"))
308            || (p.nth(offset) == Token::LParen
309                && p.nth_matches(offset + 1, Token::Reserved, "check-sat-assuming")
310                && p.nth(offset + 2) == Token::LParen)
311            || (p.nth(offset) == Token::LParen
312                && p.nth_matches(offset + 1, Token::Symbol, "simplify"))
313            || (p.nth(offset) == Token::LParen
314                && p.nth_matches(offset + 1, Token::Reserved, "set-option"))
315            || (p.nth(offset) == Token::LParen
316                && p.nth_matches(offset + 1, Token::Reserved, "set-logic"))
317            || (p.nth(offset) == Token::LParen
318                && p.nth_matches(offset + 1, Token::Reserved, "set-info"))
319            || (p.nth(offset) == Token::LParen
320                && p.nth_matches(offset + 1, Token::Reserved, "reset-assertions")
321                && p.nth(offset + 2) == Token::RParen)
322            || (p.nth(offset) == Token::LParen
323                && p.nth_matches(offset + 1, Token::Reserved, "reset")
324                && p.nth(offset + 2) == Token::RParen)
325            || (p.nth(offset) == Token::LParen
326                && p.nth_matches(offset + 1, Token::Reserved, "push"))
327            || (p.nth(offset) == Token::LParen
328                && p.nth_matches(offset + 1, Token::Reserved, "pop"))
329            || (p.nth(offset) == Token::LParen
330                && p.nth_matches(offset + 1, Token::Symbol, "minimize"))
331            || (p.nth(offset) == Token::LParen
332                && p.nth_matches(offset + 1, Token::Symbol, "maximize"))
333            || (p.nth(offset) == Token::LParen
334                && p.nth_matches(offset + 1, Token::Reserved, "get-unsat-core")
335                && p.nth(offset + 2) == Token::RParen)
336            || (p.nth(offset) == Token::LParen
337                && p.nth_matches(offset + 1, Token::Reserved, "get-unsat-assumptions")
338                && p.nth(offset + 2) == Token::RParen)
339            || (p.nth(offset) == Token::LParen
340                && p.nth_matches(offset + 1, Token::Reserved, "get-proof")
341                && p.nth(offset + 2) == Token::RParen)
342            || (p.nth(offset) == Token::LParen
343                && p.nth_matches(offset + 1, Token::Reserved, "get-option"))
344            || (p.nth(offset) == Token::LParen
345                && p.nth_matches(offset + 1, Token::Reserved, "get-model")
346                && p.nth(offset + 2) == Token::RParen)
347            || (p.nth(offset) == Token::LParen
348                && p.nth_matches(offset + 1, Token::Reserved, "get-info"))
349            || (p.nth(offset) == Token::LParen
350                && p.nth_matches(offset + 1, Token::Reserved, "get-assignment")
351                && p.nth(offset + 2) == Token::RParen)
352            || (p.nth(offset) == Token::LParen
353                && p.nth_matches(offset + 1, Token::Reserved, "get-assertions")
354                && p.nth(offset + 2) == Token::RParen)
355            || (p.nth(offset) == Token::LParen
356                && p.nth_matches(offset + 1, Token::Reserved, "exit")
357                && p.nth(offset + 2) == Token::RParen)
358            || (p.nth(offset) == Token::LParen
359                && p.nth_matches(offset + 1, Token::Symbol, "eval"))
360            || (p.nth(offset) == Token::LParen
361                && p.nth_matches(offset + 1, Token::Reserved, "echo"))
362            || (p.nth(offset) == Token::LParen
363                && p.nth_matches(offset + 1, Token::Reserved, "define-fun-rec"))
364            || (p.nth(offset) == Token::LParen
365                && p.nth_matches(offset + 1, Token::Reserved, "define-fun"))
366            || (p.nth(offset) == Token::LParen
367                && p.nth_matches(offset + 1, Token::Reserved, "declare-sort"))
368            || (p.nth(offset) == Token::LParen
369                && p.nth_matches(offset + 1, Token::Reserved, "declare-datatype"))
370            || (p.nth(offset) == Token::LParen
371                && p.nth_matches(offset + 1, Token::Reserved, "declare-const"))
372            || (p.nth(offset) == Token::LParen
373                && p.nth_matches(offset + 1, Token::Reserved, "check-sat")
374                && p.nth(offset + 2) == Token::RParen)
375            || (p.nth(offset) == Token::LParen
376                && p.nth_matches(offset + 1, Token::Symbol, "assert-soft"))
377            || (p.nth(offset) == Token::LParen
378                && p.nth_matches(offset + 1, Token::Reserved, "assert"))
379    }
380    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
381        let offset = 0;
382        if p.nth(offset) == Token::LParen
383            && p.nth_matches(offset + 1, Token::Symbol, "define-funs-rec")
384            && p.nth(offset + 2) == Token::LParen
385        {
386            p.expect(Token::LParen)?;
387            p.expect_matches(Token::Symbol, "define-funs-rec")?;
388            p.expect(Token::LParen)?;
389            let m0 = p.n_plus_one::<FunctionDec<'st>>()?;
390            p.expect(Token::RParen)?;
391            p.expect(Token::LParen)?;
392            let m1 = p.n_plus_one::<Term<'st>>()?;
393            p.expect(Token::RParen)?;
394            p.expect(Token::RParen)?;
395            #[allow(clippy::useless_conversion)]
396            return Ok(Self::DefineFunsRec(m0.into(), m1.into()));
397        }
398        if p.nth(offset) == Token::LParen
399            && p.nth_matches(offset + 1, Token::Reserved, "declare-datatypes")
400            && p.nth(offset + 2) == Token::LParen
401        {
402            p.expect(Token::LParen)?;
403            p.expect_matches(Token::Reserved, "declare-datatypes")?;
404            p.expect(Token::LParen)?;
405            let m0 = p.n_plus_one::<SortDec<'st>>()?;
406            p.expect(Token::RParen)?;
407            p.expect(Token::LParen)?;
408            let m1 = p.n_plus_one::<DatatypeDec<'st>>()?;
409            p.expect(Token::RParen)?;
410            p.expect(Token::RParen)?;
411            #[allow(clippy::useless_conversion)]
412            return Ok(Self::DeclareDatatypes(m0.into(), m1.into()));
413        }
414        if p.nth(offset) == Token::LParen
415            && p.nth_matches(offset + 1, Token::Reserved, "get-value")
416            && p.nth(offset + 2) == Token::LParen
417        {
418            p.expect(Token::LParen)?;
419            p.expect_matches(Token::Reserved, "get-value")?;
420            p.expect(Token::LParen)?;
421            let m0 = p.non_zero::<Term<'st>>()?;
422            p.expect(Token::RParen)?;
423            p.expect(Token::RParen)?;
424            #[allow(clippy::useless_conversion)] return Ok(Self::GetValue(m0.into()));
425        }
426        if p.nth(offset) == Token::LParen
427            && p.nth_matches(offset + 1, Token::Reserved, "define-sort")
428        {
429            p.expect(Token::LParen)?;
430            p.expect_matches(Token::Reserved, "define-sort")?;
431            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
432            p.expect(Token::LParen)?;
433            let m1 = p.any::<Symbol<'st>>()?;
434            p.expect(Token::RParen)?;
435            let m2 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
436            p.expect(Token::RParen)?;
437            #[allow(clippy::useless_conversion)]
438            return Ok(Self::DefineSort(m0.into(), m1.into(), m2.into()));
439        }
440        if p.nth(offset) == Token::LParen
441            && p.nth_matches(offset + 1, Token::Reserved, "declare-fun")
442        {
443            p.expect(Token::LParen)?;
444            p.expect_matches(Token::Reserved, "declare-fun")?;
445            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
446            p.expect(Token::LParen)?;
447            let m1 = p.any::<Sort<'st>>()?;
448            p.expect(Token::RParen)?;
449            let m2 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
450            p.expect(Token::RParen)?;
451            #[allow(clippy::useless_conversion)]
452            return Ok(Self::DeclareFun(m0.into(), m1.into(), m2.into()));
453        }
454        if p.nth(offset) == Token::LParen
455            && p.nth_matches(offset + 1, Token::Reserved, "check-sat-assuming")
456            && p.nth(offset + 2) == Token::LParen
457        {
458            p.expect(Token::LParen)?;
459            p.expect_matches(Token::Reserved, "check-sat-assuming")?;
460            p.expect(Token::LParen)?;
461            let m0 = p.any::<PropLiteral<'st>>()?;
462            p.expect(Token::RParen)?;
463            p.expect(Token::RParen)?;
464            #[allow(clippy::useless_conversion)]
465            return Ok(Self::CheckSatAssuming(m0.into()));
466        }
467        if p.nth(offset) == Token::LParen
468            && p.nth_matches(offset + 1, Token::Symbol, "simplify")
469        {
470            p.expect(Token::LParen)?;
471            p.expect_matches(Token::Symbol, "simplify")?;
472            let m0 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
473            p.expect(Token::RParen)?;
474            #[allow(clippy::useless_conversion)] return Ok(Self::Simplify(m0.into()));
475        }
476        if p.nth(offset) == Token::LParen
477            && p.nth_matches(offset + 1, Token::Reserved, "set-option")
478        {
479            p.expect(Token::LParen)?;
480            p.expect_matches(Token::Reserved, "set-option")?;
481            let m0 = <Option<'st> as SmtlibParse<'st>>::parse(p)?;
482            p.expect(Token::RParen)?;
483            #[allow(clippy::useless_conversion)] return Ok(Self::SetOption(m0.into()));
484        }
485        if p.nth(offset) == Token::LParen
486            && p.nth_matches(offset + 1, Token::Reserved, "set-logic")
487        {
488            p.expect(Token::LParen)?;
489            p.expect_matches(Token::Reserved, "set-logic")?;
490            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
491            p.expect(Token::RParen)?;
492            #[allow(clippy::useless_conversion)] return Ok(Self::SetLogic(m0.into()));
493        }
494        if p.nth(offset) == Token::LParen
495            && p.nth_matches(offset + 1, Token::Reserved, "set-info")
496        {
497            p.expect(Token::LParen)?;
498            p.expect_matches(Token::Reserved, "set-info")?;
499            let m0 = <Attribute<'st> as SmtlibParse<'st>>::parse(p)?;
500            p.expect(Token::RParen)?;
501            #[allow(clippy::useless_conversion)] return Ok(Self::SetInfo(m0.into()));
502        }
503        if p.nth(offset) == Token::LParen
504            && p.nth_matches(offset + 1, Token::Reserved, "reset-assertions")
505            && p.nth(offset + 2) == Token::RParen
506        {
507            p.expect(Token::LParen)?;
508            p.expect_matches(Token::Reserved, "reset-assertions")?;
509            p.expect(Token::RParen)?;
510            #[allow(clippy::useless_conversion)] return Ok(Self::ResetAssertions);
511        }
512        if p.nth(offset) == Token::LParen
513            && p.nth_matches(offset + 1, Token::Reserved, "reset")
514            && p.nth(offset + 2) == Token::RParen
515        {
516            p.expect(Token::LParen)?;
517            p.expect_matches(Token::Reserved, "reset")?;
518            p.expect(Token::RParen)?;
519            #[allow(clippy::useless_conversion)] return Ok(Self::Reset);
520        }
521        if p.nth(offset) == Token::LParen
522            && p.nth_matches(offset + 1, Token::Reserved, "push")
523        {
524            p.expect(Token::LParen)?;
525            p.expect_matches(Token::Reserved, "push")?;
526            let m0 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
527            p.expect(Token::RParen)?;
528            #[allow(clippy::useless_conversion)] return Ok(Self::Push(m0.into()));
529        }
530        if p.nth(offset) == Token::LParen
531            && p.nth_matches(offset + 1, Token::Reserved, "pop")
532        {
533            p.expect(Token::LParen)?;
534            p.expect_matches(Token::Reserved, "pop")?;
535            let m0 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
536            p.expect(Token::RParen)?;
537            #[allow(clippy::useless_conversion)] return Ok(Self::Pop(m0.into()));
538        }
539        if p.nth(offset) == Token::LParen
540            && p.nth_matches(offset + 1, Token::Symbol, "minimize")
541        {
542            p.expect(Token::LParen)?;
543            p.expect_matches(Token::Symbol, "minimize")?;
544            let m0 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
545            p.expect(Token::RParen)?;
546            #[allow(clippy::useless_conversion)] return Ok(Self::Minimize(m0.into()));
547        }
548        if p.nth(offset) == Token::LParen
549            && p.nth_matches(offset + 1, Token::Symbol, "maximize")
550        {
551            p.expect(Token::LParen)?;
552            p.expect_matches(Token::Symbol, "maximize")?;
553            let m0 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
554            p.expect(Token::RParen)?;
555            #[allow(clippy::useless_conversion)] return Ok(Self::Maximize(m0.into()));
556        }
557        if p.nth(offset) == Token::LParen
558            && p.nth_matches(offset + 1, Token::Reserved, "get-unsat-core")
559            && p.nth(offset + 2) == Token::RParen
560        {
561            p.expect(Token::LParen)?;
562            p.expect_matches(Token::Reserved, "get-unsat-core")?;
563            p.expect(Token::RParen)?;
564            #[allow(clippy::useless_conversion)] return Ok(Self::GetUnsatCore);
565        }
566        if p.nth(offset) == Token::LParen
567            && p.nth_matches(offset + 1, Token::Reserved, "get-unsat-assumptions")
568            && p.nth(offset + 2) == Token::RParen
569        {
570            p.expect(Token::LParen)?;
571            p.expect_matches(Token::Reserved, "get-unsat-assumptions")?;
572            p.expect(Token::RParen)?;
573            #[allow(clippy::useless_conversion)] return Ok(Self::GetUnsatAssumptions);
574        }
575        if p.nth(offset) == Token::LParen
576            && p.nth_matches(offset + 1, Token::Reserved, "get-proof")
577            && p.nth(offset + 2) == Token::RParen
578        {
579            p.expect(Token::LParen)?;
580            p.expect_matches(Token::Reserved, "get-proof")?;
581            p.expect(Token::RParen)?;
582            #[allow(clippy::useless_conversion)] return Ok(Self::GetProof);
583        }
584        if p.nth(offset) == Token::LParen
585            && p.nth_matches(offset + 1, Token::Reserved, "get-option")
586        {
587            p.expect(Token::LParen)?;
588            p.expect_matches(Token::Reserved, "get-option")?;
589            let m0 = <Keyword<'st> as SmtlibParse<'st>>::parse(p)?;
590            p.expect(Token::RParen)?;
591            #[allow(clippy::useless_conversion)] return Ok(Self::GetOption(m0.into()));
592        }
593        if p.nth(offset) == Token::LParen
594            && p.nth_matches(offset + 1, Token::Reserved, "get-model")
595            && p.nth(offset + 2) == Token::RParen
596        {
597            p.expect(Token::LParen)?;
598            p.expect_matches(Token::Reserved, "get-model")?;
599            p.expect(Token::RParen)?;
600            #[allow(clippy::useless_conversion)] return Ok(Self::GetModel);
601        }
602        if p.nth(offset) == Token::LParen
603            && p.nth_matches(offset + 1, Token::Reserved, "get-info")
604        {
605            p.expect(Token::LParen)?;
606            p.expect_matches(Token::Reserved, "get-info")?;
607            let m0 = <InfoFlag<'st> as SmtlibParse<'st>>::parse(p)?;
608            p.expect(Token::RParen)?;
609            #[allow(clippy::useless_conversion)] return Ok(Self::GetInfo(m0.into()));
610        }
611        if p.nth(offset) == Token::LParen
612            && p.nth_matches(offset + 1, Token::Reserved, "get-assignment")
613            && p.nth(offset + 2) == Token::RParen
614        {
615            p.expect(Token::LParen)?;
616            p.expect_matches(Token::Reserved, "get-assignment")?;
617            p.expect(Token::RParen)?;
618            #[allow(clippy::useless_conversion)] return Ok(Self::GetAssignment);
619        }
620        if p.nth(offset) == Token::LParen
621            && p.nth_matches(offset + 1, Token::Reserved, "get-assertions")
622            && p.nth(offset + 2) == Token::RParen
623        {
624            p.expect(Token::LParen)?;
625            p.expect_matches(Token::Reserved, "get-assertions")?;
626            p.expect(Token::RParen)?;
627            #[allow(clippy::useless_conversion)] return Ok(Self::GetAssertions);
628        }
629        if p.nth(offset) == Token::LParen
630            && p.nth_matches(offset + 1, Token::Reserved, "exit")
631            && p.nth(offset + 2) == Token::RParen
632        {
633            p.expect(Token::LParen)?;
634            p.expect_matches(Token::Reserved, "exit")?;
635            p.expect(Token::RParen)?;
636            #[allow(clippy::useless_conversion)] return Ok(Self::Exit);
637        }
638        if p.nth(offset) == Token::LParen
639            && p.nth_matches(offset + 1, Token::Symbol, "eval")
640        {
641            p.expect(Token::LParen)?;
642            p.expect_matches(Token::Symbol, "eval")?;
643            let m0 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
644            p.expect(Token::RParen)?;
645            #[allow(clippy::useless_conversion)] return Ok(Self::Eval(m0.into()));
646        }
647        if p.nth(offset) == Token::LParen
648            && p.nth_matches(offset + 1, Token::Reserved, "echo")
649        {
650            p.expect(Token::LParen)?;
651            p.expect_matches(Token::Reserved, "echo")?;
652            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
653            p.expect(Token::RParen)?;
654            #[allow(clippy::useless_conversion)] return Ok(Self::Echo(m0.into()));
655        }
656        if p.nth(offset) == Token::LParen
657            && p.nth_matches(offset + 1, Token::Reserved, "define-fun-rec")
658        {
659            p.expect(Token::LParen)?;
660            p.expect_matches(Token::Reserved, "define-fun-rec")?;
661            let m0 = <FunctionDef<'st> as SmtlibParse<'st>>::parse(p)?;
662            p.expect(Token::RParen)?;
663            #[allow(clippy::useless_conversion)]
664            return Ok(Self::DefineFunRec(m0.into()));
665        }
666        if p.nth(offset) == Token::LParen
667            && p.nth_matches(offset + 1, Token::Reserved, "define-fun")
668        {
669            p.expect(Token::LParen)?;
670            p.expect_matches(Token::Reserved, "define-fun")?;
671            let m0 = <FunctionDef<'st> as SmtlibParse<'st>>::parse(p)?;
672            p.expect(Token::RParen)?;
673            #[allow(clippy::useless_conversion)] return Ok(Self::DefineFun(m0.into()));
674        }
675        if p.nth(offset) == Token::LParen
676            && p.nth_matches(offset + 1, Token::Reserved, "declare-sort")
677        {
678            p.expect(Token::LParen)?;
679            p.expect_matches(Token::Reserved, "declare-sort")?;
680            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
681            let m1 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
682            p.expect(Token::RParen)?;
683            #[allow(clippy::useless_conversion)]
684            return Ok(Self::DeclareSort(m0.into(), m1.into()));
685        }
686        if p.nth(offset) == Token::LParen
687            && p.nth_matches(offset + 1, Token::Reserved, "declare-datatype")
688        {
689            p.expect(Token::LParen)?;
690            p.expect_matches(Token::Reserved, "declare-datatype")?;
691            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
692            let m1 = <DatatypeDec<'st> as SmtlibParse<'st>>::parse(p)?;
693            p.expect(Token::RParen)?;
694            #[allow(clippy::useless_conversion)]
695            return Ok(Self::DeclareDatatype(m0.into(), m1.into()));
696        }
697        if p.nth(offset) == Token::LParen
698            && p.nth_matches(offset + 1, Token::Reserved, "declare-const")
699        {
700            p.expect(Token::LParen)?;
701            p.expect_matches(Token::Reserved, "declare-const")?;
702            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
703            let m1 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
704            p.expect(Token::RParen)?;
705            #[allow(clippy::useless_conversion)]
706            return Ok(Self::DeclareConst(m0.into(), m1.into()));
707        }
708        if p.nth(offset) == Token::LParen
709            && p.nth_matches(offset + 1, Token::Reserved, "check-sat")
710            && p.nth(offset + 2) == Token::RParen
711        {
712            p.expect(Token::LParen)?;
713            p.expect_matches(Token::Reserved, "check-sat")?;
714            p.expect(Token::RParen)?;
715            #[allow(clippy::useless_conversion)] return Ok(Self::CheckSat);
716        }
717        if p.nth(offset) == Token::LParen
718            && p.nth_matches(offset + 1, Token::Symbol, "assert-soft")
719        {
720            p.expect(Token::LParen)?;
721            p.expect_matches(Token::Symbol, "assert-soft")?;
722            let m0 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
723            let m1 = p.any::<OptimizationAttribute<'st>>()?;
724            p.expect(Token::RParen)?;
725            #[allow(clippy::useless_conversion)]
726            return Ok(Self::AssertSoft(m0.into(), m1.into()));
727        }
728        if p.nth(offset) == Token::LParen
729            && p.nth_matches(offset + 1, Token::Reserved, "assert")
730        {
731            p.expect(Token::LParen)?;
732            p.expect_matches(Token::Reserved, "assert")?;
733            let m0 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
734            p.expect(Token::RParen)?;
735            #[allow(clippy::useless_conversion)] return Ok(Self::Assert(m0.into()));
736        }
737        Err(p.stuck("Command"))
738    }
739}
740impl<'st> Command<'st> {
741    pub fn has_response(&self) -> bool {
742        match self {
743            Self::Assert(_) => false,
744            Self::AssertSoft(_, _) => false,
745            Self::CheckSat => true,
746            Self::CheckSatAssuming(_) => true,
747            Self::DeclareConst(_, _) => false,
748            Self::DeclareDatatype(_, _) => false,
749            Self::DeclareDatatypes(_, _) => false,
750            Self::DeclareFun(_, _, _) => false,
751            Self::DeclareSort(_, _) => false,
752            Self::DefineFun(_) => false,
753            Self::DefineFunRec(_) => false,
754            Self::DefineFunsRec(_, _) => false,
755            Self::DefineSort(_, _, _) => false,
756            Self::Echo(_) => true,
757            Self::Eval(_) => true,
758            Self::Exit => false,
759            Self::GetAssertions => true,
760            Self::GetAssignment => true,
761            Self::GetInfo(_) => true,
762            Self::GetModel => true,
763            Self::GetOption(_) => true,
764            Self::GetProof => true,
765            Self::GetUnsatAssumptions => true,
766            Self::GetUnsatCore => true,
767            Self::GetValue(_) => true,
768            Self::Maximize(_) => false,
769            Self::Minimize(_) => false,
770            Self::Pop(_) => false,
771            Self::Push(_) => false,
772            Self::Reset => false,
773            Self::ResetAssertions => false,
774            Self::SetInfo(_) => false,
775            Self::SetLogic(_) => false,
776            Self::SetOption(_) => false,
777            Self::Simplify(_) => true,
778        }
779    }
780    pub fn parse_response(
781        &self,
782        st: &'st Storage,
783        response: &str,
784    ) -> Result<std::option::Option<SpecificSuccessResponse<'st>>, ParseError> {
785        match self {
786            Self::Assert(_) => Ok(None),
787            Self::AssertSoft(_, _) => Ok(None),
788            Self::CheckSat => {
789                Ok(
790                    Some(
791                        SpecificSuccessResponse::CheckSatResponse(
792                            <CheckSatResponse as SmtlibParse<
793                                'st,
794                            >>::parse(&mut Parser::new(st, response))?,
795                        ),
796                    ),
797                )
798            }
799            Self::CheckSatAssuming(_) => {
800                Ok(
801                    Some(
802                        SpecificSuccessResponse::CheckSatResponse(
803                            <CheckSatResponse as SmtlibParse<
804                                'st,
805                            >>::parse(&mut Parser::new(st, response))?,
806                        ),
807                    ),
808                )
809            }
810            Self::DeclareConst(_, _) => Ok(None),
811            Self::DeclareDatatype(_, _) => Ok(None),
812            Self::DeclareDatatypes(_, _) => Ok(None),
813            Self::DeclareFun(_, _, _) => Ok(None),
814            Self::DeclareSort(_, _) => Ok(None),
815            Self::DefineFun(_) => Ok(None),
816            Self::DefineFunRec(_) => Ok(None),
817            Self::DefineFunsRec(_, _) => Ok(None),
818            Self::DefineSort(_, _, _) => Ok(None),
819            Self::Echo(_) => {
820                Ok(
821                    Some(
822                        SpecificSuccessResponse::EchoResponse(
823                            <EchoResponse<
824                                'st,
825                            > as SmtlibParse<
826                                'st,
827                            >>::parse(&mut Parser::new(st, response))?,
828                        ),
829                    ),
830                )
831            }
832            Self::Eval(_) => {
833                Ok(
834                    Some(
835                        SpecificSuccessResponse::EvalResponse(
836                            <EvalResponse<
837                                'st,
838                            > as SmtlibParse<
839                                'st,
840                            >>::parse(&mut Parser::new(st, response))?,
841                        ),
842                    ),
843                )
844            }
845            Self::Exit => Ok(None),
846            Self::GetAssertions => {
847                Ok(
848                    Some(
849                        SpecificSuccessResponse::GetAssertionsResponse(
850                            <GetAssertionsResponse<
851                                'st,
852                            > as SmtlibParse<
853                                'st,
854                            >>::parse(&mut Parser::new(st, response))?,
855                        ),
856                    ),
857                )
858            }
859            Self::GetAssignment => {
860                Ok(
861                    Some(
862                        SpecificSuccessResponse::GetAssignmentResponse(
863                            <GetAssignmentResponse<
864                                'st,
865                            > as SmtlibParse<
866                                'st,
867                            >>::parse(&mut Parser::new(st, response))?,
868                        ),
869                    ),
870                )
871            }
872            Self::GetInfo(_) => {
873                Ok(
874                    Some(
875                        SpecificSuccessResponse::GetInfoResponse(
876                            <GetInfoResponse<
877                                'st,
878                            > as SmtlibParse<
879                                'st,
880                            >>::parse(&mut Parser::new(st, response))?,
881                        ),
882                    ),
883                )
884            }
885            Self::GetModel => {
886                Ok(
887                    Some(
888                        SpecificSuccessResponse::GetModelResponse(
889                            <GetModelResponse<
890                                'st,
891                            > as SmtlibParse<
892                                'st,
893                            >>::parse(&mut Parser::new(st, response))?,
894                        ),
895                    ),
896                )
897            }
898            Self::GetOption(_) => {
899                Ok(
900                    Some(
901                        SpecificSuccessResponse::GetOptionResponse(
902                            <GetOptionResponse<
903                                'st,
904                            > as SmtlibParse<
905                                'st,
906                            >>::parse(&mut Parser::new(st, response))?,
907                        ),
908                    ),
909                )
910            }
911            Self::GetProof => {
912                Ok(
913                    Some(
914                        SpecificSuccessResponse::GetProofResponse(
915                            <GetProofResponse<
916                                'st,
917                            > as SmtlibParse<
918                                'st,
919                            >>::parse(&mut Parser::new(st, response))?,
920                        ),
921                    ),
922                )
923            }
924            Self::GetUnsatAssumptions => {
925                Ok(
926                    Some(
927                        SpecificSuccessResponse::GetUnsatAssumptionsResponse(
928                            <GetUnsatAssumptionsResponse<
929                                'st,
930                            > as SmtlibParse<
931                                'st,
932                            >>::parse(&mut Parser::new(st, response))?,
933                        ),
934                    ),
935                )
936            }
937            Self::GetUnsatCore => {
938                Ok(
939                    Some(
940                        SpecificSuccessResponse::GetUnsatCoreResponse(
941                            <GetUnsatCoreResponse<
942                                'st,
943                            > as SmtlibParse<
944                                'st,
945                            >>::parse(&mut Parser::new(st, response))?,
946                        ),
947                    ),
948                )
949            }
950            Self::GetValue(_) => {
951                Ok(
952                    Some(
953                        SpecificSuccessResponse::GetValueResponse(
954                            <GetValueResponse<
955                                'st,
956                            > as SmtlibParse<
957                                'st,
958                            >>::parse(&mut Parser::new(st, response))?,
959                        ),
960                    ),
961                )
962            }
963            Self::Maximize(_) => Ok(None),
964            Self::Minimize(_) => Ok(None),
965            Self::Pop(_) => Ok(None),
966            Self::Push(_) => Ok(None),
967            Self::Reset => Ok(None),
968            Self::ResetAssertions => Ok(None),
969            Self::SetInfo(_) => Ok(None),
970            Self::SetLogic(_) => Ok(None),
971            Self::SetOption(_) => Ok(None),
972            Self::Simplify(_) => {
973                Ok(
974                    Some(
975                        SpecificSuccessResponse::SimplifyResponse(
976                            <SimplifyResponse<
977                                'st,
978                            > as SmtlibParse<
979                                'st,
980                            >>::parse(&mut Parser::new(st, response))?,
981                        ),
982                    ),
983                )
984            }
985        }
986    }
987}
988/// `(<symbol> <selector_dec>*)`
989#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
990#[cfg_attr(feature = "serde", derive(serde::Serialize))]
991pub struct ConstructorDec<'st>(pub Symbol<'st>, pub &'st [SelectorDec<'st>]);
992impl std::fmt::Display for ConstructorDec<'_> {
993    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
994        write!(f, "({} {})", self.0, self.1.iter().format(" "))
995    }
996}
997impl<'st> ConstructorDec<'st> {
998    pub fn parse(
999        st: &'st Storage,
1000        src: &str,
1001    ) -> Result<ConstructorDec<'st>, ParseError> {
1002        <ConstructorDec<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1003    }
1004}
1005impl<'st> SmtlibParse<'st> for ConstructorDec<'st> {
1006    type Output = ConstructorDec<'st>;
1007    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1008        p.nth(offset) == Token::LParen
1009    }
1010    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1011        p.expect(Token::LParen)?;
1012        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
1013        let m1 = p.any::<SelectorDec<'st>>()?;
1014        p.expect(Token::RParen)?;
1015        Ok(Self(m0, m1))
1016    }
1017}
1018#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1019#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1020pub enum DatatypeDec<'st> {
1021    /// `(<constructor_dec>+)`
1022    DatatypeDec(&'st [ConstructorDec<'st>]),
1023    /// `(par (<symbol>+) (<constructor_dec>+))`
1024    Par(&'st [Symbol<'st>], &'st [ConstructorDec<'st>]),
1025}
1026impl std::fmt::Display for DatatypeDec<'_> {
1027    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1028        match self {
1029            Self::DatatypeDec(m0) => write!(f, "({})", m0.iter().format(" ")),
1030            Self::Par(m0, m1) => {
1031                write!(
1032                    f, "(par ({}) ({}))", m0.iter().format(" "), m1.iter().format(" ")
1033                )
1034            }
1035        }
1036    }
1037}
1038impl<'st> DatatypeDec<'st> {
1039    pub fn parse(st: &'st Storage, src: &str) -> Result<DatatypeDec<'st>, ParseError> {
1040        <DatatypeDec<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1041    }
1042}
1043impl<'st> SmtlibParse<'st> for DatatypeDec<'st> {
1044    type Output = DatatypeDec<'st>;
1045    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1046        (p.nth(offset) == Token::LParen
1047            && p.nth_matches(offset + 1, Token::Reserved, "par")
1048            && p.nth(offset + 2) == Token::LParen) || (p.nth(offset) == Token::LParen)
1049    }
1050    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1051        let offset = 0;
1052        if p.nth(offset) == Token::LParen
1053            && p.nth_matches(offset + 1, Token::Reserved, "par")
1054            && p.nth(offset + 2) == Token::LParen
1055        {
1056            p.expect(Token::LParen)?;
1057            p.expect_matches(Token::Reserved, "par")?;
1058            p.expect(Token::LParen)?;
1059            let m0 = p.non_zero::<Symbol<'st>>()?;
1060            p.expect(Token::RParen)?;
1061            p.expect(Token::LParen)?;
1062            let m1 = p.non_zero::<ConstructorDec<'st>>()?;
1063            p.expect(Token::RParen)?;
1064            p.expect(Token::RParen)?;
1065            #[allow(clippy::useless_conversion)]
1066            return Ok(Self::Par(m0.into(), m1.into()));
1067        }
1068        if p.nth(offset) == Token::LParen {
1069            p.expect(Token::LParen)?;
1070            let m0 = p.non_zero::<ConstructorDec<'st>>()?;
1071            p.expect(Token::RParen)?;
1072            #[allow(clippy::useless_conversion)] return Ok(Self::DatatypeDec(m0.into()));
1073        }
1074        Err(p.stuck("DatatypeDec"))
1075    }
1076}
1077/// `<string>`
1078#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1079#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1080pub struct EchoResponse<'st>(pub &'st str);
1081impl std::fmt::Display for EchoResponse<'_> {
1082    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1083        write!(f, "{}", self.0)
1084    }
1085}
1086impl<'st> EchoResponse<'st> {
1087    pub fn parse(st: &'st Storage, src: &str) -> Result<EchoResponse<'st>, ParseError> {
1088        <EchoResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1089    }
1090}
1091impl<'st> SmtlibParse<'st> for EchoResponse<'st> {
1092    type Output = EchoResponse<'st>;
1093    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1094        String::is_start_of(offset, p)
1095    }
1096    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1097        let m0 = <String as SmtlibParse<'st>>::parse(p)?;
1098        Ok(Self(m0))
1099    }
1100}
1101#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1102#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1103pub enum ErrorBehavior {
1104    /// `continued-execution`
1105    ContinuedExecution,
1106    /// `immediate-exit`
1107    ImmediateExit,
1108}
1109impl std::fmt::Display for ErrorBehavior {
1110    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1111        match self {
1112            Self::ContinuedExecution => write!(f, "continued-execution"),
1113            Self::ImmediateExit => write!(f, "immediate-exit"),
1114        }
1115    }
1116}
1117impl<'st> ErrorBehavior {
1118    pub fn parse(st: &'st Storage, src: &str) -> Result<ErrorBehavior, ParseError> {
1119        <ErrorBehavior as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1120    }
1121}
1122impl<'st> SmtlibParse<'st> for ErrorBehavior {
1123    type Output = ErrorBehavior;
1124    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1125        (p.nth_matches(offset, Token::Symbol, "immediate-exit"))
1126            || (p.nth_matches(offset, Token::Symbol, "continued-execution"))
1127    }
1128    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1129        let offset = 0;
1130        if p.nth_matches(offset, Token::Symbol, "immediate-exit") {
1131            p.expect_matches(Token::Symbol, "immediate-exit")?;
1132            #[allow(clippy::useless_conversion)] return Ok(Self::ImmediateExit);
1133        }
1134        if p.nth_matches(offset, Token::Symbol, "continued-execution") {
1135            p.expect_matches(Token::Symbol, "continued-execution")?;
1136            #[allow(clippy::useless_conversion)] return Ok(Self::ContinuedExecution);
1137        }
1138        Err(p.stuck("ErrorBehavior"))
1139    }
1140}
1141/// `<term>`
1142#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1143#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1144pub struct EvalResponse<'st>(pub &'st Term<'st>);
1145impl std::fmt::Display for EvalResponse<'_> {
1146    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1147        write!(f, "{}", self.0)
1148    }
1149}
1150impl<'st> EvalResponse<'st> {
1151    pub fn parse(st: &'st Storage, src: &str) -> Result<EvalResponse<'st>, ParseError> {
1152        <EvalResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1153    }
1154}
1155impl<'st> SmtlibParse<'st> for EvalResponse<'st> {
1156    type Output = EvalResponse<'st>;
1157    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1158        Term::is_start_of(offset, p)
1159    }
1160    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1161        let m0 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
1162        Ok(Self(m0))
1163    }
1164}
1165#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1166#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1167pub enum FunSymbolDecl<'st> {
1168    /// `(<identifier> <sort>+ <attribute>*)`
1169    Identifier(Identifier<'st>, &'st [Sort<'st>], &'st [Attribute<'st>]),
1170    /// `(<meta_spec_constant> <sort> <attribute>*)`
1171    MetaSpecConstant(MetaSpecConstant, Sort<'st>, &'st [Attribute<'st>]),
1172    /// `(<spec_constant> <sort> <attribute>*)`
1173    SpecConstant(SpecConstant<'st>, Sort<'st>, &'st [Attribute<'st>]),
1174}
1175impl std::fmt::Display for FunSymbolDecl<'_> {
1176    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1177        match self {
1178            Self::Identifier(m0, m1, m2) => {
1179                write!(f, "({} {} {})", m0, m1.iter().format(" "), m2.iter().format(" "))
1180            }
1181            Self::MetaSpecConstant(m0, m1, m2) => {
1182                write!(f, "({} {} {})", m0, m1, m2.iter().format(" "))
1183            }
1184            Self::SpecConstant(m0, m1, m2) => {
1185                write!(f, "({} {} {})", m0, m1, m2.iter().format(" "))
1186            }
1187        }
1188    }
1189}
1190impl<'st> FunSymbolDecl<'st> {
1191    pub fn parse(st: &'st Storage, src: &str) -> Result<FunSymbolDecl<'st>, ParseError> {
1192        <FunSymbolDecl<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1193    }
1194}
1195impl<'st> SmtlibParse<'st> for FunSymbolDecl<'st> {
1196    type Output = FunSymbolDecl<'st>;
1197    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1198        (p.nth(offset) == Token::LParen) || (p.nth(offset) == Token::LParen)
1199            || (p.nth(offset) == Token::LParen)
1200    }
1201    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1202        let offset = 0;
1203        if p.nth(offset) == Token::LParen {
1204            p.expect(Token::LParen)?;
1205            let m0 = <SpecConstant<'st> as SmtlibParse<'st>>::parse(p)?;
1206            let m1 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
1207            let m2 = p.any::<Attribute<'st>>()?;
1208            p.expect(Token::RParen)?;
1209            #[allow(clippy::useless_conversion)]
1210            return Ok(Self::SpecConstant(m0.into(), m1.into(), m2.into()));
1211        }
1212        if p.nth(offset) == Token::LParen {
1213            p.expect(Token::LParen)?;
1214            let m0 = <MetaSpecConstant as SmtlibParse<'st>>::parse(p)?;
1215            let m1 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
1216            let m2 = p.any::<Attribute<'st>>()?;
1217            p.expect(Token::RParen)?;
1218            #[allow(clippy::useless_conversion)]
1219            return Ok(Self::MetaSpecConstant(m0.into(), m1.into(), m2.into()));
1220        }
1221        if p.nth(offset) == Token::LParen {
1222            p.expect(Token::LParen)?;
1223            let m0 = <Identifier<'st> as SmtlibParse<'st>>::parse(p)?;
1224            let m1 = p.non_zero::<Sort<'st>>()?;
1225            let m2 = p.any::<Attribute<'st>>()?;
1226            p.expect(Token::RParen)?;
1227            #[allow(clippy::useless_conversion)]
1228            return Ok(Self::Identifier(m0.into(), m1.into(), m2.into()));
1229        }
1230        Err(p.stuck("FunSymbolDecl"))
1231    }
1232}
1233/// `(<symbol> (<sort>*) <sort>)`
1234#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1235#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1236pub struct FunctionDec<'st>(pub Symbol<'st>, pub &'st [Sort<'st>], pub Sort<'st>);
1237impl std::fmt::Display for FunctionDec<'_> {
1238    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1239        write!(f, "({} ({}) {})", self.0, self.1.iter().format(" "), self.2)
1240    }
1241}
1242impl<'st> FunctionDec<'st> {
1243    pub fn parse(st: &'st Storage, src: &str) -> Result<FunctionDec<'st>, ParseError> {
1244        <FunctionDec<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1245    }
1246}
1247impl<'st> SmtlibParse<'st> for FunctionDec<'st> {
1248    type Output = FunctionDec<'st>;
1249    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1250        p.nth(offset) == Token::LParen
1251    }
1252    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1253        p.expect(Token::LParen)?;
1254        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
1255        p.expect(Token::LParen)?;
1256        let m1 = p.any::<Sort<'st>>()?;
1257        p.expect(Token::RParen)?;
1258        let m2 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
1259        p.expect(Token::RParen)?;
1260        Ok(Self(m0, m1, m2))
1261    }
1262}
1263/// `<symbol> (<sorted_var>*) <sort> <term>`
1264#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1265#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1266pub struct FunctionDef<'st>(
1267    pub Symbol<'st>,
1268    pub &'st [SortedVar<'st>],
1269    pub Sort<'st>,
1270    pub &'st Term<'st>,
1271);
1272impl std::fmt::Display for FunctionDef<'_> {
1273    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1274        write!(f, "{} ({}) {} {}", self.0, self.1.iter().format(" "), self.2, self.3)
1275    }
1276}
1277impl<'st> FunctionDef<'st> {
1278    pub fn parse(st: &'st Storage, src: &str) -> Result<FunctionDef<'st>, ParseError> {
1279        <FunctionDef<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1280    }
1281}
1282impl<'st> SmtlibParse<'st> for FunctionDef<'st> {
1283    type Output = FunctionDef<'st>;
1284    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1285        Symbol::is_start_of(offset, p)
1286    }
1287    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1288        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
1289        p.expect(Token::LParen)?;
1290        let m1 = p.any::<SortedVar<'st>>()?;
1291        p.expect(Token::RParen)?;
1292        let m2 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
1293        let m3 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
1294        Ok(Self(m0, m1, m2, m3))
1295    }
1296}
1297#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1298#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1299pub enum GeneralResponse<'st> {
1300    /// `(error <string>)`
1301    Error(&'st str),
1302    /// `<specific_success_response>`
1303    SpecificSuccessResponse(SpecificSuccessResponse<'st>),
1304    /// `success`
1305    Success,
1306    /// `unsupported`
1307    Unsupported,
1308}
1309impl std::fmt::Display for GeneralResponse<'_> {
1310    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1311        match self {
1312            Self::Error(m0) => write!(f, "(error {})", m0),
1313            Self::SpecificSuccessResponse(m0) => write!(f, "{}", m0),
1314            Self::Success => write!(f, "success"),
1315            Self::Unsupported => write!(f, "unsupported"),
1316        }
1317    }
1318}
1319impl<'st> GeneralResponse<'st> {
1320    pub fn parse(
1321        st: &'st Storage,
1322        src: &str,
1323    ) -> Result<GeneralResponse<'st>, ParseError> {
1324        <GeneralResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1325    }
1326}
1327impl<'st> SmtlibParse<'st> for GeneralResponse<'st> {
1328    type Output = GeneralResponse<'st>;
1329    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1330        (p.nth(offset) == Token::LParen
1331            && p.nth_matches(offset + 1, Token::Symbol, "error"))
1332            || (p.nth_matches(offset, Token::Symbol, "unsupported"))
1333            || (p.nth_matches(offset, Token::Symbol, "success"))
1334            || (SpecificSuccessResponse::is_start_of(offset, p))
1335    }
1336    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1337        let offset = 0;
1338        if p.nth(offset) == Token::LParen
1339            && p.nth_matches(offset + 1, Token::Symbol, "error")
1340        {
1341            p.expect(Token::LParen)?;
1342            p.expect_matches(Token::Symbol, "error")?;
1343            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
1344            p.expect(Token::RParen)?;
1345            #[allow(clippy::useless_conversion)] return Ok(Self::Error(m0.into()));
1346        }
1347        if p.nth_matches(offset, Token::Symbol, "unsupported") {
1348            p.expect_matches(Token::Symbol, "unsupported")?;
1349            #[allow(clippy::useless_conversion)] return Ok(Self::Unsupported);
1350        }
1351        if p.nth_matches(offset, Token::Symbol, "success") {
1352            p.expect_matches(Token::Symbol, "success")?;
1353            #[allow(clippy::useless_conversion)] return Ok(Self::Success);
1354        }
1355        if SpecificSuccessResponse::is_start_of(offset, p) {
1356            let m0 = <SpecificSuccessResponse<'st> as SmtlibParse<'st>>::parse(p)?;
1357            #[allow(clippy::useless_conversion)]
1358            return Ok(Self::SpecificSuccessResponse(m0.into()));
1359        }
1360        Err(p.stuck("GeneralResponse"))
1361    }
1362}
1363/// `(<term>*)`
1364#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1365#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1366pub struct GetAssertionsResponse<'st>(pub &'st [&'st Term<'st>]);
1367impl std::fmt::Display for GetAssertionsResponse<'_> {
1368    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1369        write!(f, "({})", self.0.iter().format(" "))
1370    }
1371}
1372impl<'st> GetAssertionsResponse<'st> {
1373    pub fn parse(
1374        st: &'st Storage,
1375        src: &str,
1376    ) -> Result<GetAssertionsResponse<'st>, ParseError> {
1377        <GetAssertionsResponse<
1378            'st,
1379        > as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1380    }
1381}
1382impl<'st> SmtlibParse<'st> for GetAssertionsResponse<'st> {
1383    type Output = GetAssertionsResponse<'st>;
1384    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1385        p.nth(offset) == Token::LParen
1386    }
1387    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1388        p.expect(Token::LParen)?;
1389        let m0 = p.any::<Term<'st>>()?;
1390        p.expect(Token::RParen)?;
1391        Ok(Self(m0))
1392    }
1393}
1394/// `(<t_valuation_pair>*)`
1395#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1396#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1397pub struct GetAssignmentResponse<'st>(pub &'st [TValuationPair<'st>]);
1398impl std::fmt::Display for GetAssignmentResponse<'_> {
1399    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1400        write!(f, "({})", self.0.iter().format(" "))
1401    }
1402}
1403impl<'st> GetAssignmentResponse<'st> {
1404    pub fn parse(
1405        st: &'st Storage,
1406        src: &str,
1407    ) -> Result<GetAssignmentResponse<'st>, ParseError> {
1408        <GetAssignmentResponse<
1409            'st,
1410        > as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1411    }
1412}
1413impl<'st> SmtlibParse<'st> for GetAssignmentResponse<'st> {
1414    type Output = GetAssignmentResponse<'st>;
1415    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1416        p.nth(offset) == Token::LParen
1417    }
1418    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1419        p.expect(Token::LParen)?;
1420        let m0 = p.any::<TValuationPair<'st>>()?;
1421        p.expect(Token::RParen)?;
1422        Ok(Self(m0))
1423    }
1424}
1425/// `(<info_response>+)`
1426#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1427#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1428pub struct GetInfoResponse<'st>(pub &'st [InfoResponse<'st>]);
1429impl std::fmt::Display for GetInfoResponse<'_> {
1430    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1431        write!(f, "({})", self.0.iter().format(" "))
1432    }
1433}
1434impl<'st> GetInfoResponse<'st> {
1435    pub fn parse(
1436        st: &'st Storage,
1437        src: &str,
1438    ) -> Result<GetInfoResponse<'st>, ParseError> {
1439        <GetInfoResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1440    }
1441}
1442impl<'st> SmtlibParse<'st> for GetInfoResponse<'st> {
1443    type Output = GetInfoResponse<'st>;
1444    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1445        p.nth(offset) == Token::LParen
1446    }
1447    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1448        p.expect(Token::LParen)?;
1449        let m0 = p.non_zero::<InfoResponse<'st>>()?;
1450        p.expect(Token::RParen)?;
1451        Ok(Self(m0))
1452    }
1453}
1454/// `(<model_response>*)`
1455#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1456#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1457pub struct GetModelResponse<'st>(pub &'st [ModelResponse<'st>]);
1458impl std::fmt::Display for GetModelResponse<'_> {
1459    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1460        write!(f, "({})", self.0.iter().format(" "))
1461    }
1462}
1463impl<'st> GetModelResponse<'st> {
1464    pub fn parse(
1465        st: &'st Storage,
1466        src: &str,
1467    ) -> Result<GetModelResponse<'st>, ParseError> {
1468        <GetModelResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1469    }
1470}
1471impl<'st> SmtlibParse<'st> for GetModelResponse<'st> {
1472    type Output = GetModelResponse<'st>;
1473    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1474        p.nth(offset) == Token::LParen
1475    }
1476    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1477        p.expect(Token::LParen)?;
1478        let m0 = p.any::<ModelResponse<'st>>()?;
1479        p.expect(Token::RParen)?;
1480        Ok(Self(m0))
1481    }
1482}
1483/// `<attribute_value>`
1484#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1485#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1486pub struct GetOptionResponse<'st>(pub AttributeValue<'st>);
1487impl std::fmt::Display for GetOptionResponse<'_> {
1488    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1489        write!(f, "{}", self.0)
1490    }
1491}
1492impl<'st> GetOptionResponse<'st> {
1493    pub fn parse(
1494        st: &'st Storage,
1495        src: &str,
1496    ) -> Result<GetOptionResponse<'st>, ParseError> {
1497        <GetOptionResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1498    }
1499}
1500impl<'st> SmtlibParse<'st> for GetOptionResponse<'st> {
1501    type Output = GetOptionResponse<'st>;
1502    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1503        AttributeValue::is_start_of(offset, p)
1504    }
1505    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1506        let m0 = <AttributeValue<'st> as SmtlibParse<'st>>::parse(p)?;
1507        Ok(Self(m0))
1508    }
1509}
1510/// `<s_expr>`
1511#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1512#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1513pub struct GetProofResponse<'st>(pub SExpr<'st>);
1514impl std::fmt::Display for GetProofResponse<'_> {
1515    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1516        write!(f, "{}", self.0)
1517    }
1518}
1519impl<'st> GetProofResponse<'st> {
1520    pub fn parse(
1521        st: &'st Storage,
1522        src: &str,
1523    ) -> Result<GetProofResponse<'st>, ParseError> {
1524        <GetProofResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1525    }
1526}
1527impl<'st> SmtlibParse<'st> for GetProofResponse<'st> {
1528    type Output = GetProofResponse<'st>;
1529    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1530        SExpr::is_start_of(offset, p)
1531    }
1532    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1533        let m0 = <SExpr<'st> as SmtlibParse<'st>>::parse(p)?;
1534        Ok(Self(m0))
1535    }
1536}
1537/// `(<symbol>*)`
1538#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1539#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1540pub struct GetUnsatAssumptionsResponse<'st>(pub &'st [Symbol<'st>]);
1541impl std::fmt::Display for GetUnsatAssumptionsResponse<'_> {
1542    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1543        write!(f, "({})", self.0.iter().format(" "))
1544    }
1545}
1546impl<'st> GetUnsatAssumptionsResponse<'st> {
1547    pub fn parse(
1548        st: &'st Storage,
1549        src: &str,
1550    ) -> Result<GetUnsatAssumptionsResponse<'st>, ParseError> {
1551        <GetUnsatAssumptionsResponse<
1552            'st,
1553        > as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1554    }
1555}
1556impl<'st> SmtlibParse<'st> for GetUnsatAssumptionsResponse<'st> {
1557    type Output = GetUnsatAssumptionsResponse<'st>;
1558    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1559        p.nth(offset) == Token::LParen
1560    }
1561    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1562        p.expect(Token::LParen)?;
1563        let m0 = p.any::<Symbol<'st>>()?;
1564        p.expect(Token::RParen)?;
1565        Ok(Self(m0))
1566    }
1567}
1568/// `(<symbol>*)`
1569#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1570#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1571pub struct GetUnsatCoreResponse<'st>(pub &'st [Symbol<'st>]);
1572impl std::fmt::Display for GetUnsatCoreResponse<'_> {
1573    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1574        write!(f, "({})", self.0.iter().format(" "))
1575    }
1576}
1577impl<'st> GetUnsatCoreResponse<'st> {
1578    pub fn parse(
1579        st: &'st Storage,
1580        src: &str,
1581    ) -> Result<GetUnsatCoreResponse<'st>, ParseError> {
1582        <GetUnsatCoreResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1583    }
1584}
1585impl<'st> SmtlibParse<'st> for GetUnsatCoreResponse<'st> {
1586    type Output = GetUnsatCoreResponse<'st>;
1587    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1588        p.nth(offset) == Token::LParen
1589    }
1590    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1591        p.expect(Token::LParen)?;
1592        let m0 = p.any::<Symbol<'st>>()?;
1593        p.expect(Token::RParen)?;
1594        Ok(Self(m0))
1595    }
1596}
1597/// `(<valuation_pair>+)`
1598#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1599#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1600pub struct GetValueResponse<'st>(pub &'st [ValuationPair<'st>]);
1601impl std::fmt::Display for GetValueResponse<'_> {
1602    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1603        write!(f, "({})", self.0.iter().format(" "))
1604    }
1605}
1606impl<'st> GetValueResponse<'st> {
1607    pub fn parse(
1608        st: &'st Storage,
1609        src: &str,
1610    ) -> Result<GetValueResponse<'st>, ParseError> {
1611        <GetValueResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1612    }
1613}
1614impl<'st> SmtlibParse<'st> for GetValueResponse<'st> {
1615    type Output = GetValueResponse<'st>;
1616    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1617        p.nth(offset) == Token::LParen
1618    }
1619    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1620        p.expect(Token::LParen)?;
1621        let m0 = p.non_zero::<ValuationPair<'st>>()?;
1622        p.expect(Token::RParen)?;
1623        Ok(Self(m0))
1624    }
1625}
1626#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1627#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1628pub enum Identifier<'st> {
1629    /// `(_ <symbol> <index>+)`
1630    Indexed(Symbol<'st>, &'st [Index<'st>]),
1631    /// `<symbol>`
1632    Simple(Symbol<'st>),
1633}
1634impl std::fmt::Display for Identifier<'_> {
1635    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1636        match self {
1637            Self::Indexed(m0, m1) => write!(f, "(_ {} {})", m0, m1.iter().format(" ")),
1638            Self::Simple(m0) => write!(f, "{}", m0),
1639        }
1640    }
1641}
1642impl<'st> Identifier<'st> {
1643    pub fn parse(st: &'st Storage, src: &str) -> Result<Identifier<'st>, ParseError> {
1644        <Identifier<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1645    }
1646}
1647impl<'st> SmtlibParse<'st> for Identifier<'st> {
1648    type Output = Identifier<'st>;
1649    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1650        (p.nth(offset) == Token::LParen
1651            && p.nth_matches(offset + 1, Token::Reserved, "_"))
1652            || (Symbol::is_start_of(offset, p))
1653    }
1654    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1655        let offset = 0;
1656        if p.nth(offset) == Token::LParen
1657            && p.nth_matches(offset + 1, Token::Reserved, "_")
1658        {
1659            p.expect(Token::LParen)?;
1660            p.expect_matches(Token::Reserved, "_")?;
1661            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
1662            let m1 = p.non_zero::<Index<'st>>()?;
1663            p.expect(Token::RParen)?;
1664            #[allow(clippy::useless_conversion)]
1665            return Ok(Self::Indexed(m0.into(), m1.into()));
1666        }
1667        if Symbol::is_start_of(offset, p) {
1668            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
1669            #[allow(clippy::useless_conversion)] return Ok(Self::Simple(m0.into()));
1670        }
1671        Err(p.stuck("Identifier"))
1672    }
1673}
1674#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1675#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1676pub enum Index<'st> {
1677    /// `<numeral>`
1678    Numeral(Numeral<'st>),
1679    /// `<symbol>`
1680    Symbol(Symbol<'st>),
1681}
1682impl std::fmt::Display for Index<'_> {
1683    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1684        match self {
1685            Self::Numeral(m0) => write!(f, "{}", m0),
1686            Self::Symbol(m0) => write!(f, "{}", m0),
1687        }
1688    }
1689}
1690impl<'st> Index<'st> {
1691    pub fn parse(st: &'st Storage, src: &str) -> Result<Index<'st>, ParseError> {
1692        <Index<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1693    }
1694}
1695impl<'st> SmtlibParse<'st> for Index<'st> {
1696    type Output = Index<'st>;
1697    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1698        (Symbol::is_start_of(offset, p)) || (Numeral::is_start_of(offset, p))
1699    }
1700    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1701        let offset = 0;
1702        if Symbol::is_start_of(offset, p) {
1703            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
1704            #[allow(clippy::useless_conversion)] return Ok(Self::Symbol(m0.into()));
1705        }
1706        if Numeral::is_start_of(offset, p) {
1707            let m0 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
1708            #[allow(clippy::useless_conversion)] return Ok(Self::Numeral(m0.into()));
1709        }
1710        Err(p.stuck("Index"))
1711    }
1712}
1713#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1714#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1715pub enum InfoFlag<'st> {
1716    /// `:all-statistics`
1717    AllStatistics,
1718    /// `:assertion-stack-levels`
1719    AssertionStackLevels,
1720    /// `:authors`
1721    Authors,
1722    /// `:error-behavior`
1723    ErrorBehavior,
1724    /// `<keyword>`
1725    Keyword(Keyword<'st>),
1726    /// `:name`
1727    Name,
1728    /// `:reason-unknown`
1729    ReasonUnknown,
1730    /// `:version`
1731    Version,
1732}
1733impl std::fmt::Display for InfoFlag<'_> {
1734    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1735        match self {
1736            Self::AllStatistics => write!(f, ":all-statistics"),
1737            Self::AssertionStackLevels => write!(f, ":assertion-stack-levels"),
1738            Self::Authors => write!(f, ":authors"),
1739            Self::ErrorBehavior => write!(f, ":error-behavior"),
1740            Self::Keyword(m0) => write!(f, "{}", m0),
1741            Self::Name => write!(f, ":name"),
1742            Self::ReasonUnknown => write!(f, ":reason-unknown"),
1743            Self::Version => write!(f, ":version"),
1744        }
1745    }
1746}
1747impl<'st> InfoFlag<'st> {
1748    pub fn parse(st: &'st Storage, src: &str) -> Result<InfoFlag<'st>, ParseError> {
1749        <InfoFlag<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1750    }
1751}
1752impl<'st> SmtlibParse<'st> for InfoFlag<'st> {
1753    type Output = InfoFlag<'st>;
1754    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1755        (p.nth_matches(offset, Token::Keyword, ":version"))
1756            || (p.nth_matches(offset, Token::Keyword, ":reason-unknown"))
1757            || (p.nth_matches(offset, Token::Keyword, ":name"))
1758            || (p.nth_matches(offset, Token::Keyword, ":error-behavior"))
1759            || (p.nth_matches(offset, Token::Keyword, ":authors"))
1760            || (p.nth_matches(offset, Token::Keyword, ":assertion-stack-levels"))
1761            || (p.nth_matches(offset, Token::Keyword, ":all-statistics"))
1762            || (Keyword::is_start_of(offset, p))
1763    }
1764    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1765        let offset = 0;
1766        if p.nth_matches(offset, Token::Keyword, ":version") {
1767            p.expect_matches(Token::Keyword, ":version")?;
1768            #[allow(clippy::useless_conversion)] return Ok(Self::Version);
1769        }
1770        if p.nth_matches(offset, Token::Keyword, ":reason-unknown") {
1771            p.expect_matches(Token::Keyword, ":reason-unknown")?;
1772            #[allow(clippy::useless_conversion)] return Ok(Self::ReasonUnknown);
1773        }
1774        if p.nth_matches(offset, Token::Keyword, ":name") {
1775            p.expect_matches(Token::Keyword, ":name")?;
1776            #[allow(clippy::useless_conversion)] return Ok(Self::Name);
1777        }
1778        if p.nth_matches(offset, Token::Keyword, ":error-behavior") {
1779            p.expect_matches(Token::Keyword, ":error-behavior")?;
1780            #[allow(clippy::useless_conversion)] return Ok(Self::ErrorBehavior);
1781        }
1782        if p.nth_matches(offset, Token::Keyword, ":authors") {
1783            p.expect_matches(Token::Keyword, ":authors")?;
1784            #[allow(clippy::useless_conversion)] return Ok(Self::Authors);
1785        }
1786        if p.nth_matches(offset, Token::Keyword, ":assertion-stack-levels") {
1787            p.expect_matches(Token::Keyword, ":assertion-stack-levels")?;
1788            #[allow(clippy::useless_conversion)] return Ok(Self::AssertionStackLevels);
1789        }
1790        if p.nth_matches(offset, Token::Keyword, ":all-statistics") {
1791            p.expect_matches(Token::Keyword, ":all-statistics")?;
1792            #[allow(clippy::useless_conversion)] return Ok(Self::AllStatistics);
1793        }
1794        if Keyword::is_start_of(offset, p) {
1795            let m0 = <Keyword<'st> as SmtlibParse<'st>>::parse(p)?;
1796            #[allow(clippy::useless_conversion)] return Ok(Self::Keyword(m0.into()));
1797        }
1798        Err(p.stuck("InfoFlag"))
1799    }
1800}
1801#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1802#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1803pub enum InfoResponse<'st> {
1804    /// `:assertion-stack-levels <numeral>`
1805    AssertionStackLevels(Numeral<'st>),
1806    /// `<attribute>`
1807    Attribute(Attribute<'st>),
1808    /// `:authors <string>`
1809    Authors(&'st str),
1810    /// `:error-behavior <error-behavior>`
1811    ErrorBehavior(ErrorBehavior),
1812    /// `:name <string>`
1813    Name(&'st str),
1814    /// `:reason-unknown <reason-unknown>`
1815    ReasonUnknown(ReasonUnknown<'st>),
1816    /// `:version <string>`
1817    Version(&'st str),
1818}
1819impl std::fmt::Display for InfoResponse<'_> {
1820    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1821        match self {
1822            Self::AssertionStackLevels(m0) => write!(f, ":assertion-stack-levels {}", m0),
1823            Self::Attribute(m0) => write!(f, "{}", m0),
1824            Self::Authors(m0) => write!(f, ":authors {}", m0),
1825            Self::ErrorBehavior(m0) => write!(f, ":error-behavior {}", m0),
1826            Self::Name(m0) => write!(f, ":name {}", m0),
1827            Self::ReasonUnknown(m0) => write!(f, ":reason-unknown {}", m0),
1828            Self::Version(m0) => write!(f, ":version {}", m0),
1829        }
1830    }
1831}
1832impl<'st> InfoResponse<'st> {
1833    pub fn parse(st: &'st Storage, src: &str) -> Result<InfoResponse<'st>, ParseError> {
1834        <InfoResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1835    }
1836}
1837impl<'st> SmtlibParse<'st> for InfoResponse<'st> {
1838    type Output = InfoResponse<'st>;
1839    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1840        (p.nth_matches(offset, Token::Keyword, ":version"))
1841            || (p.nth_matches(offset, Token::Keyword, ":reason-unknown"))
1842            || (p.nth_matches(offset, Token::Keyword, ":name"))
1843            || (p.nth_matches(offset, Token::Keyword, ":error-behavior"))
1844            || (p.nth_matches(offset, Token::Keyword, ":authors"))
1845            || (p.nth_matches(offset, Token::Keyword, ":assertion-stack-levels"))
1846            || (Attribute::is_start_of(offset, p))
1847    }
1848    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1849        let offset = 0;
1850        if p.nth_matches(offset, Token::Keyword, ":version") {
1851            p.expect_matches(Token::Keyword, ":version")?;
1852            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
1853            #[allow(clippy::useless_conversion)] return Ok(Self::Version(m0.into()));
1854        }
1855        if p.nth_matches(offset, Token::Keyword, ":reason-unknown") {
1856            p.expect_matches(Token::Keyword, ":reason-unknown")?;
1857            let m0 = <ReasonUnknown<'st> as SmtlibParse<'st>>::parse(p)?;
1858            #[allow(clippy::useless_conversion)]
1859            return Ok(Self::ReasonUnknown(m0.into()));
1860        }
1861        if p.nth_matches(offset, Token::Keyword, ":name") {
1862            p.expect_matches(Token::Keyword, ":name")?;
1863            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
1864            #[allow(clippy::useless_conversion)] return Ok(Self::Name(m0.into()));
1865        }
1866        if p.nth_matches(offset, Token::Keyword, ":error-behavior") {
1867            p.expect_matches(Token::Keyword, ":error-behavior")?;
1868            let m0 = <ErrorBehavior as SmtlibParse<'st>>::parse(p)?;
1869            #[allow(clippy::useless_conversion)]
1870            return Ok(Self::ErrorBehavior(m0.into()));
1871        }
1872        if p.nth_matches(offset, Token::Keyword, ":authors") {
1873            p.expect_matches(Token::Keyword, ":authors")?;
1874            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
1875            #[allow(clippy::useless_conversion)] return Ok(Self::Authors(m0.into()));
1876        }
1877        if p.nth_matches(offset, Token::Keyword, ":assertion-stack-levels") {
1878            p.expect_matches(Token::Keyword, ":assertion-stack-levels")?;
1879            let m0 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
1880            #[allow(clippy::useless_conversion)]
1881            return Ok(Self::AssertionStackLevels(m0.into()));
1882        }
1883        if Attribute::is_start_of(offset, p) {
1884            let m0 = <Attribute<'st> as SmtlibParse<'st>>::parse(p)?;
1885            #[allow(clippy::useless_conversion)] return Ok(Self::Attribute(m0.into()));
1886        }
1887        Err(p.stuck("InfoResponse"))
1888    }
1889}
1890/// `(logic <symbol> <logic_attribute>+)`
1891#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1892#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1893pub struct Logic<'st>(pub Symbol<'st>, pub &'st [LogicAttribute<'st>]);
1894impl std::fmt::Display for Logic<'_> {
1895    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1896        write!(f, "(logic {} {})", self.0, self.1.iter().format(" "))
1897    }
1898}
1899impl<'st> Logic<'st> {
1900    pub fn parse(st: &'st Storage, src: &str) -> Result<Logic<'st>, ParseError> {
1901        <Logic<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1902    }
1903}
1904impl<'st> SmtlibParse<'st> for Logic<'st> {
1905    type Output = Logic<'st>;
1906    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1907        p.nth(offset) == Token::LParen
1908            && p.nth_matches(offset + 1, Token::Symbol, "logic")
1909    }
1910    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1911        p.expect(Token::LParen)?;
1912        p.expect_matches(Token::Symbol, "logic")?;
1913        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
1914        let m1 = p.non_zero::<LogicAttribute<'st>>()?;
1915        p.expect(Token::RParen)?;
1916        Ok(Self(m0, m1))
1917    }
1918}
1919#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1920#[cfg_attr(feature = "serde", derive(serde::Serialize))]
1921pub enum LogicAttribute<'st> {
1922    /// `<attribute>`
1923    Attribute(Attribute<'st>),
1924    /// `:extensions <string>`
1925    Extensions(&'st str),
1926    /// `:language <string>`
1927    Language(&'st str),
1928    /// `:notes <string>`
1929    Notes(&'st str),
1930    /// `:theories (<symbol>*)`
1931    Theories(&'st [Symbol<'st>]),
1932    /// `:values <string>`
1933    Values(&'st str),
1934}
1935impl std::fmt::Display for LogicAttribute<'_> {
1936    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
1937        match self {
1938            Self::Attribute(m0) => write!(f, "{}", m0),
1939            Self::Extensions(m0) => write!(f, ":extensions {}", m0),
1940            Self::Language(m0) => write!(f, ":language {}", m0),
1941            Self::Notes(m0) => write!(f, ":notes {}", m0),
1942            Self::Theories(m0) => write!(f, ":theories ({})", m0.iter().format(" ")),
1943            Self::Values(m0) => write!(f, ":values {}", m0),
1944        }
1945    }
1946}
1947impl<'st> LogicAttribute<'st> {
1948    pub fn parse(
1949        st: &'st Storage,
1950        src: &str,
1951    ) -> Result<LogicAttribute<'st>, ParseError> {
1952        <LogicAttribute<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
1953    }
1954}
1955impl<'st> SmtlibParse<'st> for LogicAttribute<'st> {
1956    type Output = LogicAttribute<'st>;
1957    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
1958        (p.nth_matches(offset, Token::Keyword, ":theories")
1959            && p.nth(offset + 1) == Token::LParen)
1960            || (p.nth_matches(offset, Token::Keyword, ":values"))
1961            || (p.nth_matches(offset, Token::Keyword, ":notes"))
1962            || (p.nth_matches(offset, Token::Keyword, ":language"))
1963            || (p.nth_matches(offset, Token::Keyword, ":extensions"))
1964            || (Attribute::is_start_of(offset, p))
1965    }
1966    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
1967        let offset = 0;
1968        if p.nth_matches(offset, Token::Keyword, ":theories")
1969            && p.nth(offset + 1) == Token::LParen
1970        {
1971            p.expect_matches(Token::Keyword, ":theories")?;
1972            p.expect(Token::LParen)?;
1973            let m0 = p.any::<Symbol<'st>>()?;
1974            p.expect(Token::RParen)?;
1975            #[allow(clippy::useless_conversion)] return Ok(Self::Theories(m0.into()));
1976        }
1977        if p.nth_matches(offset, Token::Keyword, ":values") {
1978            p.expect_matches(Token::Keyword, ":values")?;
1979            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
1980            #[allow(clippy::useless_conversion)] return Ok(Self::Values(m0.into()));
1981        }
1982        if p.nth_matches(offset, Token::Keyword, ":notes") {
1983            p.expect_matches(Token::Keyword, ":notes")?;
1984            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
1985            #[allow(clippy::useless_conversion)] return Ok(Self::Notes(m0.into()));
1986        }
1987        if p.nth_matches(offset, Token::Keyword, ":language") {
1988            p.expect_matches(Token::Keyword, ":language")?;
1989            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
1990            #[allow(clippy::useless_conversion)] return Ok(Self::Language(m0.into()));
1991        }
1992        if p.nth_matches(offset, Token::Keyword, ":extensions") {
1993            p.expect_matches(Token::Keyword, ":extensions")?;
1994            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
1995            #[allow(clippy::useless_conversion)] return Ok(Self::Extensions(m0.into()));
1996        }
1997        if Attribute::is_start_of(offset, p) {
1998            let m0 = <Attribute<'st> as SmtlibParse<'st>>::parse(p)?;
1999            #[allow(clippy::useless_conversion)] return Ok(Self::Attribute(m0.into()));
2000        }
2001        Err(p.stuck("LogicAttribute"))
2002    }
2003}
2004/// `(<pattern> <term>)`
2005#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2006#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2007pub struct MatchCase<'st>(pub Pattern<'st>, pub &'st Term<'st>);
2008impl std::fmt::Display for MatchCase<'_> {
2009    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2010        write!(f, "({} {})", self.0, self.1)
2011    }
2012}
2013impl<'st> MatchCase<'st> {
2014    pub fn parse(st: &'st Storage, src: &str) -> Result<MatchCase<'st>, ParseError> {
2015        <MatchCase<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2016    }
2017}
2018impl<'st> SmtlibParse<'st> for MatchCase<'st> {
2019    type Output = MatchCase<'st>;
2020    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2021        p.nth(offset) == Token::LParen
2022    }
2023    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2024        p.expect(Token::LParen)?;
2025        let m0 = <Pattern<'st> as SmtlibParse<'st>>::parse(p)?;
2026        let m1 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
2027        p.expect(Token::RParen)?;
2028        Ok(Self(m0, m1))
2029    }
2030}
2031#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2032#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2033pub enum MetaSpecConstant {
2034    /// `DECIMAL`
2035    Decimal,
2036    /// `NUMERAL`
2037    Numeral,
2038    /// `STRING`
2039    String,
2040}
2041impl std::fmt::Display for MetaSpecConstant {
2042    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2043        match self {
2044            Self::Decimal => write!(f, "DECIMAL"),
2045            Self::Numeral => write!(f, "NUMERAL"),
2046            Self::String => write!(f, "STRING"),
2047        }
2048    }
2049}
2050impl<'st> MetaSpecConstant {
2051    pub fn parse(st: &'st Storage, src: &str) -> Result<MetaSpecConstant, ParseError> {
2052        <MetaSpecConstant as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2053    }
2054}
2055impl<'st> SmtlibParse<'st> for MetaSpecConstant {
2056    type Output = MetaSpecConstant;
2057    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2058        (p.nth_matches(offset, Token::Reserved, "STRING"))
2059            || (p.nth_matches(offset, Token::Reserved, "NUMERAL"))
2060            || (p.nth_matches(offset, Token::Reserved, "DECIMAL"))
2061    }
2062    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2063        let offset = 0;
2064        if p.nth_matches(offset, Token::Reserved, "STRING") {
2065            p.expect_matches(Token::Reserved, "STRING")?;
2066            #[allow(clippy::useless_conversion)] return Ok(Self::String);
2067        }
2068        if p.nth_matches(offset, Token::Reserved, "NUMERAL") {
2069            p.expect_matches(Token::Reserved, "NUMERAL")?;
2070            #[allow(clippy::useless_conversion)] return Ok(Self::Numeral);
2071        }
2072        if p.nth_matches(offset, Token::Reserved, "DECIMAL") {
2073            p.expect_matches(Token::Reserved, "DECIMAL")?;
2074            #[allow(clippy::useless_conversion)] return Ok(Self::Decimal);
2075        }
2076        Err(p.stuck("MetaSpecConstant"))
2077    }
2078}
2079#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2080#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2081pub enum ModelResponse<'st> {
2082    /// `(define-fun <function_def>)`
2083    DefineFun(FunctionDef<'st>),
2084    /// `(define-fun-rec <function_def>)`
2085    DefineFunRec(FunctionDef<'st>),
2086    /// `(define-funs-rec (<function_dec>n+1) (<term>n+1))`
2087    DefineFunsRec(&'st [FunctionDec<'st>], &'st [&'st Term<'st>]),
2088}
2089impl std::fmt::Display for ModelResponse<'_> {
2090    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2091        match self {
2092            Self::DefineFun(m0) => write!(f, "(define-fun {})", m0),
2093            Self::DefineFunRec(m0) => write!(f, "(define-fun-rec {})", m0),
2094            Self::DefineFunsRec(m0, m1) => {
2095                write!(
2096                    f, "(define-funs-rec ({}) ({}))", m0.iter().format(" "), m1.iter()
2097                    .format(" ")
2098                )
2099            }
2100        }
2101    }
2102}
2103impl<'st> ModelResponse<'st> {
2104    pub fn parse(st: &'st Storage, src: &str) -> Result<ModelResponse<'st>, ParseError> {
2105        <ModelResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2106    }
2107}
2108impl<'st> SmtlibParse<'st> for ModelResponse<'st> {
2109    type Output = ModelResponse<'st>;
2110    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2111        (p.nth(offset) == Token::LParen
2112            && p.nth_matches(offset + 1, Token::Symbol, "define-funs-rec")
2113            && p.nth(offset + 2) == Token::LParen)
2114            || (p.nth(offset) == Token::LParen
2115                && p.nth_matches(offset + 1, Token::Reserved, "define-fun-rec"))
2116            || (p.nth(offset) == Token::LParen
2117                && p.nth_matches(offset + 1, Token::Reserved, "define-fun"))
2118    }
2119    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2120        let offset = 0;
2121        if p.nth(offset) == Token::LParen
2122            && p.nth_matches(offset + 1, Token::Symbol, "define-funs-rec")
2123            && p.nth(offset + 2) == Token::LParen
2124        {
2125            p.expect(Token::LParen)?;
2126            p.expect_matches(Token::Symbol, "define-funs-rec")?;
2127            p.expect(Token::LParen)?;
2128            let m0 = p.n_plus_one::<FunctionDec<'st>>()?;
2129            p.expect(Token::RParen)?;
2130            p.expect(Token::LParen)?;
2131            let m1 = p.n_plus_one::<Term<'st>>()?;
2132            p.expect(Token::RParen)?;
2133            p.expect(Token::RParen)?;
2134            #[allow(clippy::useless_conversion)]
2135            return Ok(Self::DefineFunsRec(m0.into(), m1.into()));
2136        }
2137        if p.nth(offset) == Token::LParen
2138            && p.nth_matches(offset + 1, Token::Reserved, "define-fun-rec")
2139        {
2140            p.expect(Token::LParen)?;
2141            p.expect_matches(Token::Reserved, "define-fun-rec")?;
2142            let m0 = <FunctionDef<'st> as SmtlibParse<'st>>::parse(p)?;
2143            p.expect(Token::RParen)?;
2144            #[allow(clippy::useless_conversion)]
2145            return Ok(Self::DefineFunRec(m0.into()));
2146        }
2147        if p.nth(offset) == Token::LParen
2148            && p.nth_matches(offset + 1, Token::Reserved, "define-fun")
2149        {
2150            p.expect(Token::LParen)?;
2151            p.expect_matches(Token::Reserved, "define-fun")?;
2152            let m0 = <FunctionDef<'st> as SmtlibParse<'st>>::parse(p)?;
2153            p.expect(Token::RParen)?;
2154            #[allow(clippy::useless_conversion)] return Ok(Self::DefineFun(m0.into()));
2155        }
2156        Err(p.stuck("ModelResponse"))
2157    }
2158}
2159#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2160#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2161pub enum OptimizationAttribute<'st> {
2162    /// `<attribute>`
2163    Attribute(Attribute<'st>),
2164    /// `:id <symbol>`
2165    Id(Symbol<'st>),
2166    /// `:weight <numeral>`
2167    Weight(Numeral<'st>),
2168}
2169impl std::fmt::Display for OptimizationAttribute<'_> {
2170    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2171        match self {
2172            Self::Attribute(m0) => write!(f, "{}", m0),
2173            Self::Id(m0) => write!(f, ":id {}", m0),
2174            Self::Weight(m0) => write!(f, ":weight {}", m0),
2175        }
2176    }
2177}
2178impl<'st> OptimizationAttribute<'st> {
2179    pub fn parse(
2180        st: &'st Storage,
2181        src: &str,
2182    ) -> Result<OptimizationAttribute<'st>, ParseError> {
2183        <OptimizationAttribute<
2184            'st,
2185        > as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2186    }
2187}
2188impl<'st> SmtlibParse<'st> for OptimizationAttribute<'st> {
2189    type Output = OptimizationAttribute<'st>;
2190    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2191        (p.nth_matches(offset, Token::Keyword, ":weight"))
2192            || (p.nth_matches(offset, Token::Keyword, ":id"))
2193            || (Attribute::is_start_of(offset, p))
2194    }
2195    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2196        let offset = 0;
2197        if p.nth_matches(offset, Token::Keyword, ":weight") {
2198            p.expect_matches(Token::Keyword, ":weight")?;
2199            let m0 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
2200            #[allow(clippy::useless_conversion)] return Ok(Self::Weight(m0.into()));
2201        }
2202        if p.nth_matches(offset, Token::Keyword, ":id") {
2203            p.expect_matches(Token::Keyword, ":id")?;
2204            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
2205            #[allow(clippy::useless_conversion)] return Ok(Self::Id(m0.into()));
2206        }
2207        if Attribute::is_start_of(offset, p) {
2208            let m0 = <Attribute<'st> as SmtlibParse<'st>>::parse(p)?;
2209            #[allow(clippy::useless_conversion)] return Ok(Self::Attribute(m0.into()));
2210        }
2211        Err(p.stuck("OptimizationAttribute"))
2212    }
2213}
2214#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2215#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2216pub enum OptimizationPriority {
2217    /// `box`
2218    Box,
2219    /// `lex`
2220    Lex,
2221    /// `pareto`
2222    Pareto,
2223}
2224impl std::fmt::Display for OptimizationPriority {
2225    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2226        match self {
2227            Self::Box => write!(f, "box"),
2228            Self::Lex => write!(f, "lex"),
2229            Self::Pareto => write!(f, "pareto"),
2230        }
2231    }
2232}
2233impl<'st> OptimizationPriority {
2234    pub fn parse(
2235        st: &'st Storage,
2236        src: &str,
2237    ) -> Result<OptimizationPriority, ParseError> {
2238        <OptimizationPriority as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2239    }
2240}
2241impl<'st> SmtlibParse<'st> for OptimizationPriority {
2242    type Output = OptimizationPriority;
2243    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2244        (p.nth_matches(offset, Token::Symbol, "pareto"))
2245            || (p.nth_matches(offset, Token::Symbol, "lex"))
2246            || (p.nth_matches(offset, Token::Symbol, "box"))
2247    }
2248    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2249        let offset = 0;
2250        if p.nth_matches(offset, Token::Symbol, "pareto") {
2251            p.expect_matches(Token::Symbol, "pareto")?;
2252            #[allow(clippy::useless_conversion)] return Ok(Self::Pareto);
2253        }
2254        if p.nth_matches(offset, Token::Symbol, "lex") {
2255            p.expect_matches(Token::Symbol, "lex")?;
2256            #[allow(clippy::useless_conversion)] return Ok(Self::Lex);
2257        }
2258        if p.nth_matches(offset, Token::Symbol, "box") {
2259            p.expect_matches(Token::Symbol, "box")?;
2260            #[allow(clippy::useless_conversion)] return Ok(Self::Box);
2261        }
2262        Err(p.stuck("OptimizationPriority"))
2263    }
2264}
2265#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2266#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2267pub enum Option<'st> {
2268    /// `<attribute>`
2269    Attribute(Attribute<'st>),
2270    /// `:diagnostic-output-channel <string>`
2271    DiagnosticOutputChannel(&'st str),
2272    /// `:global-declarations <b_value>`
2273    GlobalDeclarations(BValue),
2274    /// `:interactive-mode <b_value>`
2275    InteractiveMode(BValue),
2276    /// `:opt.priority <optimization_priority>`
2277    OptPriority(OptimizationPriority),
2278    /// `:print-success <b_value>`
2279    PrintSuccess(BValue),
2280    /// `:produce-assertions <b_value>`
2281    ProduceAssertions(BValue),
2282    /// `:produce-assignments <b_value>`
2283    ProduceAssignments(BValue),
2284    /// `:produce-models <b_value>`
2285    ProduceModels(BValue),
2286    /// `:produce-proofs <b_value>`
2287    ProduceProofs(BValue),
2288    /// `:produce-unsat-assumptions <b_value>`
2289    ProduceUnsatAssumptions(BValue),
2290    /// `:produce-unsat-cores <b_value>`
2291    ProduceUnsatCores(BValue),
2292    /// `:random-seed <numeral>`
2293    RandomSeed(Numeral<'st>),
2294    /// `:regular-output-channel <string>`
2295    RegularOutputChannel(&'st str),
2296    /// `:reproducible-resource-limit <numeral>`
2297    ReproducibleResourceLimit(Numeral<'st>),
2298    /// `:verbosity <numeral>`
2299    Verbosity(Numeral<'st>),
2300}
2301impl std::fmt::Display for Option<'_> {
2302    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2303        match self {
2304            Self::Attribute(m0) => write!(f, "{}", m0),
2305            Self::DiagnosticOutputChannel(m0) => {
2306                write!(f, ":diagnostic-output-channel {}", m0)
2307            }
2308            Self::GlobalDeclarations(m0) => write!(f, ":global-declarations {}", m0),
2309            Self::InteractiveMode(m0) => write!(f, ":interactive-mode {}", m0),
2310            Self::OptPriority(m0) => write!(f, ":opt.priority {}", m0),
2311            Self::PrintSuccess(m0) => write!(f, ":print-success {}", m0),
2312            Self::ProduceAssertions(m0) => write!(f, ":produce-assertions {}", m0),
2313            Self::ProduceAssignments(m0) => write!(f, ":produce-assignments {}", m0),
2314            Self::ProduceModels(m0) => write!(f, ":produce-models {}", m0),
2315            Self::ProduceProofs(m0) => write!(f, ":produce-proofs {}", m0),
2316            Self::ProduceUnsatAssumptions(m0) => {
2317                write!(f, ":produce-unsat-assumptions {}", m0)
2318            }
2319            Self::ProduceUnsatCores(m0) => write!(f, ":produce-unsat-cores {}", m0),
2320            Self::RandomSeed(m0) => write!(f, ":random-seed {}", m0),
2321            Self::RegularOutputChannel(m0) => write!(f, ":regular-output-channel {}", m0),
2322            Self::ReproducibleResourceLimit(m0) => {
2323                write!(f, ":reproducible-resource-limit {}", m0)
2324            }
2325            Self::Verbosity(m0) => write!(f, ":verbosity {}", m0),
2326        }
2327    }
2328}
2329impl<'st> Option<'st> {
2330    pub fn parse(st: &'st Storage, src: &str) -> Result<Option<'st>, ParseError> {
2331        <Option<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2332    }
2333}
2334impl<'st> SmtlibParse<'st> for Option<'st> {
2335    type Output = Option<'st>;
2336    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2337        (p.nth_matches(offset, Token::Keyword, ":verbosity"))
2338            || (p.nth_matches(offset, Token::Keyword, ":reproducible-resource-limit"))
2339            || (p.nth_matches(offset, Token::Keyword, ":regular-output-channel"))
2340            || (p.nth_matches(offset, Token::Keyword, ":random-seed"))
2341            || (p.nth_matches(offset, Token::Keyword, ":produce-unsat-cores"))
2342            || (p.nth_matches(offset, Token::Keyword, ":produce-unsat-assumptions"))
2343            || (p.nth_matches(offset, Token::Keyword, ":produce-proofs"))
2344            || (p.nth_matches(offset, Token::Keyword, ":produce-models"))
2345            || (p.nth_matches(offset, Token::Keyword, ":produce-assignments"))
2346            || (p.nth_matches(offset, Token::Keyword, ":produce-assertions"))
2347            || (p.nth_matches(offset, Token::Keyword, ":print-success"))
2348            || (p.nth_matches(offset, Token::Keyword, ":opt.priority"))
2349            || (p.nth_matches(offset, Token::Keyword, ":interactive-mode"))
2350            || (p.nth_matches(offset, Token::Keyword, ":global-declarations"))
2351            || (p.nth_matches(offset, Token::Keyword, ":diagnostic-output-channel"))
2352            || (Attribute::is_start_of(offset, p))
2353    }
2354    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2355        let offset = 0;
2356        if p.nth_matches(offset, Token::Keyword, ":verbosity") {
2357            p.expect_matches(Token::Keyword, ":verbosity")?;
2358            let m0 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
2359            #[allow(clippy::useless_conversion)] return Ok(Self::Verbosity(m0.into()));
2360        }
2361        if p.nth_matches(offset, Token::Keyword, ":reproducible-resource-limit") {
2362            p.expect_matches(Token::Keyword, ":reproducible-resource-limit")?;
2363            let m0 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
2364            #[allow(clippy::useless_conversion)]
2365            return Ok(Self::ReproducibleResourceLimit(m0.into()));
2366        }
2367        if p.nth_matches(offset, Token::Keyword, ":regular-output-channel") {
2368            p.expect_matches(Token::Keyword, ":regular-output-channel")?;
2369            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
2370            #[allow(clippy::useless_conversion)]
2371            return Ok(Self::RegularOutputChannel(m0.into()));
2372        }
2373        if p.nth_matches(offset, Token::Keyword, ":random-seed") {
2374            p.expect_matches(Token::Keyword, ":random-seed")?;
2375            let m0 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
2376            #[allow(clippy::useless_conversion)] return Ok(Self::RandomSeed(m0.into()));
2377        }
2378        if p.nth_matches(offset, Token::Keyword, ":produce-unsat-cores") {
2379            p.expect_matches(Token::Keyword, ":produce-unsat-cores")?;
2380            let m0 = <BValue as SmtlibParse<'st>>::parse(p)?;
2381            #[allow(clippy::useless_conversion)]
2382            return Ok(Self::ProduceUnsatCores(m0.into()));
2383        }
2384        if p.nth_matches(offset, Token::Keyword, ":produce-unsat-assumptions") {
2385            p.expect_matches(Token::Keyword, ":produce-unsat-assumptions")?;
2386            let m0 = <BValue as SmtlibParse<'st>>::parse(p)?;
2387            #[allow(clippy::useless_conversion)]
2388            return Ok(Self::ProduceUnsatAssumptions(m0.into()));
2389        }
2390        if p.nth_matches(offset, Token::Keyword, ":produce-proofs") {
2391            p.expect_matches(Token::Keyword, ":produce-proofs")?;
2392            let m0 = <BValue as SmtlibParse<'st>>::parse(p)?;
2393            #[allow(clippy::useless_conversion)]
2394            return Ok(Self::ProduceProofs(m0.into()));
2395        }
2396        if p.nth_matches(offset, Token::Keyword, ":produce-models") {
2397            p.expect_matches(Token::Keyword, ":produce-models")?;
2398            let m0 = <BValue as SmtlibParse<'st>>::parse(p)?;
2399            #[allow(clippy::useless_conversion)]
2400            return Ok(Self::ProduceModels(m0.into()));
2401        }
2402        if p.nth_matches(offset, Token::Keyword, ":produce-assignments") {
2403            p.expect_matches(Token::Keyword, ":produce-assignments")?;
2404            let m0 = <BValue as SmtlibParse<'st>>::parse(p)?;
2405            #[allow(clippy::useless_conversion)]
2406            return Ok(Self::ProduceAssignments(m0.into()));
2407        }
2408        if p.nth_matches(offset, Token::Keyword, ":produce-assertions") {
2409            p.expect_matches(Token::Keyword, ":produce-assertions")?;
2410            let m0 = <BValue as SmtlibParse<'st>>::parse(p)?;
2411            #[allow(clippy::useless_conversion)]
2412            return Ok(Self::ProduceAssertions(m0.into()));
2413        }
2414        if p.nth_matches(offset, Token::Keyword, ":print-success") {
2415            p.expect_matches(Token::Keyword, ":print-success")?;
2416            let m0 = <BValue as SmtlibParse<'st>>::parse(p)?;
2417            #[allow(clippy::useless_conversion)]
2418            return Ok(Self::PrintSuccess(m0.into()));
2419        }
2420        if p.nth_matches(offset, Token::Keyword, ":opt.priority") {
2421            p.expect_matches(Token::Keyword, ":opt.priority")?;
2422            let m0 = <OptimizationPriority as SmtlibParse<'st>>::parse(p)?;
2423            #[allow(clippy::useless_conversion)] return Ok(Self::OptPriority(m0.into()));
2424        }
2425        if p.nth_matches(offset, Token::Keyword, ":interactive-mode") {
2426            p.expect_matches(Token::Keyword, ":interactive-mode")?;
2427            let m0 = <BValue as SmtlibParse<'st>>::parse(p)?;
2428            #[allow(clippy::useless_conversion)]
2429            return Ok(Self::InteractiveMode(m0.into()));
2430        }
2431        if p.nth_matches(offset, Token::Keyword, ":global-declarations") {
2432            p.expect_matches(Token::Keyword, ":global-declarations")?;
2433            let m0 = <BValue as SmtlibParse<'st>>::parse(p)?;
2434            #[allow(clippy::useless_conversion)]
2435            return Ok(Self::GlobalDeclarations(m0.into()));
2436        }
2437        if p.nth_matches(offset, Token::Keyword, ":diagnostic-output-channel") {
2438            p.expect_matches(Token::Keyword, ":diagnostic-output-channel")?;
2439            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
2440            #[allow(clippy::useless_conversion)]
2441            return Ok(Self::DiagnosticOutputChannel(m0.into()));
2442        }
2443        if Attribute::is_start_of(offset, p) {
2444            let m0 = <Attribute<'st> as SmtlibParse<'st>>::parse(p)?;
2445            #[allow(clippy::useless_conversion)] return Ok(Self::Attribute(m0.into()));
2446        }
2447        Err(p.stuck("Option"))
2448    }
2449}
2450#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2451#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2452pub enum ParFunSymbolDecl<'st> {
2453    /// `<fun_symbol_decl>`
2454    FunSymbolDecl(FunSymbolDecl<'st>),
2455    /// `(par (<symbol>+) (<identifier> <sort>+ <attribute>*))`
2456    Par(&'st [Symbol<'st>], Identifier<'st>, &'st [Sort<'st>], &'st [Attribute<'st>]),
2457}
2458impl std::fmt::Display for ParFunSymbolDecl<'_> {
2459    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2460        match self {
2461            Self::FunSymbolDecl(m0) => write!(f, "{}", m0),
2462            Self::Par(m0, m1, m2, m3) => {
2463                write!(
2464                    f, "(par ({}) ({} {} {}))", m0.iter().format(" "), m1, m2.iter()
2465                    .format(" "), m3.iter().format(" ")
2466                )
2467            }
2468        }
2469    }
2470}
2471impl<'st> ParFunSymbolDecl<'st> {
2472    pub fn parse(
2473        st: &'st Storage,
2474        src: &str,
2475    ) -> Result<ParFunSymbolDecl<'st>, ParseError> {
2476        <ParFunSymbolDecl<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2477    }
2478}
2479impl<'st> SmtlibParse<'st> for ParFunSymbolDecl<'st> {
2480    type Output = ParFunSymbolDecl<'st>;
2481    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2482        (p.nth(offset) == Token::LParen
2483            && p.nth_matches(offset + 1, Token::Reserved, "par")
2484            && p.nth(offset + 2) == Token::LParen)
2485            || (FunSymbolDecl::is_start_of(offset, p))
2486    }
2487    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2488        let offset = 0;
2489        if p.nth(offset) == Token::LParen
2490            && p.nth_matches(offset + 1, Token::Reserved, "par")
2491            && p.nth(offset + 2) == Token::LParen
2492        {
2493            p.expect(Token::LParen)?;
2494            p.expect_matches(Token::Reserved, "par")?;
2495            p.expect(Token::LParen)?;
2496            let m0 = p.non_zero::<Symbol<'st>>()?;
2497            p.expect(Token::RParen)?;
2498            p.expect(Token::LParen)?;
2499            let m1 = <Identifier<'st> as SmtlibParse<'st>>::parse(p)?;
2500            let m2 = p.non_zero::<Sort<'st>>()?;
2501            let m3 = p.any::<Attribute<'st>>()?;
2502            p.expect(Token::RParen)?;
2503            p.expect(Token::RParen)?;
2504            #[allow(clippy::useless_conversion)]
2505            return Ok(Self::Par(m0.into(), m1.into(), m2.into(), m3.into()));
2506        }
2507        if FunSymbolDecl::is_start_of(offset, p) {
2508            let m0 = <FunSymbolDecl<'st> as SmtlibParse<'st>>::parse(p)?;
2509            #[allow(clippy::useless_conversion)]
2510            return Ok(Self::FunSymbolDecl(m0.into()));
2511        }
2512        Err(p.stuck("ParFunSymbolDecl"))
2513    }
2514}
2515#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2516#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2517pub enum Pattern<'st> {
2518    /// `(<symbol> <symbol>+)`
2519    Application(Symbol<'st>, &'st [Symbol<'st>]),
2520    /// `<symbol>`
2521    Symbol(Symbol<'st>),
2522}
2523impl std::fmt::Display for Pattern<'_> {
2524    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2525        match self {
2526            Self::Application(m0, m1) => write!(f, "({} {})", m0, m1.iter().format(" ")),
2527            Self::Symbol(m0) => write!(f, "{}", m0),
2528        }
2529    }
2530}
2531impl<'st> Pattern<'st> {
2532    pub fn parse(st: &'st Storage, src: &str) -> Result<Pattern<'st>, ParseError> {
2533        <Pattern<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2534    }
2535}
2536impl<'st> SmtlibParse<'st> for Pattern<'st> {
2537    type Output = Pattern<'st>;
2538    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2539        (p.nth(offset) == Token::LParen) || (Symbol::is_start_of(offset, p))
2540    }
2541    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2542        let offset = 0;
2543        if p.nth(offset) == Token::LParen {
2544            p.expect(Token::LParen)?;
2545            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
2546            let m1 = p.non_zero::<Symbol<'st>>()?;
2547            p.expect(Token::RParen)?;
2548            #[allow(clippy::useless_conversion)]
2549            return Ok(Self::Application(m0.into(), m1.into()));
2550        }
2551        if Symbol::is_start_of(offset, p) {
2552            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
2553            #[allow(clippy::useless_conversion)] return Ok(Self::Symbol(m0.into()));
2554        }
2555        Err(p.stuck("Pattern"))
2556    }
2557}
2558#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2559#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2560pub enum PropLiteral<'st> {
2561    /// `(not <symbol>)`
2562    Not(Symbol<'st>),
2563    /// `<symbol>`
2564    Symbol(Symbol<'st>),
2565}
2566impl std::fmt::Display for PropLiteral<'_> {
2567    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2568        match self {
2569            Self::Not(m0) => write!(f, "(not {})", m0),
2570            Self::Symbol(m0) => write!(f, "{}", m0),
2571        }
2572    }
2573}
2574impl<'st> PropLiteral<'st> {
2575    pub fn parse(st: &'st Storage, src: &str) -> Result<PropLiteral<'st>, ParseError> {
2576        <PropLiteral<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2577    }
2578}
2579impl<'st> SmtlibParse<'st> for PropLiteral<'st> {
2580    type Output = PropLiteral<'st>;
2581    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2582        (p.nth(offset) == Token::LParen
2583            && p.nth_matches(offset + 1, Token::Symbol, "not"))
2584            || (Symbol::is_start_of(offset, p))
2585    }
2586    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2587        let offset = 0;
2588        if p.nth(offset) == Token::LParen
2589            && p.nth_matches(offset + 1, Token::Symbol, "not")
2590        {
2591            p.expect(Token::LParen)?;
2592            p.expect_matches(Token::Symbol, "not")?;
2593            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
2594            p.expect(Token::RParen)?;
2595            #[allow(clippy::useless_conversion)] return Ok(Self::Not(m0.into()));
2596        }
2597        if Symbol::is_start_of(offset, p) {
2598            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
2599            #[allow(clippy::useless_conversion)] return Ok(Self::Symbol(m0.into()));
2600        }
2601        Err(p.stuck("PropLiteral"))
2602    }
2603}
2604#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2605#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2606pub enum QualIdentifier<'st> {
2607    /// `<identifier>`
2608    Identifier(Identifier<'st>),
2609    /// `(as <identifier> <sort>)`
2610    Sorted(Identifier<'st>, Sort<'st>),
2611}
2612impl std::fmt::Display for QualIdentifier<'_> {
2613    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2614        match self {
2615            Self::Identifier(m0) => write!(f, "{}", m0),
2616            Self::Sorted(m0, m1) => write!(f, "(as {} {})", m0, m1),
2617        }
2618    }
2619}
2620impl<'st> QualIdentifier<'st> {
2621    pub fn parse(
2622        st: &'st Storage,
2623        src: &str,
2624    ) -> Result<QualIdentifier<'st>, ParseError> {
2625        <QualIdentifier<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2626    }
2627}
2628impl<'st> SmtlibParse<'st> for QualIdentifier<'st> {
2629    type Output = QualIdentifier<'st>;
2630    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2631        (p.nth(offset) == Token::LParen
2632            && p.nth_matches(offset + 1, Token::Reserved, "as"))
2633            || (Identifier::is_start_of(offset, p))
2634    }
2635    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2636        let offset = 0;
2637        if p.nth(offset) == Token::LParen
2638            && p.nth_matches(offset + 1, Token::Reserved, "as")
2639        {
2640            p.expect(Token::LParen)?;
2641            p.expect_matches(Token::Reserved, "as")?;
2642            let m0 = <Identifier<'st> as SmtlibParse<'st>>::parse(p)?;
2643            let m1 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
2644            p.expect(Token::RParen)?;
2645            #[allow(clippy::useless_conversion)]
2646            return Ok(Self::Sorted(m0.into(), m1.into()));
2647        }
2648        if Identifier::is_start_of(offset, p) {
2649            let m0 = <Identifier<'st> as SmtlibParse<'st>>::parse(p)?;
2650            #[allow(clippy::useless_conversion)] return Ok(Self::Identifier(m0.into()));
2651        }
2652        Err(p.stuck("QualIdentifier"))
2653    }
2654}
2655#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2656#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2657pub enum ReasonUnknown<'st> {
2658    /// `incomplete`
2659    Incomplete,
2660    /// `memout`
2661    Memout,
2662    /// `<s_expr>`
2663    SExpr(SExpr<'st>),
2664}
2665impl std::fmt::Display for ReasonUnknown<'_> {
2666    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2667        match self {
2668            Self::Incomplete => write!(f, "incomplete"),
2669            Self::Memout => write!(f, "memout"),
2670            Self::SExpr(m0) => write!(f, "{}", m0),
2671        }
2672    }
2673}
2674impl<'st> ReasonUnknown<'st> {
2675    pub fn parse(st: &'st Storage, src: &str) -> Result<ReasonUnknown<'st>, ParseError> {
2676        <ReasonUnknown<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2677    }
2678}
2679impl<'st> SmtlibParse<'st> for ReasonUnknown<'st> {
2680    type Output = ReasonUnknown<'st>;
2681    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2682        (p.nth_matches(offset, Token::Symbol, "memout"))
2683            || (p.nth_matches(offset, Token::Symbol, "incomplete"))
2684            || (SExpr::is_start_of(offset, p))
2685    }
2686    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2687        let offset = 0;
2688        if p.nth_matches(offset, Token::Symbol, "memout") {
2689            p.expect_matches(Token::Symbol, "memout")?;
2690            #[allow(clippy::useless_conversion)] return Ok(Self::Memout);
2691        }
2692        if p.nth_matches(offset, Token::Symbol, "incomplete") {
2693            p.expect_matches(Token::Symbol, "incomplete")?;
2694            #[allow(clippy::useless_conversion)] return Ok(Self::Incomplete);
2695        }
2696        if SExpr::is_start_of(offset, p) {
2697            let m0 = <SExpr<'st> as SmtlibParse<'st>>::parse(p)?;
2698            #[allow(clippy::useless_conversion)] return Ok(Self::SExpr(m0.into()));
2699        }
2700        Err(p.stuck("ReasonUnknown"))
2701    }
2702}
2703#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2704#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2705pub enum SExpr<'st> {
2706    /// `<keyword>`
2707    Keyword(Keyword<'st>),
2708    /// `(<s_expr>*)`
2709    Paren(&'st [SExpr<'st>]),
2710    /// `<reserved>`
2711    Reserved(Reserved<'st>),
2712    /// `<spec_constant>`
2713    SpecConstant(SpecConstant<'st>),
2714    /// `<symbol>`
2715    Symbol(Symbol<'st>),
2716}
2717impl std::fmt::Display for SExpr<'_> {
2718    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2719        match self {
2720            Self::Keyword(m0) => write!(f, "{}", m0),
2721            Self::Paren(m0) => write!(f, "({})", m0.iter().format(" ")),
2722            Self::Reserved(m0) => write!(f, "{}", m0),
2723            Self::SpecConstant(m0) => write!(f, "{}", m0),
2724            Self::Symbol(m0) => write!(f, "{}", m0),
2725        }
2726    }
2727}
2728impl<'st> SExpr<'st> {
2729    pub fn parse(st: &'st Storage, src: &str) -> Result<SExpr<'st>, ParseError> {
2730        <SExpr<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2731    }
2732}
2733impl<'st> SmtlibParse<'st> for SExpr<'st> {
2734    type Output = SExpr<'st>;
2735    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2736        (p.nth(offset) == Token::LParen) || (Symbol::is_start_of(offset, p))
2737            || (SpecConstant::is_start_of(offset, p))
2738            || (Reserved::is_start_of(offset, p)) || (Keyword::is_start_of(offset, p))
2739    }
2740    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2741        let offset = 0;
2742        if p.nth(offset) == Token::LParen {
2743            p.expect(Token::LParen)?;
2744            let m0 = p.any::<SExpr<'st>>()?;
2745            p.expect(Token::RParen)?;
2746            #[allow(clippy::useless_conversion)] return Ok(Self::Paren(m0.into()));
2747        }
2748        if Symbol::is_start_of(offset, p) {
2749            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
2750            #[allow(clippy::useless_conversion)] return Ok(Self::Symbol(m0.into()));
2751        }
2752        if SpecConstant::is_start_of(offset, p) {
2753            let m0 = <SpecConstant<'st> as SmtlibParse<'st>>::parse(p)?;
2754            #[allow(clippy::useless_conversion)]
2755            return Ok(Self::SpecConstant(m0.into()));
2756        }
2757        if Reserved::is_start_of(offset, p) {
2758            let m0 = <Reserved<'st> as SmtlibParse<'st>>::parse(p)?;
2759            #[allow(clippy::useless_conversion)] return Ok(Self::Reserved(m0.into()));
2760        }
2761        if Keyword::is_start_of(offset, p) {
2762            let m0 = <Keyword<'st> as SmtlibParse<'st>>::parse(p)?;
2763            #[allow(clippy::useless_conversion)] return Ok(Self::Keyword(m0.into()));
2764        }
2765        Err(p.stuck("SExpr"))
2766    }
2767}
2768/// `<command>*`
2769#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2770#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2771pub struct Script<'st>(pub &'st [Command<'st>]);
2772impl std::fmt::Display for Script<'_> {
2773    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2774        write!(f, "{}", self.0.iter().format("\n"))
2775    }
2776}
2777impl<'st> Script<'st> {
2778    pub fn parse(st: &'st Storage, src: &str) -> Result<Script<'st>, ParseError> {
2779        <Script<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2780    }
2781}
2782impl<'st> SmtlibParse<'st> for Script<'st> {
2783    type Output = Script<'st>;
2784    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2785        todo!("{offset:?}, {p:?}")
2786    }
2787    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2788        let m0 = p.any::<Command<'st>>()?;
2789        Ok(Self(m0))
2790    }
2791}
2792/// `(<symbol> <sort>)`
2793#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2794#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2795pub struct SelectorDec<'st>(pub Symbol<'st>, pub Sort<'st>);
2796impl std::fmt::Display for SelectorDec<'_> {
2797    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2798        write!(f, "({} {})", self.0, self.1)
2799    }
2800}
2801impl<'st> SelectorDec<'st> {
2802    pub fn parse(st: &'st Storage, src: &str) -> Result<SelectorDec<'st>, ParseError> {
2803        <SelectorDec<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2804    }
2805}
2806impl<'st> SmtlibParse<'st> for SelectorDec<'st> {
2807    type Output = SelectorDec<'st>;
2808    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2809        p.nth(offset) == Token::LParen
2810    }
2811    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2812        p.expect(Token::LParen)?;
2813        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
2814        let m1 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
2815        p.expect(Token::RParen)?;
2816        Ok(Self(m0, m1))
2817    }
2818}
2819/// `<term>`
2820#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2821#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2822pub struct SimplifyResponse<'st>(pub &'st Term<'st>);
2823impl std::fmt::Display for SimplifyResponse<'_> {
2824    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2825        write!(f, "{}", self.0)
2826    }
2827}
2828impl<'st> SimplifyResponse<'st> {
2829    pub fn parse(
2830        st: &'st Storage,
2831        src: &str,
2832    ) -> Result<SimplifyResponse<'st>, ParseError> {
2833        <SimplifyResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2834    }
2835}
2836impl<'st> SmtlibParse<'st> for SimplifyResponse<'st> {
2837    type Output = SimplifyResponse<'st>;
2838    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2839        Term::is_start_of(offset, p)
2840    }
2841    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2842        let m0 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
2843        Ok(Self(m0))
2844    }
2845}
2846#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2847#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2848pub enum Sort<'st> {
2849    /// `(<identifier> <sort>+)`
2850    Parametric(Identifier<'st>, &'st [Sort<'st>]),
2851    /// `<identifier>`
2852    Sort(Identifier<'st>),
2853}
2854impl std::fmt::Display for Sort<'_> {
2855    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2856        match self {
2857            Self::Parametric(m0, m1) => write!(f, "({} {})", m0, m1.iter().format(" ")),
2858            Self::Sort(m0) => write!(f, "{}", m0),
2859        }
2860    }
2861}
2862impl<'st> Sort<'st> {
2863    pub fn parse(st: &'st Storage, src: &str) -> Result<Sort<'st>, ParseError> {
2864        <Sort<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2865    }
2866}
2867impl<'st> SmtlibParse<'st> for Sort<'st> {
2868    type Output = Sort<'st>;
2869    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2870        (Identifier::is_start_of(offset, p)) || (p.nth(offset) == Token::LParen)
2871    }
2872    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2873        let offset = 0;
2874        if Identifier::is_start_of(offset, p) {
2875            let m0 = <Identifier<'st> as SmtlibParse<'st>>::parse(p)?;
2876            #[allow(clippy::useless_conversion)] return Ok(Self::Sort(m0.into()));
2877        }
2878        if p.nth(offset) == Token::LParen {
2879            p.expect(Token::LParen)?;
2880            let m0 = <Identifier<'st> as SmtlibParse<'st>>::parse(p)?;
2881            let m1 = p.non_zero::<Sort<'st>>()?;
2882            p.expect(Token::RParen)?;
2883            #[allow(clippy::useless_conversion)]
2884            return Ok(Self::Parametric(m0.into(), m1.into()));
2885        }
2886        Err(p.stuck("Sort"))
2887    }
2888}
2889/// `(<symbol> <numeral>)`
2890#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2891#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2892pub struct SortDec<'st>(pub Symbol<'st>, pub Numeral<'st>);
2893impl std::fmt::Display for SortDec<'_> {
2894    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2895        write!(f, "({} {})", self.0, self.1)
2896    }
2897}
2898impl<'st> SortDec<'st> {
2899    pub fn parse(st: &'st Storage, src: &str) -> Result<SortDec<'st>, ParseError> {
2900        <SortDec<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2901    }
2902}
2903impl<'st> SmtlibParse<'st> for SortDec<'st> {
2904    type Output = SortDec<'st>;
2905    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2906        p.nth(offset) == Token::LParen
2907    }
2908    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2909        p.expect(Token::LParen)?;
2910        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
2911        let m1 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
2912        p.expect(Token::RParen)?;
2913        Ok(Self(m0, m1))
2914    }
2915}
2916/// `(<identifier> <numeral> <attribute>*)`
2917#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2918#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2919pub struct SortSymbolDecl<'st>(
2920    pub Identifier<'st>,
2921    pub Numeral<'st>,
2922    pub &'st [Attribute<'st>],
2923);
2924impl std::fmt::Display for SortSymbolDecl<'_> {
2925    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2926        write!(f, "({} {} {})", self.0, self.1, self.2.iter().format(" "))
2927    }
2928}
2929impl<'st> SortSymbolDecl<'st> {
2930    pub fn parse(
2931        st: &'st Storage,
2932        src: &str,
2933    ) -> Result<SortSymbolDecl<'st>, ParseError> {
2934        <SortSymbolDecl<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2935    }
2936}
2937impl<'st> SmtlibParse<'st> for SortSymbolDecl<'st> {
2938    type Output = SortSymbolDecl<'st>;
2939    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2940        p.nth(offset) == Token::LParen
2941    }
2942    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2943        p.expect(Token::LParen)?;
2944        let m0 = <Identifier<'st> as SmtlibParse<'st>>::parse(p)?;
2945        let m1 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
2946        let m2 = p.any::<Attribute<'st>>()?;
2947        p.expect(Token::RParen)?;
2948        Ok(Self(m0, m1, m2))
2949    }
2950}
2951/// `(<symbol> <sort>)`
2952#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2953#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2954pub struct SortedVar<'st>(pub Symbol<'st>, pub Sort<'st>);
2955impl std::fmt::Display for SortedVar<'_> {
2956    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2957        write!(f, "({} {})", self.0, self.1)
2958    }
2959}
2960impl<'st> SortedVar<'st> {
2961    pub fn parse(st: &'st Storage, src: &str) -> Result<SortedVar<'st>, ParseError> {
2962        <SortedVar<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
2963    }
2964}
2965impl<'st> SmtlibParse<'st> for SortedVar<'st> {
2966    type Output = SortedVar<'st>;
2967    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
2968        p.nth(offset) == Token::LParen
2969    }
2970    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
2971        p.expect(Token::LParen)?;
2972        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
2973        let m1 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
2974        p.expect(Token::RParen)?;
2975        Ok(Self(m0, m1))
2976    }
2977}
2978#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
2979#[cfg_attr(feature = "serde", derive(serde::Serialize))]
2980pub enum SpecConstant<'st> {
2981    /// `<binary>`
2982    Binary(Binary<'st>),
2983    /// `<decimal>`
2984    Decimal(Decimal<'st>),
2985    /// `<hexadecimal>`
2986    Hexadecimal(Hexadecimal<'st>),
2987    /// `<numeral>`
2988    Numeral(Numeral<'st>),
2989    /// `<string>`
2990    String(&'st str),
2991}
2992impl std::fmt::Display for SpecConstant<'_> {
2993    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2994        match self {
2995            Self::Binary(m0) => write!(f, "{}", m0),
2996            Self::Decimal(m0) => write!(f, "{}", m0),
2997            Self::Hexadecimal(m0) => write!(f, "{}", m0),
2998            Self::Numeral(m0) => write!(f, "{}", m0),
2999            Self::String(m0) => write!(f, "{}", m0),
3000        }
3001    }
3002}
3003impl<'st> SpecConstant<'st> {
3004    pub fn parse(st: &'st Storage, src: &str) -> Result<SpecConstant<'st>, ParseError> {
3005        <SpecConstant<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
3006    }
3007}
3008impl<'st> SmtlibParse<'st> for SpecConstant<'st> {
3009    type Output = SpecConstant<'st>;
3010    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
3011        (String::is_start_of(offset, p)) || (Numeral::is_start_of(offset, p))
3012            || (Hexadecimal::is_start_of(offset, p)) || (Decimal::is_start_of(offset, p))
3013            || (Binary::is_start_of(offset, p))
3014    }
3015    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
3016        let offset = 0;
3017        if String::is_start_of(offset, p) {
3018            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
3019            #[allow(clippy::useless_conversion)] return Ok(Self::String(m0.into()));
3020        }
3021        if Numeral::is_start_of(offset, p) {
3022            let m0 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
3023            #[allow(clippy::useless_conversion)] return Ok(Self::Numeral(m0.into()));
3024        }
3025        if Hexadecimal::is_start_of(offset, p) {
3026            let m0 = <Hexadecimal<'st> as SmtlibParse<'st>>::parse(p)?;
3027            #[allow(clippy::useless_conversion)] return Ok(Self::Hexadecimal(m0.into()));
3028        }
3029        if Decimal::is_start_of(offset, p) {
3030            let m0 = <Decimal<'st> as SmtlibParse<'st>>::parse(p)?;
3031            #[allow(clippy::useless_conversion)] return Ok(Self::Decimal(m0.into()));
3032        }
3033        if Binary::is_start_of(offset, p) {
3034            let m0 = <Binary<'st> as SmtlibParse<'st>>::parse(p)?;
3035            #[allow(clippy::useless_conversion)] return Ok(Self::Binary(m0.into()));
3036        }
3037        Err(p.stuck("SpecConstant"))
3038    }
3039}
3040#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
3041#[cfg_attr(feature = "serde", derive(serde::Serialize))]
3042pub enum SpecificSuccessResponse<'st> {
3043    /// `<check_sat_response>`
3044    CheckSatResponse(CheckSatResponse),
3045    /// `<echo_response>`
3046    EchoResponse(EchoResponse<'st>),
3047    /// `<eval_response>`
3048    EvalResponse(EvalResponse<'st>),
3049    /// `<get_assertions_response>`
3050    GetAssertionsResponse(GetAssertionsResponse<'st>),
3051    /// `<get_assignment_response>`
3052    GetAssignmentResponse(GetAssignmentResponse<'st>),
3053    /// `<get_info_response>`
3054    GetInfoResponse(GetInfoResponse<'st>),
3055    /// `<get_model_response>`
3056    GetModelResponse(GetModelResponse<'st>),
3057    /// `<get_option_response>`
3058    GetOptionResponse(GetOptionResponse<'st>),
3059    /// `<get_proof_response>`
3060    GetProofResponse(GetProofResponse<'st>),
3061    /// `<get_unsat_assumptions_response>`
3062    GetUnsatAssumptionsResponse(GetUnsatAssumptionsResponse<'st>),
3063    /// `<get_unsat_core_response>`
3064    GetUnsatCoreResponse(GetUnsatCoreResponse<'st>),
3065    /// `<get_value_response>`
3066    GetValueResponse(GetValueResponse<'st>),
3067    /// `<simplify_response>`
3068    SimplifyResponse(SimplifyResponse<'st>),
3069}
3070impl std::fmt::Display for SpecificSuccessResponse<'_> {
3071    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
3072        match self {
3073            Self::CheckSatResponse(m0) => write!(f, "{}", m0),
3074            Self::EchoResponse(m0) => write!(f, "{}", m0),
3075            Self::EvalResponse(m0) => write!(f, "{}", m0),
3076            Self::GetAssertionsResponse(m0) => write!(f, "{}", m0),
3077            Self::GetAssignmentResponse(m0) => write!(f, "{}", m0),
3078            Self::GetInfoResponse(m0) => write!(f, "{}", m0),
3079            Self::GetModelResponse(m0) => write!(f, "{}", m0),
3080            Self::GetOptionResponse(m0) => write!(f, "{}", m0),
3081            Self::GetProofResponse(m0) => write!(f, "{}", m0),
3082            Self::GetUnsatAssumptionsResponse(m0) => write!(f, "{}", m0),
3083            Self::GetUnsatCoreResponse(m0) => write!(f, "{}", m0),
3084            Self::GetValueResponse(m0) => write!(f, "{}", m0),
3085            Self::SimplifyResponse(m0) => write!(f, "{}", m0),
3086        }
3087    }
3088}
3089impl<'st> SpecificSuccessResponse<'st> {
3090    pub fn parse(
3091        st: &'st Storage,
3092        src: &str,
3093    ) -> Result<SpecificSuccessResponse<'st>, ParseError> {
3094        <SpecificSuccessResponse<
3095            'st,
3096        > as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
3097    }
3098}
3099impl<'st> SmtlibParse<'st> for SpecificSuccessResponse<'st> {
3100    type Output = SpecificSuccessResponse<'st>;
3101    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
3102        (SimplifyResponse::is_start_of(offset, p))
3103            || (GetValueResponse::is_start_of(offset, p))
3104            || (GetUnsatCoreResponse::is_start_of(offset, p))
3105            || (GetUnsatAssumptionsResponse::is_start_of(offset, p))
3106            || (GetProofResponse::is_start_of(offset, p))
3107            || (GetOptionResponse::is_start_of(offset, p))
3108            || (GetModelResponse::is_start_of(offset, p))
3109            || (GetInfoResponse::is_start_of(offset, p))
3110            || (GetAssignmentResponse::is_start_of(offset, p))
3111            || (GetAssertionsResponse::is_start_of(offset, p))
3112            || (EvalResponse::is_start_of(offset, p))
3113            || (EchoResponse::is_start_of(offset, p))
3114            || (CheckSatResponse::is_start_of(offset, p))
3115    }
3116    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
3117        let offset = 0;
3118        if SimplifyResponse::is_start_of(offset, p) {
3119            let m0 = <SimplifyResponse<'st> as SmtlibParse<'st>>::parse(p)?;
3120            #[allow(clippy::useless_conversion)]
3121            return Ok(Self::SimplifyResponse(m0.into()));
3122        }
3123        if GetValueResponse::is_start_of(offset, p) {
3124            let m0 = <GetValueResponse<'st> as SmtlibParse<'st>>::parse(p)?;
3125            #[allow(clippy::useless_conversion)]
3126            return Ok(Self::GetValueResponse(m0.into()));
3127        }
3128        if GetUnsatCoreResponse::is_start_of(offset, p) {
3129            let m0 = <GetUnsatCoreResponse<'st> as SmtlibParse<'st>>::parse(p)?;
3130            #[allow(clippy::useless_conversion)]
3131            return Ok(Self::GetUnsatCoreResponse(m0.into()));
3132        }
3133        if GetUnsatAssumptionsResponse::is_start_of(offset, p) {
3134            let m0 = <GetUnsatAssumptionsResponse<'st> as SmtlibParse<'st>>::parse(p)?;
3135            #[allow(clippy::useless_conversion)]
3136            return Ok(Self::GetUnsatAssumptionsResponse(m0.into()));
3137        }
3138        if GetProofResponse::is_start_of(offset, p) {
3139            let m0 = <GetProofResponse<'st> as SmtlibParse<'st>>::parse(p)?;
3140            #[allow(clippy::useless_conversion)]
3141            return Ok(Self::GetProofResponse(m0.into()));
3142        }
3143        if GetOptionResponse::is_start_of(offset, p) {
3144            let m0 = <GetOptionResponse<'st> as SmtlibParse<'st>>::parse(p)?;
3145            #[allow(clippy::useless_conversion)]
3146            return Ok(Self::GetOptionResponse(m0.into()));
3147        }
3148        if GetModelResponse::is_start_of(offset, p) {
3149            let m0 = <GetModelResponse<'st> as SmtlibParse<'st>>::parse(p)?;
3150            #[allow(clippy::useless_conversion)]
3151            return Ok(Self::GetModelResponse(m0.into()));
3152        }
3153        if GetInfoResponse::is_start_of(offset, p) {
3154            let m0 = <GetInfoResponse<'st> as SmtlibParse<'st>>::parse(p)?;
3155            #[allow(clippy::useless_conversion)]
3156            return Ok(Self::GetInfoResponse(m0.into()));
3157        }
3158        if GetAssignmentResponse::is_start_of(offset, p) {
3159            let m0 = <GetAssignmentResponse<'st> as SmtlibParse<'st>>::parse(p)?;
3160            #[allow(clippy::useless_conversion)]
3161            return Ok(Self::GetAssignmentResponse(m0.into()));
3162        }
3163        if GetAssertionsResponse::is_start_of(offset, p) {
3164            let m0 = <GetAssertionsResponse<'st> as SmtlibParse<'st>>::parse(p)?;
3165            #[allow(clippy::useless_conversion)]
3166            return Ok(Self::GetAssertionsResponse(m0.into()));
3167        }
3168        if EvalResponse::is_start_of(offset, p) {
3169            let m0 = <EvalResponse<'st> as SmtlibParse<'st>>::parse(p)?;
3170            #[allow(clippy::useless_conversion)]
3171            return Ok(Self::EvalResponse(m0.into()));
3172        }
3173        if EchoResponse::is_start_of(offset, p) {
3174            let m0 = <EchoResponse<'st> as SmtlibParse<'st>>::parse(p)?;
3175            #[allow(clippy::useless_conversion)]
3176            return Ok(Self::EchoResponse(m0.into()));
3177        }
3178        if CheckSatResponse::is_start_of(offset, p) {
3179            let m0 = <CheckSatResponse as SmtlibParse<'st>>::parse(p)?;
3180            #[allow(clippy::useless_conversion)]
3181            return Ok(Self::CheckSatResponse(m0.into()));
3182        }
3183        Err(p.stuck("SpecificSuccessResponse"))
3184    }
3185}
3186/// `(<symbol> <b_value>)`
3187#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
3188#[cfg_attr(feature = "serde", derive(serde::Serialize))]
3189pub struct TValuationPair<'st>(pub Symbol<'st>, pub BValue);
3190impl std::fmt::Display for TValuationPair<'_> {
3191    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
3192        write!(f, "({} {})", self.0, self.1)
3193    }
3194}
3195impl<'st> TValuationPair<'st> {
3196    pub fn parse(
3197        st: &'st Storage,
3198        src: &str,
3199    ) -> Result<TValuationPair<'st>, ParseError> {
3200        <TValuationPair<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
3201    }
3202}
3203impl<'st> SmtlibParse<'st> for TValuationPair<'st> {
3204    type Output = TValuationPair<'st>;
3205    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
3206        p.nth(offset) == Token::LParen
3207    }
3208    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
3209        p.expect(Token::LParen)?;
3210        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
3211        let m1 = <BValue as SmtlibParse<'st>>::parse(p)?;
3212        p.expect(Token::RParen)?;
3213        Ok(Self(m0, m1))
3214    }
3215}
3216#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
3217#[cfg_attr(feature = "serde", derive(serde::Serialize))]
3218pub enum Term<'st> {
3219    /// `(! <term> <attribute>+)`
3220    Annotation(&'st Term<'st>, &'st [Attribute<'st>]),
3221    /// `(<qual_identifier> <term>+)`
3222    Application(QualIdentifier<'st>, &'st [&'st Term<'st>]),
3223    /// `(exists (<sorted_var>+) <term>)`
3224    Exists(&'st [SortedVar<'st>], &'st Term<'st>),
3225    /// `(forall (<sorted_var>+) <term>)`
3226    Forall(&'st [SortedVar<'st>], &'st Term<'st>),
3227    /// `<qual_identifier>`
3228    Identifier(QualIdentifier<'st>),
3229    /// `(let (<var_binding>+) <term>)`
3230    Let(&'st [VarBinding<'st>], &'st Term<'st>),
3231    /// `(match <term> (<match_case>+))`
3232    Match(&'st Term<'st>, &'st [MatchCase<'st>]),
3233    /// `<spec_constant>`
3234    SpecConstant(SpecConstant<'st>),
3235}
3236impl std::fmt::Display for Term<'_> {
3237    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
3238        match self {
3239            Self::Annotation(m0, m1) => write!(f, "(! {} {})", m0, m1.iter().format(" ")),
3240            Self::Application(m0, m1) => write!(f, "({} {})", m0, m1.iter().format(" ")),
3241            Self::Exists(m0, m1) => {
3242                write!(f, "(exists ({}) {})", m0.iter().format(" "), m1)
3243            }
3244            Self::Forall(m0, m1) => {
3245                write!(f, "(forall ({}) {})", m0.iter().format(" "), m1)
3246            }
3247            Self::Identifier(m0) => write!(f, "{}", m0),
3248            Self::Let(m0, m1) => write!(f, "(let ({}) {})", m0.iter().format(" "), m1),
3249            Self::Match(m0, m1) => {
3250                write!(f, "(match {} ({}))", m0, m1.iter().format(" "))
3251            }
3252            Self::SpecConstant(m0) => write!(f, "{}", m0),
3253        }
3254    }
3255}
3256impl<'st> Term<'st> {
3257    pub fn parse(st: &'st Storage, src: &str) -> Result<&'st Term<'st>, ParseError> {
3258        <Term<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
3259    }
3260}
3261impl<'st> SmtlibParse<'st> for Term<'st> {
3262    type Output = &'st Term<'st>;
3263    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
3264        (p.nth(offset) == Token::LParen
3265            && p.nth_matches(offset + 1, Token::Reserved, "match"))
3266            || (p.nth(offset) == Token::LParen
3267                && p.nth_matches(offset + 1, Token::Reserved, "let")
3268                && p.nth(offset + 2) == Token::LParen)
3269            || (p.nth(offset) == Token::LParen
3270                && p.nth_matches(offset + 1, Token::Reserved, "forall")
3271                && p.nth(offset + 2) == Token::LParen)
3272            || (p.nth(offset) == Token::LParen
3273                && p.nth_matches(offset + 1, Token::Reserved, "exists")
3274                && p.nth(offset + 2) == Token::LParen)
3275            || (p.nth(offset) == Token::LParen
3276                && p.nth_matches(offset + 1, Token::Reserved, "!"))
3277            || (SpecConstant::is_start_of(offset, p))
3278            || (QualIdentifier::is_start_of(offset, p))
3279            || (p.nth(offset) == Token::LParen)
3280    }
3281    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
3282        let offset = 0;
3283        if p.nth(offset) == Token::LParen
3284            && p.nth_matches(offset + 1, Token::Reserved, "match")
3285        {
3286            p.expect(Token::LParen)?;
3287            p.expect_matches(Token::Reserved, "match")?;
3288            let m0 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
3289            p.expect(Token::LParen)?;
3290            let m1 = p.non_zero::<MatchCase<'st>>()?;
3291            p.expect(Token::RParen)?;
3292            p.expect(Token::RParen)?;
3293            #[allow(clippy::useless_conversion)]
3294            return Ok(p.storage.alloc(Self::Match(m0.into(), m1.into())));
3295        }
3296        if p.nth(offset) == Token::LParen
3297            && p.nth_matches(offset + 1, Token::Reserved, "let")
3298            && p.nth(offset + 2) == Token::LParen
3299        {
3300            p.expect(Token::LParen)?;
3301            p.expect_matches(Token::Reserved, "let")?;
3302            p.expect(Token::LParen)?;
3303            let m0 = p.non_zero::<VarBinding<'st>>()?;
3304            p.expect(Token::RParen)?;
3305            let m1 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
3306            p.expect(Token::RParen)?;
3307            #[allow(clippy::useless_conversion)]
3308            return Ok(p.storage.alloc(Self::Let(m0.into(), m1.into())));
3309        }
3310        if p.nth(offset) == Token::LParen
3311            && p.nth_matches(offset + 1, Token::Reserved, "forall")
3312            && p.nth(offset + 2) == Token::LParen
3313        {
3314            p.expect(Token::LParen)?;
3315            p.expect_matches(Token::Reserved, "forall")?;
3316            p.expect(Token::LParen)?;
3317            let m0 = p.non_zero::<SortedVar<'st>>()?;
3318            p.expect(Token::RParen)?;
3319            let m1 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
3320            p.expect(Token::RParen)?;
3321            #[allow(clippy::useless_conversion)]
3322            return Ok(p.storage.alloc(Self::Forall(m0.into(), m1.into())));
3323        }
3324        if p.nth(offset) == Token::LParen
3325            && p.nth_matches(offset + 1, Token::Reserved, "exists")
3326            && p.nth(offset + 2) == Token::LParen
3327        {
3328            p.expect(Token::LParen)?;
3329            p.expect_matches(Token::Reserved, "exists")?;
3330            p.expect(Token::LParen)?;
3331            let m0 = p.non_zero::<SortedVar<'st>>()?;
3332            p.expect(Token::RParen)?;
3333            let m1 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
3334            p.expect(Token::RParen)?;
3335            #[allow(clippy::useless_conversion)]
3336            return Ok(p.storage.alloc(Self::Exists(m0.into(), m1.into())));
3337        }
3338        if p.nth(offset) == Token::LParen
3339            && p.nth_matches(offset + 1, Token::Reserved, "!")
3340        {
3341            p.expect(Token::LParen)?;
3342            p.expect_matches(Token::Reserved, "!")?;
3343            let m0 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
3344            let m1 = p.non_zero::<Attribute<'st>>()?;
3345            p.expect(Token::RParen)?;
3346            #[allow(clippy::useless_conversion)]
3347            return Ok(p.storage.alloc(Self::Annotation(m0.into(), m1.into())));
3348        }
3349        if SpecConstant::is_start_of(offset, p) {
3350            let m0 = <SpecConstant<'st> as SmtlibParse<'st>>::parse(p)?;
3351            #[allow(clippy::useless_conversion)]
3352            return Ok(p.storage.alloc(Self::SpecConstant(m0.into())));
3353        }
3354        if QualIdentifier::is_start_of(offset, p) {
3355            let m0 = <QualIdentifier<'st> as SmtlibParse<'st>>::parse(p)?;
3356            #[allow(clippy::useless_conversion)]
3357            return Ok(p.storage.alloc(Self::Identifier(m0.into())));
3358        }
3359        if p.nth(offset) == Token::LParen {
3360            p.expect(Token::LParen)?;
3361            let m0 = <QualIdentifier<'st> as SmtlibParse<'st>>::parse(p)?;
3362            let m1 = p.non_zero::<Term<'st>>()?;
3363            p.expect(Token::RParen)?;
3364            #[allow(clippy::useless_conversion)]
3365            return Ok(p.storage.alloc(Self::Application(m0.into(), m1.into())));
3366        }
3367        Err(p.stuck("Term"))
3368    }
3369}
3370#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
3371#[cfg_attr(feature = "serde", derive(serde::Serialize))]
3372pub enum TheoryAttribute<'st> {
3373    /// `<attribute>`
3374    Attribute(Attribute<'st>),
3375    /// `:definition <string>`
3376    Definition(&'st str),
3377    /// `:funs (<par_fun_symbol_decl>+)`
3378    Funs(&'st [ParFunSymbolDecl<'st>]),
3379    /// `:funs-description <string>`
3380    FunsDescription(&'st str),
3381    /// `:notes <string>`
3382    Notes(&'st str),
3383    /// `:sorts (<sort_symbol_decl>+)`
3384    Sorts(&'st [SortSymbolDecl<'st>]),
3385    /// `:sorts-description <string>`
3386    SortsDescription(&'st str),
3387    /// `:values <string>`
3388    Values(&'st str),
3389}
3390impl std::fmt::Display for TheoryAttribute<'_> {
3391    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
3392        match self {
3393            Self::Attribute(m0) => write!(f, "{}", m0),
3394            Self::Definition(m0) => write!(f, ":definition {}", m0),
3395            Self::Funs(m0) => write!(f, ":funs ({})", m0.iter().format(" ")),
3396            Self::FunsDescription(m0) => write!(f, ":funs-description {}", m0),
3397            Self::Notes(m0) => write!(f, ":notes {}", m0),
3398            Self::Sorts(m0) => write!(f, ":sorts ({})", m0.iter().format(" ")),
3399            Self::SortsDescription(m0) => write!(f, ":sorts-description {}", m0),
3400            Self::Values(m0) => write!(f, ":values {}", m0),
3401        }
3402    }
3403}
3404impl<'st> TheoryAttribute<'st> {
3405    pub fn parse(
3406        st: &'st Storage,
3407        src: &str,
3408    ) -> Result<TheoryAttribute<'st>, ParseError> {
3409        <TheoryAttribute<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
3410    }
3411}
3412impl<'st> SmtlibParse<'st> for TheoryAttribute<'st> {
3413    type Output = TheoryAttribute<'st>;
3414    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
3415        (p.nth_matches(offset, Token::Keyword, ":sorts")
3416            && p.nth(offset + 1) == Token::LParen)
3417            || (p.nth_matches(offset, Token::Keyword, ":funs")
3418                && p.nth(offset + 1) == Token::LParen)
3419            || (p.nth_matches(offset, Token::Keyword, ":values"))
3420            || (p.nth_matches(offset, Token::Keyword, ":sorts-description"))
3421            || (p.nth_matches(offset, Token::Keyword, ":notes"))
3422            || (p.nth_matches(offset, Token::Keyword, ":funs-description"))
3423            || (p.nth_matches(offset, Token::Keyword, ":definition"))
3424            || (Attribute::is_start_of(offset, p))
3425    }
3426    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
3427        let offset = 0;
3428        if p.nth_matches(offset, Token::Keyword, ":sorts")
3429            && p.nth(offset + 1) == Token::LParen
3430        {
3431            p.expect_matches(Token::Keyword, ":sorts")?;
3432            p.expect(Token::LParen)?;
3433            let m0 = p.non_zero::<SortSymbolDecl<'st>>()?;
3434            p.expect(Token::RParen)?;
3435            #[allow(clippy::useless_conversion)] return Ok(Self::Sorts(m0.into()));
3436        }
3437        if p.nth_matches(offset, Token::Keyword, ":funs")
3438            && p.nth(offset + 1) == Token::LParen
3439        {
3440            p.expect_matches(Token::Keyword, ":funs")?;
3441            p.expect(Token::LParen)?;
3442            let m0 = p.non_zero::<ParFunSymbolDecl<'st>>()?;
3443            p.expect(Token::RParen)?;
3444            #[allow(clippy::useless_conversion)] return Ok(Self::Funs(m0.into()));
3445        }
3446        if p.nth_matches(offset, Token::Keyword, ":values") {
3447            p.expect_matches(Token::Keyword, ":values")?;
3448            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
3449            #[allow(clippy::useless_conversion)] return Ok(Self::Values(m0.into()));
3450        }
3451        if p.nth_matches(offset, Token::Keyword, ":sorts-description") {
3452            p.expect_matches(Token::Keyword, ":sorts-description")?;
3453            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
3454            #[allow(clippy::useless_conversion)]
3455            return Ok(Self::SortsDescription(m0.into()));
3456        }
3457        if p.nth_matches(offset, Token::Keyword, ":notes") {
3458            p.expect_matches(Token::Keyword, ":notes")?;
3459            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
3460            #[allow(clippy::useless_conversion)] return Ok(Self::Notes(m0.into()));
3461        }
3462        if p.nth_matches(offset, Token::Keyword, ":funs-description") {
3463            p.expect_matches(Token::Keyword, ":funs-description")?;
3464            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
3465            #[allow(clippy::useless_conversion)]
3466            return Ok(Self::FunsDescription(m0.into()));
3467        }
3468        if p.nth_matches(offset, Token::Keyword, ":definition") {
3469            p.expect_matches(Token::Keyword, ":definition")?;
3470            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
3471            #[allow(clippy::useless_conversion)] return Ok(Self::Definition(m0.into()));
3472        }
3473        if Attribute::is_start_of(offset, p) {
3474            let m0 = <Attribute<'st> as SmtlibParse<'st>>::parse(p)?;
3475            #[allow(clippy::useless_conversion)] return Ok(Self::Attribute(m0.into()));
3476        }
3477        Err(p.stuck("TheoryAttribute"))
3478    }
3479}
3480/// `(theory <symbol> <theory_attribute>+)`
3481#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
3482#[cfg_attr(feature = "serde", derive(serde::Serialize))]
3483pub struct TheoryDecl<'st>(pub Symbol<'st>, pub &'st [TheoryAttribute<'st>]);
3484impl std::fmt::Display for TheoryDecl<'_> {
3485    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
3486        write!(f, "(theory {} {})", self.0, self.1.iter().format(" "))
3487    }
3488}
3489impl<'st> TheoryDecl<'st> {
3490    pub fn parse(st: &'st Storage, src: &str) -> Result<TheoryDecl<'st>, ParseError> {
3491        <TheoryDecl<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
3492    }
3493}
3494impl<'st> SmtlibParse<'st> for TheoryDecl<'st> {
3495    type Output = TheoryDecl<'st>;
3496    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
3497        p.nth(offset) == Token::LParen
3498            && p.nth_matches(offset + 1, Token::Symbol, "theory")
3499    }
3500    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
3501        p.expect(Token::LParen)?;
3502        p.expect_matches(Token::Symbol, "theory")?;
3503        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
3504        let m1 = p.non_zero::<TheoryAttribute<'st>>()?;
3505        p.expect(Token::RParen)?;
3506        Ok(Self(m0, m1))
3507    }
3508}
3509/// `(<term> <term>)`
3510#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
3511#[cfg_attr(feature = "serde", derive(serde::Serialize))]
3512pub struct ValuationPair<'st>(pub &'st Term<'st>, pub &'st Term<'st>);
3513impl std::fmt::Display for ValuationPair<'_> {
3514    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
3515        write!(f, "({} {})", self.0, self.1)
3516    }
3517}
3518impl<'st> ValuationPair<'st> {
3519    pub fn parse(st: &'st Storage, src: &str) -> Result<ValuationPair<'st>, ParseError> {
3520        <ValuationPair<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
3521    }
3522}
3523impl<'st> SmtlibParse<'st> for ValuationPair<'st> {
3524    type Output = ValuationPair<'st>;
3525    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
3526        p.nth(offset) == Token::LParen
3527    }
3528    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
3529        p.expect(Token::LParen)?;
3530        let m0 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
3531        let m1 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
3532        p.expect(Token::RParen)?;
3533        Ok(Self(m0, m1))
3534    }
3535}
3536/// `(<symbol> <term>)`
3537#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
3538#[cfg_attr(feature = "serde", derive(serde::Serialize))]
3539pub struct VarBinding<'st>(pub Symbol<'st>, pub &'st Term<'st>);
3540impl std::fmt::Display for VarBinding<'_> {
3541    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
3542        write!(f, "({} {})", self.0, self.1)
3543    }
3544}
3545impl<'st> VarBinding<'st> {
3546    pub fn parse(st: &'st Storage, src: &str) -> Result<VarBinding<'st>, ParseError> {
3547        <VarBinding<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
3548    }
3549}
3550impl<'st> SmtlibParse<'st> for VarBinding<'st> {
3551    type Output = VarBinding<'st>;
3552    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
3553        p.nth(offset) == Token::LParen
3554    }
3555    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
3556        p.expect(Token::LParen)?;
3557        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
3558        let m1 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
3559        p.expect(Token::RParen)?;
3560        Ok(Self(m0, m1))
3561    }
3562}