Enum smt2parser::concrete::Term [−][src]
pub enum Term<Constant = Constant, QualIdentifier = QualIdentifier, Keyword = Keyword, SExpr = SExpr, Symbol = Symbol, Sort = Sort> {
Constant(Constant),
QualIdentifier(QualIdentifier),
Application {
qual_identifier: QualIdentifier,
arguments: Vec<Self>,
},
Let {
var_bindings: Vec<(Symbol, Self)>,
term: Box<Self>,
},
Forall {
vars: Vec<(Symbol, Sort)>,
term: Box<Self>,
},
Exists {
vars: Vec<(Symbol, Sort)>,
term: Box<Self>,
},
Match {
term: Box<Self>,
cases: Vec<(Vec<Symbol>, Self)>,
},
Attributes {
term: Box<Self>,
attributes: Vec<(Keyword, AttributeValue<Constant, Symbol, SExpr>)>,
},
}
Expand description
Concrete syntax for a term.
Variants
Fields of Application
qual_identifier: QualIdentifier
arguments: Vec<Self>
Fields of Attributes
term: Box<Self>
attributes: Vec<(Keyword, AttributeValue<Constant, Symbol, SExpr>)>
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
impl<'de, Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> Deserialize<'de> for Term<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> where
Constant: Deserialize<'de>,
QualIdentifier: Deserialize<'de>,
Keyword: Deserialize<'de>,
SExpr: Deserialize<'de>,
Symbol: Deserialize<'de>,
Sort: Deserialize<'de>,
impl<'de, Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> Deserialize<'de> for Term<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> where
Constant: Deserialize<'de>,
QualIdentifier: Deserialize<'de>,
Keyword: Deserialize<'de>,
SExpr: Deserialize<'de>,
Symbol: Deserialize<'de>,
Sort: Deserialize<'de>,
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
This method tests for self
and other
values to be equal, and is used
by ==
. Read more
impl<Constant: Eq, QualIdentifier: Eq, Keyword: Eq, SExpr: Eq, Symbol: Eq, Sort: Eq> Eq for Term<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort>
impl<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> StructuralEq for Term<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort>
impl<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> StructuralPartialEq for Term<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort>
Auto Trait Implementations
impl<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> RefUnwindSafe for Term<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> where
Constant: RefUnwindSafe,
Keyword: RefUnwindSafe,
QualIdentifier: RefUnwindSafe,
SExpr: RefUnwindSafe,
Sort: RefUnwindSafe,
Symbol: RefUnwindSafe,
impl<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> Send for Term<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> where
Constant: Send,
Keyword: Send,
QualIdentifier: Send,
SExpr: Send,
Sort: Send,
Symbol: Send,
impl<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> Sync for Term<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> where
Constant: Sync,
Keyword: Sync,
QualIdentifier: Sync,
SExpr: Sync,
Sort: Sync,
Symbol: Sync,
impl<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> Unpin for Term<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> where
Constant: Unpin,
Keyword: Unpin,
QualIdentifier: Unpin,
SExpr: Unpin,
Sort: Unpin,
Symbol: Unpin,
impl<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> UnwindSafe for Term<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> where
Constant: UnwindSafe,
Keyword: UnwindSafe,
QualIdentifier: UnwindSafe,
SExpr: UnwindSafe,
Sort: UnwindSafe,
Symbol: UnwindSafe,
Blanket Implementations
Mutably borrows from an owned value. Read more