From 9f6821a51890ee795fe53285b486be1520513699 Mon Sep 17 00:00:00 2001 From: joaomhmpereira Date: Wed, 23 Oct 2024 18:08:14 +0100 Subject: [PATCH] Add scripts for EQ3 --- bench/eq2.sh | 55 ++++++++++++++++--------- bench/eq3.sh | 90 +++++++++++++++++++++++++++++++++++++++++ bench/run_benchmarks.py | 62 +++++++++++++++++++++++++--- 3 files changed, 182 insertions(+), 25 deletions(-) create mode 100644 bench/eq3.sh diff --git a/bench/eq2.sh b/bench/eq2.sh index a4973307..33afdb09 100644 --- a/bench/eq2.sh +++ b/bench/eq2.sh @@ -4,53 +4,68 @@ opam sw z3-bitwuzla eval $(opam env) #### QF_FP #### -python3 single_query.py --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_z3 --prover smtml-z3 -python3 single_query.py --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_singe --output-filename QF_FP_bitwuzla --prover smtml-bitwuzla +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_z3 --prover smtml-z3 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_singe --output-filename QF_FP_bitwuzla --prover smtml-bitwuzla +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_z3_solver --prover z3 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_bitwuzla_solver --prover bitwuzla #### QF_LIA #### -python3 single_query.py --dir smt-comp/smtlib/non-incremental/QF_LIA --output-dir csvs_single --output-filename QF_LIA_z3 --prover smtml-z3 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_LIA --output-dir csvs_single --output-filename QF_LIA_z3 --prover smtml-z3 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_LIA --output-dir csvs_single --output-filename QF_LIA_z3_solver --prover z3 #### QF_BV #### -python3 single_query.py --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_z3 --prover smtml-z3 -python3 single_query.py --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_bitwuzla --prover smtml-bitwuzla +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_z3 --prover smtml-z3 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_bitwuzla --prover smtml-bitwuzla +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_z3_solver --prover z3 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_bitwuzla --prover smtml-bitwuzla #### QF_S #### -python3 single_query.py --dir smt-comp/smtlib/non-incremental/QF_S --output-dir csvs_single --output-filename QF_S_z3 --prover smtml-z3 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_S --output-dir csvs_single --output-filename QF_S_z3 --prover smtml-z3 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_S --output-dir csvs_single --output-filename QF_S_z3_solver --prover z3 #### QF_SLIA #### -python3 single_query.py --dir smt-comp/smtlib/non-incremental/QF_SLIA --output-dir csvs_single --output-filename QF_SLIA_z3 --prover smtml-z3 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_SLIA --output-dir csvs_single --output-filename QF_SLIA_z3 --prover smtml-z3 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_SLIA --output-dir csvs_single --output-filename QF_SLIA_z3_solver --prover z3 ## cvc5 ## opam sw cvc5 eval $(opam env) #### QF_FP #### -python3 single_query.py --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_cvc5 --prover smtml-cvc5 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_cvc5 --prover smtml-cvc5 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_cvc5_solver --prover cvc5 #### QF_LIA #### -python3 single_query.py --dir smt-comp/smtlib/non-incremental/QF_LIA --output-dir csvs_single --output-filename QF_LIA_cvc5 --prover smtml-cvc5 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_LIA --output-dir csvs_single --output-filename QF_LIA_cvc5 --prover smtml-cvc5 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_LIA --output-dir csvs_single --output-filename QF_LIA_cvc5_solver --prover cvc5 #### QF_BV #### -python3 single_query.py --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_cvc5 --prover smtml-cvc5 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_cvc5 --prover smtml-cvc5 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_cvc5_solver --prover cvc5 #### QF_S #### -python3 single_query.py --dir smt-comp/smtlib/non-incremental/QF_S --output-dir csvs_single --output-filename QF_S_cvc5 --prover smtml-cvc5 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_S --output-dir csvs_single --output-filename QF_S_cvc5 --prover smtml-cvc5 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_S --output-dir csvs_single --output-filename QF_S_cvc5_solver --prover cvc5 #### QF_SLIA #### -python3 single_query.py --dir smt-comp/smtlib/non-incremental/QF_SLIA --output-dir csvs_single --output-filename QF_SLIA_cvc5 --prover smtml-cvc5 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_SLIA --output-dir csvs_single --output-filename QF_SLIA_cvc5 --prover smtml-cvc5 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_SLIA --output-dir csvs_single --output-filename QF_SLIA_cvc5_solver --prover cvc5 ## Colibri2 ## opam sw colibri2 eval $(opam env) #### QF_FP #### -python3 single_query.py --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_colibri2 --prover smtml-colibri2 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_colibri2 --prover smtml-colibri2 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_colibri2_solver --prover colibri2 #### QF_LIA #### -python3 single_query.py --dir smt-comp/smtlib/non-incremental/QF_LIA --output-dir csvs_single --output-filename QF_LIA_colibri2 --prover smtml-colibri2 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_LIA --output-dir csvs_single --output-filename QF_LIA_colibri2 --prover smtml-colibri2 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_LIA --output-dir csvs_single --output-filename QF_LIA_colibri2_solver --prover colibri2 #### QF_BV #### -python3 single_query.py --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_colibri2 --prover smtml-colibri2 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_colibri2 --prover smtml-colibri2 +python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_colibri2_solver --prover colibri2 ## Concat CSVs ## #### QF_FP #### -python3 plots.py --output csvs_single/QF_FP_all.csv --concat csvs_single/QF_FP_z3.csv csvs_single/QF_FP_bitwuzla.csv csvs_single/QF_FP_cvc5.csv csvs_single/QF_FP_colibri2.csv +python3 plots.py --output csvs_single/QF_FP_all.csv --concat --files csvs_single/QF_FP_z3.csv csvs_single/QF_FP_bitwuzla.csv csvs_single/QF_FP_cvc5.csv csvs_single/QF_FP_colibri2.csv csvs_single/QF_FP_z3_solver.csv csvs_single/QF_FP_bitwuzla_solver.csv csvs_single/QF_FP_cvc5_solver.csv csvs_single/QF_FP_colibri2_solver.csv #### QF_LIA #### -python3 plots.py --output csvs_single/QF_LIA_all.csv --concat csvs_single/QF_LIA_z3.csv csvs_single/QF_LIA_cvc5.csv csvs_single/QF_LIA_colibri2.csv +python3 plots.py --output csvs_single/QF_LIA_all.csv --concat --files csvs_single/QF_LIA_z3.csv csvs_single/QF_LIA_cvc5.csv csvs_single/QF_LIA_colibri2.csv csvs_single/QF_LIA_z3_solver.csv csvs_single/QF_LIA_cvc5_solver.csv csvs_single/QF_LIA_colibri2_solver.csv #### QF_BV #### -python3 plots.py --output csvs_single/QF_BV_all.csv --concat csvs_single/QF_BV_z3.csv csvs_single/QF_BV_bitwuzla.csv csvs_single/QF_BV_cvc5.csv csvs_single/QF_BV_colibri2.csv +python3 plots.py --output csvs_single/QF_BV_all.csv --concat --files csvs_single/QF_BV_z3.csv csvs_single/QF_BV_bitwuzla.csv csvs_single/QF_BV_cvc5.csv csvs_single/QF_BV_colibri2.csv csvs_single/QF_BV_z3_solver.csv csvs_single/QF_BV_bitwuzla_solver.csv csvs_single/QF_BV_cvc5_solver.csv csvs_single/QF_BV_colibri2_solver.csv #### QF_S #### -python3 plots.py --output csvs_single/QF_S_all.csv --concat csvs_single/QF_S_z3.csv csvs_single/QF_S_cvc5.csv +python3 plots.py --output csvs_single/QF_S_all.csv --concat --files csvs_single/QF_S_z3.csv csvs_single/QF_S_cvc5.csv csvs_single/QF_S_z3_solver.csv csvs_single/QF_S_cvc5_solver.csv #### QF_SLIA #### -python3 plots.py --output csvs_single/QF_SLIA_all.csv --concat csvs_single/QF_SLIA_z3.csv csvs_single/QF_SLIA_cvc5.csv +python3 plots.py --output csvs_single/QF_SLIA_all.csv --concat --files csvs_single/QF_SLIA_z3.csv csvs_single/QF_SLIA_cvc5.csv csvs_single/QF_SLIA_z3_solver.csv csvs_single/QF_SLIA_cvc5_solver.csv ## Generate plots ## #### QF_FP #### diff --git a/bench/eq3.sh b/bench/eq3.sh new file mode 100644 index 00000000..98a6e258 --- /dev/null +++ b/bench/eq3.sh @@ -0,0 +1,90 @@ +#!/bin/bash + +opam sw z3-bitwuzla +eval $(opam env) + +#### QF_FP #### +## Z3 ## +if [ -e "csvs_single/QF_FP_z3_solver.csv" ]; then + : # do nothing +else + python3 run_benchmarks.py --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_z3_solver --prover z3 +fi + +python3 run_benchmarks.py --multi -F QF_FP_paths.list --output-dir csvs_multi --output-filename QF_FP_z3 --prover smtml-z3 + +## Bitwuzla ## +if [ -e "csvs_single/QF_FP_bitwuzla_solver.csv" ]; then + : # do nothing +else + python3 run_benchmarks.py --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_bitwuzla_solver --prover bitwuzla +fi + +python3 run_benchmarks.py --multi -F QF_FP_paths.list --output-dir csvs_multi --output-filename QF_FP_bitwuzla_solver --prover bitwuzla + +#### QF_LIA #### +## Z3 ## +if [ -e "csvs_single/QF_LIA_z3_solver.csv" ]; then + : # do nothing +else + python3 run_benchmarks.py --dir smt-comp/smtlib/non-incremental/QF_LIA --output-dir csvs_single --output-filename QF_LIA_z3_solver --prover z3 +fi + +python3 run_benchmarks.py --multi -F QF_LIA_paths.list --output-dir csvs_multi --output-filename QF_LIA_z3 --prover smtml-z3 + +#### QF_BV #### +## Z3 ## +if [ -e "csvs_single/QF_BV_z3_solver.csv" ]; then + : # do nothing +else + python3 run_benchmarks.py --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_z3_solver --prover z3 +fi + +python3 run_benchmarks.py --multi -F QF_BV_paths.list --output-dir csvs_multi --output-filename QF_BV_z3 --prover smtml-z3 + +## Bitwuzla ## +if [ -e "csvs_single/QF_BV_bitwuzla_solver.csv" ]; then + : # do nothing +else + python3 run_benchmarks.py --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_bitwuzla_solver --prover bitwuzla +fi + +python3 run_benchmarks.py --multi -F QF_BV_paths.list --output-dir csvs_multi --output-filename QF_BV_bitwuzla_solver --prover bitwuzla + +#### QF_S #### +## Z3 ## +if [ -e "csvs_single/QF_S_z3_solver.csv" ]; then + : # do nothing +else + python3 run_benchmarks.py --dir smt-comp/smtlib/non-incremental/QF_S --output-dir csvs_single --output-filename QF_S_z3_solver --prover z3 +fi + +python3 run_benchmarks.py --multi -F QF_S_paths.list --output-dir csvs_multi --output-filename QF_S_z3 --prover smtml-z3 + +#### QF_SLIA #### +## Z3 ## +if [ -e "csvs_single/QF_SLIA_z3_solver.csv" ]; then + : # do nothing +else + python3 run_benchmarks.py --dir smt-comp/smtlib/non-incremental/QF_SLIA --output-dir csvs_single --output-filename QF_SLIA_z3_solver --prover z3 +fi + +python3 run_benchmarks.py --multi -F QF_SLIA_paths.list --output-dir csvs_multi --output-filename QF_SLIA_z3 --prover smtml-z3 + + +## Generate plots ## + +## QF_FP ## +python3 plots.py --multi --QF-FP --output plot_QF_FP_multi --files csvs_multi/QF_FP_z3.csv csvs_multi/QF_FP_bitwuzla.csv csvs_single/QF_FP_z3_solver.csv csvs_single/QF_FP_bitwuzla_solver.csv + +## QF_LIA ## +python3 plots.py --multi --QF-LIA --output plot_QF_LIA_multi --files csvs_multi/QF_LIA_z3.csv csvs_single/QF_LIA_z3_solver.csv + +## QF_BV ## +python3 plots.py --multi --QF-BV --output plot_QF_BV_multi --files csvs_multi/QF_BV_z3.csv csvs_multi/QF_BV_bitwuzla.csv csvs_single/QF_BV_z3_solver.csv csvs_single/QF_BV_bitwuzla_solver.csv + +## QF_S ## +python3 plots.py --multi --QF-S --output plot_QF_S_multi --files csvs_multi/QF_S_z3.csv csvs_single/QF_S_z3_solver.csv + +## QF_SLIA ## +python3 plots.py --multi --QF-SLIA --output plot_QF_SLIA_multi --files csvs_multi/QF_SLIA_z3.csv csvs_single/QF_SLIA_z3_solver.csv \ No newline at end of file diff --git a/bench/run_benchmarks.py b/bench/run_benchmarks.py index 60e86601..93869bdf 100644 --- a/bench/run_benchmarks.py +++ b/bench/run_benchmarks.py @@ -3,6 +3,8 @@ import csv import sqlite3 import argparse +import glob +import pandas as pd def print_error(msg): print(f"\033[91m{msg}\033[0m") @@ -62,25 +64,75 @@ def automate_benchpress_single(directory_to_benchmark, output_csv_dir, output_cs except Exception as e: print_error(f"Error during SQLite to CSV process: {e}") -def automate_multi_query(): - pass +def get_latest_n_csvs(n): + result = subprocess.run(['ls', '-d', os.path.join('/home/smtml/smtml/bench', 'res-multi-query-*')], + stdout=subprocess.PIPE, text=True, shell=True) + query_dirs = result.stdout.splitlines() + query_dirs = query_dirs[-n:] + csv_files = [] + for query_dir in query_dirs: + csv_file = glob(os.path.join(query_dir, '*.csv')) + if csv_file: + csv_files.append(csv_file[0]) + return csv_files + +def concatenate_csvs(csv_paths, output_dir, output_file): + df_list = [pd.read_csv(csv_file) for csv_file in csv_paths] + concatenated_df = pd.concat(df_list, ignore_index=True) + concatenated_df.to_csv(os.path.join(output_dir, output_file), index=False) + +def split_file(input_file, output_prefix, lines_per_file=1000): + with open(input_file, 'r') as file: + lines = file.readlines() + total_files = len(lines) // lines_per_file + (1 if len(lines) % lines_per_file else 0) + aux_files = [] + for i in range(total_files): + start_index = i * lines_per_file + end_index = start_index + lines_per_file + aux_lines = lines[start_index:end_index] + output_file = f"{output_prefix}_{i+1}.txt" + aux_files.append(output_file) + with open(output_file, 'w') as aux_file: + aux_file.writelines(aux_lines) + return aux_files + +def run_multi_query(list_file, prover): + try: + command = ['dune', 'exec', '--', './runner/runner.exe', 'multi-query', '-p', prover, '-F', list_file] + subprocess.run(command, check=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE) + return True + except subprocess.CalledProcessError as e: + print_error(f"Error running multi-query: {e.stderr.decode()}") + +def automate_multi_query(list_file, output_csv_dir, output_csv_name, prover): + try: + aux_files = split_file(list_file, "aux") + for i, file in enumerate(aux_files): + run_multi_query(file, prover) + csv_files = get_latest_n_csvs(i+1) + concatenate_csvs(csv_files, output_csv_dir, output_csv_name) + [os.remove(file) for file in aux_files] + print_success(f"CSV file has been successfully stored in {output_csv_dir}.") + except Exception as e: + print_error(f"Error during multi-query process: {e}") if __name__ == "__main__": parser = argparse.ArgumentParser(description="Automate benchpress and convert the output to CSV.") parser.add_argument("--dir", type=str, help="The directory to benchmark.") parser.add_argument("--output-dir", type=str, help="The directory to store the CSV files.") parser.add_argument("--output-filename", type=str, default="benchpress_output", help="The name of the CSV file.") - parser.add_argument("--config", type=str, default="/home/smtml/smtml/bench/benchpress.sexp", help="The name of the CSV file.") + parser.add_argument("--config", type=str, default="/home/smtml/smtml/bench/benchpress.sexp", help="The benchpress config file.") parser.add_argument("--prover", type=str, help="The solver to be used.") parser.add_argument("--single", action="store_true", help="Run single-query mode.") parser.add_argument("--multi", action="store_true", help="Run multi-query mode.") parser.add_argument("-j", type=int, help="Number of threads to use.") parser.add_argument("-t", type=int, help="Timeout (in seconds).") + parser.add_argument("-F", type=str, help="The file with the list of benchmarks.") args = parser.parse_args() - + if args.single: automate_benchpress_single(args.dir, args.output_dir, args.output_filename, args.config, args.prover) elif args.multi: - automate_multi_query() + automate_multi_query(args.F, args.output_dir, args.output_filename, args.prover) else: print_error("Please specify --single or --multi.") \ No newline at end of file