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 locally resolved symbols.
• A different prefix is applied depending on the symbol kind (datatype, sorts, functions, variables, etc).
• “Global” symbols (those which don’t resolve locally) are ignored.
• Symbol names may be re-used after a reset or a pop command, but are otherwise unique (disregarding the more limited lexical scoping of variables).

Implementations

impl<V> SymbolNormalizer<V>

pub fn new(visitor: V, config: SymbolNormalizerConfig) -> Self

pub fn current_local_symbols(&self) -> &BTreeMap<SymbolKind, Vec<String>>

Original names of the current local symbols.

pub fn max_local_symbols(&self) -> &BTreeMap<SymbolKind, usize>

Max number of the local symbols simulatenously used.

pub fn global_symbols(&self) -> &BTreeSet<String>

All symbol names that failed to be resolved locally at least once (e.g. theory defined symbols).

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, Command = Command, Error = Error>, 

type V = V

type Error = Error

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

Delegate visitor

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

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

fn visit_reset(&mut self) -> Result<Command, Error>

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

fn visit_fresh_symbol(
    &mut self,
    value: String,
    kind: SymbolKind
) -> 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_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>