smtlib-lowlevel 0.1.1

#![allow(clippy::all)]
//! This file is autogenerated! DO NOT EDIT!

use crate::lexicon::*;
use crate::parse::{ParseError, Parser, Token};
use itertools::Itertools;

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum SpecConstant {
    /// `<numeral>`
    Numeral(Numeral),
    /// `<decimal>`
    Decimal(Decimal),
    /// `<hexadecimal>`
    Hexadecimal(Hexadecimal),
    /// `<binary>`
    Binary(Binary),
    /// `<string>`
    String(String),
}

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 SpecConstant {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for SpecConstant {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (String::is_start_of(offset + 0, p))
            || (Binary::is_start_of(offset + 0, p))
            || (Hexadecimal::is_start_of(offset + 0, p))
            || (Decimal::is_start_of(offset + 0, p))
            || (Numeral::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if String::is_start_of(offset + 0, p) {
            let m0 = <String as SmtlibParse>::parse(p)?;
            return Ok(Self::String(m0.into()));
        }
        if Binary::is_start_of(offset + 0, p) {
            let m0 = <Binary as SmtlibParse>::parse(p)?;
            return Ok(Self::Binary(m0.into()));
        }
        if Hexadecimal::is_start_of(offset + 0, p) {
            let m0 = <Hexadecimal as SmtlibParse>::parse(p)?;
            return Ok(Self::Hexadecimal(m0.into()));
        }
        if Decimal::is_start_of(offset + 0, p) {
            let m0 = <Decimal as SmtlibParse>::parse(p)?;
            return Ok(Self::Decimal(m0.into()));
        }
        if Numeral::is_start_of(offset + 0, p) {
            let m0 = <Numeral as SmtlibParse>::parse(p)?;
            return Ok(Self::Numeral(m0.into()));
        }
        Err(p.stuck("spec_constant"))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum SExpr {
    /// `<spec_constant>`
    SpecConstant(SpecConstant),
    /// `<symbol>`
    Symbol(Symbol),
    /// `<reserved>`
    Reserved(Reserved),
    /// `<keyword>`
    Keyword(Keyword),
    /// `(<s_expr>*)`
    Paren(Vec<SExpr>),
}

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 SExpr {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for SExpr {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth(offset + 0) == Token::LParen)
            || (Keyword::is_start_of(offset + 0, p))
            || (Reserved::is_start_of(offset + 0, p))
            || (Symbol::is_start_of(offset + 0, p))
            || (SpecConstant::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth(offset + 0) == Token::LParen {
            p.expect(Token::LParen)?;
            let m0 = p.any::<SExpr>()?;
            p.expect(Token::RParen)?;
            return Ok(Self::Paren(m0.into()));
        }
        if Keyword::is_start_of(offset + 0, p) {
            let m0 = <Keyword as SmtlibParse>::parse(p)?;
            return Ok(Self::Keyword(m0.into()));
        }
        if Reserved::is_start_of(offset + 0, p) {
            let m0 = <Reserved as SmtlibParse>::parse(p)?;
            return Ok(Self::Reserved(m0.into()));
        }
        if Symbol::is_start_of(offset + 0, p) {
            let m0 = <Symbol as SmtlibParse>::parse(p)?;
            return Ok(Self::Symbol(m0.into()));
        }
        if SpecConstant::is_start_of(offset + 0, p) {
            let m0 = <SpecConstant as SmtlibParse>::parse(p)?;
            return Ok(Self::SpecConstant(m0.into()));
        }
        Err(p.stuck("s_expr"))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum Index {
    /// `<numeral>`
    Numeral(Numeral),
    /// `<symbol>`
    Symbol(Symbol),
}

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 Index {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for Index {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (Symbol::is_start_of(offset + 0, p)) || (Numeral::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if Symbol::is_start_of(offset + 0, p) {
            let m0 = <Symbol as SmtlibParse>::parse(p)?;
            return Ok(Self::Symbol(m0.into()));
        }
        if Numeral::is_start_of(offset + 0, p) {
            let m0 = <Numeral as SmtlibParse>::parse(p)?;
            return Ok(Self::Numeral(m0.into()));
        }
        Err(p.stuck("index"))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum Identifier {
    /// `<symbol>`
    Simple(Symbol),
    /// `(_ <symbol> <index>+)`
    Indexed(Symbol, Vec<Index>),
}

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 Identifier {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for Identifier {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth(offset + 0) == Token::LParen && p.nth_matches(offset + 1, Token::Reserved, "_"))
            || (Symbol::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth(offset + 0) == Token::LParen && p.nth_matches(offset + 1, Token::Reserved, "_") {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "_")?;
            let m0 = <Symbol as SmtlibParse>::parse(p)?;
            let m1 = p.non_zero::<Index>()?;
            p.expect(Token::RParen)?;
            return Ok(Self::Indexed(m0.into(), m1.into()));
        }
        if Symbol::is_start_of(offset + 0, p) {
            let m0 = <Symbol as SmtlibParse>::parse(p)?;
            return Ok(Self::Simple(m0.into()));
        }
        Err(p.stuck("identifier"))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum AttributeValue {
    /// `<spec_constant>`
    SpecConstant(SpecConstant),
    /// `<symbol>`
    Symbol(Symbol),
    /// `(<s_expr>)`
    Expr(SExpr),
}

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 AttributeValue {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for AttributeValue {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth(offset + 0) == Token::LParen)
            || (Symbol::is_start_of(offset + 0, p))
            || (SpecConstant::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth(offset + 0) == Token::LParen {
            p.expect(Token::LParen)?;
            let m0 = <SExpr as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::Expr(m0.into()));
        }
        if Symbol::is_start_of(offset + 0, p) {
            let m0 = <Symbol as SmtlibParse>::parse(p)?;
            return Ok(Self::Symbol(m0.into()));
        }
        if SpecConstant::is_start_of(offset + 0, p) {
            let m0 = <SpecConstant as SmtlibParse>::parse(p)?;
            return Ok(Self::SpecConstant(m0.into()));
        }
        Err(p.stuck("attribute_value"))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum Attribute {
    /// `<keyword>`
    Keyword(Keyword),
    /// `<keyword> <attribute_value>`
    WithValue(Keyword, AttributeValue),
}

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 Attribute {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for Attribute {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (Keyword::is_start_of(offset + 0, p) && AttributeValue::is_start_of(offset + 1, p))
            || (Keyword::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if Keyword::is_start_of(offset + 0, p) && AttributeValue::is_start_of(offset + 1, p) {
            let m0 = <Keyword as SmtlibParse>::parse(p)?;
            let m1 = <AttributeValue as SmtlibParse>::parse(p)?;
            return Ok(Self::WithValue(m0.into(), m1.into()));
        }
        if Keyword::is_start_of(offset + 0, p) {
            let m0 = <Keyword as SmtlibParse>::parse(p)?;
            return Ok(Self::Keyword(m0.into()));
        }
        Err(p.stuck("attribute"))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum Sort {
    /// `<identifier>`
    Sort(Identifier),
    /// `(<identifier> <sort>+)`
    Parametric(Identifier, Vec<Sort>),
}

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 Sort {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for Sort {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (Identifier::is_start_of(offset + 0, p)) || (p.nth(offset + 0) == Token::LParen)
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if Identifier::is_start_of(offset + 0, p) {
            let m0 = <Identifier as SmtlibParse>::parse(p)?;
            return Ok(Self::Sort(m0.into()));
        }
        if p.nth(offset + 0) == Token::LParen {
            p.expect(Token::LParen)?;
            let m0 = <Identifier as SmtlibParse>::parse(p)?;
            let m1 = p.non_zero::<Sort>()?;
            p.expect(Token::RParen)?;
            return Ok(Self::Parametric(m0.into(), m1.into()));
        }
        Err(p.stuck("sort"))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum QualIdentifier {
    /// `<identifier>`
    Identifier(Identifier),
    /// `(as <identifier> <sort>)`
    Sorted(Identifier, Sort),
}

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 QualIdentifier {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for QualIdentifier {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth(offset + 0) == Token::LParen && p.nth_matches(offset + 1, Token::Reserved, "as"))
            || (Identifier::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth(offset + 0) == Token::LParen && p.nth_matches(offset + 1, Token::Reserved, "as") {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "as")?;
            let m0 = <Identifier as SmtlibParse>::parse(p)?;
            let m1 = <Sort as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::Sorted(m0.into(), m1.into()));
        }
        if Identifier::is_start_of(offset + 0, p) {
            let m0 = <Identifier as SmtlibParse>::parse(p)?;
            return Ok(Self::Identifier(m0.into()));
        }
        Err(p.stuck("qual_identifier"))
    }
}

/// `(<symbol> <term>)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct VarBinding(pub Symbol, pub Term);

impl std::fmt::Display for VarBinding {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({} {})", self.0, self.1)
    }
}

impl VarBinding {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for VarBinding {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Symbol as SmtlibParse>::parse(p)?;
        let m1 = <Term as SmtlibParse>::parse(p)?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into(), m1.into()))
    }
}

/// `(<symbol> <sort>)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct SortedVar(pub Symbol, pub Sort);

impl std::fmt::Display for SortedVar {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({} {})", self.0, self.1)
    }
}

impl SortedVar {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for SortedVar {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Symbol as SmtlibParse>::parse(p)?;
        let m1 = <Sort as SmtlibParse>::parse(p)?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into(), m1.into()))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum Pattern {
    /// `<symbol>`
    Symbol(Symbol),
    /// `(<symbol> <symbol>+)`
    Application(Symbol, Vec<Symbol>),
}

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 Pattern {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for Pattern {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth(offset + 0) == Token::LParen) || (Symbol::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth(offset + 0) == Token::LParen {
            p.expect(Token::LParen)?;
            let m0 = <Symbol as SmtlibParse>::parse(p)?;
            let m1 = p.non_zero::<Symbol>()?;
            p.expect(Token::RParen)?;
            return Ok(Self::Application(m0.into(), m1.into()));
        }
        if Symbol::is_start_of(offset + 0, p) {
            let m0 = <Symbol as SmtlibParse>::parse(p)?;
            return Ok(Self::Symbol(m0.into()));
        }
        Err(p.stuck("pattern"))
    }
}

/// `(<pattern> <term>)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct MatchCase(pub Pattern, pub Term);

impl std::fmt::Display for MatchCase {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({} {})", self.0, self.1)
    }
}

impl MatchCase {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for MatchCase {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Pattern as SmtlibParse>::parse(p)?;
        let m1 = <Term as SmtlibParse>::parse(p)?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into(), m1.into()))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum Term {
    /// `<spec_constant>`
    SpecConstant(SpecConstant),
    /// `<qual_identifier>`
    Identifier(QualIdentifier),
    /// `(<qual_identifier> <term>+)`
    Application(QualIdentifier, Vec<Term>),
    /// `(let (<var_binding>+) <term>)`
    Let(Vec<VarBinding>, Box<Term>),
    /// `(forall (<sorted_var>+) <term>)`
    Forall(Vec<SortedVar>, Box<Term>),
    /// `(exists (<sorted_var>+) <term>)`
    Exists(Vec<SortedVar>, Box<Term>),
    /// `(match <term> (<match_case>+))`
    Match(Box<Term>, Vec<MatchCase>),
    /// `(! <term> <attribute>+)`
    Annotation(Box<Term>, Vec<Attribute>),
}

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 Term {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for Term {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth(offset + 0) == Token::LParen && p.nth_matches(offset + 1, Token::Reserved, "match"))
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "exists")
                && p.nth(offset + 2) == Token::LParen)
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "forall")
                && p.nth(offset + 2) == Token::LParen)
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "let")
                && p.nth(offset + 2) == Token::LParen)
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "!"))
            || (p.nth(offset + 0) == Token::LParen)
            || (QualIdentifier::is_start_of(offset + 0, p))
            || (SpecConstant::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth(offset + 0) == Token::LParen && p.nth_matches(offset + 1, Token::Reserved, "match")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "match")?;
            let m0 = <Term as SmtlibParse>::parse(p)?;
            p.expect(Token::LParen)?;
            let m1 = p.non_zero::<MatchCase>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::RParen)?;
            return Ok(Self::Match(m0.into(), m1.into()));
        }
        if p.nth(offset + 0) == 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>()?;
            p.expect(Token::RParen)?;
            let m1 = <Term as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::Exists(m0.into(), m1.into()));
        }
        if p.nth(offset + 0) == 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>()?;
            p.expect(Token::RParen)?;
            let m1 = <Term as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::Forall(m0.into(), m1.into()));
        }
        if p.nth(offset + 0) == 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>()?;
            p.expect(Token::RParen)?;
            let m1 = <Term as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::Let(m0.into(), m1.into()));
        }
        if p.nth(offset + 0) == Token::LParen && p.nth_matches(offset + 1, Token::Reserved, "!") {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "!")?;
            let m0 = <Term as SmtlibParse>::parse(p)?;
            let m1 = p.non_zero::<Attribute>()?;
            p.expect(Token::RParen)?;
            return Ok(Self::Annotation(m0.into(), m1.into()));
        }
        if p.nth(offset + 0) == Token::LParen {
            p.expect(Token::LParen)?;
            let m0 = <QualIdentifier as SmtlibParse>::parse(p)?;
            let m1 = p.non_zero::<Term>()?;
            p.expect(Token::RParen)?;
            return Ok(Self::Application(m0.into(), m1.into()));
        }
        if QualIdentifier::is_start_of(offset + 0, p) {
            let m0 = <QualIdentifier as SmtlibParse>::parse(p)?;
            return Ok(Self::Identifier(m0.into()));
        }
        if SpecConstant::is_start_of(offset + 0, p) {
            let m0 = <SpecConstant as SmtlibParse>::parse(p)?;
            return Ok(Self::SpecConstant(m0.into()));
        }
        Err(p.stuck("term"))
    }
}

