diff options
author | Andres Noetzli <noetzli@stanford.edu> | 2019-05-20 11:24:31 -0700 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-05-20 11:24:31 -0700 |
commit | 16ade2e20b6fd2afc49b8ea70d128ae665dff409 (patch) | |
tree | cb5deee01a81c06839716056ac690949bfc0f3a3 | |
parent | 5fcb1dd18bf01a95198c4981e2d81da64f5a4848 (diff) |
[SMT-COMP 2019] Update run scripts to match tracks (#3018)
The "Application Track" has been renamed to "Incremental Track" this
year, so this commit renames the script accordingly and updates the name
of the CVC4 binary that the script calls to be just `cvc4`. The commit
also adds an initial script for the model validation track.
-rwxr-xr-x[-rw-r--r--] | contrib/run-script-smtcomp2019 | 0 | ||||
-rwxr-xr-x | contrib/run-script-smtcomp2019-incremental (renamed from contrib/run-script-smtcomp2019-application) | 2 | ||||
-rwxr-xr-x | contrib/run-script-smtcomp2019-model-validation | 25 | ||||
-rwxr-xr-x[-rw-r--r--] | contrib/run-script-smtcomp2019-unsat-cores | 0 |
4 files changed, 26 insertions, 1 deletions
diff --git a/contrib/run-script-smtcomp2019 b/contrib/run-script-smtcomp2019 index d25783453..d25783453 100644..100755 --- a/contrib/run-script-smtcomp2019 +++ b/contrib/run-script-smtcomp2019 diff --git a/contrib/run-script-smtcomp2019-application b/contrib/run-script-smtcomp2019-incremental index a7d4d985c..12c91a036 100755 --- a/contrib/run-script-smtcomp2019-application +++ b/contrib/run-script-smtcomp2019-incremental @@ -1,6 +1,6 @@ #!/bin/bash -cvc4=./cvc4-application +cvc4=./cvc4 line="" while [[ -z "$line" ]]; do diff --git a/contrib/run-script-smtcomp2019-model-validation b/contrib/run-script-smtcomp2019-model-validation new file mode 100755 index 000000000..f4b812fd6 --- /dev/null +++ b/contrib/run-script-smtcomp2019-model-validation @@ -0,0 +1,25 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_]*\) *) *$') + +# use: finishwith [params..] +# to run cvc4 and let it output whatever it will to stdout. +function finishwith { + $cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench +} + +case "$logic" in + +QF_BV) + finishwith --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cadical --bv-eq-slicer=auto --no-bv-abstraction + ;; +*) + # just run the default + finishwith + ;; + +esac + diff --git a/contrib/run-script-smtcomp2019-unsat-cores b/contrib/run-script-smtcomp2019-unsat-cores index 1454e7a8a..1454e7a8a 100644..100755 --- a/contrib/run-script-smtcomp2019-unsat-cores +++ b/contrib/run-script-smtcomp2019-unsat-cores |