pub struct SymbolNormalizer<V> { /* private fields */ }
Expand description
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 apop
command, but are otherwise unique (disregarding the more limited lexical scoping of variables).
Implementations§
Source§impl<V> SymbolNormalizer<V>
impl<V> SymbolNormalizer<V>
pub fn new(visitor: V, config: SymbolNormalizerConfig) -> Self
Sourcepub fn current_local_symbols(&self) -> &BTreeMap<SymbolKind, Vec<String>>
pub fn current_local_symbols(&self) -> &BTreeMap<SymbolKind, Vec<String>>
Original names of the current local symbols.
Sourcepub fn max_local_symbols(&self) -> &BTreeMap<SymbolKind, usize>
pub fn max_local_symbols(&self) -> &BTreeMap<SymbolKind, usize>
Max number of the local symbols simulatenously used.
Sourcepub fn global_symbols(&self) -> &BTreeSet<String>
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§
Source§impl<V: Debug> Debug for SymbolNormalizer<V>
impl<V: Debug> Debug for SymbolNormalizer<V>
Source§impl<V: Default> Default for SymbolNormalizer<V>
impl<V: Default> Default for SymbolNormalizer<V>
Source§fn default() -> SymbolNormalizer<V>
fn default() -> SymbolNormalizer<V>
Returns the “default value” for a type. Read more
Source§impl<V, Error> Rewriter for SymbolNormalizer<V>
impl<V, Error> Rewriter for SymbolNormalizer<V>
type V = V
type Error = Error
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>
Auto Trait Implementations§
impl<V> Freeze for SymbolNormalizer<V>where
V: Freeze,
impl<V> RefUnwindSafe for SymbolNormalizer<V>where
V: RefUnwindSafe,
impl<V> Send for SymbolNormalizer<V>where
V: Send,
impl<V> Sync for SymbolNormalizer<V>where
V: Sync,
impl<V> Unpin for SymbolNormalizer<V>where
V: Unpin,
impl<V> UnwindSafe for SymbolNormalizer<V>where
V: UnwindSafe,
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more