Enum smt2parser::concrete::Term [−][src]
pub enum Term { Constant(Constant), QualIdentifier(QualIdentifier), Application { qual_identifier: QualIdentifier, arguments: Vec<Term>, }, Let { var_bindings: Vec<(Symbol, Term)>, term: Box<Term>, }, Forall { vars: Vec<(Symbol, Sort)>, term: Box<Term>, }, Exists { vars: Vec<(Symbol, Sort)>, term: Box<Term>, }, Match { term: Box<Term>, cases: Vec<(Vec<Symbol>, Term)>, }, Attributes { term: Box<Term>, attributes: Vec<(Keyword, AttributeValue)>, }, }
Expand description
Concrete syntax for a term.
Variants
Constant(Constant)
QualIdentifier(QualIdentifier)
Show fields
Fields of Application
qual_identifier: QualIdentifier
arguments: Vec<Term>
Implementations
pub fn accept<V, T, E, S1, S2, S3, S4, S5, S6>(
self,
visitor: &mut V
) -> Result<T, E> where
V: SortVisitor<S1, T = S2, E = E> + SymbolVisitor<T = S1, E = E> + QualIdentifierVisitor<Identifier<S1>, S2, T = S3, E = E> + ConstantVisitor<T = S4, E = E> + KeywordVisitor<T = S5, E = E> + SExprVisitor<S4, S1, S5, T = S6, E = E> + TermVisitor<S4, S3, S5, S6, S1, S2, T = T, E = E>,
pub fn accept<V, T, E, S1, S2, S3, S4, S5, S6>(
self,
visitor: &mut V
) -> Result<T, E> where
V: SortVisitor<S1, T = S2, E = E> + SymbolVisitor<T = S1, E = E> + QualIdentifierVisitor<Identifier<S1>, S2, T = S3, E = E> + ConstantVisitor<T = S4, E = E> + KeywordVisitor<T = S5, E = E> + SExprVisitor<S4, S1, S5, T = S6, E = E> + TermVisitor<S4, S3, S5, S6, S1, S2, T = T, E = E>,
Visit a concrete term.
Trait Implementations
fn visit_declare_datatype(
&mut self,
symbol: Symbol,
datatype: DatatypeDec
) -> Result<Self::T, Self::E>
fn visit_declare_datatypes(
&mut self,
datatypes: Vec<(Symbol, Numeral, DatatypeDec)>
) -> Result<Self::T, Self::E>
fn visit_declare_fun(
&mut self,
symbol: Symbol,
parameters: Vec<Sort>,
sort: Sort
) -> Result<Self::T, Self::E>
fn visit_define_funs_rec(
&mut self,
funs: Vec<(FunctionDec, Term)>
) -> Result<Self::T, Self::E>
fn visit_define_sort(
&mut self,
symbol: Symbol,
parameters: Vec<Symbol>,
sort: Sort
) -> Result<Self::T, Self::E>
fn visit_set_info(
&mut self,
keyword: Keyword,
value: AttributeValue
) -> Result<Self::T, Self::E>
fn visit_set_option(
&mut self,
keyword: Keyword,
value: AttributeValue
) -> Result<Self::T, Self::E>
fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error> where
__D: Deserializer<'de>,
fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error> where
__D: Deserializer<'de>,
Deserialize this value from the given Serde deserializer. Read more
Auto Trait Implementations
impl RefUnwindSafe for Term
impl UnwindSafe for Term
Blanket Implementations
Mutably borrows from an owned value. Read more