Trait Rewriter 

pub trait Rewriter {
    type V: Smt2Visitor;
    type Error: From<<Self::V as Smt2Visitor>::Error>;

    // Required method
    fn visitor(&mut self) -> &mut Self::V;

    // Provided methods
    fn process_constant(
        &mut self,
        value: <Self::V as Smt2Visitor>::Constant,
    ) -> Result<<Self::V as Smt2Visitor>::Constant, Self::Error> { ... }
    fn process_symbol(
        &mut self,
        value: <Self::V as Smt2Visitor>::Symbol,
    ) -> Result<<Self::V as Smt2Visitor>::Symbol, Self::Error> { ... }
    fn process_keyword(
        &mut self,
        value: <Self::V as Smt2Visitor>::Keyword,
    ) -> Result<<Self::V as Smt2Visitor>::Keyword, Self::Error> { ... }
    fn process_s_expr(
        &mut self,
        value: <Self::V as Smt2Visitor>::SExpr,
    ) -> Result<<Self::V as Smt2Visitor>::SExpr, Self::Error> { ... }
    fn process_sort(
        &mut self,
        value: <Self::V as Smt2Visitor>::Sort,
    ) -> Result<<Self::V as Smt2Visitor>::Sort, Self::Error> { ... }
    fn process_qual_identifier(
        &mut self,
        value: <Self::V as Smt2Visitor>::QualIdentifier,
    ) -> Result<<Self::V as Smt2Visitor>::QualIdentifier, Self::Error> { ... }
    fn process_term(
        &mut self,
        value: <Self::V as Smt2Visitor>::Term,
    ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error> { ... }
    fn process_command(
        &mut self,
        value: <Self::V as Smt2Visitor>::Command,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_numeral_constant(
        &mut self,
        value: Numeral,
    ) -> Result<<Self::V as Smt2Visitor>::Constant, Self::Error> { ... }
    fn visit_decimal_constant(
        &mut self,
        value: Decimal,
    ) -> Result<<Self::V as Smt2Visitor>::Constant, Self::Error> { ... }
    fn visit_hexadecimal_constant(
        &mut self,
        value: Hexadecimal,
    ) -> Result<<Self::V as Smt2Visitor>::Constant, Self::Error> { ... }
    fn visit_binary_constant(
        &mut self,
        value: Binary,
    ) -> Result<<Self::V as Smt2Visitor>::Constant, Self::Error> { ... }
    fn visit_string_constant(
        &mut self,
        value: String,
    ) -> Result<<Self::V as Smt2Visitor>::Constant, Self::Error> { ... }
    fn visit_bound_symbol(
        &mut self,
        value: String,
    ) -> Result<<Self::V as Smt2Visitor>::Symbol, Self::Error> { ... }
    fn visit_fresh_symbol(
        &mut self,
        value: String,
        kind: SymbolKind,
    ) -> Result<<Self::V as Smt2Visitor>::Symbol, Self::Error> { ... }
    fn visit_any_symbol(
        &mut self,
        value: String,
    ) -> Result<<Self::V as Smt2Visitor>::Symbol, Self::Error> { ... }
    fn bind_symbol(&mut self, symbol: &<Self::V as Smt2Visitor>::Symbol) { ... }
    fn unbind_symbol(&mut self, symbol: &<Self::V as Smt2Visitor>::Symbol) { ... }
    fn visit_keyword(
        &mut self,
        value: String,
    ) -> Result<<Self::V as Smt2Visitor>::Keyword, Self::Error> { ... }
    fn visit_constant_s_expr(
        &mut self,
        value: <Self::V as Smt2Visitor>::Constant,
    ) -> Result<<Self::V as Smt2Visitor>::SExpr, Self::Error> { ... }
    fn visit_symbol_s_expr(
        &mut self,
        value: <Self::V as Smt2Visitor>::Symbol,
    ) -> Result<<Self::V as Smt2Visitor>::SExpr, Self::Error> { ... }
    fn visit_keyword_s_expr(
        &mut self,
        value: <Self::V as Smt2Visitor>::Keyword,
    ) -> Result<<Self::V as Smt2Visitor>::SExpr, Self::Error> { ... }
    fn visit_application_s_expr(
        &mut self,
        values: Vec<<Self::V as Smt2Visitor>::SExpr>,
    ) -> Result<<Self::V as Smt2Visitor>::SExpr, Self::Error> { ... }
    fn visit_simple_sort(
        &mut self,
        identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>,
    ) -> Result<<Self::V as Smt2Visitor>::Sort, Self::Error> { ... }
    fn visit_parameterized_sort(
        &mut self,
        identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>,
        parameters: Vec<<Self::V as Smt2Visitor>::Sort>,
    ) -> Result<<Self::V as Smt2Visitor>::Sort, Self::Error> { ... }
    fn visit_simple_identifier(
        &mut self,
        identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>,
    ) -> Result<<Self::V as Smt2Visitor>::QualIdentifier, Self::Error> { ... }
    fn visit_sorted_identifier(
        &mut self,
        identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>,
        sort: <Self::V as Smt2Visitor>::Sort,
    ) -> Result<<Self::V as Smt2Visitor>::QualIdentifier, Self::Error> { ... }
    fn visit_constant(
        &mut self,
        constant: <Self::V as Smt2Visitor>::Constant,
    ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error> { ... }
    fn visit_qual_identifier(
        &mut self,
        qual_identifier: <Self::V as Smt2Visitor>::QualIdentifier,
    ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error> { ... }
    fn visit_application(
        &mut self,
        qual_identifier: <Self::V as Smt2Visitor>::QualIdentifier,
        arguments: Vec<<Self::V as Smt2Visitor>::Term>,
    ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error> { ... }
    fn visit_let(
        &mut self,
        var_bindings: Vec<(<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Term)>,
        term: <Self::V as Smt2Visitor>::Term,
    ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error> { ... }
    fn visit_forall(
        &mut self,
        vars: Vec<(<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort)>,
        term: <Self::V as Smt2Visitor>::Term,
    ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error> { ... }
    fn visit_exists(
        &mut self,
        vars: Vec<(<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort)>,
        term: <Self::V as Smt2Visitor>::Term,
    ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error> { ... }
    fn visit_match(
        &mut self,
        term: <Self::V as Smt2Visitor>::Term,
        cases: Vec<(Vec<<Self::V as Smt2Visitor>::Symbol>, <Self::V as Smt2Visitor>::Term)>,
    ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error> { ... }
    fn visit_attributes(
        &mut self,
        term: <Self::V as Smt2Visitor>::Term,
        attributes: Vec<(<Self::V as Smt2Visitor>::Keyword, AttributeValue<<Self::V as Smt2Visitor>::Constant, <Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::SExpr>)>,
    ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error> { ... }
    fn visit_assert(
        &mut self,
        term: <Self::V as Smt2Visitor>::Term,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_check_sat(
        &mut self,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_check_sat_assuming(
        &mut self,
        literals: Vec<(<Self::V as Smt2Visitor>::Symbol, bool)>,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_declare_const(
        &mut self,
        symbol: <Self::V as Smt2Visitor>::Symbol,
        sort: <Self::V as Smt2Visitor>::Sort,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_declare_datatype(
        &mut self,
        symbol: <Self::V as Smt2Visitor>::Symbol,
        datatype: DatatypeDec<<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort>,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_declare_datatypes(
        &mut self,
        datatypes: Vec<(<Self::V as Smt2Visitor>::Symbol, Numeral, DatatypeDec<<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort>)>,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_declare_fun(
        &mut self,
        symbol: <Self::V as Smt2Visitor>::Symbol,
        parameters: Vec<<Self::V as Smt2Visitor>::Sort>,
        sort: <Self::V as Smt2Visitor>::Sort,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_declare_sort(
        &mut self,
        symbol: <Self::V as Smt2Visitor>::Symbol,
        arity: Numeral,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_define_fun(
        &mut self,
        sig: FunctionDec<<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort>,
        term: <Self::V as Smt2Visitor>::Term,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_define_fun_rec(
        &mut self,
        sig: FunctionDec<<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort>,
        term: <Self::V as Smt2Visitor>::Term,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_define_funs_rec(
        &mut self,
        funs: Vec<(FunctionDec<<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort>, <Self::V as Smt2Visitor>::Term)>,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_define_sort(
        &mut self,
        symbol: <Self::V as Smt2Visitor>::Symbol,
        parameters: Vec<<Self::V as Smt2Visitor>::Symbol>,
        sort: <Self::V as Smt2Visitor>::Sort,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_echo(
        &mut self,
        message: String,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_exit(
        &mut self,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_get_assertions(
        &mut self,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_get_assignment(
        &mut self,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_get_info(
        &mut self,
        flag: <Self::V as Smt2Visitor>::Keyword,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_get_model(
        &mut self,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_get_option(
        &mut self,
        keyword: <Self::V as Smt2Visitor>::Keyword,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_get_proof(
        &mut self,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_get_unsat_assumptions(
        &mut self,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_get_unsat_core(
        &mut self,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_get_value(
        &mut self,
        terms: Vec<<Self::V as Smt2Visitor>::Term>,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_pop(
        &mut self,
        level: Numeral,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_push(
        &mut self,
        level: Numeral,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_reset(
        &mut self,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_reset_assertions(
        &mut self,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_set_info(
        &mut self,
        keyword: <Self::V as Smt2Visitor>::Keyword,
        value: AttributeValue<<Self::V as Smt2Visitor>::Constant, <Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::SExpr>,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_set_logic(
        &mut self,
        symbol: <Self::V as Smt2Visitor>::Symbol,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
    fn visit_set_option(
        &mut self,
        keyword: <Self::V as Smt2Visitor>::Keyword,
        value: AttributeValue<<Self::V as Smt2Visitor>::Constant, <Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::SExpr>,
    ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error> { ... }
}

Helper trait to create variants of an existing Smt2Visitor.

Required Associated Types

type V: Smt2Visitor

type Error: From<<Self::V as Smt2Visitor>::Error>

Required Methods

fn visitor(&mut self) -> &mut Self::V

Delegate visitor

Provided Methods

fn process_constant( &mut self, value: <Self::V as Smt2Visitor>::Constant, ) -> Result<<Self::V as Smt2Visitor>::Constant, Self::Error>

fn process_symbol( &mut self, value: <Self::V as Smt2Visitor>::Symbol, ) -> Result<<Self::V as Smt2Visitor>::Symbol, Self::Error>

fn process_keyword( &mut self, value: <Self::V as Smt2Visitor>::Keyword, ) -> Result<<Self::V as Smt2Visitor>::Keyword, Self::Error>

fn process_s_expr( &mut self, value: <Self::V as Smt2Visitor>::SExpr, ) -> Result<<Self::V as Smt2Visitor>::SExpr, Self::Error>

fn process_sort( &mut self, value: <Self::V as Smt2Visitor>::Sort, ) -> Result<<Self::V as Smt2Visitor>::Sort, Self::Error>

fn process_qual_identifier( &mut self, value: <Self::V as Smt2Visitor>::QualIdentifier, ) -> Result<<Self::V as Smt2Visitor>::QualIdentifier, Self::Error>

fn process_term( &mut self, value: <Self::V as Smt2Visitor>::Term, ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error>

fn process_command( &mut self, value: <Self::V as Smt2Visitor>::Command, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_numeral_constant( &mut self, value: Numeral, ) -> Result<<Self::V as Smt2Visitor>::Constant, Self::Error>

fn visit_decimal_constant( &mut self, value: Decimal, ) -> Result<<Self::V as Smt2Visitor>::Constant, Self::Error>

fn visit_hexadecimal_constant( &mut self, value: Hexadecimal, ) -> Result<<Self::V as Smt2Visitor>::Constant, Self::Error>

fn visit_binary_constant( &mut self, value: Binary, ) -> Result<<Self::V as Smt2Visitor>::Constant, Self::Error>

fn visit_string_constant( &mut self, value: String, ) -> Result<<Self::V as Smt2Visitor>::Constant, Self::Error>

fn visit_bound_symbol( &mut self, value: String, ) -> Result<<Self::V as Smt2Visitor>::Symbol, Self::Error>

fn visit_fresh_symbol( &mut self, value: String, kind: SymbolKind, ) -> Result<<Self::V as Smt2Visitor>::Symbol, Self::Error>

fn visit_any_symbol( &mut self, value: String, ) -> Result<<Self::V as Smt2Visitor>::Symbol, Self::Error>

fn bind_symbol(&mut self, symbol: &<Self::V as Smt2Visitor>::Symbol)

fn unbind_symbol(&mut self, symbol: &<Self::V as Smt2Visitor>::Symbol)

fn visit_keyword( &mut self, value: String, ) -> Result<<Self::V as Smt2Visitor>::Keyword, Self::Error>

fn visit_constant_s_expr( &mut self, value: <Self::V as Smt2Visitor>::Constant, ) -> Result<<Self::V as Smt2Visitor>::SExpr, Self::Error>

fn visit_symbol_s_expr( &mut self, value: <Self::V as Smt2Visitor>::Symbol, ) -> Result<<Self::V as Smt2Visitor>::SExpr, Self::Error>

fn visit_keyword_s_expr( &mut self, value: <Self::V as Smt2Visitor>::Keyword, ) -> Result<<Self::V as Smt2Visitor>::SExpr, Self::Error>

fn visit_application_s_expr( &mut self, values: Vec<<Self::V as Smt2Visitor>::SExpr>, ) -> Result<<Self::V as Smt2Visitor>::SExpr, Self::Error>

fn visit_simple_sort( &mut self, identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>, ) -> Result<<Self::V as Smt2Visitor>::Sort, Self::Error>

fn visit_parameterized_sort( &mut self, identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>, parameters: Vec<<Self::V as Smt2Visitor>::Sort>, ) -> Result<<Self::V as Smt2Visitor>::Sort, Self::Error>

fn visit_simple_identifier( &mut self, identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>, ) -> Result<<Self::V as Smt2Visitor>::QualIdentifier, Self::Error>

fn visit_sorted_identifier( &mut self, identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>, sort: <Self::V as Smt2Visitor>::Sort, ) -> Result<<Self::V as Smt2Visitor>::QualIdentifier, Self::Error>

fn visit_constant( &mut self, constant: <Self::V as Smt2Visitor>::Constant, ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error>

fn visit_qual_identifier( &mut self, qual_identifier: <Self::V as Smt2Visitor>::QualIdentifier, ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error>

fn visit_application( &mut self, qual_identifier: <Self::V as Smt2Visitor>::QualIdentifier, arguments: Vec<<Self::V as Smt2Visitor>::Term>, ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error>

fn visit_let( &mut self, var_bindings: Vec<(<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Term)>, term: <Self::V as Smt2Visitor>::Term, ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error>

fn visit_forall( &mut self, vars: Vec<(<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort)>, term: <Self::V as Smt2Visitor>::Term, ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error>

fn visit_exists( &mut self, vars: Vec<(<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort)>, term: <Self::V as Smt2Visitor>::Term, ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error>

fn visit_match( &mut self, term: <Self::V as Smt2Visitor>::Term, cases: Vec<(Vec<<Self::V as Smt2Visitor>::Symbol>, <Self::V as Smt2Visitor>::Term)>, ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error>

fn visit_attributes( &mut self, term: <Self::V as Smt2Visitor>::Term, attributes: Vec<(<Self::V as Smt2Visitor>::Keyword, AttributeValue<<Self::V as Smt2Visitor>::Constant, <Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::SExpr>)>, ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error>

fn visit_assert( &mut self, term: <Self::V as Smt2Visitor>::Term, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_check_sat( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_check_sat_assuming( &mut self, literals: Vec<(<Self::V as Smt2Visitor>::Symbol, bool)>, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_declare_const( &mut self, symbol: <Self::V as Smt2Visitor>::Symbol, sort: <Self::V as Smt2Visitor>::Sort, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_declare_datatype( &mut self, symbol: <Self::V as Smt2Visitor>::Symbol, datatype: DatatypeDec<<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort>, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_declare_datatypes( &mut self, datatypes: Vec<(<Self::V as Smt2Visitor>::Symbol, Numeral, DatatypeDec<<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort>)>, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_declare_fun( &mut self, symbol: <Self::V as Smt2Visitor>::Symbol, parameters: Vec<<Self::V as Smt2Visitor>::Sort>, sort: <Self::V as Smt2Visitor>::Sort, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_declare_sort( &mut self, symbol: <Self::V as Smt2Visitor>::Symbol, arity: Numeral, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_define_fun( &mut self, sig: FunctionDec<<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort>, term: <Self::V as Smt2Visitor>::Term, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_define_fun_rec( &mut self, sig: FunctionDec<<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort>, term: <Self::V as Smt2Visitor>::Term, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_define_funs_rec( &mut self, funs: Vec<(FunctionDec<<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort>, <Self::V as Smt2Visitor>::Term)>, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_define_sort( &mut self, symbol: <Self::V as Smt2Visitor>::Symbol, parameters: Vec<<Self::V as Smt2Visitor>::Symbol>, sort: <Self::V as Smt2Visitor>::Sort, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_echo( &mut self, message: String, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_exit( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_get_assertions( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_get_assignment( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_get_info( &mut self, flag: <Self::V as Smt2Visitor>::Keyword, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_get_model( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_get_option( &mut self, keyword: <Self::V as Smt2Visitor>::Keyword, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_get_proof( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_get_unsat_assumptions( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_get_unsat_core( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_get_value( &mut self, terms: Vec<<Self::V as Smt2Visitor>::Term>, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_pop( &mut self, level: Numeral, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_push( &mut self, level: Numeral, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_reset( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_reset_assertions( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_set_info( &mut self, keyword: <Self::V as Smt2Visitor>::Keyword, value: AttributeValue<<Self::V as Smt2Visitor>::Constant, <Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::SExpr>, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_set_logic( &mut self, symbol: <Self::V as Smt2Visitor>::Symbol, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

fn visit_set_option( &mut self, keyword: <Self::V as Smt2Visitor>::Keyword, value: AttributeValue<<Self::V as Smt2Visitor>::Constant, <Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::SExpr>, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Implementors

impl<V, Error> Rewriter for SymbolNormalizer<V>

where V: Smt2Visitor<Symbol = Symbol, Command = Command, Error = Error>,

type V = V

type Error = Error

impl<V, Error> Rewriter for TesterModernizer<V>

where V: Smt2Visitor<QualIdentifier = QualIdentifier, Symbol = Symbol, Error = Error>,

type V = V

type Error = Error