Trait smt2parser::rewriter::Rewriter[−][src]

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

Show 66 methods    fn visitor(&mut self) -> &mut Self::V;

    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> { ... }

}
Expand description

Helper trait to create variants of an existing Smt2Visitor.

Associated Types

Required methods

Delegate visitor

Provided methods

Implementors