Struct smt2::syntax::response::Definition

pub struct Definition {
    pub rec: bool,
    pub declarations: Vec<Located<Declaration>>,
    pub bodies: Vec<Located<Term>>,
    pub comments: String,
}

Model function definition. <model_response> ::= ( define-fun <function_def> ) | ( define-fun-rec <function_def> ) | ( define-funs-rec ( <function_dec>n+1 ) ( n+1 ) ) <function_def> ::= ( <sorted_var>* )

Fields

rec: bool

declarations: Vec<Located<Declaration>>

bodies: Vec<Located<Term>>

comments: String

Trait Implementations

impl Display for Definition

fn fmt(&self, f: &mut Formatter<'_, '_>) -> Result

impl Parsable for Definition

fn parse<L>(lexer: &mut Peekable<L>) -> Result<Located<Definition>> where
    L: Iterator<Item = Result<Located<Token>>>, 

Parse from a lexer. Separators are handled depending on the flavor parameter.