smtlib_lowlevel/

ast.rs

//! Generated by `cargo xtask ast`, do not edit by hand.

use crate::parse::{Token, Parser, ParseError};
use crate::storage::Storage;
use itertools::Itertools;
use crate::lexicon::*;
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum SpecConstant<'st> {
    /// `<numeral>`
    Numeral(Numeral<'st>),
    /// `<decimal>`
    Decimal(Decimal<'st>),
    /// `<hexadecimal>`
    Hexadecimal(Hexadecimal<'st>),
    /// `<binary>`
    Binary(Binary<'st>),
    /// `<string>`
    String(&'st str),
}
impl std::fmt::Display for SpecConstant<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::Numeral(m0) => write!(f, "{}", m0),
            Self::Decimal(m0) => write!(f, "{}", m0),
            Self::Hexadecimal(m0) => write!(f, "{}", m0),
            Self::Binary(m0) => write!(f, "{}", m0),
            Self::String(m0) => write!(f, "{}", m0),
        }
    }
}
impl<'st> SpecConstant<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<SpecConstant<'st>, ParseError> {
        <SpecConstant<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for SpecConstant<'st> {
    type Output = SpecConstant<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (String::is_start_of(offset, p)) || (Binary::is_start_of(offset, p))
            || (Hexadecimal::is_start_of(offset, p)) || (Decimal::is_start_of(offset, p))
            || (Numeral::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if String::is_start_of(offset, p) {
            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::String(m0.into()));
        }
        if Binary::is_start_of(offset, p) {
            let m0 = <Binary<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Binary(m0.into()));
        }
        if Hexadecimal::is_start_of(offset, p) {
            let m0 = <Hexadecimal<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Hexadecimal(m0.into()));
        }
        if Decimal::is_start_of(offset, p) {
            let m0 = <Decimal<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Decimal(m0.into()));
        }
        if Numeral::is_start_of(offset, p) {
            let m0 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Numeral(m0.into()));
        }
        Err(p.stuck("SpecConstant"))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum SExpr<'st> {
    /// `<spec_constant>`
    SpecConstant(SpecConstant<'st>),
    /// `<symbol>`
    Symbol(Symbol<'st>),
    /// `<reserved>`
    Reserved(Reserved<'st>),
    /// `<keyword>`
    Keyword(Keyword<'st>),
    /// `(<s_expr>*)`
    Paren(&'st [SExpr<'st>]),
}
impl std::fmt::Display for SExpr<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::SpecConstant(m0) => write!(f, "{}", m0),
            Self::Symbol(m0) => write!(f, "{}", m0),
            Self::Reserved(m0) => write!(f, "{}", m0),
            Self::Keyword(m0) => write!(f, "{}", m0),
            Self::Paren(m0) => write!(f, "({})", m0.iter().format(" ")),
        }
    }
}
impl<'st> SExpr<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<SExpr<'st>, ParseError> {
        <SExpr<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for SExpr<'st> {
    type Output = SExpr<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth(offset) == Token::LParen) || (Keyword::is_start_of(offset, p))
            || (Reserved::is_start_of(offset, p)) || (Symbol::is_start_of(offset, p))
            || (SpecConstant::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth(offset) == Token::LParen {
            p.expect(Token::LParen)?;
            let m0 = p.any::<SExpr<'st>>()?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Paren(m0.into()));
        }
        if Keyword::is_start_of(offset, p) {
            let m0 = <Keyword<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Keyword(m0.into()));
        }
        if Reserved::is_start_of(offset, p) {
            let m0 = <Reserved<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Reserved(m0.into()));
        }
        if Symbol::is_start_of(offset, p) {
            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Symbol(m0.into()));
        }
        if SpecConstant::is_start_of(offset, p) {
            let m0 = <SpecConstant<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::SpecConstant(m0.into()));
        }
        Err(p.stuck("SExpr"))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum Index<'st> {
    /// `<numeral>`
    Numeral(Numeral<'st>),
    /// `<symbol>`
    Symbol(Symbol<'st>),
}
impl std::fmt::Display for Index<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::Numeral(m0) => write!(f, "{}", m0),
            Self::Symbol(m0) => write!(f, "{}", m0),
        }
    }
}
impl<'st> Index<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<Index<'st>, ParseError> {
        <Index<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for Index<'st> {
    type Output = Index<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (Symbol::is_start_of(offset, p)) || (Numeral::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if Symbol::is_start_of(offset, p) {
            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Symbol(m0.into()));
        }
        if Numeral::is_start_of(offset, p) {
            let m0 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Numeral(m0.into()));
        }
        Err(p.stuck("Index"))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum Identifier<'st> {
    /// `<symbol>`
    Simple(Symbol<'st>),
    /// `(_ <symbol> <index>+)`
    Indexed(Symbol<'st>, &'st [Index<'st>]),
}
impl std::fmt::Display for Identifier<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::Simple(m0) => write!(f, "{}", m0),
            Self::Indexed(m0, m1) => write!(f, "(_ {} {})", m0, m1.iter().format(" ")),
        }
    }
}
impl<'st> Identifier<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<Identifier<'st>, ParseError> {
        <Identifier<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for Identifier<'st> {
    type Output = Identifier<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "_"))
            || (Symbol::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "_")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "_")?;
            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
            let m1 = p.non_zero::<Index<'st>>()?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::Indexed(m0.into(), m1.into()));
        }
        if Symbol::is_start_of(offset, p) {
            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Simple(m0.into()));
        }
        Err(p.stuck("Identifier"))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum AttributeValue<'st> {
    /// `<spec_constant>`
    SpecConstant(SpecConstant<'st>),
    /// `<symbol>`
    Symbol(Symbol<'st>),
    /// `(<s_expr>)`
    Expr(SExpr<'st>),
}
impl std::fmt::Display for AttributeValue<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::SpecConstant(m0) => write!(f, "{}", m0),
            Self::Symbol(m0) => write!(f, "{}", m0),
            Self::Expr(m0) => write!(f, "({})", m0),
        }
    }
}
impl<'st> AttributeValue<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<AttributeValue<'st>, ParseError> {
        <AttributeValue<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for AttributeValue<'st> {
    type Output = AttributeValue<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth(offset) == Token::LParen) || (Symbol::is_start_of(offset, p))
            || (SpecConstant::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth(offset) == Token::LParen {
            p.expect(Token::LParen)?;
            let m0 = <SExpr<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Expr(m0.into()));
        }
        if Symbol::is_start_of(offset, p) {
            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Symbol(m0.into()));
        }
        if SpecConstant::is_start_of(offset, p) {
            let m0 = <SpecConstant<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::SpecConstant(m0.into()));
        }
        Err(p.stuck("AttributeValue"))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum Attribute<'st> {
    /// `<keyword>`
    Keyword(Keyword<'st>),
    /// `<keyword> <attribute_value>`
    WithValue(Keyword<'st>, AttributeValue<'st>),
}
impl std::fmt::Display for Attribute<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::Keyword(m0) => write!(f, "{}", m0),
            Self::WithValue(m0, m1) => write!(f, "{} {}", m0, m1),
        }
    }
}
impl<'st> Attribute<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<Attribute<'st>, ParseError> {
        <Attribute<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for Attribute<'st> {
    type Output = Attribute<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (Keyword::is_start_of(offset, p) && AttributeValue::is_start_of(offset + 1, p))
            || (Keyword::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if Keyword::is_start_of(offset, p) && AttributeValue::is_start_of(offset + 1, p)
        {
            let m0 = <Keyword<'st> as SmtlibParse<'st>>::parse(p)?;
            let m1 = <AttributeValue<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::WithValue(m0.into(), m1.into()));
        }
        if Keyword::is_start_of(offset, p) {
            let m0 = <Keyword<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Keyword(m0.into()));
        }
        Err(p.stuck("Attribute"))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum Sort<'st> {
    /// `<identifier>`
    Sort(Identifier<'st>),
    /// `(<identifier> <sort>+)`
    Parametric(Identifier<'st>, &'st [Sort<'st>]),
}
impl std::fmt::Display for Sort<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::Sort(m0) => write!(f, "{}", m0),
            Self::Parametric(m0, m1) => write!(f, "({} {})", m0, m1.iter().format(" ")),
        }
    }
}
impl<'st> Sort<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<Sort<'st>, ParseError> {
        <Sort<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for Sort<'st> {
    type Output = Sort<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (Identifier::is_start_of(offset, p)) || (p.nth(offset) == Token::LParen)
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if Identifier::is_start_of(offset, p) {
            let m0 = <Identifier<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Sort(m0.into()));
        }
        if p.nth(offset) == Token::LParen {
            p.expect(Token::LParen)?;
            let m0 = <Identifier<'st> as SmtlibParse<'st>>::parse(p)?;
            let m1 = p.non_zero::<Sort<'st>>()?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::Parametric(m0.into(), m1.into()));
        }
        Err(p.stuck("Sort"))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum QualIdentifier<'st> {
    /// `<identifier>`
    Identifier(Identifier<'st>),
    /// `(as <identifier> <sort>)`
    Sorted(Identifier<'st>, Sort<'st>),
}
impl std::fmt::Display for QualIdentifier<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::Identifier(m0) => write!(f, "{}", m0),
            Self::Sorted(m0, m1) => write!(f, "(as {} {})", m0, m1),
        }
    }
}
impl<'st> QualIdentifier<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<QualIdentifier<'st>, ParseError> {
        <QualIdentifier<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for QualIdentifier<'st> {
    type Output = QualIdentifier<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "as"))
            || (Identifier::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "as")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "as")?;
            let m0 = <Identifier<'st> as SmtlibParse<'st>>::parse(p)?;
            let m1 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::Sorted(m0.into(), m1.into()));
        }
        if Identifier::is_start_of(offset, p) {
            let m0 = <Identifier<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Identifier(m0.into()));
        }
        Err(p.stuck("QualIdentifier"))
    }
}
/// `(<symbol> <term>)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct VarBinding<'st>(pub Symbol<'st>, pub &'st Term<'st>);
impl std::fmt::Display for VarBinding<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({} {})", self.0, self.1)
    }
}
impl<'st> VarBinding<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<VarBinding<'st>, ParseError> {
        <VarBinding<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for VarBinding<'st> {
    type Output = VarBinding<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
        let m1 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
        p.expect(Token::RParen)?;
        Ok(Self(m0, m1))
    }
}
/// `(<symbol> <sort>)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct SortedVar<'st>(pub Symbol<'st>, pub Sort<'st>);
impl std::fmt::Display for SortedVar<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({} {})", self.0, self.1)
    }
}
impl<'st> SortedVar<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<SortedVar<'st>, ParseError> {
        <SortedVar<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for SortedVar<'st> {
    type Output = SortedVar<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
        let m1 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
        p.expect(Token::RParen)?;
        Ok(Self(m0, m1))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum Pattern<'st> {
    /// `<symbol>`
    Symbol(Symbol<'st>),
    /// `(<symbol> <symbol>+)`
    Application(Symbol<'st>, &'st [Symbol<'st>]),
}
impl std::fmt::Display for Pattern<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::Symbol(m0) => write!(f, "{}", m0),
            Self::Application(m0, m1) => write!(f, "({} {})", m0, m1.iter().format(" ")),
        }
    }
}
impl<'st> Pattern<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<Pattern<'st>, ParseError> {
        <Pattern<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for Pattern<'st> {
    type Output = Pattern<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth(offset) == Token::LParen) || (Symbol::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth(offset) == Token::LParen {
            p.expect(Token::LParen)?;
            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
            let m1 = p.non_zero::<Symbol<'st>>()?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::Application(m0.into(), m1.into()));
        }
        if Symbol::is_start_of(offset, p) {
            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Symbol(m0.into()));
        }
        Err(p.stuck("Pattern"))
    }
}
/// `(<pattern> <term>)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct MatchCase<'st>(pub Pattern<'st>, pub &'st Term<'st>);
impl std::fmt::Display for MatchCase<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({} {})", self.0, self.1)
    }
}
impl<'st> MatchCase<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<MatchCase<'st>, ParseError> {
        <MatchCase<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for MatchCase<'st> {
    type Output = MatchCase<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Pattern<'st> as SmtlibParse<'st>>::parse(p)?;
        let m1 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
        p.expect(Token::RParen)?;
        Ok(Self(m0, m1))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum Term<'st> {
    /// `<spec_constant>`
    SpecConstant(SpecConstant<'st>),
    /// `<qual_identifier>`
    Identifier(QualIdentifier<'st>),
    /// `(<qual_identifier> <term>+)`
    Application(QualIdentifier<'st>, &'st [&'st Term<'st>]),
    /// `(let (<var_binding>+) <term>)`
    Let(&'st [VarBinding<'st>], &'st Term<'st>),
    /// `(forall (<sorted_var>+) <term>)`
    Forall(&'st [SortedVar<'st>], &'st Term<'st>),
    /// `(exists (<sorted_var>+) <term>)`
    Exists(&'st [SortedVar<'st>], &'st Term<'st>),
    /// `(match <term> (<match_case>+))`
    Match(&'st Term<'st>, &'st [MatchCase<'st>]),
    /// `(! <term> <attribute>+)`
    Annotation(&'st Term<'st>, &'st [Attribute<'st>]),
}
impl std::fmt::Display for Term<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::SpecConstant(m0) => write!(f, "{}", m0),
            Self::Identifier(m0) => write!(f, "{}", m0),
            Self::Application(m0, m1) => write!(f, "({} {})", m0, m1.iter().format(" ")),
            Self::Let(m0, m1) => write!(f, "(let ({}) {})", m0.iter().format(" "), m1),
            Self::Forall(m0, m1) => {
                write!(f, "(forall ({}) {})", m0.iter().format(" "), m1)
            }
            Self::Exists(m0, m1) => {
                write!(f, "(exists ({}) {})", m0.iter().format(" "), m1)
            }
            Self::Match(m0, m1) => {
                write!(f, "(match {} ({}))", m0, m1.iter().format(" "))
            }
            Self::Annotation(m0, m1) => write!(f, "(! {} {})", m0, m1.iter().format(" ")),
        }
    }
}
impl<'st> Term<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<&'st Term<'st>, ParseError> {
        <Term<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for Term<'st> {
    type Output = &'st Term<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "match"))
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "exists")
                && p.nth(offset + 2) == Token::LParen)
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "forall")
                && p.nth(offset + 2) == Token::LParen)
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "let")
                && p.nth(offset + 2) == Token::LParen)
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "!"))
            || (p.nth(offset) == Token::LParen)
            || (QualIdentifier::is_start_of(offset, p))
            || (SpecConstant::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "match")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "match")?;
            let m0 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::LParen)?;
            let m1 = p.non_zero::<MatchCase<'st>>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(p.storage.alloc(Self::Match(m0.into(), m1.into())));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "exists")
            && p.nth(offset + 2) == Token::LParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "exists")?;
            p.expect(Token::LParen)?;
            let m0 = p.non_zero::<SortedVar<'st>>()?;
            p.expect(Token::RParen)?;
            let m1 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(p.storage.alloc(Self::Exists(m0.into(), m1.into())));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "forall")
            && p.nth(offset + 2) == Token::LParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "forall")?;
            p.expect(Token::LParen)?;
            let m0 = p.non_zero::<SortedVar<'st>>()?;
            p.expect(Token::RParen)?;
            let m1 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(p.storage.alloc(Self::Forall(m0.into(), m1.into())));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "let")
            && p.nth(offset + 2) == Token::LParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "let")?;
            p.expect(Token::LParen)?;
            let m0 = p.non_zero::<VarBinding<'st>>()?;
            p.expect(Token::RParen)?;
            let m1 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(p.storage.alloc(Self::Let(m0.into(), m1.into())));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "!")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "!")?;
            let m0 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
            let m1 = p.non_zero::<Attribute<'st>>()?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(p.storage.alloc(Self::Annotation(m0.into(), m1.into())));
        }
        if p.nth(offset) == Token::LParen {
            p.expect(Token::LParen)?;
            let m0 = <QualIdentifier<'st> as SmtlibParse<'st>>::parse(p)?;
            let m1 = p.non_zero::<Term<'st>>()?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(p.storage.alloc(Self::Application(m0.into(), m1.into())));
        }
        if QualIdentifier::is_start_of(offset, p) {
            let m0 = <QualIdentifier<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(p.storage.alloc(Self::Identifier(m0.into())));
        }
        if SpecConstant::is_start_of(offset, p) {
            let m0 = <SpecConstant<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(p.storage.alloc(Self::SpecConstant(m0.into())));
        }
        Err(p.stuck("Term"))
    }
}
/// `(<identifier> <numeral> <attribute>*)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct SortSymbolDecl<'st>(
    pub Identifier<'st>,
    pub Numeral<'st>,
    pub &'st [Attribute<'st>],
);
impl std::fmt::Display for SortSymbolDecl<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({} {} {})", self.0, self.1, self.2.iter().format(" "))
    }
}
impl<'st> SortSymbolDecl<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<SortSymbolDecl<'st>, ParseError> {
        <SortSymbolDecl<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for SortSymbolDecl<'st> {
    type Output = SortSymbolDecl<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Identifier<'st> as SmtlibParse<'st>>::parse(p)?;
        let m1 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
        let m2 = p.any::<Attribute<'st>>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0, m1, m2))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum MetaSpecConstant {
    /// `NUMERAL`
    Numeral,
    /// `DECIMAL`
    Decimal,
    /// `STRING`
    String,
}
impl std::fmt::Display for MetaSpecConstant {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::Numeral => write!(f, "NUMERAL"),
            Self::Decimal => write!(f, "DECIMAL"),
            Self::String => write!(f, "STRING"),
        }
    }
}
impl<'st> MetaSpecConstant {
    pub fn parse(st: &'st Storage, src: &str) -> Result<MetaSpecConstant, ParseError> {
        <MetaSpecConstant as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for MetaSpecConstant {
    type Output = MetaSpecConstant;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth_matches(offset, Token::Reserved, "STRING"))
            || (p.nth_matches(offset, Token::Reserved, "DECIMAL"))
            || (p.nth_matches(offset, Token::Reserved, "NUMERAL"))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth_matches(offset, Token::Reserved, "STRING") {
            p.expect_matches(Token::Reserved, "STRING")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::String);
        }
        if p.nth_matches(offset, Token::Reserved, "DECIMAL") {
            p.expect_matches(Token::Reserved, "DECIMAL")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Decimal);
        }
        if p.nth_matches(offset, Token::Reserved, "NUMERAL") {
            p.expect_matches(Token::Reserved, "NUMERAL")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Numeral);
        }
        Err(p.stuck("MetaSpecConstant"))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum FunSymbolDecl<'st> {
    /// `(<spec_constant> <sort> <attribute>*)`
    SpecConstant(SpecConstant<'st>, Sort<'st>, &'st [Attribute<'st>]),
    /// `(<meta_spec_constant> <sort> <attribute>*)`
    MetaSpecConstant(MetaSpecConstant, Sort<'st>, &'st [Attribute<'st>]),
    /// `(<identifier> <sort>+ <attribute>*)`
    Identifier(Identifier<'st>, &'st [Sort<'st>], &'st [Attribute<'st>]),
}
impl std::fmt::Display for FunSymbolDecl<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::SpecConstant(m0, m1, m2) => {
                write!(f, "({} {} {})", m0, m1, m2.iter().format(" "))
            }
            Self::MetaSpecConstant(m0, m1, m2) => {
                write!(f, "({} {} {})", m0, m1, m2.iter().format(" "))
            }
            Self::Identifier(m0, m1, m2) => {
                write!(f, "({} {} {})", m0, m1.iter().format(" "), m2.iter().format(" "))
            }
        }
    }
}
impl<'st> FunSymbolDecl<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<FunSymbolDecl<'st>, ParseError> {
        <FunSymbolDecl<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for FunSymbolDecl<'st> {
    type Output = FunSymbolDecl<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth(offset) == Token::LParen) || (p.nth(offset) == Token::LParen)
            || (p.nth(offset) == Token::LParen)
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth(offset) == Token::LParen {
            p.expect(Token::LParen)?;
            let m0 = <Identifier<'st> as SmtlibParse<'st>>::parse(p)?;
            let m1 = p.non_zero::<Sort<'st>>()?;
            let m2 = p.any::<Attribute<'st>>()?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::Identifier(m0.into(), m1.into(), m2.into()));
        }
        if p.nth(offset) == Token::LParen {
            p.expect(Token::LParen)?;
            let m0 = <MetaSpecConstant as SmtlibParse<'st>>::parse(p)?;
            let m1 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
            let m2 = p.any::<Attribute<'st>>()?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::MetaSpecConstant(m0.into(), m1.into(), m2.into()));
        }
        if p.nth(offset) == Token::LParen {
            p.expect(Token::LParen)?;
            let m0 = <SpecConstant<'st> as SmtlibParse<'st>>::parse(p)?;
            let m1 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
            let m2 = p.any::<Attribute<'st>>()?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::SpecConstant(m0.into(), m1.into(), m2.into()));
        }
        Err(p.stuck("FunSymbolDecl"))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum ParFunSymbolDecl<'st> {
    /// `(par (<symbol>+) (<identifier> <sort>+ <attribute>*))`
    Par(&'st [Symbol<'st>], Identifier<'st>, &'st [Sort<'st>], &'st [Attribute<'st>]),
    /// `<fun_symbol_decl>`
    FunSymbolDecl(FunSymbolDecl<'st>),
}
impl std::fmt::Display for ParFunSymbolDecl<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::Par(m0, m1, m2, m3) => {
                write!(
                    f, "(par ({}) ({} {} {}))", m0.iter().format(" "), m1, m2.iter()
                    .format(" "), m3.iter().format(" ")
                )
            }
            Self::FunSymbolDecl(m0) => write!(f, "{}", m0),
        }
    }
}
impl<'st> ParFunSymbolDecl<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<ParFunSymbolDecl<'st>, ParseError> {
        <ParFunSymbolDecl<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for ParFunSymbolDecl<'st> {
    type Output = ParFunSymbolDecl<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "par")
            && p.nth(offset + 2) == Token::LParen)
            || (FunSymbolDecl::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "par")
            && p.nth(offset + 2) == Token::LParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "par")?;
            p.expect(Token::LParen)?;
            let m0 = p.non_zero::<Symbol<'st>>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::LParen)?;
            let m1 = <Identifier<'st> as SmtlibParse<'st>>::parse(p)?;
            let m2 = p.non_zero::<Sort<'st>>()?;
            let m3 = p.any::<Attribute<'st>>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::Par(m0.into(), m1.into(), m2.into(), m3.into()));
        }
        if FunSymbolDecl::is_start_of(offset, p) {
            let m0 = <FunSymbolDecl<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::FunSymbolDecl(m0.into()));
        }
        Err(p.stuck("ParFunSymbolDecl"))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum TheoryAttribute<'st> {
    /// `:sorts (<sort_symbol_decl>+)`
    Sorts(&'st [SortSymbolDecl<'st>]),
    /// `:funs (<par_fun_symbol_decl>+)`
    Funs(&'st [ParFunSymbolDecl<'st>]),
    /// `:sorts-description <string>`
    SortsDescription(&'st str),
    /// `:funs-description <string>`
    FunsDescription(&'st str),
    /// `:definition <string>`
    Definition(&'st str),
    /// `:values <string>`
    Values(&'st str),
    /// `:notes <string>`
    Notes(&'st str),
    /// `<attribute>`
    Attribute(Attribute<'st>),
}
impl std::fmt::Display for TheoryAttribute<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::Sorts(m0) => write!(f, ":sorts ({})", m0.iter().format(" ")),
            Self::Funs(m0) => write!(f, ":funs ({})", m0.iter().format(" ")),
            Self::SortsDescription(m0) => write!(f, ":sorts-description {}", m0),
            Self::FunsDescription(m0) => write!(f, ":funs-description {}", m0),
            Self::Definition(m0) => write!(f, ":definition {}", m0),
            Self::Values(m0) => write!(f, ":values {}", m0),
            Self::Notes(m0) => write!(f, ":notes {}", m0),
            Self::Attribute(m0) => write!(f, "{}", m0),
        }
    }
}
impl<'st> TheoryAttribute<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<TheoryAttribute<'st>, ParseError> {
        <TheoryAttribute<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for TheoryAttribute<'st> {
    type Output = TheoryAttribute<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth_matches(offset, Token::Keyword, ":funs")
            && p.nth(offset + 1) == Token::LParen)
            || (p.nth_matches(offset, Token::Keyword, ":sorts")
                && p.nth(offset + 1) == Token::LParen)
            || (p.nth_matches(offset, Token::Keyword, ":notes"))
            || (p.nth_matches(offset, Token::Keyword, ":values"))
            || (p.nth_matches(offset, Token::Keyword, ":definition"))
            || (p.nth_matches(offset, Token::Keyword, ":funs-description"))
            || (p.nth_matches(offset, Token::Keyword, ":sorts-description"))
            || (Attribute::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth_matches(offset, Token::Keyword, ":funs")
            && p.nth(offset + 1) == Token::LParen
        {
            p.expect_matches(Token::Keyword, ":funs")?;
            p.expect(Token::LParen)?;
            let m0 = p.non_zero::<ParFunSymbolDecl<'st>>()?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Funs(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":sorts")
            && p.nth(offset + 1) == Token::LParen
        {
            p.expect_matches(Token::Keyword, ":sorts")?;
            p.expect(Token::LParen)?;
            let m0 = p.non_zero::<SortSymbolDecl<'st>>()?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Sorts(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":notes") {
            p.expect_matches(Token::Keyword, ":notes")?;
            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Notes(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":values") {
            p.expect_matches(Token::Keyword, ":values")?;
            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Values(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":definition") {
            p.expect_matches(Token::Keyword, ":definition")?;
            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Definition(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":funs-description") {
            p.expect_matches(Token::Keyword, ":funs-description")?;
            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::FunsDescription(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":sorts-description") {
            p.expect_matches(Token::Keyword, ":sorts-description")?;
            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::SortsDescription(m0.into()));
        }
        if Attribute::is_start_of(offset, p) {
            let m0 = <Attribute<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Attribute(m0.into()));
        }
        Err(p.stuck("TheoryAttribute"))
    }
}
/// `(theory <symbol> <theory_attribute>+)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct TheoryDecl<'st>(pub Symbol<'st>, pub &'st [TheoryAttribute<'st>]);
impl std::fmt::Display for TheoryDecl<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "(theory {} {})", self.0, self.1.iter().format(" "))
    }
}
impl<'st> TheoryDecl<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<TheoryDecl<'st>, ParseError> {
        <TheoryDecl<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for TheoryDecl<'st> {
    type Output = TheoryDecl<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Symbol, "theory")
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        p.expect_matches(Token::Symbol, "theory")?;
        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
        let m1 = p.non_zero::<TheoryAttribute<'st>>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0, m1))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum LogicAttribute<'st> {
    /// `:theories (<symbol>*)`
    Theories(&'st [Symbol<'st>]),
    /// `:language <string>`
    Language(&'st str),
    /// `:extensions <string>`
    Extensions(&'st str),
    /// `:values <string>`
    Values(&'st str),
    /// `:notes <string>`
    Notes(&'st str),
    /// `<attribute>`
    Attribute(Attribute<'st>),
}
impl std::fmt::Display for LogicAttribute<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::Theories(m0) => write!(f, ":theories ({})", m0.iter().format(" ")),
            Self::Language(m0) => write!(f, ":language {}", m0),
            Self::Extensions(m0) => write!(f, ":extensions {}", m0),
            Self::Values(m0) => write!(f, ":values {}", m0),
            Self::Notes(m0) => write!(f, ":notes {}", m0),
            Self::Attribute(m0) => write!(f, "{}", m0),
        }
    }
}
impl<'st> LogicAttribute<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<LogicAttribute<'st>, ParseError> {
        <LogicAttribute<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for LogicAttribute<'st> {
    type Output = LogicAttribute<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth_matches(offset, Token::Keyword, ":theories")
            && p.nth(offset + 1) == Token::LParen)
            || (p.nth_matches(offset, Token::Keyword, ":notes"))
            || (p.nth_matches(offset, Token::Keyword, ":values"))
            || (p.nth_matches(offset, Token::Keyword, ":extensions"))
            || (p.nth_matches(offset, Token::Keyword, ":language"))
            || (Attribute::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth_matches(offset, Token::Keyword, ":theories")
            && p.nth(offset + 1) == Token::LParen
        {
            p.expect_matches(Token::Keyword, ":theories")?;
            p.expect(Token::LParen)?;
            let m0 = p.any::<Symbol<'st>>()?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Theories(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":notes") {
            p.expect_matches(Token::Keyword, ":notes")?;
            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Notes(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":values") {
            p.expect_matches(Token::Keyword, ":values")?;
            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Values(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":extensions") {
            p.expect_matches(Token::Keyword, ":extensions")?;
            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Extensions(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":language") {
            p.expect_matches(Token::Keyword, ":language")?;
            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Language(m0.into()));
        }
        if Attribute::is_start_of(offset, p) {
            let m0 = <Attribute<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Attribute(m0.into()));
        }
        Err(p.stuck("LogicAttribute"))
    }
}
/// `(logic <symbol> <logic_attribute>+)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct Logic<'st>(pub Symbol<'st>, pub &'st [LogicAttribute<'st>]);
impl std::fmt::Display for Logic<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "(logic {} {})", self.0, self.1.iter().format(" "))
    }
}
impl<'st> Logic<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<Logic<'st>, ParseError> {
        <Logic<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for Logic<'st> {
    type Output = Logic<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Symbol, "logic")
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        p.expect_matches(Token::Symbol, "logic")?;
        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
        let m1 = p.non_zero::<LogicAttribute<'st>>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0, m1))
    }
}
/// `(<symbol> <numeral>)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct SortDec<'st>(pub Symbol<'st>, pub Numeral<'st>);
impl std::fmt::Display for SortDec<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({} {})", self.0, self.1)
    }
}
impl<'st> SortDec<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<SortDec<'st>, ParseError> {
        <SortDec<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for SortDec<'st> {
    type Output = SortDec<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
        let m1 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
        p.expect(Token::RParen)?;
        Ok(Self(m0, m1))
    }
}
/// `(<symbol> <sort>)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct SelectorDec<'st>(pub Symbol<'st>, pub Sort<'st>);
impl std::fmt::Display for SelectorDec<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({} {})", self.0, self.1)
    }
}
impl<'st> SelectorDec<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<SelectorDec<'st>, ParseError> {
        <SelectorDec<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for SelectorDec<'st> {
    type Output = SelectorDec<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
        let m1 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
        p.expect(Token::RParen)?;
        Ok(Self(m0, m1))
    }
}
/// `(<symbol> <selector_dec>*)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct ConstructorDec<'st>(pub Symbol<'st>, pub &'st [SelectorDec<'st>]);
impl std::fmt::Display for ConstructorDec<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({} {})", self.0, self.1.iter().format(" "))
    }
}
impl<'st> ConstructorDec<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<ConstructorDec<'st>, ParseError> {
        <ConstructorDec<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for ConstructorDec<'st> {
    type Output = ConstructorDec<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
        let m1 = p.any::<SelectorDec<'st>>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0, m1))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum DatatypeDec<'st> {
    /// `(<constructor_dec>+)`
    DatatypeDec(&'st [ConstructorDec<'st>]),
    /// `(par (<symbol>+) (<constructor_dec>+))`
    Par(&'st [Symbol<'st>], &'st [ConstructorDec<'st>]),
}
impl std::fmt::Display for DatatypeDec<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::DatatypeDec(m0) => write!(f, "({})", m0.iter().format(" ")),
            Self::Par(m0, m1) => {
                write!(
                    f, "(par ({}) ({}))", m0.iter().format(" "), m1.iter().format(" ")
                )
            }
        }
    }
}
impl<'st> DatatypeDec<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<DatatypeDec<'st>, ParseError> {
        <DatatypeDec<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for DatatypeDec<'st> {
    type Output = DatatypeDec<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "par")
            && p.nth(offset + 2) == Token::LParen) || (p.nth(offset) == Token::LParen)
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "par")
            && p.nth(offset + 2) == Token::LParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "par")?;
            p.expect(Token::LParen)?;
            let m0 = p.non_zero::<Symbol<'st>>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::LParen)?;
            let m1 = p.non_zero::<ConstructorDec<'st>>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::Par(m0.into(), m1.into()));
        }
        if p.nth(offset) == Token::LParen {
            p.expect(Token::LParen)?;
            let m0 = p.non_zero::<ConstructorDec<'st>>()?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::DatatypeDec(m0.into()));
        }
        Err(p.stuck("DatatypeDec"))
    }
}
/// `(<symbol> (<sort>*) <sort>)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct FunctionDec<'st>(pub Symbol<'st>, pub &'st [Sort<'st>], pub Sort<'st>);
impl std::fmt::Display for FunctionDec<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({} ({}) {})", self.0, self.1.iter().format(" "), self.2)
    }
}
impl<'st> FunctionDec<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<FunctionDec<'st>, ParseError> {
        <FunctionDec<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for FunctionDec<'st> {
    type Output = FunctionDec<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
        p.expect(Token::LParen)?;
        let m1 = p.any::<Sort<'st>>()?;
        p.expect(Token::RParen)?;
        let m2 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
        p.expect(Token::RParen)?;
        Ok(Self(m0, m1, m2))
    }
}
/// `<symbol> (<sorted_var>*) <sort> <term>`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct FunctionDef<'st>(
    pub Symbol<'st>,
    pub &'st [SortedVar<'st>],
    pub Sort<'st>,
    pub &'st Term<'st>,
);
impl std::fmt::Display for FunctionDef<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "{} ({}) {} {}", self.0, self.1.iter().format(" "), self.2, self.3)
    }
}
impl<'st> FunctionDef<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<FunctionDef<'st>, ParseError> {
        <FunctionDef<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for FunctionDef<'st> {
    type Output = FunctionDef<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        Symbol::is_start_of(offset, p)
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
        p.expect(Token::LParen)?;
        let m1 = p.any::<SortedVar<'st>>()?;
        p.expect(Token::RParen)?;
        let m2 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
        let m3 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
        Ok(Self(m0, m1, m2, m3))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum PropLiteral<'st> {
    /// `<symbol>`
    Symbol(Symbol<'st>),
    /// `<symbol>`
    Not(Symbol<'st>),
}
impl std::fmt::Display for PropLiteral<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::Symbol(m0) => write!(f, "{}", m0),
            Self::Not(m0) => write!(f, "{}", m0),
        }
    }
}
impl<'st> PropLiteral<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<PropLiteral<'st>, ParseError> {
        <PropLiteral<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for PropLiteral<'st> {
    type Output = PropLiteral<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (Symbol::is_start_of(offset, p)) || (Symbol::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if Symbol::is_start_of(offset, p) {
            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Not(m0.into()));
        }
        if Symbol::is_start_of(offset, p) {
            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Symbol(m0.into()));
        }
        Err(p.stuck("PropLiteral"))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum Command<'st> {
    /// `(assert <term>)`
    Assert(&'st Term<'st>),
    /// `(check-sat)`
    CheckSat,
    /// `(check-sat-assuming (<prop_literal>*))`
    CheckSatAssuming(&'st [PropLiteral<'st>]),
    /// `(declare-const <symbol> <sort>)`
    DeclareConst(Symbol<'st>, Sort<'st>),
    /// `(declare-datatype <symbol> <datatype_dec>)`
    DeclareDatatype(Symbol<'st>, DatatypeDec<'st>),
    /// `(declare-datatypes (<sort_dec>n+1) (<datatype_dec>n+1))`
    DeclareDatatypes(&'st [SortDec<'st>], &'st [DatatypeDec<'st>]),
    /// `(declare-fun <symbol> (<sort>*) <sort>)`
    DeclareFun(Symbol<'st>, &'st [Sort<'st>], Sort<'st>),
    /// `(declare-sort <symbol> <numeral>)`
    DeclareSort(Symbol<'st>, Numeral<'st>),
    /// `(define-fun <function_def>)`
    DefineFun(FunctionDef<'st>),
    /// `(define-fun-rec <function_def>)`
    DefineFunRec(FunctionDef<'st>),
    /// `(define-funs-rec (<function_dec>n+1) (<term>n+1))`
    DefineFunsRec(&'st [FunctionDec<'st>], &'st [&'st Term<'st>]),
    /// `(define-sort <symbol> (<symbol>*) <sort>)`
    DefineSort(Symbol<'st>, &'st [Symbol<'st>], Sort<'st>),
    /// `(echo <string>)`
    Echo(&'st str),
    /// `(exit)`
    Exit,
    /// `(get-assertions)`
    GetAssertions,
    /// `(get-assignment)`
    GetAssignment,
    /// `(get-info <info_flag>)`
    GetInfo(InfoFlag<'st>),
    /// `(get-model)`
    GetModel,
    /// `(get-option <keyword>)`
    GetOption(Keyword<'st>),
    /// `(get-proof)`
    GetProof,
    /// `(get-unsat-assumptions)`
    GetUnsatAssumptions,
    /// `(get-unsat-core)`
    GetUnsatCore,
    /// `(get-value (<term>+))`
    GetValue(&'st [&'st Term<'st>]),
    /// `(pop <numeral>)`
    Pop(Numeral<'st>),
    /// `(push <numeral>)`
    Push(Numeral<'st>),
    /// `(reset)`
    Reset,
    /// `(reset-assertions)`
    ResetAssertions,
    /// `(set-info <attribute>)`
    SetInfo(Attribute<'st>),
    /// `(set-logic <symbol>)`
    SetLogic(Symbol<'st>),
    /// `(set-option <option>)`
    SetOption(Option<'st>),
    /// `(simplify <term>)`
    Simplify(&'st Term<'st>),
}
impl std::fmt::Display for Command<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::Assert(m0) => write!(f, "(assert {})", m0),
            Self::CheckSat => write!(f, "(check-sat)"),
            Self::CheckSatAssuming(m0) => {
                write!(f, "(check-sat-assuming ({}))", m0.iter().format(" "))
            }
            Self::DeclareConst(m0, m1) => write!(f, "(declare-const {} {})", m0, m1),
            Self::DeclareDatatype(m0, m1) => {
                write!(f, "(declare-datatype {} {})", m0, m1)
            }
            Self::DeclareDatatypes(m0, m1) => {
                write!(
                    f, "(declare-datatypes ({}) ({}))", m0.iter().format(" "), m1.iter()
                    .format(" ")
                )
            }
            Self::DeclareFun(m0, m1, m2) => {
                write!(f, "(declare-fun {} ({}) {})", m0, m1.iter().format(" "), m2)
            }
            Self::DeclareSort(m0, m1) => write!(f, "(declare-sort {} {})", m0, m1),
            Self::DefineFun(m0) => write!(f, "(define-fun {})", m0),
            Self::DefineFunRec(m0) => write!(f, "(define-fun-rec {})", m0),
            Self::DefineFunsRec(m0, m1) => {
                write!(
                    f, "(define-funs-rec ({}) ({}))", m0.iter().format(" "), m1.iter()
                    .format(" ")
                )
            }
            Self::DefineSort(m0, m1, m2) => {
                write!(f, "(define-sort {} ({}) {})", m0, m1.iter().format(" "), m2)
            }
            Self::Echo(m0) => write!(f, "(echo {})", m0),
            Self::Exit => write!(f, "(exit)"),
            Self::GetAssertions => write!(f, "(get-assertions)"),
            Self::GetAssignment => write!(f, "(get-assignment)"),
            Self::GetInfo(m0) => write!(f, "(get-info {})", m0),
            Self::GetModel => write!(f, "(get-model)"),
            Self::GetOption(m0) => write!(f, "(get-option {})", m0),
            Self::GetProof => write!(f, "(get-proof)"),
            Self::GetUnsatAssumptions => write!(f, "(get-unsat-assumptions)"),
            Self::GetUnsatCore => write!(f, "(get-unsat-core)"),
            Self::GetValue(m0) => write!(f, "(get-value ({}))", m0.iter().format(" ")),
            Self::Pop(m0) => write!(f, "(pop {})", m0),
            Self::Push(m0) => write!(f, "(push {})", m0),
            Self::Reset => write!(f, "(reset)"),
            Self::ResetAssertions => write!(f, "(reset-assertions)"),
            Self::SetInfo(m0) => write!(f, "(set-info {})", m0),
            Self::SetLogic(m0) => write!(f, "(set-logic {})", m0),
            Self::SetOption(m0) => write!(f, "(set-option {})", m0),
            Self::Simplify(m0) => write!(f, "(simplify {})", m0),
        }
    }
}
impl<'st> Command<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<Command<'st>, ParseError> {
        <Command<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for Command<'st> {
    type Output = Command<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Symbol, "define-funs-rec")
            && p.nth(offset + 2) == Token::LParen)
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "declare-datatypes")
                && p.nth(offset + 2) == Token::LParen)
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "get-value")
                && p.nth(offset + 2) == Token::LParen)
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "define-sort"))
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "declare-fun"))
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "check-sat-assuming")
                && p.nth(offset + 2) == Token::LParen)
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Symbol, "simplify"))
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "set-option"))
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "set-logic"))
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "set-info"))
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "reset-assertions")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "reset")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "push"))
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "pop"))
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "get-unsat-core")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "get-unsat-assumptions")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "get-proof")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "get-option"))
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "get-model")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "get-info"))
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "get-assignment")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "get-assertions")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "exit")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "echo"))
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "define-fun-rec"))
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "define-fun"))
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "declare-sort"))
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "declare-datatype"))
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "declare-const"))
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "check-sat")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "assert"))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Symbol, "define-funs-rec")
            && p.nth(offset + 2) == Token::LParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Symbol, "define-funs-rec")?;
            p.expect(Token::LParen)?;
            let m0 = p.n_plus_one::<FunctionDec<'st>>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::LParen)?;
            let m1 = p.n_plus_one::<Term<'st>>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::DefineFunsRec(m0.into(), m1.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "declare-datatypes")
            && p.nth(offset + 2) == Token::LParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "declare-datatypes")?;
            p.expect(Token::LParen)?;
            let m0 = p.n_plus_one::<SortDec<'st>>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::LParen)?;
            let m1 = p.n_plus_one::<DatatypeDec<'st>>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::DeclareDatatypes(m0.into(), m1.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "get-value")
            && p.nth(offset + 2) == Token::LParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "get-value")?;
            p.expect(Token::LParen)?;
            let m0 = p.non_zero::<Term<'st>>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::GetValue(m0.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "define-sort")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "define-sort")?;
            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::LParen)?;
            let m1 = p.any::<Symbol<'st>>()?;
            p.expect(Token::RParen)?;
            let m2 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::DefineSort(m0.into(), m1.into(), m2.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "declare-fun")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "declare-fun")?;
            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::LParen)?;
            let m1 = p.any::<Sort<'st>>()?;
            p.expect(Token::RParen)?;
            let m2 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::DeclareFun(m0.into(), m1.into(), m2.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "check-sat-assuming")
            && p.nth(offset + 2) == Token::LParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "check-sat-assuming")?;
            p.expect(Token::LParen)?;
            let m0 = p.any::<PropLiteral<'st>>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::CheckSatAssuming(m0.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Symbol, "simplify")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Symbol, "simplify")?;
            let m0 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Simplify(m0.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "set-option")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "set-option")?;
            let m0 = <Option<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::SetOption(m0.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "set-logic")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "set-logic")?;
            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::SetLogic(m0.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "set-info")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "set-info")?;
            let m0 = <Attribute<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::SetInfo(m0.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "reset-assertions")
            && p.nth(offset + 2) == Token::RParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "reset-assertions")?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::ResetAssertions);
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "reset")
            && p.nth(offset + 2) == Token::RParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "reset")?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Reset);
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "push")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "push")?;
            let m0 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Push(m0.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "pop")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "pop")?;
            let m0 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Pop(m0.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "get-unsat-core")
            && p.nth(offset + 2) == Token::RParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "get-unsat-core")?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::GetUnsatCore);
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "get-unsat-assumptions")
            && p.nth(offset + 2) == Token::RParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "get-unsat-assumptions")?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::GetUnsatAssumptions);
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "get-proof")
            && p.nth(offset + 2) == Token::RParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "get-proof")?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::GetProof);
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "get-option")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "get-option")?;
            let m0 = <Keyword<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::GetOption(m0.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "get-model")
            && p.nth(offset + 2) == Token::RParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "get-model")?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::GetModel);
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "get-info")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "get-info")?;
            let m0 = <InfoFlag<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::GetInfo(m0.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "get-assignment")
            && p.nth(offset + 2) == Token::RParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "get-assignment")?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::GetAssignment);
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "get-assertions")
            && p.nth(offset + 2) == Token::RParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "get-assertions")?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::GetAssertions);
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "exit")
            && p.nth(offset + 2) == Token::RParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "exit")?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Exit);
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "echo")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "echo")?;
            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Echo(m0.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "define-fun-rec")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "define-fun-rec")?;
            let m0 = <FunctionDef<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::DefineFunRec(m0.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "define-fun")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "define-fun")?;
            let m0 = <FunctionDef<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::DefineFun(m0.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "declare-sort")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "declare-sort")?;
            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
            let m1 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::DeclareSort(m0.into(), m1.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "declare-datatype")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "declare-datatype")?;
            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
            let m1 = <DatatypeDec<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::DeclareDatatype(m0.into(), m1.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "declare-const")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "declare-const")?;
            let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
            let m1 = <Sort<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::DeclareConst(m0.into(), m1.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "check-sat")
            && p.nth(offset + 2) == Token::RParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "check-sat")?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::CheckSat);
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "assert")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "assert")?;
            let m0 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Assert(m0.into()));
        }
        Err(p.stuck("Command"))
    }
}
impl<'st> Command<'st> {
    pub fn has_response(&self) -> bool {
        match self {
            Self::Assert(_) => false,
            Self::CheckSat => true,
            Self::CheckSatAssuming(_) => true,
            Self::DeclareConst(_, _) => false,
            Self::DeclareDatatype(_, _) => false,
            Self::DeclareDatatypes(_, _) => false,
            Self::DeclareFun(_, _, _) => false,
            Self::DeclareSort(_, _) => false,
            Self::DefineFun(_) => false,
            Self::DefineFunRec(_) => false,
            Self::DefineFunsRec(_, _) => false,
            Self::DefineSort(_, _, _) => false,
            Self::Echo(_) => true,
            Self::Exit => false,
            Self::GetAssertions => true,
            Self::GetAssignment => true,
            Self::GetInfo(_) => true,
            Self::GetModel => true,
            Self::GetOption(_) => true,
            Self::GetProof => true,
            Self::GetUnsatAssumptions => true,
            Self::GetUnsatCore => true,
            Self::GetValue(_) => true,
            Self::Pop(_) => false,
            Self::Push(_) => false,
            Self::Reset => false,
            Self::ResetAssertions => false,
            Self::SetInfo(_) => false,
            Self::SetLogic(_) => false,
            Self::SetOption(_) => false,
            Self::Simplify(_) => true,
        }
    }
    pub fn parse_response(
        &self,
        st: &'st Storage,
        response: &str,
    ) -> Result<std::option::Option<SpecificSuccessResponse<'st>>, ParseError> {
        match self {
            Self::Assert(_) => Ok(None),
            Self::CheckSat => {
                Ok(
                    Some(
                        SpecificSuccessResponse::CheckSatResponse(
                            <CheckSatResponse as SmtlibParse<
                                'st,
                            >>::parse(&mut Parser::new(st, response))?,
                        ),
                    ),
                )
            }
            Self::CheckSatAssuming(_) => {
                Ok(
                    Some(
                        SpecificSuccessResponse::CheckSatResponse(
                            <CheckSatResponse as SmtlibParse<
                                'st,
                            >>::parse(&mut Parser::new(st, response))?,
                        ),
                    ),
                )
            }
            Self::DeclareConst(_, _) => Ok(None),
            Self::DeclareDatatype(_, _) => Ok(None),
            Self::DeclareDatatypes(_, _) => Ok(None),
            Self::DeclareFun(_, _, _) => Ok(None),
            Self::DeclareSort(_, _) => Ok(None),
            Self::DefineFun(_) => Ok(None),
            Self::DefineFunRec(_) => Ok(None),
            Self::DefineFunsRec(_, _) => Ok(None),
            Self::DefineSort(_, _, _) => Ok(None),
            Self::Echo(_) => {
                Ok(
                    Some(
                        SpecificSuccessResponse::EchoResponse(
                            <EchoResponse<
                                'st,
                            > as SmtlibParse<
                                'st,
                            >>::parse(&mut Parser::new(st, response))?,
                        ),
                    ),
                )
            }
            Self::Exit => Ok(None),
            Self::GetAssertions => {
                Ok(
                    Some(
                        SpecificSuccessResponse::GetAssertionsResponse(
                            <GetAssertionsResponse<
                                'st,
                            > as SmtlibParse<
                                'st,
                            >>::parse(&mut Parser::new(st, response))?,
                        ),
                    ),
                )
            }
            Self::GetAssignment => {
                Ok(
                    Some(
                        SpecificSuccessResponse::GetAssignmentResponse(
                            <GetAssignmentResponse<
                                'st,
                            > as SmtlibParse<
                                'st,
                            >>::parse(&mut Parser::new(st, response))?,
                        ),
                    ),
                )
            }
            Self::GetInfo(_) => {
                Ok(
                    Some(
                        SpecificSuccessResponse::GetInfoResponse(
                            <GetInfoResponse<
                                'st,
                            > as SmtlibParse<
                                'st,
                            >>::parse(&mut Parser::new(st, response))?,
                        ),
                    ),
                )
            }
            Self::GetModel => {
                Ok(
                    Some(
                        SpecificSuccessResponse::GetModelResponse(
                            <GetModelResponse<
                                'st,
                            > as SmtlibParse<
                                'st,
                            >>::parse(&mut Parser::new(st, response))?,
                        ),
                    ),
                )
            }
            Self::GetOption(_) => {
                Ok(
                    Some(
                        SpecificSuccessResponse::GetOptionResponse(
                            <GetOptionResponse<
                                'st,
                            > as SmtlibParse<
                                'st,
                            >>::parse(&mut Parser::new(st, response))?,
                        ),
                    ),
                )
            }
            Self::GetProof => {
                Ok(
                    Some(
                        SpecificSuccessResponse::GetProofResponse(
                            <GetProofResponse<
                                'st,
                            > as SmtlibParse<
                                'st,
                            >>::parse(&mut Parser::new(st, response))?,
                        ),
                    ),
                )
            }
            Self::GetUnsatAssumptions => {
                Ok(
                    Some(
                        SpecificSuccessResponse::GetUnsatAssumptionsResponse(
                            <GetUnsatAssumptionsResponse<
                                'st,
                            > as SmtlibParse<
                                'st,
                            >>::parse(&mut Parser::new(st, response))?,
                        ),
                    ),
                )
            }
            Self::GetUnsatCore => {
                Ok(
                    Some(
                        SpecificSuccessResponse::GetUnsatCoreResponse(
                            <GetUnsatCoreResponse<
                                'st,
                            > as SmtlibParse<
                                'st,
                            >>::parse(&mut Parser::new(st, response))?,
                        ),
                    ),
                )
            }
            Self::GetValue(_) => {
                Ok(
                    Some(
                        SpecificSuccessResponse::GetValueResponse(
                            <GetValueResponse<
                                'st,
                            > as SmtlibParse<
                                'st,
                            >>::parse(&mut Parser::new(st, response))?,
                        ),
                    ),
                )
            }
            Self::Pop(_) => Ok(None),
            Self::Push(_) => Ok(None),
            Self::Reset => Ok(None),
            Self::ResetAssertions => Ok(None),
            Self::SetInfo(_) => Ok(None),
            Self::SetLogic(_) => Ok(None),
            Self::SetOption(_) => Ok(None),
            Self::Simplify(_) => {
                Ok(
                    Some(
                        SpecificSuccessResponse::SimplifyResponse(
                            <SimplifyResponse<
                                'st,
                            > as SmtlibParse<
                                'st,
                            >>::parse(&mut Parser::new(st, response))?,
                        ),
                    ),
                )
            }
        }
    }
}
/// `<command>*`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct Script<'st>(pub &'st [Command<'st>]);
impl std::fmt::Display for Script<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "{}", self.0.iter().format("\n"))
    }
}
impl<'st> Script<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<Script<'st>, ParseError> {
        <Script<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for Script<'st> {
    type Output = Script<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        todo!("{offset:?}, {p:?}")
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let m0 = p.any::<Command<'st>>()?;
        Ok(Self(m0))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum Option<'st> {
    /// `:diagnostic-output-channel <string>`
    DiagnosticOutputChannel(&'st str),
    /// `:global-declarations <b_value>`
    GlobalDeclarations(BValue),
    /// `:interactive-mode <b_value>`
    InteractiveMode(BValue),
    /// `:print-success <b_value>`
    PrintSuccess(BValue),
    /// `:produce-assertions <b_value>`
    ProduceAssertions(BValue),
    /// `:produce-assignments <b_value>`
    ProduceAssignments(BValue),
    /// `:produce-models <b_value>`
    ProduceModels(BValue),
    /// `:produce-proofs <b_value>`
    ProduceProofs(BValue),
    /// `:produce-unsat-assumptions <b_value>`
    ProduceUnsatAssumptions(BValue),
    /// `:produce-unsat-cores <b_value>`
    ProduceUnsatCores(BValue),
    /// `:random-seed <numeral>`
    RandomSeed(Numeral<'st>),
    /// `:regular-output-channel <string>`
    RegularOutputChannel(&'st str),
    /// `:reproducible-resource-limit <numeral>`
    ReproducibleResourceLimit(Numeral<'st>),
    /// `:verbosity <numeral>`
    Verbosity(Numeral<'st>),
    /// `<attribute>`
    Attribute(Attribute<'st>),
}
impl std::fmt::Display for Option<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::DiagnosticOutputChannel(m0) => {
                write!(f, ":diagnostic-output-channel {}", m0)
            }
            Self::GlobalDeclarations(m0) => write!(f, ":global-declarations {}", m0),
            Self::InteractiveMode(m0) => write!(f, ":interactive-mode {}", m0),
            Self::PrintSuccess(m0) => write!(f, ":print-success {}", m0),
            Self::ProduceAssertions(m0) => write!(f, ":produce-assertions {}", m0),
            Self::ProduceAssignments(m0) => write!(f, ":produce-assignments {}", m0),
            Self::ProduceModels(m0) => write!(f, ":produce-models {}", m0),
            Self::ProduceProofs(m0) => write!(f, ":produce-proofs {}", m0),
            Self::ProduceUnsatAssumptions(m0) => {
                write!(f, ":produce-unsat-assumptions {}", m0)
            }
            Self::ProduceUnsatCores(m0) => write!(f, ":produce-unsat-cores {}", m0),
            Self::RandomSeed(m0) => write!(f, ":random-seed {}", m0),
            Self::RegularOutputChannel(m0) => write!(f, ":regular-output-channel {}", m0),
            Self::ReproducibleResourceLimit(m0) => {
                write!(f, ":reproducible-resource-limit {}", m0)
            }
            Self::Verbosity(m0) => write!(f, ":verbosity {}", m0),
            Self::Attribute(m0) => write!(f, "{}", m0),
        }
    }
}
impl<'st> Option<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<Option<'st>, ParseError> {
        <Option<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for Option<'st> {
    type Output = Option<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth_matches(offset, Token::Keyword, ":verbosity"))
            || (p.nth_matches(offset, Token::Keyword, ":reproducible-resource-limit"))
            || (p.nth_matches(offset, Token::Keyword, ":regular-output-channel"))
            || (p.nth_matches(offset, Token::Keyword, ":random-seed"))
            || (p.nth_matches(offset, Token::Keyword, ":produce-unsat-cores"))
            || (p.nth_matches(offset, Token::Keyword, ":produce-unsat-assumptions"))
            || (p.nth_matches(offset, Token::Keyword, ":produce-proofs"))
            || (p.nth_matches(offset, Token::Keyword, ":produce-models"))
            || (p.nth_matches(offset, Token::Keyword, ":produce-assignments"))
            || (p.nth_matches(offset, Token::Keyword, ":produce-assertions"))
            || (p.nth_matches(offset, Token::Keyword, ":print-success"))
            || (p.nth_matches(offset, Token::Keyword, ":interactive-mode"))
            || (p.nth_matches(offset, Token::Keyword, ":global-declarations"))
            || (p.nth_matches(offset, Token::Keyword, ":diagnostic-output-channel"))
            || (Attribute::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth_matches(offset, Token::Keyword, ":verbosity") {
            p.expect_matches(Token::Keyword, ":verbosity")?;
            let m0 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Verbosity(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":reproducible-resource-limit") {
            p.expect_matches(Token::Keyword, ":reproducible-resource-limit")?;
            let m0 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::ReproducibleResourceLimit(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":regular-output-channel") {
            p.expect_matches(Token::Keyword, ":regular-output-channel")?;
            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::RegularOutputChannel(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":random-seed") {
            p.expect_matches(Token::Keyword, ":random-seed")?;
            let m0 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::RandomSeed(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":produce-unsat-cores") {
            p.expect_matches(Token::Keyword, ":produce-unsat-cores")?;
            let m0 = <BValue as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::ProduceUnsatCores(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":produce-unsat-assumptions") {
            p.expect_matches(Token::Keyword, ":produce-unsat-assumptions")?;
            let m0 = <BValue as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::ProduceUnsatAssumptions(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":produce-proofs") {
            p.expect_matches(Token::Keyword, ":produce-proofs")?;
            let m0 = <BValue as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::ProduceProofs(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":produce-models") {
            p.expect_matches(Token::Keyword, ":produce-models")?;
            let m0 = <BValue as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::ProduceModels(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":produce-assignments") {
            p.expect_matches(Token::Keyword, ":produce-assignments")?;
            let m0 = <BValue as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::ProduceAssignments(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":produce-assertions") {
            p.expect_matches(Token::Keyword, ":produce-assertions")?;
            let m0 = <BValue as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::ProduceAssertions(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":print-success") {
            p.expect_matches(Token::Keyword, ":print-success")?;
            let m0 = <BValue as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::PrintSuccess(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":interactive-mode") {
            p.expect_matches(Token::Keyword, ":interactive-mode")?;
            let m0 = <BValue as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::InteractiveMode(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":global-declarations") {
            p.expect_matches(Token::Keyword, ":global-declarations")?;
            let m0 = <BValue as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::GlobalDeclarations(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":diagnostic-output-channel") {
            p.expect_matches(Token::Keyword, ":diagnostic-output-channel")?;
            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::DiagnosticOutputChannel(m0.into()));
        }
        if Attribute::is_start_of(offset, p) {
            let m0 = <Attribute<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Attribute(m0.into()));
        }
        Err(p.stuck("Option"))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum InfoFlag<'st> {
    /// `:all-statistics`
    AllStatistics,
    /// `:assertion-stack-levels`
    AssertionStackLevels,
    /// `:authors`
    Authors,
    /// `:error-behavior`
    ErrorBehavior,
    /// `:name`
    Name,
    /// `:reason-unknown`
    ReasonUnknown,
    /// `:version`
    Version,
    /// `<keyword>`
    Keyword(Keyword<'st>),
}
impl std::fmt::Display for InfoFlag<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::AllStatistics => write!(f, ":all-statistics"),
            Self::AssertionStackLevels => write!(f, ":assertion-stack-levels"),
            Self::Authors => write!(f, ":authors"),
            Self::ErrorBehavior => write!(f, ":error-behavior"),
            Self::Name => write!(f, ":name"),
            Self::ReasonUnknown => write!(f, ":reason-unknown"),
            Self::Version => write!(f, ":version"),
            Self::Keyword(m0) => write!(f, "{}", m0),
        }
    }
}
impl<'st> InfoFlag<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<InfoFlag<'st>, ParseError> {
        <InfoFlag<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for InfoFlag<'st> {
    type Output = InfoFlag<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth_matches(offset, Token::Keyword, ":version"))
            || (p.nth_matches(offset, Token::Keyword, ":reason-unknown"))
            || (p.nth_matches(offset, Token::Keyword, ":name"))
            || (p.nth_matches(offset, Token::Keyword, ":error-behavior"))
            || (p.nth_matches(offset, Token::Keyword, ":authors"))
            || (p.nth_matches(offset, Token::Keyword, ":assertion-stack-levels"))
            || (p.nth_matches(offset, Token::Keyword, ":all-statistics"))
            || (Keyword::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth_matches(offset, Token::Keyword, ":version") {
            p.expect_matches(Token::Keyword, ":version")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Version);
        }
        if p.nth_matches(offset, Token::Keyword, ":reason-unknown") {
            p.expect_matches(Token::Keyword, ":reason-unknown")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::ReasonUnknown);
        }
        if p.nth_matches(offset, Token::Keyword, ":name") {
            p.expect_matches(Token::Keyword, ":name")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Name);
        }
        if p.nth_matches(offset, Token::Keyword, ":error-behavior") {
            p.expect_matches(Token::Keyword, ":error-behavior")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::ErrorBehavior);
        }
        if p.nth_matches(offset, Token::Keyword, ":authors") {
            p.expect_matches(Token::Keyword, ":authors")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Authors);
        }
        if p.nth_matches(offset, Token::Keyword, ":assertion-stack-levels") {
            p.expect_matches(Token::Keyword, ":assertion-stack-levels")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::AssertionStackLevels);
        }
        if p.nth_matches(offset, Token::Keyword, ":all-statistics") {
            p.expect_matches(Token::Keyword, ":all-statistics")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::AllStatistics);
        }
        if Keyword::is_start_of(offset, p) {
            let m0 = <Keyword<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Keyword(m0.into()));
        }
        Err(p.stuck("InfoFlag"))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum ErrorBehavior {
    /// `immediate-exit`
    ImmediateExit,
    /// `continued-execution`
    ContinuedExecution,
}
impl std::fmt::Display for ErrorBehavior {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::ImmediateExit => write!(f, "immediate-exit"),
            Self::ContinuedExecution => write!(f, "continued-execution"),
        }
    }
}
impl<'st> ErrorBehavior {
    pub fn parse(st: &'st Storage, src: &str) -> Result<ErrorBehavior, ParseError> {
        <ErrorBehavior as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for ErrorBehavior {
    type Output = ErrorBehavior;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth_matches(offset, Token::Symbol, "continued-execution"))
            || (p.nth_matches(offset, Token::Symbol, "immediate-exit"))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth_matches(offset, Token::Symbol, "continued-execution") {
            p.expect_matches(Token::Symbol, "continued-execution")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::ContinuedExecution);
        }
        if p.nth_matches(offset, Token::Symbol, "immediate-exit") {
            p.expect_matches(Token::Symbol, "immediate-exit")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::ImmediateExit);
        }
        Err(p.stuck("ErrorBehavior"))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum ReasonUnknown<'st> {
    /// `memout`
    Memout,
    /// `incomplete`
    Incomplete,
    /// `<s_expr>`
    SExpr(SExpr<'st>),
}
impl std::fmt::Display for ReasonUnknown<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::Memout => write!(f, "memout"),
            Self::Incomplete => write!(f, "incomplete"),
            Self::SExpr(m0) => write!(f, "{}", m0),
        }
    }
}
impl<'st> ReasonUnknown<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<ReasonUnknown<'st>, ParseError> {
        <ReasonUnknown<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for ReasonUnknown<'st> {
    type Output = ReasonUnknown<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth_matches(offset, Token::Symbol, "incomplete"))
            || (p.nth_matches(offset, Token::Symbol, "memout"))
            || (SExpr::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth_matches(offset, Token::Symbol, "incomplete") {
            p.expect_matches(Token::Symbol, "incomplete")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Incomplete);
        }
        if p.nth_matches(offset, Token::Symbol, "memout") {
            p.expect_matches(Token::Symbol, "memout")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Memout);
        }
        if SExpr::is_start_of(offset, p) {
            let m0 = <SExpr<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::SExpr(m0.into()));
        }
        Err(p.stuck("ReasonUnknown"))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum ModelResponse<'st> {
    /// `(define-fun <function_def>)`
    DefineFun(FunctionDef<'st>),
    /// `(define-fun-rec <function_def>)`
    DefineFunRec(FunctionDef<'st>),
    /// `(define-funs-rec (<function_dec>n+1) (<term>n+1))`
    DefineFunsRec(&'st [FunctionDec<'st>], &'st [&'st Term<'st>]),
}
impl std::fmt::Display for ModelResponse<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::DefineFun(m0) => write!(f, "(define-fun {})", m0),
            Self::DefineFunRec(m0) => write!(f, "(define-fun-rec {})", m0),
            Self::DefineFunsRec(m0, m1) => {
                write!(
                    f, "(define-funs-rec ({}) ({}))", m0.iter().format(" "), m1.iter()
                    .format(" ")
                )
            }
        }
    }
}
impl<'st> ModelResponse<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<ModelResponse<'st>, ParseError> {
        <ModelResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for ModelResponse<'st> {
    type Output = ModelResponse<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Symbol, "define-funs-rec")
            && p.nth(offset + 2) == Token::LParen)
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "define-fun-rec"))
            || (p.nth(offset) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "define-fun"))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Symbol, "define-funs-rec")
            && p.nth(offset + 2) == Token::LParen
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Symbol, "define-funs-rec")?;
            p.expect(Token::LParen)?;
            let m0 = p.n_plus_one::<FunctionDec<'st>>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::LParen)?;
            let m1 = p.n_plus_one::<Term<'st>>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::DefineFunsRec(m0.into(), m1.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "define-fun-rec")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "define-fun-rec")?;
            let m0 = <FunctionDef<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::DefineFunRec(m0.into()));
        }
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "define-fun")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "define-fun")?;
            let m0 = <FunctionDef<'st> as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::DefineFun(m0.into()));
        }
        Err(p.stuck("ModelResponse"))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum InfoResponse<'st> {
    /// `:assertion-stack-levels <numeral>`
    AssertionStackLevels(Numeral<'st>),
    /// `:authors <string>`
    Authors(&'st str),
    /// `:error-behavior <error-behavior>`
    ErrorBehavior(ErrorBehavior),
    /// `:name <string>`
    Name(&'st str),
    /// `:reason-unknown <reason-unknown>`
    ReasonUnknown(ReasonUnknown<'st>),
    /// `:version <string>`
    Version(&'st str),
    /// `<attribute>`
    Attribute(Attribute<'st>),
}
impl std::fmt::Display for InfoResponse<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::AssertionStackLevels(m0) => write!(f, ":assertion-stack-levels {}", m0),
            Self::Authors(m0) => write!(f, ":authors {}", m0),
            Self::ErrorBehavior(m0) => write!(f, ":error-behavior {}", m0),
            Self::Name(m0) => write!(f, ":name {}", m0),
            Self::ReasonUnknown(m0) => write!(f, ":reason-unknown {}", m0),
            Self::Version(m0) => write!(f, ":version {}", m0),
            Self::Attribute(m0) => write!(f, "{}", m0),
        }
    }
}
impl<'st> InfoResponse<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<InfoResponse<'st>, ParseError> {
        <InfoResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for InfoResponse<'st> {
    type Output = InfoResponse<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth_matches(offset, Token::Keyword, ":version"))
            || (p.nth_matches(offset, Token::Keyword, ":reason-unknown"))
            || (p.nth_matches(offset, Token::Keyword, ":name"))
            || (p.nth_matches(offset, Token::Keyword, ":error-behavior"))
            || (p.nth_matches(offset, Token::Keyword, ":authors"))
            || (p.nth_matches(offset, Token::Keyword, ":assertion-stack-levels"))
            || (Attribute::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth_matches(offset, Token::Keyword, ":version") {
            p.expect_matches(Token::Keyword, ":version")?;
            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Version(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":reason-unknown") {
            p.expect_matches(Token::Keyword, ":reason-unknown")?;
            let m0 = <ReasonUnknown<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::ReasonUnknown(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":name") {
            p.expect_matches(Token::Keyword, ":name")?;
            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Name(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":error-behavior") {
            p.expect_matches(Token::Keyword, ":error-behavior")?;
            let m0 = <ErrorBehavior as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::ErrorBehavior(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":authors") {
            p.expect_matches(Token::Keyword, ":authors")?;
            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Authors(m0.into()));
        }
        if p.nth_matches(offset, Token::Keyword, ":assertion-stack-levels") {
            p.expect_matches(Token::Keyword, ":assertion-stack-levels")?;
            let m0 = <Numeral<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::AssertionStackLevels(m0.into()));
        }
        if Attribute::is_start_of(offset, p) {
            let m0 = <Attribute<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Attribute(m0.into()));
        }
        Err(p.stuck("InfoResponse"))
    }
}
/// `(<term> <term>)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct ValuationPair<'st>(pub &'st Term<'st>, pub &'st Term<'st>);
impl std::fmt::Display for ValuationPair<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({} {})", self.0, self.1)
    }
}
impl<'st> ValuationPair<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<ValuationPair<'st>, ParseError> {
        <ValuationPair<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for ValuationPair<'st> {
    type Output = ValuationPair<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
        let m1 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
        p.expect(Token::RParen)?;
        Ok(Self(m0, m1))
    }
}
/// `(<symbol> <b_value>)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct TValuationPair<'st>(pub Symbol<'st>, pub BValue);
impl std::fmt::Display for TValuationPair<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({} {})", self.0, self.1)
    }
}
impl<'st> TValuationPair<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<TValuationPair<'st>, ParseError> {
        <TValuationPair<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for TValuationPair<'st> {
    type Output = TValuationPair<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Symbol<'st> as SmtlibParse<'st>>::parse(p)?;
        let m1 = <BValue as SmtlibParse<'st>>::parse(p)?;
        p.expect(Token::RParen)?;
        Ok(Self(m0, m1))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum CheckSatResponse {
    /// `sat`
    Sat,
    /// `unsat`
    Unsat,
    /// `unknown`
    Unknown,
}
impl std::fmt::Display for CheckSatResponse {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::Sat => write!(f, "sat"),
            Self::Unsat => write!(f, "unsat"),
            Self::Unknown => write!(f, "unknown"),
        }
    }
}
impl<'st> CheckSatResponse {
    pub fn parse(st: &'st Storage, src: &str) -> Result<CheckSatResponse, ParseError> {
        <CheckSatResponse as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for CheckSatResponse {
    type Output = CheckSatResponse;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth_matches(offset, Token::Symbol, "unknown"))
            || (p.nth_matches(offset, Token::Symbol, "unsat"))
            || (p.nth_matches(offset, Token::Symbol, "sat"))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth_matches(offset, Token::Symbol, "unknown") {
            p.expect_matches(Token::Symbol, "unknown")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Unknown);
        }
        if p.nth_matches(offset, Token::Symbol, "unsat") {
            p.expect_matches(Token::Symbol, "unsat")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Unsat);
        }
        if p.nth_matches(offset, Token::Symbol, "sat") {
            p.expect_matches(Token::Symbol, "sat")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Sat);
        }
        Err(p.stuck("CheckSatResponse"))
    }
}
/// `<string>`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct EchoResponse<'st>(pub &'st str);
impl std::fmt::Display for EchoResponse<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "{}", self.0)
    }
}
impl<'st> EchoResponse<'st> {
    pub fn parse(st: &'st Storage, src: &str) -> Result<EchoResponse<'st>, ParseError> {
        <EchoResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for EchoResponse<'st> {
    type Output = EchoResponse<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        String::is_start_of(offset, p)
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let m0 = <String as SmtlibParse<'st>>::parse(p)?;
        Ok(Self(m0))
    }
}
/// `(<term>*)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct GetAssertionsResponse<'st>(pub &'st [&'st Term<'st>]);
impl std::fmt::Display for GetAssertionsResponse<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({})", self.0.iter().format(" "))
    }
}
impl<'st> GetAssertionsResponse<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<GetAssertionsResponse<'st>, ParseError> {
        <GetAssertionsResponse<
            'st,
        > as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for GetAssertionsResponse<'st> {
    type Output = GetAssertionsResponse<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = p.any::<Term<'st>>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0))
    }
}
/// `(<t_valuation_pair>*)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct GetAssignmentResponse<'st>(pub &'st [TValuationPair<'st>]);
impl std::fmt::Display for GetAssignmentResponse<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({})", self.0.iter().format(" "))
    }
}
impl<'st> GetAssignmentResponse<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<GetAssignmentResponse<'st>, ParseError> {
        <GetAssignmentResponse<
            'st,
        > as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for GetAssignmentResponse<'st> {
    type Output = GetAssignmentResponse<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = p.any::<TValuationPair<'st>>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0))
    }
}
/// `(<info_response>+)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct GetInfoResponse<'st>(pub &'st [InfoResponse<'st>]);
impl std::fmt::Display for GetInfoResponse<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({})", self.0.iter().format(" "))
    }
}
impl<'st> GetInfoResponse<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<GetInfoResponse<'st>, ParseError> {
        <GetInfoResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for GetInfoResponse<'st> {
    type Output = GetInfoResponse<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = p.non_zero::<InfoResponse<'st>>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0))
    }
}
/// `(<model_response>*)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct GetModelResponse<'st>(pub &'st [ModelResponse<'st>]);
impl std::fmt::Display for GetModelResponse<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({})", self.0.iter().format(" "))
    }
}
impl<'st> GetModelResponse<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<GetModelResponse<'st>, ParseError> {
        <GetModelResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for GetModelResponse<'st> {
    type Output = GetModelResponse<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = p.any::<ModelResponse<'st>>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0))
    }
}
/// `<attribute_value>`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct GetOptionResponse<'st>(pub AttributeValue<'st>);
impl std::fmt::Display for GetOptionResponse<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "{}", self.0)
    }
}
impl<'st> GetOptionResponse<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<GetOptionResponse<'st>, ParseError> {
        <GetOptionResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for GetOptionResponse<'st> {
    type Output = GetOptionResponse<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        AttributeValue::is_start_of(offset, p)
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let m0 = <AttributeValue<'st> as SmtlibParse<'st>>::parse(p)?;
        Ok(Self(m0))
    }
}
/// `<s_expr>`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct GetProofResponse<'st>(pub SExpr<'st>);
impl std::fmt::Display for GetProofResponse<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "{}", self.0)
    }
}
impl<'st> GetProofResponse<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<GetProofResponse<'st>, ParseError> {
        <GetProofResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for GetProofResponse<'st> {
    type Output = GetProofResponse<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        SExpr::is_start_of(offset, p)
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let m0 = <SExpr<'st> as SmtlibParse<'st>>::parse(p)?;
        Ok(Self(m0))
    }
}
/// `(<symbol>*)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct GetUnsatAssumptionsResponse<'st>(pub &'st [Symbol<'st>]);
impl std::fmt::Display for GetUnsatAssumptionsResponse<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({})", self.0.iter().format(" "))
    }
}
impl<'st> GetUnsatAssumptionsResponse<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<GetUnsatAssumptionsResponse<'st>, ParseError> {
        <GetUnsatAssumptionsResponse<
            'st,
        > as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for GetUnsatAssumptionsResponse<'st> {
    type Output = GetUnsatAssumptionsResponse<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = p.any::<Symbol<'st>>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0))
    }
}
/// `(<symbol>*)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct GetUnsatCoreResponse<'st>(pub &'st [Symbol<'st>]);
impl std::fmt::Display for GetUnsatCoreResponse<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({})", self.0.iter().format(" "))
    }
}
impl<'st> GetUnsatCoreResponse<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<GetUnsatCoreResponse<'st>, ParseError> {
        <GetUnsatCoreResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for GetUnsatCoreResponse<'st> {
    type Output = GetUnsatCoreResponse<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = p.any::<Symbol<'st>>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0))
    }
}
/// `(<valuation_pair>+)`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct GetValueResponse<'st>(pub &'st [ValuationPair<'st>]);
impl std::fmt::Display for GetValueResponse<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({})", self.0.iter().format(" "))
    }
}
impl<'st> GetValueResponse<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<GetValueResponse<'st>, ParseError> {
        <GetValueResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for GetValueResponse<'st> {
    type Output = GetValueResponse<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        p.nth(offset) == Token::LParen
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = p.non_zero::<ValuationPair<'st>>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0))
    }
}
/// `<term>`
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub struct SimplifyResponse<'st>(pub &'st Term<'st>);
impl std::fmt::Display for SimplifyResponse<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "{}", self.0)
    }
}
impl<'st> SimplifyResponse<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<SimplifyResponse<'st>, ParseError> {
        <SimplifyResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for SimplifyResponse<'st> {
    type Output = SimplifyResponse<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        Term::is_start_of(offset, p)
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let m0 = <Term<'st> as SmtlibParse<'st>>::parse(p)?;
        Ok(Self(m0))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum SpecificSuccessResponse<'st> {
    /// `<get_unsat_assumptions_response>`
    GetUnsatAssumptionsResponse(GetUnsatAssumptionsResponse<'st>),
    /// `<check_sat_response>`
    CheckSatResponse(CheckSatResponse),
    /// `<echo_response>`
    EchoResponse(EchoResponse<'st>),
    /// `<get_assertions_response>`
    GetAssertionsResponse(GetAssertionsResponse<'st>),
    /// `<get_assignment_response>`
    GetAssignmentResponse(GetAssignmentResponse<'st>),
    /// `<get_info_response>`
    GetInfoResponse(GetInfoResponse<'st>),
    /// `<get_model_response>`
    GetModelResponse(GetModelResponse<'st>),
    /// `<get_option_response>`
    GetOptionResponse(GetOptionResponse<'st>),
    /// `<get_proof_response>`
    GetProofResponse(GetProofResponse<'st>),
    /// `<get_unsat_core_response>`
    GetUnsatCoreResponse(GetUnsatCoreResponse<'st>),
    /// `<get_value_response>`
    GetValueResponse(GetValueResponse<'st>),
    /// `<simplify_response>`
    SimplifyResponse(SimplifyResponse<'st>),
}
impl std::fmt::Display for SpecificSuccessResponse<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::GetUnsatAssumptionsResponse(m0) => write!(f, "{}", m0),
            Self::CheckSatResponse(m0) => write!(f, "{}", m0),
            Self::EchoResponse(m0) => write!(f, "{}", m0),
            Self::GetAssertionsResponse(m0) => write!(f, "{}", m0),
            Self::GetAssignmentResponse(m0) => write!(f, "{}", m0),
            Self::GetInfoResponse(m0) => write!(f, "{}", m0),
            Self::GetModelResponse(m0) => write!(f, "{}", m0),
            Self::GetOptionResponse(m0) => write!(f, "{}", m0),
            Self::GetProofResponse(m0) => write!(f, "{}", m0),
            Self::GetUnsatCoreResponse(m0) => write!(f, "{}", m0),
            Self::GetValueResponse(m0) => write!(f, "{}", m0),
            Self::SimplifyResponse(m0) => write!(f, "{}", m0),
        }
    }
}
impl<'st> SpecificSuccessResponse<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<SpecificSuccessResponse<'st>, ParseError> {
        <SpecificSuccessResponse<
            'st,
        > as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for SpecificSuccessResponse<'st> {
    type Output = SpecificSuccessResponse<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (SimplifyResponse::is_start_of(offset, p))
            || (GetValueResponse::is_start_of(offset, p))
            || (GetUnsatCoreResponse::is_start_of(offset, p))
            || (GetProofResponse::is_start_of(offset, p))
            || (GetOptionResponse::is_start_of(offset, p))
            || (GetModelResponse::is_start_of(offset, p))
            || (GetInfoResponse::is_start_of(offset, p))
            || (GetAssignmentResponse::is_start_of(offset, p))
            || (GetAssertionsResponse::is_start_of(offset, p))
            || (EchoResponse::is_start_of(offset, p))
            || (CheckSatResponse::is_start_of(offset, p))
            || (GetUnsatAssumptionsResponse::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if SimplifyResponse::is_start_of(offset, p) {
            let m0 = <SimplifyResponse<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::SimplifyResponse(m0.into()));
        }
        if GetValueResponse::is_start_of(offset, p) {
            let m0 = <GetValueResponse<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::GetValueResponse(m0.into()));
        }
        if GetUnsatCoreResponse::is_start_of(offset, p) {
            let m0 = <GetUnsatCoreResponse<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::GetUnsatCoreResponse(m0.into()));
        }
        if GetProofResponse::is_start_of(offset, p) {
            let m0 = <GetProofResponse<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::GetProofResponse(m0.into()));
        }
        if GetOptionResponse::is_start_of(offset, p) {
            let m0 = <GetOptionResponse<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::GetOptionResponse(m0.into()));
        }
        if GetModelResponse::is_start_of(offset, p) {
            let m0 = <GetModelResponse<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::GetModelResponse(m0.into()));
        }
        if GetInfoResponse::is_start_of(offset, p) {
            let m0 = <GetInfoResponse<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::GetInfoResponse(m0.into()));
        }
        if GetAssignmentResponse::is_start_of(offset, p) {
            let m0 = <GetAssignmentResponse<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::GetAssignmentResponse(m0.into()));
        }
        if GetAssertionsResponse::is_start_of(offset, p) {
            let m0 = <GetAssertionsResponse<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::GetAssertionsResponse(m0.into()));
        }
        if EchoResponse::is_start_of(offset, p) {
            let m0 = <EchoResponse<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::EchoResponse(m0.into()));
        }
        if CheckSatResponse::is_start_of(offset, p) {
            let m0 = <CheckSatResponse as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::CheckSatResponse(m0.into()));
        }
        if GetUnsatAssumptionsResponse::is_start_of(offset, p) {
            let m0 = <GetUnsatAssumptionsResponse<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::GetUnsatAssumptionsResponse(m0.into()));
        }
        Err(p.stuck("SpecificSuccessResponse"))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize))]
