Trait smt2parser::visitors::TermVisitor

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

type T

type E

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_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>

Implementors

impl TermVisitor<(), (), (), (), (), ()> for Smt2Counters

type T = Term

type E = Error

impl<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> TermVisitor<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> for SyntaxBuilder

type T = Term<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort>

type E = Error

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, 

type T = V::Term

type E = R::Error