/// `(<identifier> <numeral> <attribute>*)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct SortSymbolDecl(pub Identifier, pub Numeral, pub Vec<Attribute>);

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 SortSymbolDecl {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for SortSymbolDecl {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Identifier as SmtlibParse>::parse(p)?;
        let m1 = <Numeral as SmtlibParse>::parse(p)?;
        let m2 = p.any::<Attribute>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into(), m1.into(), m2.into()))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
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 MetaSpecConstant {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for MetaSpecConstant {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth_matches(offset + 0, Token::Reserved, "STRING"))
            || (p.nth_matches(offset + 0, Token::Reserved, "DECIMAL"))
            || (p.nth_matches(offset + 0, Token::Reserved, "NUMERAL"))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth_matches(offset + 0, Token::Reserved, "STRING") {
            p.expect_matches(Token::Reserved, "STRING")?;
            return Ok(Self::String);
        }
        if p.nth_matches(offset + 0, Token::Reserved, "DECIMAL") {
            p.expect_matches(Token::Reserved, "DECIMAL")?;
            return Ok(Self::Decimal);
        }
        if p.nth_matches(offset + 0, Token::Reserved, "NUMERAL") {
            p.expect_matches(Token::Reserved, "NUMERAL")?;
            return Ok(Self::Numeral);
        }
        Err(p.stuck("meta_spec_constant"))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum FunSymbolDecl {
    /// `(<spec_constant> <sort> <attribute>*)`
    SpecConstant(SpecConstant, Sort, Vec<Attribute>),
    /// `(<meta_spec_constant> <sort> <attribute>*)`
    MetaSpecConstant(MetaSpecConstant, Sort, Vec<Attribute>),
    /// `(<identifier> <sort>+ <attribute>*)`
    Identifier(Identifier, Vec<Sort>, Vec<Attribute>),
}

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 FunSymbolDecl {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for FunSymbolDecl {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth(offset + 0) == Token::LParen)
            || (p.nth(offset + 0) == Token::LParen)
            || (p.nth(offset + 0) == Token::LParen)
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth(offset + 0) == Token::LParen {
            p.expect(Token::LParen)?;
            let m0 = <Identifier as SmtlibParse>::parse(p)?;
            let m1 = p.non_zero::<Sort>()?;
            let m2 = p.any::<Attribute>()?;
            p.expect(Token::RParen)?;
            return Ok(Self::Identifier(m0.into(), m1.into(), m2.into()));
        }
        if p.nth(offset + 0) == Token::LParen {
            p.expect(Token::LParen)?;
            let m0 = <MetaSpecConstant as SmtlibParse>::parse(p)?;
            let m1 = <Sort as SmtlibParse>::parse(p)?;
            let m2 = p.any::<Attribute>()?;
            p.expect(Token::RParen)?;
            return Ok(Self::MetaSpecConstant(m0.into(), m1.into(), m2.into()));
        }
        if p.nth(offset + 0) == Token::LParen {
            p.expect(Token::LParen)?;
            let m0 = <SpecConstant as SmtlibParse>::parse(p)?;
            let m1 = <Sort as SmtlibParse>::parse(p)?;
            let m2 = p.any::<Attribute>()?;
            p.expect(Token::RParen)?;
            return Ok(Self::SpecConstant(m0.into(), m1.into(), m2.into()));
        }
        Err(p.stuck("fun_symbol_decl"))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum ParFunSymbolDecl {
    /// `(par (<symbol>+) (<identifier> <sort>+ <attribute>*))`
    Par(Vec<Symbol>, Identifier, Vec<Sort>, Vec<Attribute>),
    /// `<fun_symbol_decl>`
    FunSymbolDecl(FunSymbolDecl),
}

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 ParFunSymbolDecl {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for ParFunSymbolDecl {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth(offset + 0) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "par")
            && p.nth(offset + 2) == Token::LParen)
            || (FunSymbolDecl::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth(offset + 0) == 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>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::LParen)?;
            let m1 = <Identifier as SmtlibParse>::parse(p)?;
            let m2 = p.non_zero::<Sort>()?;
            let m3 = p.any::<Attribute>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::RParen)?;
            return Ok(Self::Par(m0.into(), m1.into(), m2.into(), m3.into()));
        }
        if FunSymbolDecl::is_start_of(offset + 0, p) {
            let m0 = <FunSymbolDecl as SmtlibParse>::parse(p)?;
            return Ok(Self::FunSymbolDecl(m0.into()));
        }
        Err(p.stuck("par_fun_symbol_decl"))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum TheoryAttribute {
    /// `:sorts (<sort_symbol_decl>+)`
    Sorts(Vec<SortSymbolDecl>),
    /// `:funs (<par_fun_symbol_decl>+)`
    Funs(Vec<ParFunSymbolDecl>),
    /// `:sorts-description <string>`
    SortsDescription(String),
    /// `:funs-description <string>`
    FunsDescription(String),
    /// `:definition <string>`
    Definition(String),
    /// `:values <string>`
    Values(String),
    /// `:notes <string>`
    Notes(String),
    /// `<attribute>`
    Attribute(Attribute),
}

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 TheoryAttribute {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for TheoryAttribute {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth_matches(offset + 0, Token::Keyword, ":funs") && p.nth(offset + 1) == Token::LParen)
            || (p.nth_matches(offset + 0, Token::Keyword, ":sorts")
                && p.nth(offset + 1) == Token::LParen)
            || (p.nth_matches(offset + 0, Token::Keyword, ":notes"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":values"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":definition"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":funs-description"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":sorts-description"))
            || (Attribute::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth_matches(offset + 0, 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>()?;
            p.expect(Token::RParen)?;
            return Ok(Self::Funs(m0.into()));
        }
        if p.nth_matches(offset + 0, 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>()?;
            p.expect(Token::RParen)?;
            return Ok(Self::Sorts(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":notes") {
            p.expect_matches(Token::Keyword, ":notes")?;
            let m0 = <String as SmtlibParse>::parse(p)?;
            return Ok(Self::Notes(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":values") {
            p.expect_matches(Token::Keyword, ":values")?;
            let m0 = <String as SmtlibParse>::parse(p)?;
            return Ok(Self::Values(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":definition") {
            p.expect_matches(Token::Keyword, ":definition")?;
            let m0 = <String as SmtlibParse>::parse(p)?;
            return Ok(Self::Definition(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":funs-description") {
            p.expect_matches(Token::Keyword, ":funs-description")?;
            let m0 = <String as SmtlibParse>::parse(p)?;
            return Ok(Self::FunsDescription(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":sorts-description") {
            p.expect_matches(Token::Keyword, ":sorts-description")?;
            let m0 = <String as SmtlibParse>::parse(p)?;
            return Ok(Self::SortsDescription(m0.into()));
        }
        if Attribute::is_start_of(offset + 0, p) {
            let m0 = <Attribute as SmtlibParse>::parse(p)?;
            return Ok(Self::Attribute(m0.into()));
        }
        Err(p.stuck("theory_attribute"))
    }
}

/// `(theory <symbol> <theory_attribute>+)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct TheoryDecl(pub Symbol, pub Vec<TheoryAttribute>);

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 TheoryDecl {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for TheoryDecl {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen && p.nth_matches(offset + 1, Token::Symbol, "theory")
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        p.expect_matches(Token::Symbol, "theory")?;
        let m0 = <Symbol as SmtlibParse>::parse(p)?;
        let m1 = p.non_zero::<TheoryAttribute>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into(), m1.into()))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum LogicAttribute {
    /// `:theories (<symbol>+)`
    Theories(Vec<Symbol>),
    /// `:language <string>`
    Language(String),
    /// `:extensions <string>`
    Extensions(String),
    /// `:values <string>`
    Values(String),
    /// `:notes <string>`
    Notes(String),
    /// `<attribute>`
    Attribute(Attribute),
}

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 LogicAttribute {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for LogicAttribute {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth_matches(offset + 0, Token::Keyword, ":theories")
            && p.nth(offset + 1) == Token::LParen)
            || (p.nth_matches(offset + 0, Token::Keyword, ":notes"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":values"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":extensions"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":language"))
            || (Attribute::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth_matches(offset + 0, Token::Keyword, ":theories")
            && p.nth(offset + 1) == Token::LParen
        {
            p.expect_matches(Token::Keyword, ":theories")?;
            p.expect(Token::LParen)?;
            let m0 = p.non_zero::<Symbol>()?;
            p.expect(Token::RParen)?;
            return Ok(Self::Theories(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":notes") {
            p.expect_matches(Token::Keyword, ":notes")?;
            let m0 = <String as SmtlibParse>::parse(p)?;
            return Ok(Self::Notes(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":values") {
            p.expect_matches(Token::Keyword, ":values")?;
            let m0 = <String as SmtlibParse>::parse(p)?;
            return Ok(Self::Values(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":extensions") {
            p.expect_matches(Token::Keyword, ":extensions")?;
            let m0 = <String as SmtlibParse>::parse(p)?;
            return Ok(Self::Extensions(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":language") {
            p.expect_matches(Token::Keyword, ":language")?;
            let m0 = <String as SmtlibParse>::parse(p)?;
            return Ok(Self::Language(m0.into()));
        }
        if Attribute::is_start_of(offset + 0, p) {
            let m0 = <Attribute as SmtlibParse>::parse(p)?;
            return Ok(Self::Attribute(m0.into()));
        }
        Err(p.stuck("logic_attribute"))
    }
}

/// `(logic <symbol> <logic_attribute>+)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct Logic(pub Symbol, pub Vec<LogicAttribute>);

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 Logic {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for Logic {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen && p.nth_matches(offset + 1, Token::Symbol, "logic")
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        p.expect_matches(Token::Symbol, "logic")?;
        let m0 = <Symbol as SmtlibParse>::parse(p)?;
        let m1 = p.non_zero::<LogicAttribute>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into(), m1.into()))
    }
}

/// `(<symbol> <numeral>)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct SortDec(pub Symbol, pub Numeral);

impl std::fmt::Display for SortDec {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({} {})", self.0, self.1)
    }
}

impl SortDec {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for SortDec {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Symbol as SmtlibParse>::parse(p)?;
        let m1 = <Numeral as SmtlibParse>::parse(p)?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into(), m1.into()))
    }
}

/// `(<symbol> <sort>)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct SelectorDec(pub Symbol, pub Sort);

impl std::fmt::Display for SelectorDec {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({} {})", self.0, self.1)
    }
}

impl SelectorDec {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for SelectorDec {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Symbol as SmtlibParse>::parse(p)?;
        let m1 = <Sort as SmtlibParse>::parse(p)?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into(), m1.into()))
    }
}

/// `(<symbol> <selector_dec>*)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct ConstructorDec(pub Symbol, pub Vec<SelectorDec>);

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 ConstructorDec {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for ConstructorDec {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Symbol as SmtlibParse>::parse(p)?;
        let m1 = p.any::<SelectorDec>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into(), m1.into()))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum DatatypeDec {
    /// `(<constructor_dec>+)`
    DatatypeDec(Vec<ConstructorDec>),
    /// `(par (<symbol>+) (<constructor_dec>+))`
    Par(Vec<Symbol>, Vec<ConstructorDec>),
}

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 DatatypeDec {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for DatatypeDec {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth(offset + 0) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "par")
            && p.nth(offset + 2) == Token::LParen)
            || (p.nth(offset + 0) == Token::LParen)
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth(offset + 0) == 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>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::LParen)?;
            let m1 = p.non_zero::<ConstructorDec>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::RParen)?;
            return Ok(Self::Par(m0.into(), m1.into()));
        }
        if p.nth(offset + 0) == Token::LParen {
            p.expect(Token::LParen)?;
            let m0 = p.non_zero::<ConstructorDec>()?;
            p.expect(Token::RParen)?;
            return Ok(Self::DatatypeDec(m0.into()));
        }
        Err(p.stuck("datatype_dec"))
    }
}

/// `(<symbol> (<sorted_var>*) <sort>)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct FunctionDec(pub Symbol, pub Vec<SortedVar>, pub Sort);

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 FunctionDec {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for FunctionDec {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Symbol as SmtlibParse>::parse(p)?;
        p.expect(Token::LParen)?;
        let m1 = p.any::<SortedVar>()?;
        p.expect(Token::RParen)?;
        let m2 = <Sort as SmtlibParse>::parse(p)?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into(), m1.into(), m2.into()))
    }
}

/// `<symbol> (<sorted_var>*) <sort> <term>`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct FunctionDef(pub Symbol, pub Vec<SortedVar>, pub Sort, pub Term);

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 FunctionDef {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for FunctionDef {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        Symbol::is_start_of(offset + 0, p)
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let m0 = <Symbol as SmtlibParse>::parse(p)?;
        p.expect(Token::LParen)?;
        let m1 = p.any::<SortedVar>()?;
        p.expect(Token::RParen)?;
        let m2 = <Sort as SmtlibParse>::parse(p)?;
        let m3 = <Term as SmtlibParse>::parse(p)?;
        Ok(Self(m0.into(), m1.into(), m2.into(), m3.into()))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum PropLiteral {
    /// `<symbol>`
    Symbol(Symbol),
    /// `<symbol>`
    Not(Symbol),
}

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 PropLiteral {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for PropLiteral {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (Symbol::is_start_of(offset + 0, p)) || (Symbol::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if Symbol::is_start_of(offset + 0, p) {
            let m0 = <Symbol as SmtlibParse>::parse(p)?;
            return Ok(Self::Not(m0.into()));
        }
        if Symbol::is_start_of(offset + 0, p) {
            let m0 = <Symbol as SmtlibParse>::parse(p)?;
            return Ok(Self::Symbol(m0.into()));
        }
        Err(p.stuck("prop_literal"))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum Command {
    /// `(assert <term>)`
    Assert(Term),
    /// `(check-sat)`
    CheckSat,
    /// `(check-sat-assuming (<prop_literal>*))`
    CheckSatAssuming(Vec<PropLiteral>),
    /// `(declare-const <symbol> <sort>)`
    DeclareConst(Symbol, Sort),
    /// `(declare-datatype <symbol> <datatype_dec>)`
    DeclareDatatype(Symbol, DatatypeDec),
    /// `(declare-datatypes (<sort_dec>n+1) (<datatype_dec>n+1))`
    DeclareDatatypes(Vec<SortDec>, Vec<DatatypeDec>),
    /// `(declare-fun <symbol> (<sort>*) <sort>)`
    DeclareFun(Symbol, Vec<Sort>, Sort),
    /// `(declare-sort <symbol> <numeral>)`
    DeclareSort(Symbol, Numeral),
    /// `(define-fun <function_def>)`
    DefineFun(FunctionDef),
    /// `(define-fun-rec <function_def>)`
    DefineFunRec(FunctionDef),
    /// `(define-funs-rec (<function_dec>n+1) (<term>n+1))`
    DefineFunsRec(Vec<FunctionDec>, Vec<Term>),
    /// `(define-sort <symbol> (<symbol>*) <sort>)`
    DefineSort(Symbol, Vec<Symbol>, Sort),
    /// `(echo <string>)`
    Echo(String),
    /// `(exit)`
    Exit,
    /// `(get-assertions)`
    GetAssertions,
    /// `(get-assignment)`
    GetAssignment,
    /// `(get-info <info_flag>)`
    GetInfo(InfoFlag),
    /// `(get-model)`
    GetModel,
    /// `(get-option <keyword>)`
    GetOption(Keyword),
    /// `(get-proof)`
    GetProof,
    /// `(get-unsat-assumptions)`
    GetUnsatAssumptions,
    /// `(get-unsat-core)`
    GetUnsatCore,
    /// `(get-value (<term>+))`
    GetValue(Vec<Term>),
    /// `(pop <numeral>)`
    Pop(Numeral),
    /// `(push <numeral>)`
    Push(Numeral),
    /// `(reset)`
    Reset,
    /// `(reset-assertions)`
    ResetAssertions,
    /// `(set-info <attribute>)`
    SetInfo(Attribute),
    /// `(set-logic <symbol>)`
    SetLogic(Symbol),
    /// `(set-option <option>)`
    SetOption(Option),
}

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),
        }
    }
}

impl Command {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for Command {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth(offset + 0) == Token::LParen
            && p.nth_matches(offset + 1, Token::Symbol, "define-funs-rec")
            && p.nth(offset + 2) == Token::LParen)
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "declare-datatypes")
                && p.nth(offset + 2) == Token::LParen)
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "get-value")
                && p.nth(offset + 2) == Token::LParen)
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "define-sort"))
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "declare-fun"))
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "check-sat-assuming")
                && p.nth(offset + 2) == Token::LParen)
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "set-option"))
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "set-logic"))
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "set-info"))
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "reset-assertions")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "reset")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "push"))
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "pop"))
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "get-unsat-core")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "get-unsat-assumptions")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "get-proof")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "get-option"))
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "get-model")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "get-info"))
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "get-assignment")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "get-assertions")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "exit")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "echo"))
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "define-fun-rec"))
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "define-fun"))
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "declare-sort"))
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "declare-datatype"))
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "declare-const"))
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "check-sat")
                && p.nth(offset + 2) == Token::RParen)
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "assert"))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth(offset + 0) == 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>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::LParen)?;
            let m1 = p.n_plus_one::<Term>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::RParen)?;
            return Ok(Self::DefineFunsRec(m0.into(), m1.into()));
        }
        if p.nth(offset + 0) == 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>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::LParen)?;
            let m1 = p.n_plus_one::<DatatypeDec>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::RParen)?;
            return Ok(Self::DeclareDatatypes(m0.into(), m1.into()));
        }
        if p.nth(offset + 0) == 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>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::RParen)?;
            return Ok(Self::GetValue(m0.into()));
        }
        if p.nth(offset + 0) == 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 as SmtlibParse>::parse(p)?;
            p.expect(Token::LParen)?;
            let m1 = p.any::<Symbol>()?;
            p.expect(Token::RParen)?;
            let m2 = <Sort as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::DefineSort(m0.into(), m1.into(), m2.into()));
        }
        if p.nth(offset + 0) == 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 as SmtlibParse>::parse(p)?;
            p.expect(Token::LParen)?;
            let m1 = p.any::<Sort>()?;
            p.expect(Token::RParen)?;
            let m2 = <Sort as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::DeclareFun(m0.into(), m1.into(), m2.into()));
        }
        if p.nth(offset + 0) == 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>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::RParen)?;
            return Ok(Self::CheckSatAssuming(m0.into()));
        }
        if p.nth(offset + 0) == 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 as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::SetOption(m0.into()));
        }
        if p.nth(offset + 0) == 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 as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::SetLogic(m0.into()));
        }
        if p.nth(offset + 0) == 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 as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::SetInfo(m0.into()));
        }
        if p.nth(offset + 0) == 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)?;
            return Ok(Self::ResetAssertions);
        }
        if p.nth(offset + 0) == 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)?;
            return Ok(Self::Reset);
        }
        if p.nth(offset + 0) == Token::LParen && p.nth_matches(offset + 1, Token::Reserved, "push")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "push")?;
            let m0 = <Numeral as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::Push(m0.into()));
        }
        if p.nth(offset + 0) == Token::LParen && p.nth_matches(offset + 1, Token::Reserved, "pop") {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "pop")?;
            let m0 = <Numeral as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::Pop(m0.into()));
        }
        if p.nth(offset + 0) == 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)?;
            return Ok(Self::GetUnsatCore);
        }
        if p.nth(offset + 0) == 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)?;
            return Ok(Self::GetUnsatAssumptions);
        }
        if p.nth(offset + 0) == 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)?;
            return Ok(Self::GetProof);
        }
        if p.nth(offset + 0) == 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 as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::GetOption(m0.into()));
        }
        if p.nth(offset + 0) == 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)?;
            return Ok(Self::GetModel);
        }
        if p.nth(offset + 0) == 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 as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::GetInfo(m0.into()));
        }
        if p.nth(offset + 0) == 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)?;
            return Ok(Self::GetAssignment);
        }
        if p.nth(offset + 0) == 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)?;
            return Ok(Self::GetAssertions);
        }
        if p.nth(offset + 0) == 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)?;
            return Ok(Self::Exit);
        }
        if p.nth(offset + 0) == 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>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::Echo(m0.into()));
        }
        if p.nth(offset + 0) == 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 as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::DefineFunRec(m0.into()));
        }
        if p.nth(offset + 0) == 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 as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::DefineFun(m0.into()));
        }
        if p.nth(offset + 0) == 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 as SmtlibParse>::parse(p)?;
            let m1 = <Numeral as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::DeclareSort(m0.into(), m1.into()));
        }
        if p.nth(offset + 0) == 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 as SmtlibParse>::parse(p)?;
            let m1 = <DatatypeDec as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::DeclareDatatype(m0.into(), m1.into()));
        }
        if p.nth(offset + 0) == 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 as SmtlibParse>::parse(p)?;
            let m1 = <Sort as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::DeclareConst(m0.into(), m1.into()));
        }
        if p.nth(offset + 0) == 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)?;
            return Ok(Self::CheckSat);
        }
        if p.nth(offset + 0) == Token::LParen
            && p.nth_matches(offset + 1, Token::Reserved, "assert")
        {
            p.expect(Token::LParen)?;
            p.expect_matches(Token::Reserved, "assert")?;
            let m0 = <Term as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::Assert(m0.into()));
        }
        Err(p.stuck("command"))
    }
}

