Skip to content

Commit

Permalink
Add scripts for EQ3
Browse files Browse the repository at this point in the history
  • Loading branch information
@joaomhmpereira @filipeom
joaomhmpereira authored and filipeom committed Oct 24, 2024
1 parent 76990a4 commit 9f6821a
Show file tree
Hide file tree
Showing 3 changed files with 182 additions and 25 deletions.
55 changes: 35 additions & 20 deletions bench/eq2.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 ####
Expand Down
90 changes: 90 additions & 0 deletions bench/eq3.sh
View file
Original file line number Diff line number Diff line change
@@ -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
62 changes: 57 additions & 5 deletions bench/run_benchmarks.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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")
Expand Down Expand Up @@ -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.")

0 comments on commit 9f6821a

Please sign in to comment.