From c9e25618c1b0edc7c2350b507295b9dcfc0e683d Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 20 May 2019 11:07:09 -0700 Subject: [SMT-COMP 2019] Update run scripts to match tracks 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. --- contrib/run-script-smtcomp2019 | 0 contrib/run-script-smtcomp2019-application | 84 ------------------------- contrib/run-script-smtcomp2019-incremental | 84 +++++++++++++++++++++++++ contrib/run-script-smtcomp2019-model-validation | 25 ++++++++ contrib/run-script-smtcomp2019-unsat-cores | 0 5 files changed, 109 insertions(+), 84 deletions(-) mode change 100644 => 100755 contrib/run-script-smtcomp2019 delete mode 100755 contrib/run-script-smtcomp2019-application create mode 100755 contrib/run-script-smtcomp2019-incremental create mode 100755 contrib/run-script-smtcomp2019-model-validation mode change 100644 => 100755 contrib/run-script-smtcomp2019-unsat-cores diff --git a/contrib/run-script-smtcomp2019 b/contrib/run-script-smtcomp2019 old mode 100644 new mode 100755 diff --git a/contrib/run-script-smtcomp2019-application b/contrib/run-script-smtcomp2019-application deleted file mode 100755 index a7d4d985c..000000000 --- a/contrib/run-script-smtcomp2019-application +++ /dev/null @@ -1,84 +0,0 @@ -#!/bin/bash - -cvc4=./cvc4-application - -line="" -while [[ -z "$line" ]]; do - read line -done -if [ "$line" != '(set-option :print-success true)' ]; then - echo 'ERROR: first line supposed to be set-option :print-success, but got: "'"$line"'"' >&2 - exit 1 -fi -echo success -line="" -while [[ -z "$line" ]]; do - read line -done -logic=$(expr "$line" : ' *(set-logic *\([A-Z_]*\) *) *$') -if [ -z "$logic" ]; then - echo 'ERROR: second line supposed to be set-logic, but got: "'"$line"'"' >&2 - exit 1 -fi -echo success - -function runcvc4 { - # we run in this way for line-buffered input, otherwise memory's a - # concern (plus it mimics what we'll end up getting from an - # application-track trace runner?) - $cvc4 --force-logic="$logic" -L smt2.6 --print-success --no-checking --no-interactive "$@" <&0- -} - -case "$logic" in - -ALIA|QF_ALIA|QF_LRA|QF_UFLIA|QF_UFLRA|UFLRA) - runcvc4 --incremental - ;; -ANIA|QF_ANIA|QF_NIA|QF_UFNIA|QF_NRA) - runcvc4 --tear-down-incremental=1 - ;; -LIA|LRA) - runcvc4 --incremental - ;; -QF_AUFLIA) - runcvc4 --no-arrays-eager-index --arrays-eager-lemmas --incremental - ;; -QF_BV) - runcvc4 --incremental --bitblast=eager --bv-sat-solver=cadical - ;; -QF_LIA) - runcvc4 --tear-down-incremental=1 --unconstrained-simp - ;; -QF_UFBV) - runcvc4 --incremental - ;; -QF_UF) - runcvc4 --incremental - ;; -QF_AUFBV) - runcvc4 --incremental - ;; -QF_ABV) - runcvc4 --incremental - ;; -ABVFP) - runcvc4 --incremental - ;; -BVFP) - runcvc4 --incremental - ;; -QF_ABVFP) - runcvc4 --incremental - ;; -QF_BVFP) - runcvc4 --incremental - ;; -QF_FP) - runcvc4 --incremental - ;; -*) - # just run the default - runcvc4 --incremental - ;; - -esac diff --git a/contrib/run-script-smtcomp2019-incremental b/contrib/run-script-smtcomp2019-incremental new file mode 100755 index 000000000..12c91a036 --- /dev/null +++ b/contrib/run-script-smtcomp2019-incremental @@ -0,0 +1,84 @@ +#!/bin/bash + +cvc4=./cvc4 + +line="" +while [[ -z "$line" ]]; do + read line +done +if [ "$line" != '(set-option :print-success true)' ]; then + echo 'ERROR: first line supposed to be set-option :print-success, but got: "'"$line"'"' >&2 + exit 1 +fi +echo success +line="" +while [[ -z "$line" ]]; do + read line +done +logic=$(expr "$line" : ' *(set-logic *\([A-Z_]*\) *) *$') +if [ -z "$logic" ]; then + echo 'ERROR: second line supposed to be set-logic, but got: "'"$line"'"' >&2 + exit 1 +fi +echo success + +function runcvc4 { + # we run in this way for line-buffered input, otherwise memory's a + # concern (plus it mimics what we'll end up getting from an + # application-track trace runner?) + $cvc4 --force-logic="$logic" -L smt2.6 --print-success --no-checking --no-interactive "$@" <&0- +} + +case "$logic" in + +ALIA|QF_ALIA|QF_LRA|QF_UFLIA|QF_UFLRA|UFLRA) + runcvc4 --incremental + ;; +ANIA|QF_ANIA|QF_NIA|QF_UFNIA|QF_NRA) + runcvc4 --tear-down-incremental=1 + ;; +LIA|LRA) + runcvc4 --incremental + ;; +QF_AUFLIA) + runcvc4 --no-arrays-eager-index --arrays-eager-lemmas --incremental + ;; +QF_BV) + runcvc4 --incremental --bitblast=eager --bv-sat-solver=cadical + ;; +QF_LIA) + runcvc4 --tear-down-incremental=1 --unconstrained-simp + ;; +QF_UFBV) + runcvc4 --incremental + ;; +QF_UF) + runcvc4 --incremental + ;; +QF_AUFBV) + runcvc4 --incremental + ;; +QF_ABV) + runcvc4 --incremental + ;; +ABVFP) + runcvc4 --incremental + ;; +BVFP) + runcvc4 --incremental + ;; +QF_ABVFP) + runcvc4 --incremental + ;; +QF_BVFP) + runcvc4 --incremental + ;; +QF_FP) + runcvc4 --incremental + ;; +*) + # just run the default + runcvc4 --incremental + ;; + +esac 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 old mode 100644 new mode 100755 -- cgit v1.2.3