Struct SymbolNormalizer

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

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>