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