in smt2parser/src/main.rs [92:140]
fn main() -> std::io::Result<()> {
let options = Options::from_args();
match options.operation {
Operation::Print {
normalize_symbols,
max_randomized_symbols,
symbol_randomization_seed,
inputs,
} => {
let randomization_space = smt2parser::visitors::SymbolKind::iter()
.map(|k| (k, max_randomized_symbols))
.collect();
let randomization_seed = symbol_randomization_seed.unwrap_or_else(rand::random);
let config = SymbolNormalizerConfig {
randomization_space,
randomization_seed,
};
if normalize_symbols {
let mut normalizer = SymbolNormalizer::new(SyntaxBuilder, config);
for input in inputs {
// 1. Parse input commands while rewriting `is-Foo` into `(_ is Foo)` on the fly with TesterModernizer.
process_file(TesterModernizer::new(SyntaxBuilder), input, |command| {
// 2. Re-visit the syntax for name resolution and normalization.
let command = command.accept(&mut normalizer).unwrap();
println!("{}", command);
})?;
}
} else {
for input in inputs {
process_file(SyntaxBuilder, input, |command| println!("{}", command))?;
}
}
}
Operation::Count {
keywords,
symbols,
inputs,
} => {
let keywords = read_words(keywords)?;
let symbols = read_words(symbols)?;
let mut state = Smt2Counters::new(keywords, symbols);
for input in inputs {
state = process_file(state, input, |_| {})?;
}
println!("{:#?}", state)
}
}
Ok(())
}