Struct smt2parser::renaming::SymbolNormalizer

pub struct SymbolNormalizer<V> { /* fields omitted */ }

A Rewriter implementation that normalizes local symbols into x0, x1, etc.

• Normalization applies to all symbols disregarding their usage (datatype, sorts, functions, variables, etc).
• “Global” symbols (those which don’t resolve locally) are ignored.

Implementations

impl<V> SymbolNormalizer<V>

pub fn new(visitor: V) -> Self

pub fn get_symbol(idx: usize) -> Symbol

pub fn local_symbols(&self) -> impl IntoIterator<Item = &String>

Initial names of all local symbols that were renamed.

pub fn global_symbols(&self) -> impl IntoIterator<Item = &String>

Symbols that failed to resolve locally (e.g. theory defined).

Trait Implementations

impl<V: Debug> Debug for SymbolNormalizer<V>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<V: Default> Default for SymbolNormalizer<V>

fn default() -> SymbolNormalizer<V>

Returns the “default value” for a type.

impl<V, Error> Rewriter for SymbolNormalizer<V> where
    V: Smt2Visitor<Symbol = Symbol, Error = Error>, 

type V = V

type Error = Error

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

Delegate visitor

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

fn visit_fresh_symbol(&mut self, value: String) -> Result<Symbol, Error>

fn bind_symbol(&mut self, symbol: &Symbol)

fn unbind_symbol(&mut self, symbol: &Symbol)

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_any_symbol(
    &mut self,
    value: String
) -> Result<<Self::V as Smt2Visitor>::Symbol, Self::Error>

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>