-
Notifications
You must be signed in to change notification settings - Fork 8
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Allow specifying number of benchmarks in eval scripts
Due to the large cpu usage of the evaluation scripts we introduce a `-n` flag that allows specifying the number of benchmarks to use in each evaluation script. Thereby reducing the cpu usage of each script and producing an approximation of the real results
- Loading branch information
Showing
4 changed files
with
453 additions
and
66 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,31 +1,118 @@ | ||
| #!/bin/sh | ||
|
|
||
| TEMPLATE=./tmp.XXXXXXXXXX | ||
|
|
||
| show_help() { | ||
| echo "Usage: $0 [-n VALUE] [--help]" | ||
| echo | ||
| echo "Options:" | ||
| echo " -n VALUE Number of benchmarks to run." | ||
| echo " --help Show this help message and exit." | ||
| exit 0 | ||
| } | ||
|
|
||
| sample_benchmarks() { | ||
| src=$1 | ||
| dst=$2 | ||
| n=$3 | ||
|
|
||
| echo "Sampling '$n' benchmarks from '$src' to '$dst'" | ||
| files=$(find $src -type f -name "*.smt2" | shuf -n $n) | ||
| for file in $files; do | ||
| cp $file $dst | ||
| done | ||
|
|
||
| return 0 | ||
| } | ||
|
|
||
| QF_BV_DIR=./smt-comp/smtlib/non-incremental/QF_BV | ||
| QF_FP_DIR=./smt-comp/smtlib/non-incremental/QF_FP | ||
| QF_LIA_DIR=./smt-comp/smtlib/non-incremental/QF_LIA | ||
| QF_SLIA_DIR=./smt-comp/smtlib/non-incremental/QF_SLIA | ||
| QF_S_DIR=./smt-comp/smtlib/non-incremental/QF_S | ||
|
|
||
| n_value="" | ||
| dry_value=false | ||
|
|
||
| while [[ $# -gt 0 ]]; do | ||
| case $1 in | ||
| -n) | ||
| shift | ||
| if [[ -z "$1" || "$1" == -* ]]; then | ||
| echo "Error: Missing value for -n option." | ||
| exit 1 | ||
| fi | ||
| n_value=$1 | ||
| shift | ||
| ;; | ||
| --dry) | ||
| dry_value=true | ||
| shift | ||
| ;; | ||
| --help) | ||
| show_help | ||
| ;; | ||
| *) | ||
| echo "Error: Unknown argument: $1" | ||
| show_help | ||
| ;; | ||
| esac | ||
| done | ||
|
|
||
| if [[ -n "$n_value" ]]; then | ||
| echo "Sampling $n_value benchmarks ..." | ||
| qf_bv=$(mktemp -d "$TEMPLATE") | ||
| sample_benchmarks "$QF_BV_DIR" "$qf_bv" "$n_value" | ||
| QF_BV_DIR="$qf_bv" | ||
|
|
||
| qf_fp=$(mktemp -d "$TEMPLATE") | ||
| sample_benchmarks "$QF_FP_DIR" "$qf_fp" "$n_value" | ||
| QF_FP_DIR="$qf_fp" | ||
|
|
||
| qf_lia=$(mktemp -d "$TEMPLATE") | ||
| sample_benchmarks "$QF_LIA_DIR" "$qf_lia" "$n_value" | ||
| QF_LIA_DIR="$qf_lia" | ||
|
|
||
| qf_slia=$(mktemp -d "$TEMPLATE") | ||
| sample_benchmarks "$QF_SLIA_DIR" "$qf_slia" "$n_value" | ||
| QF_SLIA_DIR="$qf_slia" | ||
|
|
||
| qf_s=$(mktemp -d "$TEMPLATE") | ||
| sample_benchmarks "$QF_S_DIR" "$qf_s" "$n_value" | ||
| QF_S_DIR="$qf_s" | ||
| fi | ||
|
|
||
| $dry_value && exit 0 | ||
|
|
||
| mkdir eq1 | ||
|
|
||
| opam sw z3-bitwuzla | ||
| eval $(opam env) | ||
|
|
||
| mkdir eq1/z3-bitwuzla | ||
| benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_BV -p z3 -p smtml-z3 -p bitwuzla -p smtml-bitwuzla > eq1/z3-bitwuzla/qf_bv.out | ||
| benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_FP -p z3 -p smtml-z3 -p bitwuzla -p smtml-bitwuzla > eq1/z3-bitwuzla/qf_fp.out | ||
| benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_LIA -p z3 -p smtml-z3 > eq1/z3-bitwuzla/qf_lia.out | ||
| benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_SLIA -p z3 -p smtml-z3 > eq1/z3-bitwuzla/qf_slia.out | ||
| benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_S -p z3 -p smtml-z3 > eq1/z3-bitwuzla/qf_s.out | ||
| echo "Running Z3 and bitwuzla ..." | ||
| benchpress run -c benchpress.sexp --task eq1 $QF_BV_DIR -p z3 -p smtml-z3 -p bitwuzla -p smtml-bitwuzla > eq1/z3-bitwuzla/qf_bv.out | ||
| benchpress run -c benchpress.sexp --task eq1 $QF_FP_DIR -p z3 -p smtml-z3 -p bitwuzla -p smtml-bitwuzla > eq1/z3-bitwuzla/qf_fp.out | ||
| benchpress run -c benchpress.sexp --task eq1 $QF_LIA_DIR -p z3 -p smtml-z3 > eq1/z3-bitwuzla/qf_lia.out | ||
| benchpress run -c benchpress.sexp --task eq1 $QF_SLIA_DIR -p z3 -p smtml-z3 > eq1/z3-bitwuzla/qf_slia.out | ||
| benchpress run -c benchpress.sexp --task eq1 $QF_S_DIR -p z3 -p smtml-z3 > eq1/z3-bitwuzla/qf_s.out | ||
|
|
||
| opam sw cvc5 | ||
| eval $(opam env) | ||
|
|
||
| mkdir eq1/cvc5 | ||
| benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_BV -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_bv.out | ||
| benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_FP -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_fp.out | ||
| benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_LIA -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_lia.out | ||
| benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_SLIA -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_slia.out | ||
| benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_S -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_s.out | ||
| echo "Running cvc5 ..." | ||
| benchpress run -c benchpress.sexp --task eq1 $QF_BV_DIR -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_bv.out | ||
| benchpress run -c benchpress.sexp --task eq1 $QF_FP_DIR -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_fp.out | ||
| benchpress run -c benchpress.sexp --task eq1 $QF_LIA_DIR -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_lia.out | ||
| benchpress run -c benchpress.sexp --task eq1 $QF_SLIA_DIR -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_slia.out | ||
| benchpress run -c benchpress.sexp --task eq1 $QF_S_DIR -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_s.out | ||
|
|
||
| opam sw colibri2 | ||
| eval $(opam env) | ||
|
|
||
| mkdir eq1/colibri2 | ||
| benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_BV -p colibri2 -p smtml-colibri2 > eq1/colibri2/qf_bv.out | ||
| benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_FP -p colibri2 -p smtml-colibri2 > eq1/colibri2/qf_fp.out | ||
| benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_LIA -p colibri2 -p smtml-colibri2 > eq1/colibri2/qf_lia.out | ||
| echo "Running Colibri2 ..." | ||
| benchpress run -c benchpress.sexp --task eq1 $QF_BV_DIR -p colibri2 -p smtml-colibri2 > eq1/colibri2/qf_bv.out | ||
| benchpress run -c benchpress.sexp --task eq1 $QF_FP_DIR -p colibri2 -p smtml-colibri2 > eq1/colibri2/qf_fp.out | ||
| benchpress run -c benchpress.sexp --task eq1 $QF_LIA_DIR -p colibri2 -p smtml-colibri2 > eq1/colibri2/qf_lia.out |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.