Trait smt2parser::visitors::CommandVisitor[−][src]

pub trait CommandVisitor<Term, Symbol, Sort, Keyword, Constant, SExpr> {
    type T;
    type E;

Show 30 methods    fn visit_assert(&mut self, term: Term) -> Result<Self::T, Self::E>;

    fn visit_check_sat(&mut self) -> Result<Self::T, Self::E>;

    fn visit_check_sat_assuming(
        &mut self, 
        literals: Vec<(Symbol, bool)>
    ) -> Result<Self::T, Self::E>;

    fn visit_declare_const(
        &mut self, 
        symbol: Symbol, 
        sort: Sort
    ) -> Result<Self::T, Self::E>;

    fn visit_declare_datatype(
        &mut self, 
        symbol: Symbol, 
        datatype: DatatypeDec<Symbol, Sort>
    ) -> Result<Self::T, Self::E>;

    fn visit_declare_datatypes(
        &mut self, 
        datatypes: Vec<(Symbol, Numeral, DatatypeDec<Symbol, Sort>)>
    ) -> 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_declare_sort(
        &mut self, 
        symbol: Symbol, 
        arity: Numeral
    ) -> Result<Self::T, Self::E>;

    fn visit_define_fun(
        &mut self, 
        sig: FunctionDec<Symbol, Sort>, 
        term: Term
    ) -> Result<Self::T, Self::E>;

    fn visit_define_fun_rec(
        &mut self, 
        sig: FunctionDec<Symbol, Sort>, 
        term: Term
    ) -> Result<Self::T, Self::E>;

    fn visit_define_funs_rec(
        &mut self, 
        funs: Vec<(FunctionDec<Symbol, Sort>, 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_echo(&mut self, message: String) -> Result<Self::T, Self::E>;

    fn visit_exit(&mut self) -> Result<Self::T, Self::E>;

    fn visit_get_assertions(&mut self) -> Result<Self::T, Self::E>;

    fn visit_get_assignment(&mut self) -> Result<Self::T, Self::E>;

    fn visit_get_info(&mut self, flag: Keyword) -> Result<Self::T, Self::E>;

    fn visit_get_model(&mut self) -> Result<Self::T, Self::E>;

    fn visit_get_option(&mut self, keyword: Keyword) -> Result<Self::T, Self::E>;

    fn visit_get_proof(&mut self) -> Result<Self::T, Self::E>;

    fn visit_get_unsat_assumptions(&mut self) -> Result<Self::T, Self::E>;

    fn visit_get_unsat_core(&mut self) -> Result<Self::T, Self::E>;

    fn visit_get_value(&mut self, terms: Vec<Term>) -> Result<Self::T, Self::E>;

    fn visit_pop(&mut self, level: Numeral) -> Result<Self::T, Self::E>;

    fn visit_push(&mut self, level: Numeral) -> Result<Self::T, Self::E>;

    fn visit_reset(&mut self) -> Result<Self::T, Self::E>;

    fn visit_reset_assertions(&mut self) -> Result<Self::T, Self::E>;

    fn visit_set_info(
        &mut self, 
        keyword: Keyword, 
        value: AttributeValue<Constant, Symbol, SExpr>
    ) -> Result<Self::T, Self::E>;

    fn visit_set_logic(&mut self, symbol: Symbol) -> Result<Self::T, Self::E>;

    fn visit_set_option(
        &mut self, 
        keyword: Keyword, 
        value: AttributeValue<Constant, Symbol, SExpr>
    ) -> Result<Self::T, Self::E>;

}

Associated Types

Required methods

Implementors