Struct smt2parser::renaming::TesterModernizer [−][src]
pub struct TesterModernizer<V>(_);
Expand description
A Rewriter
implementation that converts old-style testers is-Foo
into a proper indexed identifier (_ is Foo)
.
Implementations
Trait Implementations
Returns the “default value” for a type. Read more
impl<V, Error> Rewriter for TesterModernizer<V> where
V: Smt2Visitor<QualIdentifier = QualIdentifier, Symbol = Symbol, Error = Error>,
impl<V, Error> Rewriter for TesterModernizer<V> where
V: Smt2Visitor<QualIdentifier = QualIdentifier, Symbol = Symbol, Error = Error>,
type V = V
type Error = Error
fn visit_simple_identifier(
&mut self,
value: Identifier<Symbol>
) -> Result<QualIdentifier, Error>
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_bound_symbol(
&mut self,
value: String
) -> Result<<Self::V as Smt2Visitor>::Symbol, Self::Error>
fn visit_fresh_symbol(
&mut self,
value: String
) -> Result<<Self::V as Smt2Visitor>::Symbol, 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_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_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_get_info(
&mut self,
flag: <Self::V as Smt2Visitor>::Keyword
) -> 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_unsat_assumptions(
&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_push(
&mut self,
level: Numeral
) -> 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> RefUnwindSafe for TesterModernizer<V> where
V: RefUnwindSafe,
impl<V> Send for TesterModernizer<V> where
V: Send,
impl<V> Sync for TesterModernizer<V> where
V: Sync,
impl<V> Unpin for TesterModernizer<V> where
V: Unpin,
impl<V> UnwindSafe for TesterModernizer<V> where
V: UnwindSafe,
Blanket Implementations
Mutably borrows from an owned value. Read more
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,
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,
type T = <V as Smt2Visitor>::Command
pub fn visit_assert(
&mut Self,
<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>
pub 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>
pub fn visit_check_sat_assuming(
&mut Self,
Vec<(<V as Smt2Visitor>::Symbol, bool), Global>
) -> 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>
pub fn visit_declare_const(
&mut Self,
<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>
pub fn visit_declare_datatype(
&mut Self,
<V as Smt2Visitor>::Symbol,
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>
pub fn visit_declare_datatypes(
&mut Self,
Vec<(<V as Smt2Visitor>::Symbol, BigUint, DatatypeDec<<V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>), Global>
) -> 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>
pub fn visit_declare_fun(
&mut Self,
<V as Smt2Visitor>::Symbol,
Vec<<V as Smt2Visitor>::Sort, Global>,
<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>
pub fn visit_declare_sort(
&mut Self,
<V as Smt2Visitor>::Symbol,
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>
pub fn visit_define_fun(
&mut Self,
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>
pub fn visit_define_fun_rec(
&mut Self,
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>
pub fn visit_define_funs_rec(
&mut Self,
Vec<(FunctionDec<<V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort>, <V as Smt2Visitor>::Term), Global>
) -> 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>
pub fn visit_define_sort(
&mut Self,
<V as Smt2Visitor>::Symbol,
Vec<<V as Smt2Visitor>::Symbol, Global>,
<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>
pub fn visit_echo(
&mut Self,
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>
pub 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>
pub 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>
pub 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>
pub fn visit_get_info(
&mut Self,
<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>
pub 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>
pub fn visit_get_option(
&mut Self,
<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>
pub 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>
pub 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>
pub 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>
pub fn visit_get_value(
&mut Self,
Vec<<V as Smt2Visitor>::Term, Global>
) -> 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>
pub fn visit_pop(
&mut Self,
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>
pub fn visit_push(
&mut Self,
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>
pub 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>
pub 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>
pub fn visit_set_info(
&mut Self,
<V as Smt2Visitor>::Keyword,
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>
pub fn visit_set_logic(
&mut Self,
<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>
pub fn visit_set_option(
&mut Self,
<V as Smt2Visitor>::Keyword,
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>
type T = <V as Smt2Visitor>::Constant
pub fn visit_numeral_constant(
&mut Self,
BigUint
) -> Result<<R as ConstantVisitor>::T, <R as ConstantVisitor>::E>
pub fn visit_decimal_constant(
&mut Self,
Ratio<BigInt>
) -> Result<<R as ConstantVisitor>::T, <R as ConstantVisitor>::E>
pub fn visit_hexadecimal_constant(
&mut Self,
Vec<u8, Global>
) -> Result<<R as ConstantVisitor>::T, <R as ConstantVisitor>::E>
pub fn visit_binary_constant(
&mut Self,
Vec<bool, Global>
) -> Result<<R as ConstantVisitor>::T, <R as ConstantVisitor>::E>
pub fn visit_string_constant(
&mut Self,
String
) -> Result<<R as ConstantVisitor>::T, <R as ConstantVisitor>::E>
type T = <V as Smt2Visitor>::Keyword
pub fn visit_keyword(
&mut Self,
String
) -> Result<<R as KeywordVisitor>::T, <R as KeywordVisitor>::E>
impl<R, V> QualIdentifierVisitor<Identifier<<V as Smt2Visitor>::Symbol>, <V as Smt2Visitor>::Sort> for R where
R: Rewriter<V = V>,
V: Smt2Visitor,
impl<R, V> QualIdentifierVisitor<Identifier<<V as Smt2Visitor>::Symbol>, <V as Smt2Visitor>::Sort> for R where
R: Rewriter<V = V>,
V: Smt2Visitor,
type T = <V as Smt2Visitor>::QualIdentifier
pub fn visit_simple_identifier(
&mut Self,
Identifier<<V as Smt2Visitor>::Symbol>
) -> Result<<R as QualIdentifierVisitor<Identifier<<V as Smt2Visitor>::Symbol>, <V as Smt2Visitor>::Sort>>::T, <R as QualIdentifierVisitor<Identifier<<V as Smt2Visitor>::Symbol>, <V as Smt2Visitor>::Sort>>::E>
pub fn visit_sorted_identifier(
&mut Self,
Identifier<<V as Smt2Visitor>::Symbol>,
<V as Smt2Visitor>::Sort
) -> Result<<R as QualIdentifierVisitor<Identifier<<V as Smt2Visitor>::Symbol>, <V as Smt2Visitor>::Sort>>::T, <R as QualIdentifierVisitor<Identifier<<V as Smt2Visitor>::Symbol>, <V as Smt2Visitor>::Sort>>::E>
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,
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,
type T = <V as Smt2Visitor>::SExpr
pub fn visit_constant_s_expr(
&mut Self,
<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>
pub fn visit_symbol_s_expr(
&mut Self,
<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>
pub fn visit_keyword_s_expr(
&mut Self,
<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>
pub fn visit_application_s_expr(
&mut Self,
Vec<<R as SExprVisitor<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Keyword>>::T, Global>
) -> 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>
type Constant = <V as Smt2Visitor>::Constant
type QualIdentifier = <V as Smt2Visitor>::QualIdentifier
type Keyword = <V as Smt2Visitor>::Keyword
type Sort = <V as Smt2Visitor>::Sort
type SExpr = <V as Smt2Visitor>::SExpr
type Symbol = <V as Smt2Visitor>::Symbol
type Term = <V as Smt2Visitor>::Term
type Command = <V as Smt2Visitor>::Command
impl<R, V> SortVisitor<<V as Smt2Visitor>::Symbol> for R where
R: Rewriter<V = V>,
V: Smt2Visitor,
impl<R, V> SortVisitor<<V as Smt2Visitor>::Symbol> for R where
R: Rewriter<V = V>,
V: Smt2Visitor,
type T = <V as Smt2Visitor>::Sort
pub fn visit_simple_sort(
&mut Self,
Identifier<<V as Smt2Visitor>::Symbol>
) -> Result<<R as SortVisitor<<V as Smt2Visitor>::Symbol>>::T, <R as SortVisitor<<V as Smt2Visitor>::Symbol>>::E>
pub fn visit_parameterized_sort(
&mut Self,
Identifier<<V as Smt2Visitor>::Symbol>,
Vec<<R as SortVisitor<<V as Smt2Visitor>::Symbol>>::T, Global>
) -> Result<<R as SortVisitor<<V as Smt2Visitor>::Symbol>>::T, <R as SortVisitor<<V as Smt2Visitor>::Symbol>>::E>
type T = <V as Smt2Visitor>::Symbol
pub fn visit_fresh_symbol(
&mut Self,
String
) -> Result<<R as SymbolVisitor>::T, <R as SymbolVisitor>::E>
pub fn visit_bound_symbol(
&mut Self,
String
) -> Result<<R as SymbolVisitor>::T, <R as SymbolVisitor>::E>
pub fn visit_any_symbol(
&mut Self,
String
) -> Result<<R as SymbolVisitor>::T, <R as SymbolVisitor>::E>
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,
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,
type T = <V as Smt2Visitor>::Term
pub fn visit_constant(
&mut Self,
<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>
pub fn visit_qual_identifier(
&mut Self,
<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>
pub fn visit_application(
&mut Self,
<V as Smt2Visitor>::QualIdentifier,
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, Global>
) -> 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>
pub fn visit_let(
&mut Self,
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), Global>,
<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>
pub fn visit_forall(
&mut Self,
Vec<(<V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort), Global>,
<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>
pub fn visit_exists(
&mut Self,
Vec<(<V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort), Global>,
<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>
pub fn visit_match(
&mut Self,
<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,
Vec<(Vec<<V as Smt2Visitor>::Symbol, Global>, <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), Global>
) -> 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>
pub fn visit_attributes(
&mut Self,
<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,
Vec<(<V as Smt2Visitor>::Keyword, AttributeValue<<V as Smt2Visitor>::Constant, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::SExpr>), Global>
) -> 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>