Skip to content

Artifact fixes #253

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
filipeom merged 1 commit into from
Nov 24, 2024
Merged

Artifact fixes #253

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 17 additions & 5 deletions bench/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ solver usage, with notable improvements for batched solver interactions.

## Getting the Artifact

You can download the artifact through [Zenodo](https://zenodo.org/records/13959671/files/smtml_0.3.tar.gz?download=1).
You can download the artifact through [Zenodo](https://zenodo.org/records/14104822).

## Tested platforms

Expand All @@ -29,7 +29,7 @@ modification, and distribution.

## MD5 Hash of the Artifact

8edce799971395168bdf728c9a136399
46c6e43adf9bd5d9a922b3b7db307d12

## Building and Running the Docker Image

Expand Down Expand Up @@ -191,10 +191,14 @@ $ git submodule update --remote -- smt-comp/
```

2. Run the `eq1.sh` script. Note that, this script can take up multiple
hours to complete.
hours to complete. Therefore, to avoid running the entire dataset specify
a number of benchmark to run with the `-n` flag. This will run the benchmarks
quicker, but only provide an aproximation of the papers results.

```sh
$ ./eq1.sh
# Or, to just run 20 benchmarks to finish quickly
$ ./eq1.sh -n 20
```

The script will generate the results in directory `eq1`, which
Expand Down Expand Up @@ -237,10 +241,14 @@ $ git submodule update --remote -- smt-comp/
```

2. Run the `eq2.sh` script. Note that, this script can take up multiple
hours to complete.
hours to complete. Therefore, to avoid running the entire dataset specify
a number of benchmark to run with the `-n` flag. This will run the benchmarks
quicker, but only provide an aproximation of the papers results.

```sh
$ ./eq2.sh
# Or, to just run 20 benchmarks to finish quickly
$ ./eq2.sh -n 20
```

The script will generate the following files:
Expand Down Expand Up @@ -315,10 +323,14 @@ $ git submodule update --remote -- smt-testcomp23/
```

2. Run the `testcomp.sh` script. Note that, this script can take up multiple
hours to complete.
hours to complete. Therefore, to avoid running the entire dataset specify
a number of benchmark to run with the `-n` flag. This will run the benchmarks
quicker, but only provide an aproximation of the papers results.

```sh
$ ./testcomp.sh
# Or, to just run 20 benchmarks to finish quickly
$ ./testcomp.sh -n 20
```

The script will generate the following files:
Expand Down
2 changes: 1 addition & 1 deletion bench/eq1.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#!/bin/sh
#!/bin/bash

TEMPLATE=./tmp.XXXXXXXXXX

Expand Down
2 changes: 1 addition & 1 deletion bench/eq2.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@ python3 run_benchmarks.py --single --dir $QF_LIA_DIR --output-dir csvs_single --
python3 run_benchmarks.py --single --dir $QF_BV_DIR --output-dir csvs_single --output-filename QF_BV_z3 --prover smtml-z3
python3 run_benchmarks.py --single --dir $QF_BV_DIR --output-dir csvs_single --output-filename QF_BV_bitwuzla --prover smtml-bitwuzla
python3 run_benchmarks.py --single --dir $QF_BV_DIR --output-dir csvs_single --output-filename QF_BV_z3_solver --prover z3
python3 run_benchmarks.py --single --dir $QF_BV_DIR --output-dir csvs_single --output-filename QF_BV_bitwuzla --prover smtml-bitwuzla
python3 run_benchmarks.py --single --dir $QF_BV_DIR --output-dir csvs_single --output-filename QF_BV_bitwuzla_solver --prover bitwuzla
#### QF_S ####
python3 run_benchmarks.py --single --dir $QF_S_DIR --output-dir csvs_single --output-filename QF_S_z3 --prover smtml-z3
python3 run_benchmarks.py --single --dir $QF_S_DIR --output-dir csvs_single --output-filename QF_S_z3_solver --prover z3
Expand Down
6 changes: 4 additions & 2 deletions bench/eq3.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -127,6 +127,8 @@ fi

$dry_value && exit 0

mkdir csvs_multi

opam sw z3-bitwuzla
eval $(opam env)

Expand All @@ -147,7 +149,7 @@ else
python3 run_benchmarks.py --single --dir $QF_FP_DIR --output-dir csvs_single --output-filename QF_FP_bitwuzla_solver --prover bitwuzla
fi

python3 run_benchmarks.py --multi -F $QF_FP_LIST --output-dir csvs_multi --output-filename QF_FP_bitwuzla_solver --prover bitwuzla
python3 run_benchmarks.py --multi -F $QF_FP_LIST --output-dir csvs_multi --output-filename QF_FP_bitwuzla --prover smtml-bitwuzla

#### QF_LIA ####
## Z3 ##
Expand Down Expand Up @@ -176,7 +178,7 @@ else
python3 run_benchmarks.py --single --dir $QF_BV_DIR --output-dir csvs_single --output-filename QF_BV_bitwuzla_solver --prover bitwuzla
fi

python3 run_benchmarks.py --multi -F $QF_BV_LIST --output-dir csvs_multi --output-filename QF_BV_bitwuzla_solver --prover bitwuzla
python3 run_benchmarks.py --multi -F $QF_BV_LIST --output-dir csvs_multi --output-filename QF_BV_bitwuzla --prover smtml-bitwuzla

#### QF_S ####
## Z3 ##
Expand Down
8 changes: 4 additions & 4 deletions bench/run_benchmarks.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ def get_latest_sqlite_file(benchpress_data_dir):
files = [f for f in os.listdir(benchpress_data_dir) if f.endswith('.sqlite')]
if not files:
raise FileNotFoundError("No .sqlite files found in benchpress data directory.")

latest_file = max(files, key=lambda x: os.path.getmtime(os.path.join(benchpress_data_dir, x)))
return os.path.join(benchpress_data_dir, latest_file)

Expand Down Expand Up @@ -65,13 +65,13 @@ def automate_benchpress_single(directory_to_benchmark, output_csv_dir, output_cs
print_error(f"Error during SQLite to CSV process: {e}")

def get_latest_n_csvs(n):
result = subprocess.run(['ls', '-d', os.path.join('/home/smtml/smtml/bench', 'res-multi-query-*')],
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'))
csv_file = glob.glob(os.path.join(query_dir, '*.csv'))
if csv_file:
csv_files.append(csv_file[0])
return csv_files
Expand Down Expand Up @@ -135,4 +135,4 @@ def automate_multi_query(list_file, output_csv_dir, output_csv_name, prover):
elif args.multi:
automate_multi_query(args.F, args.output_dir, args.output_filename, args.prover)
else:
print_error("Please specify --single or --multi.")
print_error("Please specify --single or --multi.")
6 changes: 3 additions & 3 deletions bench/runner/multi_query.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,11 +75,11 @@ let main _hook provers from_file dirs =
let results =
List.map
(fun p ->
let ((status, stdout, _stderr, _) as result) =
let ((status, stdout, stderr, _) as result) =
Tool.fork_and_run ?from_file p dirs
in
Fmt.pr "@[<v 2>Run %a@;Exited: %a@;Stdout:@; %a@]@." Tool.pp_prover p
pp_exit_status status Fmt.string (String.escaped stdout);
Fmt.pr "@[<v 2>Run %a@;Exited: %a@;Stdout:@; %a@;Stderr:@; %a@]@." Tool.pp_prover p
pp_exit_status status Fmt.string (String.escaped stdout) Fmt.string (String.escaped stderr);
(p, result) )
provers
in
Expand Down