Trait smt2parser::visitors::TermVisitor [−][src]
pub trait TermVisitor<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> { type T; type E; fn visit_constant(&mut self, constant: Constant) -> Result<Self::T, Self::E>; fn visit_qual_identifier(
&mut self,
qual_identifier: QualIdentifier
) -> Result<Self::T, Self::E>; fn visit_application(
&mut self,
qual_identifier: QualIdentifier,
arguments: Vec<Self::T>
) -> Result<Self::T, Self::E>; fn visit_let(
&mut self,
var_bindings: Vec<(Symbol, Self::T)>,
term: Self::T
) -> Result<Self::T, Self::E>; fn visit_forall(
&mut self,
vars: Vec<(Symbol, Sort)>,
term: Self::T
) -> Result<Self::T, Self::E>; fn visit_exists(
&mut self,
vars: Vec<(Symbol, Sort)>,
term: Self::T
) -> Result<Self::T, Self::E>; fn visit_match(
&mut self,
term: Self::T,
cases: Vec<(Vec<Symbol>, Self::T)>
) -> Result<Self::T, Self::E>; fn visit_attributes(
&mut self,
term: Self::T,
attributes: Vec<(Keyword, AttributeValue<Constant, Symbol, SExpr>)>
) -> Result<Self::T, Self::E>; }
Associated Types
Required methods
fn visit_constant(&mut self, constant: Constant) -> Result<Self::T, Self::E>
fn visit_qual_identifier(
&mut self,
qual_identifier: QualIdentifier
) -> Result<Self::T, Self::E>
fn visit_application(
&mut self,
qual_identifier: QualIdentifier,
arguments: Vec<Self::T>
) -> Result<Self::T, Self::E>
fn visit_let(
&mut self,
var_bindings: Vec<(Symbol, Self::T)>,
term: Self::T
) -> Result<Self::T, Self::E>
fn visit_match(
&mut self,
term: Self::T,
cases: Vec<(Vec<Symbol>, Self::T)>
) -> Result<Self::T, Self::E>
fn visit_attributes(
&mut self,
term: Self::T,
attributes: Vec<(Keyword, AttributeValue<Constant, Symbol, SExpr>)>
) -> Result<Self::T, Self::E>
Implementors
impl<R, V> TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort> for R where
R: Rewriter<V = V>,
V: Smt2Visitor,