fn main()

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();
}