in smt2proxy/src/main.rs [210:271]
fn main() {
let options = Options::from_iter(iter_args());
let smt2proxy_normalize_symbols = options.smt2proxy_config.smt2proxy_normalize_symbols;
if options.version {
std::process::Command::new("z3")
.arg("-version")
.status()
.unwrap();
return;
}
// Spawn the command processor in a separate thread.
let (sender, receiver) = std::sync::mpsc::channel();
let handler = {
let z3_args = make_z3_args(&options);
let processor = smt2proxy::CommandProcessor::from(options.smt2proxy_config);
std::thread::spawn(move || {
process_events(receiver, z3_args, processor);
})
};
// Setup the input file.
let stdin = std::io::stdin();
let input: Box<dyn std::io::BufRead> = if options.r#in {
Box::new(stdin.lock())
} else {
let path_opt = options
.extra
.last()
.filter(|s| !s.contains('='))
.map(std::path::PathBuf::from);
let path = options
.file
.or(path_opt)
.expect("Input file is required unless flags `-in` or `-version` are passed.");
let f = std::fs::File::open(&path)
.unwrap_or_else(|_| panic!("Failed to open input file {:?}", path));
Box::new(std::io::BufReader::new(f))
};
// Send the input commands to the command processor.
let stream: Box<dyn Iterator<Item = std::result::Result<_, _>>> = {
if smt2proxy_normalize_symbols {
let builder =
smt2parser::renaming::TesterModernizer::new(smt2parser::concrete::SyntaxBuilder);
Box::new(smt2parser::CommandStream::new(input, builder, None))
} else {
let builder = smt2parser::concrete::SyntaxBuilder;
Box::new(smt2parser::CommandStream::new(input, builder, None))
}
};
for result in stream {
sender.send(Event::Query(Box::new(result))).unwrap();
}
// Send EOF to z3.
sender.send(Event::Done).unwrap();
// Wait for the command processor to terminate.
handler.join().unwrap();
}