pub enum GeneralResponse<'st> {
    /// `success`
    Success,
    /// `<specific_success_response>`
    SpecificSuccessResponse(SpecificSuccessResponse<'st>),
    /// `unsupported`
    Unsupported,
    /// `(error <string>)`
    Error(&'st str),
}
impl std::fmt::Display for GeneralResponse<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        match self {
            Self::Success => write!(f, "success"),
            Self::SpecificSuccessResponse(m0) => write!(f, "{}", m0),
            Self::Unsupported => write!(f, "unsupported"),
            Self::Error(m0) => write!(f, "(error {})", m0),
        }
    }
}
impl<'st> GeneralResponse<'st> {
    pub fn parse(
        st: &'st Storage,
        src: &str,
    ) -> Result<GeneralResponse<'st>, ParseError> {
        <GeneralResponse<'st> as SmtlibParse<'st>>::parse(&mut Parser::new(st, src))
    }
}
impl<'st> SmtlibParse<'st> for GeneralResponse<'st> {
    type Output = GeneralResponse<'st>;
    fn is_start_of(offset: usize, p: &mut Parser<'st, '_>) -> bool {
        (p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Symbol, "error"))
            || (p.nth_matches(offset, Token::Symbol, "unsupported"))
            || (p.nth_matches(offset, Token::Symbol, "success"))
            || (SpecificSuccessResponse::is_start_of(offset, p))
    }
    fn parse(p: &mut Parser<'st, '_>) -> Result<Self::Output, ParseError> {
        let offset = 0;
        if p.nth(offset) == Token::LParen
            && p.nth_matches(offset + 1, Token::Symbol, "error")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Symbol, "error")?;
            let m0 = <String as SmtlibParse<'st>>::parse(p)?;
            p.expect(Token::RParen)?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Error(m0.into()));
        }
        if p.nth_matches(offset, Token::Symbol, "unsupported") {
            p.expect_matches(Token::Symbol, "unsupported")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Unsupported);
        }
        if p.nth_matches(offset, Token::Symbol, "success") {
            p.expect_matches(Token::Symbol, "success")?;
            #[allow(clippy::useless_conversion)] return Ok(Self::Success);
        }
        if SpecificSuccessResponse::is_start_of(offset, p) {
            let m0 = <SpecificSuccessResponse<'st> as SmtlibParse<'st>>::parse(p)?;
            #[allow(clippy::useless_conversion)]
            return Ok(Self::SpecificSuccessResponse(m0.into()));
        }
        Err(p.stuck("GeneralResponse"))
    }
}