Struct SymbolNormalizer

Source
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 a pop command, but are otherwise unique (disregarding the more limited lexical scoping of variables).

Implementations§

Source§

impl<V> SymbolNormalizer<V>

Source

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

Source

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

Original names of the current local symbols.

Source

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

Max number of the local symbols simulatenously used.

Source

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>

Source§

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

Formats the value using the given formatter. Read more
Source§

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

Source§

fn default() -> SymbolNormalizer<V>

Returns the “default value” for a type. Read more
Source§

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

Source§

type V = V

Source§

type Error = Error

Source§

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

Delegate visitor
Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

fn process_constant( &mut self, value: <Self::V as Smt2Visitor>::Constant, ) -> Result<<Self::V as Smt2Visitor>::Constant, Self::Error>

Source§

fn process_symbol( &mut self, value: <Self::V as Smt2Visitor>::Symbol, ) -> Result<<Self::V as Smt2Visitor>::Symbol, Self::Error>

Source§

fn process_keyword( &mut self, value: <Self::V as Smt2Visitor>::Keyword, ) -> Result<<Self::V as Smt2Visitor>::Keyword, Self::Error>

Source§

fn process_s_expr( &mut self, value: <Self::V as Smt2Visitor>::SExpr, ) -> Result<<Self::V as Smt2Visitor>::SExpr, Self::Error>

Source§

fn process_sort( &mut self, value: <Self::V as Smt2Visitor>::Sort, ) -> Result<<Self::V as Smt2Visitor>::Sort, Self::Error>

Source§

fn process_qual_identifier( &mut self, value: <Self::V as Smt2Visitor>::QualIdentifier, ) -> Result<<Self::V as Smt2Visitor>::QualIdentifier, Self::Error>

Source§

