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,
kind: SymbolKind
) -> 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