fn main()

in amzn-smt-prediction/src/main.rs [148:232]


fn main() -> std::io::Result<()> {
    let args: Vec<String> = env::args().collect();

    if args.len() < 4 {
        println!("Usage: amzn-smt-prediction <dataset> <path_to_benchmark_list> <name_for_output>");
        println!("Valid values of dataset: smtcomp, kepler, other");
        exit(1)
    }

    let dataset = &args[1];
    let path = &args[2];
    let out_name = &args[3];

    // Open list of benchmarks
    let b_list = File::open(path)?;
    let list_reader = BufReader::new(&b_list);

    // Open output file
    let out_file = File::create(format!("off_features_{}.csv", out_name))?;
    let mut out_writer = BufWriter::new(&out_file);

    // Write the header corresponding to the dataset
    out_writer.write_all(string_counter_csv_header(dataset).as_bytes())?;

    for line in list_reader.lines() {
        let mut file_name;

        // Prepend file path
        match dataset.as_str() {
            "smtcomp" | "kepler" => file_name = String::from("SMT_Comp_2020"),
            "script" => file_name = String::from("./"),
            "other" => {
                println!("No dataset specified. Looking for benchmarks in current directory.");
                file_name = String::from("./");
            }
            _ => {
                println!("Invalid value for dataset.");
                exit(1)
            }
        }

        file_name.push_str(&line?);

        println!("{}", file_name);

        // Open benchmark file
        let b_file = File::open(&file_name)?;
        let file_reader = BufReader::new(b_file);

        // Parse formulas
        let formulas = Script::<Term>::parse(file_reader);

        match formulas {
            Ok(script) => {
                let mut counter = StringCounter::default();

                // Count the String predicates
                assert_eq!(script.visit_asserted(&mut counter), ControlFlow::CONTINUE);

                // Write a line to the CSV file
                match dataset.as_str() {
                    "smtcomp" | "script" => {
                        out_writer.write_all(string_counter_csv_smtcomp(counter).as_bytes())?
                    }
                    "kepler" => {
                        out_writer.write_all(string_counter_csv_kepler(counter).as_bytes())?
                    }
                    "other" => out_writer.write_all(string_counter_csv_all(counter).as_bytes())?,
                    _ => {
                        println!("Invalid value for dataset.");
                        exit(1)
                    }
                }
            }
            Err(e) => {
                println!("Error on current benchmark.");
                eprintln!("{:?}", e);
                exit(1);
            }
        }
        out_writer.flush()?;
    }

    Ok(())
}