fn process_term( &mut self, value: <Self::V as Smt2Visitor>::Term, ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error>

Source§

fn process_command( &mut self, value: <Self::V as Smt2Visitor>::Command, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Source§

fn visit_numeral_constant( &mut self, value: Numeral, ) -> Result<<Self::V as Smt2Visitor>::Constant, Self::Error>

Source§

fn visit_decimal_constant( &mut self, value: Decimal, ) -> Result<<Self::V as Smt2Visitor>::Constant, Self::Error>

Source§

fn visit_hexadecimal_constant( &mut self, value: Hexadecimal, ) -> Result<<Self::V as Smt2Visitor>::Constant, Self::Error>

Source§

fn visit_binary_constant( &mut self, value: Binary, ) -> Result<<Self::V as Smt2Visitor>::Constant, Self::Error>

Source§

fn visit_string_constant( &mut self, value: String, ) -> Result<<Self::V as Smt2Visitor>::Constant, Self::Error>

Source§

fn visit_any_symbol( &mut self, value: String, ) -> Result<<Self::V as Smt2Visitor>::Symbol, Self::Error>

Source§

fn visit_keyword( &mut self, value: String, ) -> Result<<Self::V as Smt2Visitor>::Keyword, Self::Error>

Source§

fn visit_constant_s_expr( &mut self, value: <Self::V as Smt2Visitor>::Constant, ) -> Result<<Self::V as Smt2Visitor>::SExpr, Self::Error>

Source§

fn visit_symbol_s_expr( &mut self, value: <Self::V as Smt2Visitor>::Symbol, ) -> Result<<Self::V as Smt2Visitor>::SExpr, Self::Error>

Source§

fn visit_keyword_s_expr( &mut self, value: <Self::V as Smt2Visitor>::Keyword, ) -> Result<<Self::V as Smt2Visitor>::SExpr, Self::Error>

Source§

fn visit_application_s_expr( &mut self, values: Vec<<Self::V as Smt2Visitor>::SExpr>, ) -> Result<<Self::V as Smt2Visitor>::SExpr, Self::Error>

Source§

fn visit_simple_sort( &mut self, identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>, ) -> Result<<Self::V as Smt2Visitor>::Sort, Self::Error>

Source§

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>

Source§

fn visit_simple_identifier( &mut self, identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>, ) -> Result<<Self::V as Smt2Visitor>::QualIdentifier, Self::Error>

Source§

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>

Source§

fn visit_constant( &mut self, constant: <Self::V as Smt2Visitor>::Constant, ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error>

Source§

fn visit_qual_identifier( &mut self, qual_identifier: <Self::V as Smt2Visitor>::QualIdentifier, ) -> Result<<Self::V as Smt2Visitor>::Term, Self::Error>

Source§

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>

Source§

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>

Source§

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>

Source§

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>

Source§

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>

Source§

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>

Source§

fn visit_assert( &mut self, term: <Self::V as Smt2Visitor>::Term, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Source§

fn visit_check_sat( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Source§

fn visit_check_sat_assuming( &mut self, literals: Vec<(<Self::V as Smt2Visitor>::Symbol, bool)>, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Source§

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>

Source§

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>

Source§

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>

Source§

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>

Source§

fn visit_declare_sort( &mut self, symbol: <Self::V as Smt2Visitor>::Symbol, arity: Numeral, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Source§

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>

Source§

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>

Source§

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>

Source§

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>

Source§

fn visit_echo( &mut self, message: String, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Source§

fn visit_exit( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Source§

fn visit_get_assertions( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Source§

fn visit_get_assignment( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Source§

fn visit_get_info( &mut self, flag: <Self::V as Smt2Visitor>::Keyword, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Source§

fn visit_get_model( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Source§

fn visit_get_option( &mut self, keyword: <Self::V as Smt2Visitor>::Keyword, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Source§

fn visit_get_proof( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Source§

fn visit_get_unsat_assumptions( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Source§

fn visit_get_unsat_core( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Source§

fn visit_get_value( &mut self, terms: Vec<<Self::V as Smt2Visitor>::Term>, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Source§

fn visit_reset_assertions( &mut self, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Source§

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>

Source§

fn visit_set_logic( &mut self, symbol: <Self::V as Smt2Visitor>::Symbol, ) -> Result<<Self::V as Smt2Visitor>::Command, Self::Error>

Source§

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> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<R, V> CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr> for R
where R: Rewriter<V = V>, V: Smt2Visitor,

Source§

type T = <V as Smt2Visitor>::Command

Source§

type E = <R as Rewriter>::Error

Source§

fn visit_assert( &mut self, term: <V as Smt2Visitor>::Term, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_check_sat( &mut self, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_check_sat_assuming( &mut self, literals: Vec<(<V as Smt2Visitor>::Symbol, bool)>, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_declare_const( &mut self, symbol: <V as Smt2Visitor>::Symbol, sort: <V as Smt2Visitor>::Sort, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_declare_datatype( &mut self, symbol: <V as Smt2Visitor>::Symbol, datatype: DatatypeDec<<V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_declare_datatypes( &mut self, datatypes: Vec<(<V as Smt2Visitor>::Symbol, BigUint, DatatypeDec<<V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>)>, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_declare_fun( &mut self, symbol: <V as Smt2Visitor>::Symbol, parameters: Vec<<V as Smt2Visitor>::Sort>, sort: <V as Smt2Visitor>::Sort, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_declare_sort( &mut self, symbol: <V as Smt2Visitor>::Symbol, arity: BigUint, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_define_fun( &mut self, sig: FunctionDec<<V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>, term: <V as Smt2Visitor>::Term, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_define_fun_rec( &mut self, sig: FunctionDec<<V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>, term: <V as Smt2Visitor>::Term, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_define_funs_rec( &mut self, funs: Vec<(FunctionDec<<V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>, <V as Smt2Visitor>::Term)>, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_define_sort( &mut self, symbol: <V as Smt2Visitor>::Symbol, parameters: Vec<<V as Smt2Visitor>::Symbol>, sort: <V as Smt2Visitor>::Sort, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_echo( &mut self, message: String, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_exit( &mut self, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_get_assertions( &mut self, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_get_assignment( &mut self, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_get_info( &mut self, flag: <V as Smt2Visitor>::Keyword, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_get_model( &mut self, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_get_option( &mut self, keyword: <V as Smt2Visitor>::Keyword, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_get_proof( &mut self, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_get_unsat_assumptions( &mut self, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_get_unsat_core( &mut self, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_get_value( &mut self, terms: Vec<<V as Smt2Visitor>::Term>, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_pop( &mut self, level: BigUint, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_push( &mut self, level: BigUint, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_reset( &mut self, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_reset_assertions( &mut self, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_set_info( &mut self, keyword: <V as Smt2Visitor>::Keyword, value: AttributeValue<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::SExpr>, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_set_logic( &mut self, symbol: <V as Smt2Visitor>::Symbol, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

fn visit_set_option( &mut self, keyword: <V as Smt2Visitor>::Keyword, value: AttributeValue<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::SExpr>, ) -> Result<<R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::T, <R as CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr>>::E>

Source§

impl<R, V> ConstantVisitor for R
where R: Rewriter<V = V>, V: Smt2Visitor,

Source§

type T = <V as Smt2Visitor>::Constant

Source§

type E = <R as Rewriter>::Error

Source§

fn visit_numeral_constant( &mut self, value: BigUint, ) -> Result<<R as ConstantVisitor>::T, <R as ConstantVisitor>::E>

Source§

fn visit_decimal_constant( &mut self, value: Ratio<BigInt>, ) -> Result<<R as ConstantVisitor>::T, <R as ConstantVisitor>::E>

Source§

fn visit_hexadecimal_constant( &mut self, value: Vec<u8>, ) -> Result<<R as ConstantVisitor>::T, <R as ConstantVisitor>::E>

Source§

fn visit_binary_constant( &mut self, value: Vec<bool>, ) -> Result<<R as ConstantVisitor>::T, <R as ConstantVisitor>::E>

Source§

fn visit_string_constant( &mut self, value: String, ) -> Result<<R as ConstantVisitor>::T, <R as ConstantVisitor>::E>

Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<R, V> KeywordVisitor for R
where R: Rewriter<V = V>, V: Smt2Visitor,

Source§

type T = <V as Smt2Visitor>::Keyword

Source§

type E = <R as Rewriter>::Error

Source§

fn visit_keyword( &mut self, value: String, ) -> Result<<R as KeywordVisitor>::T, <R as KeywordVisitor>::E>

Source§

impl<R, V> QualIdentifierVisitor<Identifier<<V as Smt2Visitor>::Symbol>, <V as Smt2Visitor>::Sort> for R
where R: Rewriter<V = V>, V: Smt2Visitor,

Source§

impl<R, V> SExprVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Keyword> for R
where R: Rewriter<V = V>, V: Smt2Visitor,

Source§

type T = <V as Smt2Visitor>::SExpr

Source§

type E = <R as Rewriter>::Error

Source§

fn visit_constant_s_expr( &mut self, value: <V as Smt2Visitor>::Constant, ) -> Result<<R as SExprVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Keyword>>::T, <R as SExprVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Keyword>>::E>

Source§

fn visit_symbol_s_expr( &mut self, value: <V as Smt2Visitor>::Symbol, ) -> Result<<R as SExprVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Keyword>>::T, <R as SExprVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Keyword>>::E>

Source§

fn visit_keyword_s_expr( &mut self, value: <V as Smt2Visitor>::Keyword, ) -> Result<<R as SExprVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Keyword>>::T, <R as SExprVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Keyword>>::E>

Source§

fn visit_application_s_expr( &mut self, values: Vec<<R as SExprVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Keyword>>::T>, ) -> Result<<R as SExprVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Keyword>>::T, <R as SExprVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Keyword>>::E>

Source§

impl<R, V> Smt2Visitor for R
where R: Rewriter<V = V>, V: Smt2Visitor,

Source§

impl<R, V> SortVisitor<<V as Smt2Visitor>::Symbol> for R
where R: Rewriter<V = V>, V: Smt2Visitor,

Source§

type T = <V as Smt2Visitor>::Sort

Source§

type E = <R as Rewriter>::Error

Source§

fn visit_simple_sort( &mut self, identifier: Identifier<<V as Smt2Visitor>::Symbol>, ) -> Result<<R as SortVisitor<<V as Smt2Visitor>::Symbol>>::T, <R as SortVisitor<<V as Smt2Visitor>::Symbol>>::E>

Source§

fn visit_parameterized_sort( &mut self, identifier: Identifier<<V as Smt2Visitor>::Symbol>, parameters: Vec<<R as SortVisitor<<V as Smt2Visitor>::Symbol>>::T>, ) -> Result<<R as SortVisitor<<V as Smt2Visitor>::Symbol>>::T, <R as SortVisitor<<V as Smt2Visitor>::Symbol>>::E>

Source§

impl<R, V> SymbolVisitor for R
where R: Rewriter<V = V>, V: Smt2Visitor,

Source§

type T = <V as Smt2Visitor>::Symbol

Source§

type E = <R as Rewriter>::Error

Source§

fn visit_fresh_symbol( &mut self, value: String, kind: SymbolKind, ) -> Result<<R as SymbolVisitor>::T, <R as SymbolVisitor>::E>

Source§

fn visit_bound_symbol( &mut self, value: String, ) -> Result<<R as SymbolVisitor>::T, <R as SymbolVisitor>::E>

Source§

fn visit_any_symbol( &mut self, value: String, ) -> Result<<R as SymbolVisitor>::T, <R as SymbolVisitor>::E>

Source§

fn bind_symbol(&mut self, symbol: &<R as SymbolVisitor>::T)

Source§

fn unbind_symbol(&mut self, symbol: &<R as SymbolVisitor>::T)

Source§

impl<R, V> TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort> for R
where R: Rewriter<V = V>, V: Smt2Visitor,

Source§

type T = <V as Smt2Visitor>::Term

Source§

type E = <R as Rewriter>::Error

Source§

fn visit_constant( &mut self, constant: <V as Smt2Visitor>::Constant, ) -> Result<<R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::T, <R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::E>

Source§

fn visit_qual_identifier( &mut self, qual_identifier: <V as Smt2Visitor>::QualIdentifier, ) -> Result<<R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::T, <R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::E>

Source§

fn visit_application( &mut self, qual_identifier: <V as Smt2Visitor>::QualIdentifier, arguments: Vec<<R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::T>, ) -> Result<<R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::T, <R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::E>

Source§

fn visit_let( &mut self, var_bindings: Vec<(<V as Smt2Visitor>::Symbol, <R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::T)>, term: <R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::T, ) -> Result<<R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::T, <R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::E>

Source§

fn visit_forall( &mut self, vars: Vec<(<V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort)>, term: <R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::T, ) -> Result<<R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::T, <R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::E>

Source§

fn visit_exists( &mut self, vars: Vec<(<V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort)>, term: <R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::T, ) -> Result<<R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::T, <R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::E>

Source§

fn visit_match( &mut self, term: <R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::T, cases: Vec<(Vec<<V as Smt2Visitor>::Symbol>, <R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::T)>, ) -> Result<<R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::T, <R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::E>

Source§

fn visit_attributes( &mut self, term: <R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::T, attributes: Vec<(<V as Smt2Visitor>::Keyword, AttributeValue<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::SExpr>)>, ) -> Result<<R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::T, <R as TermVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::QualIdentifier, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::SExpr, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>>::E>

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
Source§

impl<V, T> VZip<V> for T
where V: MultiLane<T>,

Source§

fn vzip(self) -> V