impl Command {
    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,
        }
    }
    pub fn parse_response(
        &self,
        response: &str,
    ) -> Result<std::option::Option<SpecificSuccessResponse>, ParseError> {
        match self {
            Self::Assert(_) => Ok(None),
            Self::CheckSat => Ok(Some(SpecificSuccessResponse::CheckSatResponse(
                CheckSatResponse::parse(response)?,
            ))),
            Self::CheckSatAssuming(_) => Ok(Some(SpecificSuccessResponse::CheckSatResponse(
                CheckSatResponse::parse(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::parse(response)?,
            ))),
            Self::Exit => Ok(None),
            Self::GetAssertions => Ok(Some(SpecificSuccessResponse::GetAssertionsResponse(
                GetAssertionsResponse::parse(response)?,
            ))),
            Self::GetAssignment => Ok(Some(SpecificSuccessResponse::GetAssignmentResponse(
                GetAssignmentResponse::parse(response)?,
            ))),
            Self::GetInfo(_) => Ok(Some(SpecificSuccessResponse::GetInfoResponse(
                GetInfoResponse::parse(response)?,
            ))),
            Self::GetModel => Ok(Some(SpecificSuccessResponse::GetModelResponse(
                GetModelResponse::parse(response)?,
            ))),
            Self::GetOption(_) => Ok(Some(SpecificSuccessResponse::GetOptionResponse(
                GetOptionResponse::parse(response)?,
            ))),
            Self::GetProof => Ok(Some(SpecificSuccessResponse::GetProofResponse(
                GetProofResponse::parse(response)?,
            ))),
            Self::GetUnsatAssumptions => {
                Ok(Some(SpecificSuccessResponse::GetUnsatAssumptionsResponse(
                    GetUnsatAssumptionsResponse::parse(response)?,
                )))
            }
            Self::GetUnsatCore => Ok(Some(SpecificSuccessResponse::GetUnsatCoreResponse(
                GetUnsatCoreResponse::parse(response)?,
            ))),
            Self::GetValue(_) => Ok(Some(SpecificSuccessResponse::GetValueResponse(
                GetValueResponse::parse(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),
        }
    }
}

/// `<command>*`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct Script(pub Vec<Command>);

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 Script {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for Script {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        todo!()
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let m0 = p.any::<Command>()?;
        Ok(Self(m0.into()))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum Option {
    /// `:diagnostic-output-channel <string>`
    DiagnosticOutputChannel(String),
    /// `: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),
    /// `:regular-output-channel <string>`
    RegularOutputChannel(String),
    /// `:reproducible-resource-limit <numeral>`
    ReproducibleResourceLimit(Numeral),
    /// `:verbosity <numeral>`
    Verbosity(Numeral),
    /// `<attribute>`
    Attribute(Attribute),
}

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 Option {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for Option {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth_matches(offset + 0, Token::Keyword, ":verbosity"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":reproducible-resource-limit"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":regular-output-channel"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":random-seed"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":produce-unsat-cores"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":produce-unsat-assumptions"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":produce-proofs"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":produce-models"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":produce-assignments"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":produce-assertions"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":print-success"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":interactive-mode"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":global-declarations"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":diagnostic-output-channel"))
            || (Attribute::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth_matches(offset + 0, Token::Keyword, ":verbosity") {
            p.expect_matches(Token::Keyword, ":verbosity")?;
            let m0 = <Numeral as SmtlibParse>::parse(p)?;
            return Ok(Self::Verbosity(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":reproducible-resource-limit") {
            p.expect_matches(Token::Keyword, ":reproducible-resource-limit")?;
            let m0 = <Numeral as SmtlibParse>::parse(p)?;
            return Ok(Self::ReproducibleResourceLimit(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":regular-output-channel") {
            p.expect_matches(Token::Keyword, ":regular-output-channel")?;
            let m0 = <String as SmtlibParse>::parse(p)?;
            return Ok(Self::RegularOutputChannel(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":random-seed") {
            p.expect_matches(Token::Keyword, ":random-seed")?;
            let m0 = <Numeral as SmtlibParse>::parse(p)?;
            return Ok(Self::RandomSeed(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":produce-unsat-cores") {
            p.expect_matches(Token::Keyword, ":produce-unsat-cores")?;
            let m0 = <BValue as SmtlibParse>::parse(p)?;
            return Ok(Self::ProduceUnsatCores(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":produce-unsat-assumptions") {
            p.expect_matches(Token::Keyword, ":produce-unsat-assumptions")?;
            let m0 = <BValue as SmtlibParse>::parse(p)?;
            return Ok(Self::ProduceUnsatAssumptions(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":produce-proofs") {
            p.expect_matches(Token::Keyword, ":produce-proofs")?;
            let m0 = <BValue as SmtlibParse>::parse(p)?;
            return Ok(Self::ProduceProofs(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":produce-models") {
            p.expect_matches(Token::Keyword, ":produce-models")?;
            let m0 = <BValue as SmtlibParse>::parse(p)?;
            return Ok(Self::ProduceModels(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":produce-assignments") {
            p.expect_matches(Token::Keyword, ":produce-assignments")?;
            let m0 = <BValue as SmtlibParse>::parse(p)?;
            return Ok(Self::ProduceAssignments(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":produce-assertions") {
            p.expect_matches(Token::Keyword, ":produce-assertions")?;
            let m0 = <BValue as SmtlibParse>::parse(p)?;
            return Ok(Self::ProduceAssertions(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":print-success") {
            p.expect_matches(Token::Keyword, ":print-success")?;
            let m0 = <BValue as SmtlibParse>::parse(p)?;
            return Ok(Self::PrintSuccess(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":interactive-mode") {
            p.expect_matches(Token::Keyword, ":interactive-mode")?;
            let m0 = <BValue as SmtlibParse>::parse(p)?;
            return Ok(Self::InteractiveMode(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":global-declarations") {
            p.expect_matches(Token::Keyword, ":global-declarations")?;
            let m0 = <BValue as SmtlibParse>::parse(p)?;
            return Ok(Self::GlobalDeclarations(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":diagnostic-output-channel") {
            p.expect_matches(Token::Keyword, ":diagnostic-output-channel")?;
            let m0 = <String as SmtlibParse>::parse(p)?;
            return Ok(Self::DiagnosticOutputChannel(m0.into()));
        }
        if Attribute::is_start_of(offset + 0, p) {
            let m0 = <Attribute as SmtlibParse>::parse(p)?;
            return Ok(Self::Attribute(m0.into()));
        }
        Err(p.stuck("option"))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum InfoFlag {
    /// `:all-statistics`
    AllStatistics,
    /// `:assertion-stack-levels`
    AssertionStackLevels,
    /// `:authors`
    Authors,
    /// `:error-behavior`
    ErrorBehavior,
    /// `:name`
    Name,
    /// `:reason-unknown`
    ReasonUnknown,
    /// `:version`
    Version,
    /// `<keyword>`
    Keyword(Keyword),
}

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 InfoFlag {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for InfoFlag {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth_matches(offset + 0, Token::Keyword, ":version"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":reason-unknown"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":name"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":error-behavior"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":authors"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":assertion-stack-levels"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":all-statistics"))
            || (Keyword::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth_matches(offset + 0, Token::Keyword, ":version") {
            p.expect_matches(Token::Keyword, ":version")?;
            return Ok(Self::Version);
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":reason-unknown") {
            p.expect_matches(Token::Keyword, ":reason-unknown")?;
            return Ok(Self::ReasonUnknown);
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":name") {
            p.expect_matches(Token::Keyword, ":name")?;
            return Ok(Self::Name);
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":error-behavior") {
            p.expect_matches(Token::Keyword, ":error-behavior")?;
            return Ok(Self::ErrorBehavior);
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":authors") {
            p.expect_matches(Token::Keyword, ":authors")?;
            return Ok(Self::Authors);
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":assertion-stack-levels") {
            p.expect_matches(Token::Keyword, ":assertion-stack-levels")?;
            return Ok(Self::AssertionStackLevels);
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":all-statistics") {
            p.expect_matches(Token::Keyword, ":all-statistics")?;
            return Ok(Self::AllStatistics);
        }
        if Keyword::is_start_of(offset + 0, p) {
            let m0 = <Keyword as SmtlibParse>::parse(p)?;
            return Ok(Self::Keyword(m0.into()));
        }
        Err(p.stuck("info_flag"))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
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 ErrorBehavior {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for ErrorBehavior {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth_matches(offset + 0, Token::Symbol, "continued-execution"))
            || (p.nth_matches(offset + 0, Token::Symbol, "immediate-exit"))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth_matches(offset + 0, Token::Symbol, "continued-execution") {
            p.expect_matches(Token::Symbol, "continued-execution")?;
            return Ok(Self::ContinuedExecution);
        }
        if p.nth_matches(offset + 0, Token::Symbol, "immediate-exit") {
            p.expect_matches(Token::Symbol, "immediate-exit")?;
            return Ok(Self::ImmediateExit);
        }
        Err(p.stuck("error_behavior"))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum ReasonUnknown {
    /// `memout`
    Memout,
    /// `incomplete`
    Incomplete,
    /// `<s_expr>`
    SExpr(SExpr),
}

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 ReasonUnknown {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for ReasonUnknown {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth_matches(offset + 0, Token::Symbol, "incomplete"))
            || (p.nth_matches(offset + 0, Token::Symbol, "memout"))
            || (SExpr::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth_matches(offset + 0, Token::Symbol, "incomplete") {
            p.expect_matches(Token::Symbol, "incomplete")?;
            return Ok(Self::Incomplete);
        }
        if p.nth_matches(offset + 0, Token::Symbol, "memout") {
            p.expect_matches(Token::Symbol, "memout")?;
            return Ok(Self::Memout);
        }
        if SExpr::is_start_of(offset + 0, p) {
            let m0 = <SExpr as SmtlibParse>::parse(p)?;
            return Ok(Self::SExpr(m0.into()));
        }
        Err(p.stuck("reason_unknown"))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum ModelResponse {
    /// `(define-fun <function_def>)`
    DefineFun(FunctionDef),
    /// `(define-fun-rec <function_def>)`
    DefineFunRec(FunctionDef),
    /// `(define-funs-rec (<function_dec>n+1) (<term>n+1))`
    DefineFunsRec(Vec<FunctionDec>, Vec<Term>),
}

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 ModelResponse {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for ModelResponse {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth(offset + 0) == Token::LParen
            && p.nth_matches(offset + 1, Token::Symbol, "define-funs-rec")
            && p.nth(offset + 2) == Token::LParen)
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "define-fun-rec"))
            || (p.nth(offset + 0) == Token::LParen
                && p.nth_matches(offset + 1, Token::Reserved, "define-fun"))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth(offset + 0) == 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>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::LParen)?;
            let m1 = p.n_plus_one::<Term>()?;
            p.expect(Token::RParen)?;
            p.expect(Token::RParen)?;
            return Ok(Self::DefineFunsRec(m0.into(), m1.into()));
        }
        if p.nth(offset + 0) == 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 as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::DefineFunRec(m0.into()));
        }
        if p.nth(offset + 0) == 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 as SmtlibParse>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::DefineFun(m0.into()));
        }
        Err(p.stuck("model_response"))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum InfoResponse {
    /// `:assertion-stack-levels <numeral>`
    AssertionStackLevels(Numeral),
    /// `:authors <string>`
    Authors(String),
    /// `:error-behavior <error-behavior>`
    ErrorBehavior(ErrorBehavior),
    /// `:name <string>`
    Name(String),
    /// `:reason-unknown <reason-unknown>`
    ReasonUnknown(ReasonUnknown),
    /// `:version <string>`
    Version(String),
    /// `<attribute>`
    Attribute(Attribute),
}

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 InfoResponse {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for InfoResponse {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth_matches(offset + 0, Token::Keyword, ":version"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":reason-unknown"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":name"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":error-behavior"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":authors"))
            || (p.nth_matches(offset + 0, Token::Keyword, ":assertion-stack-levels"))
            || (Attribute::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth_matches(offset + 0, Token::Keyword, ":version") {
            p.expect_matches(Token::Keyword, ":version")?;
            let m0 = <String as SmtlibParse>::parse(p)?;
            return Ok(Self::Version(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":reason-unknown") {
            p.expect_matches(Token::Keyword, ":reason-unknown")?;
            let m0 = <ReasonUnknown as SmtlibParse>::parse(p)?;
            return Ok(Self::ReasonUnknown(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":name") {
            p.expect_matches(Token::Keyword, ":name")?;
            let m0 = <String as SmtlibParse>::parse(p)?;
            return Ok(Self::Name(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":error-behavior") {
            p.expect_matches(Token::Keyword, ":error-behavior")?;
            let m0 = <ErrorBehavior as SmtlibParse>::parse(p)?;
            return Ok(Self::ErrorBehavior(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":authors") {
            p.expect_matches(Token::Keyword, ":authors")?;
            let m0 = <String as SmtlibParse>::parse(p)?;
            return Ok(Self::Authors(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Keyword, ":assertion-stack-levels") {
            p.expect_matches(Token::Keyword, ":assertion-stack-levels")?;
            let m0 = <Numeral as SmtlibParse>::parse(p)?;
            return Ok(Self::AssertionStackLevels(m0.into()));
        }
        if Attribute::is_start_of(offset + 0, p) {
            let m0 = <Attribute as SmtlibParse>::parse(p)?;
            return Ok(Self::Attribute(m0.into()));
        }
        Err(p.stuck("info_response"))
    }
}

/// `(<term> <term>)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct ValuationPair(pub Term, pub Term);

impl std::fmt::Display for ValuationPair {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({} {})", self.0, self.1)
    }
}

impl ValuationPair {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for ValuationPair {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Term as SmtlibParse>::parse(p)?;
        let m1 = <Term as SmtlibParse>::parse(p)?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into(), m1.into()))
    }
}

/// `(<symbol> <b_value>)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct TValuationPair(pub Symbol, 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 TValuationPair {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for TValuationPair {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = <Symbol as SmtlibParse>::parse(p)?;
        let m1 = <BValue as SmtlibParse>::parse(p)?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into(), m1.into()))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
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 CheckSatResponse {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for CheckSatResponse {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth_matches(offset + 0, Token::Symbol, "unknown"))
            || (p.nth_matches(offset + 0, Token::Symbol, "unsat"))
            || (p.nth_matches(offset + 0, Token::Symbol, "sat"))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth_matches(offset + 0, Token::Symbol, "unknown") {
            p.expect_matches(Token::Symbol, "unknown")?;
            return Ok(Self::Unknown);
        }
        if p.nth_matches(offset + 0, Token::Symbol, "unsat") {
            p.expect_matches(Token::Symbol, "unsat")?;
            return Ok(Self::Unsat);
        }
        if p.nth_matches(offset + 0, Token::Symbol, "sat") {
            p.expect_matches(Token::Symbol, "sat")?;
            return Ok(Self::Sat);
        }
        Err(p.stuck("check_sat_response"))
    }
}

/// `<string>`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct EchoResponse(pub String);

impl std::fmt::Display for EchoResponse {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "{}", self.0)
    }
}

impl EchoResponse {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for EchoResponse {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        String::is_start_of(offset + 0, p)
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let m0 = <String as SmtlibParse>::parse(p)?;
        Ok(Self(m0.into()))
    }
}

/// `(<term>*)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct GetAssertionsResponse(pub Vec<Term>);

impl std::fmt::Display for GetAssertionsResponse {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({})", self.0.iter().format(" "))
    }
}

impl GetAssertionsResponse {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for GetAssertionsResponse {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = p.any::<Term>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into()))
    }
}

/// `(<t_valuation_pair>*)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct GetAssignmentResponse(pub Vec<TValuationPair>);

impl std::fmt::Display for GetAssignmentResponse {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({})", self.0.iter().format(" "))
    }
}

impl GetAssignmentResponse {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for GetAssignmentResponse {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = p.any::<TValuationPair>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into()))
    }
}

/// `(<info_response>+)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct GetInfoResponse(pub Vec<InfoResponse>);

impl std::fmt::Display for GetInfoResponse {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({})", self.0.iter().format(" "))
    }
}

impl GetInfoResponse {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for GetInfoResponse {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = p.non_zero::<InfoResponse>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into()))
    }
}

/// `(<model_response>*)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct GetModelResponse(pub Vec<ModelResponse>);

impl std::fmt::Display for GetModelResponse {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({})", self.0.iter().format(" "))
    }
}

impl GetModelResponse {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for GetModelResponse {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = p.any::<ModelResponse>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into()))
    }
}

/// `<attribute_value>`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct GetOptionResponse(pub AttributeValue);

impl std::fmt::Display for GetOptionResponse {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "{}", self.0)
    }
}

impl GetOptionResponse {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for GetOptionResponse {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        AttributeValue::is_start_of(offset + 0, p)
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let m0 = <AttributeValue as SmtlibParse>::parse(p)?;
        Ok(Self(m0.into()))
    }
}

/// `<s_expr>`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct GetProofResponse(pub SExpr);

impl std::fmt::Display for GetProofResponse {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "{}", self.0)
    }
}

impl GetProofResponse {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for GetProofResponse {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        SExpr::is_start_of(offset + 0, p)
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let m0 = <SExpr as SmtlibParse>::parse(p)?;
        Ok(Self(m0.into()))
    }
}

/// `(<symbol>*)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct GetUnsatAssumptionsResponse(pub Vec<Symbol>);

impl std::fmt::Display for GetUnsatAssumptionsResponse {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({})", self.0.iter().format(" "))
    }
}

impl GetUnsatAssumptionsResponse {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for GetUnsatAssumptionsResponse {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = p.any::<Symbol>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into()))
    }
}

/// `(<symbol>*)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct GetUnsatCoreResponse(pub Vec<Symbol>);

impl std::fmt::Display for GetUnsatCoreResponse {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({})", self.0.iter().format(" "))
    }
}

impl GetUnsatCoreResponse {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for GetUnsatCoreResponse {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = p.any::<Symbol>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into()))
    }
}

/// `(<valuation_pair>+)`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct GetValueResponse(pub Vec<ValuationPair>);

impl std::fmt::Display for GetValueResponse {
    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
        write!(f, "({})", self.0.iter().format(" "))
    }
}

impl GetValueResponse {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for GetValueResponse {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        p.nth(offset + 0) == Token::LParen
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        p.expect(Token::LParen)?;
        let m0 = p.non_zero::<ValuationPair>()?;
        p.expect(Token::RParen)?;
        Ok(Self(m0.into()))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum SpecificSuccessResponse {
    /// `<get_unsat_assumptions_response>`
    GetUnsatAssumptionsResponse(GetUnsatAssumptionsResponse),
    /// `<check_sat_response>`
    CheckSatResponse(CheckSatResponse),
    /// `<echo_response>`
    EchoResponse(EchoResponse),
    /// `<get_assertions_response>`
    GetAssertionsResponse(GetAssertionsResponse),
    /// `<get_assignment_response>`
    GetAssignmentResponse(GetAssignmentResponse),
    /// `<get_info_response>`
    GetInfoResponse(GetInfoResponse),
    /// `<get_model_response>`
    GetModelResponse(GetModelResponse),
    /// `<get_option_response>`
    GetOptionResponse(GetOptionResponse),
    /// `<get_proof_response>`
    GetProofResponse(GetProofResponse),
    /// `<get_unsat_core_response>`
    GetUnsatCoreResponse(GetUnsatCoreResponse),
    /// `<get_value_response>`
    GetValueResponse(GetValueResponse),
}

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),
        }
    }
}

impl SpecificSuccessResponse {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for SpecificSuccessResponse {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (GetValueResponse::is_start_of(offset + 0, p))
            || (GetUnsatCoreResponse::is_start_of(offset + 0, p))
            || (GetProofResponse::is_start_of(offset + 0, p))
            || (GetOptionResponse::is_start_of(offset + 0, p))
            || (GetModelResponse::is_start_of(offset + 0, p))
            || (GetInfoResponse::is_start_of(offset + 0, p))
            || (GetAssignmentResponse::is_start_of(offset + 0, p))
            || (GetAssertionsResponse::is_start_of(offset + 0, p))
            || (EchoResponse::is_start_of(offset + 0, p))
            || (CheckSatResponse::is_start_of(offset + 0, p))
            || (GetUnsatAssumptionsResponse::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if GetValueResponse::is_start_of(offset + 0, p) {
            let m0 = <GetValueResponse as SmtlibParse>::parse(p)?;
            return Ok(Self::GetValueResponse(m0.into()));
        }
        if GetUnsatCoreResponse::is_start_of(offset + 0, p) {
            let m0 = <GetUnsatCoreResponse as SmtlibParse>::parse(p)?;
            return Ok(Self::GetUnsatCoreResponse(m0.into()));
        }
        if GetProofResponse::is_start_of(offset + 0, p) {
            let m0 = <GetProofResponse as SmtlibParse>::parse(p)?;
            return Ok(Self::GetProofResponse(m0.into()));
        }
        if GetOptionResponse::is_start_of(offset + 0, p) {
            let m0 = <GetOptionResponse as SmtlibParse>::parse(p)?;
            return Ok(Self::GetOptionResponse(m0.into()));
        }
        if GetModelResponse::is_start_of(offset + 0, p) {
            let m0 = <GetModelResponse as SmtlibParse>::parse(p)?;
            return Ok(Self::GetModelResponse(m0.into()));
        }
        if GetInfoResponse::is_start_of(offset + 0, p) {
            let m0 = <GetInfoResponse as SmtlibParse>::parse(p)?;
            return Ok(Self::GetInfoResponse(m0.into()));
        }
        if GetAssignmentResponse::is_start_of(offset + 0, p) {
            let m0 = <GetAssignmentResponse as SmtlibParse>::parse(p)?;
            return Ok(Self::GetAssignmentResponse(m0.into()));
        }
        if GetAssertionsResponse::is_start_of(offset + 0, p) {
            let m0 = <GetAssertionsResponse as SmtlibParse>::parse(p)?;
            return Ok(Self::GetAssertionsResponse(m0.into()));
        }
        if EchoResponse::is_start_of(offset + 0, p) {
            let m0 = <EchoResponse as SmtlibParse>::parse(p)?;
            return Ok(Self::EchoResponse(m0.into()));
        }
        if CheckSatResponse::is_start_of(offset + 0, p) {
            let m0 = <CheckSatResponse as SmtlibParse>::parse(p)?;
            return Ok(Self::CheckSatResponse(m0.into()));
        }
        if GetUnsatAssumptionsResponse::is_start_of(offset + 0, p) {
            let m0 = <GetUnsatAssumptionsResponse as SmtlibParse>::parse(p)?;
            return Ok(Self::GetUnsatAssumptionsResponse(m0.into()));
        }
        Err(p.stuck("specific_success_response"))
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum GeneralResponse {
    /// `success`
    Success,
    /// `<specific_success_response>`
    SpecificSuccessResponse(SpecificSuccessResponse),
    /// `unsupported`
    Unsupported,
    /// `(error <string>)`
    Error(String),
}

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 GeneralResponse {
    pub fn parse(src: &str) -> Result<Self, ParseError> {
        SmtlibParse::parse(&mut Parser::new(src))
    }
}
impl SmtlibParse for GeneralResponse {
    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
        (p.nth(offset + 0) == Token::LParen && p.nth_matches(offset + 1, Token::Symbol, "error"))
            || (p.nth_matches(offset + 0, Token::Symbol, "unsupported"))
            || (p.nth_matches(offset + 0, Token::Symbol, "success"))
            || (SpecificSuccessResponse::is_start_of(offset + 0, p))
    }
    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
        let offset = 0;
        if p.nth(offset + 0) == 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>::parse(p)?;
            p.expect(Token::RParen)?;
            return Ok(Self::Error(m0.into()));
        }
        if p.nth_matches(offset + 0, Token::Symbol, "unsupported") {
            p.expect_matches(Token::Symbol, "unsupported")?;
            return Ok(Self::Unsupported);
        }
        if p.nth_matches(offset + 0, Token::Symbol, "success") {
            p.expect_matches(Token::Symbol, "success")?;
            return Ok(Self::Success);
        }
        if SpecificSuccessResponse::is_start_of(offset + 0, p) {
            let m0 = <SpecificSuccessResponse as SmtlibParse>::parse(p)?;
            return Ok(Self::SpecificSuccessResponse(m0.into()));
        }
        Err(p.stuck("general_response"))
    }
}