From 02b3aba2273232504e76e0c7d49226ef2a27977f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 22 May 2017 11:00:10 -0500 Subject: [PATCH] Initial draft of 2017 competition scripts. --- contrib/run-script-casc26-fnt | 37 +++++ contrib/run-script-casc26-fof | 51 +++++++ contrib/run-script-casc26-tfa | 41 ++++++ contrib/run-script-smtcomp2017 | 144 +++++++++++++++++++ contrib/run-script-smtcomp2017-application | 51 +++++++ contrib/run-script-sygusComp2017-CLIA | 16 +++ contrib/run-script-sygusComp2017-GENERAL | 33 +++++ contrib/run-script-sygusComp2017-INV | 16 +++ contrib/run-script-sygusComp2017-PBE_BitVec | 16 +++ contrib/run-script-sygusComp2017-PBE_Strings | 16 +++ 10 files changed, 421 insertions(+) create mode 100644 contrib/run-script-casc26-fnt create mode 100644 contrib/run-script-casc26-fof create mode 100644 contrib/run-script-casc26-tfa create mode 100644 contrib/run-script-smtcomp2017 create mode 100644 contrib/run-script-smtcomp2017-application create mode 100755 contrib/run-script-sygusComp2017-CLIA create mode 100755 contrib/run-script-sygusComp2017-GENERAL create mode 100755 contrib/run-script-sygusComp2017-INV create mode 100755 contrib/run-script-sygusComp2017-PBE_BitVec create mode 100755 contrib/run-script-sygusComp2017-PBE_Strings diff --git a/contrib/run-script-casc26-fnt b/contrib/run-script-casc26-fnt new file mode 100644 index 000000000..bc37180a6 --- /dev/null +++ b/contrib/run-script-casc26-fnt @@ -0,0 +1,37 @@ +#!/bin/bash + +here=`dirname $0` +cvc4=$here/cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-fnt casc j8 : $bench at $2..." + +# use: trywith [params..] +# to attempt a run. If an SZS ontology result is printed, then +# the run script terminates immediately. Otherwise, this +# function returns normally. +function trywith { + limit=$1; shift; + echo "--- Run $@ at $limit..."; + (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null | + (read w1 w2 w3 result w4 w5; + case "$result" in + Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; + CounterSatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi +} +function finishwith { + echo "--- Run $@..."; + $cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench +} + +# designed for 300 seconds +trywith 60 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair +trywith 30 --finite-model-find --uf-ss=no-minimal --sort-inference --uf-ss-fair +trywith 60 --finite-model-find --decision=internal --sort-inference --uf-ss-fair +finishwith --finite-model-find --mbqi=abs --sort-inference --uf-ss-fair +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-casc26-fof b/contrib/run-script-casc26-fof new file mode 100644 index 000000000..77553a5ae --- /dev/null +++ b/contrib/run-script-casc26-fof @@ -0,0 +1,51 @@ +#!/bin/bash + +# script is used for FOF division, also SLD division + +here=`dirname $0` +cvc4=$here/cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-fof casc j8 : $bench at $2..." + +# use: trywith [params..] +# to attempt a run. If an SZS ontology result is printed, then +# the run script terminates immediately. Otherwise, this +# function returns normally. +function trywith { + limit=$1; shift; + echo "--- Run $@ at $limit..."; + (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null | + (read w1 w2 w3 result w4 w5; + case "$result" in + Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; + Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi +} +function finishwith { + echo "--- Run $@..."; + $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench +} + +# designed for 300 seconds +trywith 20 --relational-triggers --full-saturate-quant +trywith 20 --no-e-matching --full-saturate-quant +trywith 15 --finite-model-find --mbqi=abs +trywith 5 --multi-trigger-when-single --full-saturate-quant +trywith 5 --trigger-sel=max --full-saturate-quant +trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant +trywith 10 --multi-trigger-cache --full-saturate-quant +trywith 5 --no-multi-trigger-linear --full-saturate-quant +trywith 15 --finite-model-find --no-quant-cf --sort-inference --uf-ss-fair +trywith 15 --prenex-quant=none --full-saturate-quant +trywith 15 --fs-inst --decision=internal --full-saturate-quant +trywith 15 --relevant-triggers --full-saturate-quant +trywith 15 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair +trywith 30 --fs-inst --full-saturate-quant +trywith 30 --no-quant-cf --full-saturate-quant +finishwith --qcf-vo-exp --full-saturate-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-casc26-tfa b/contrib/run-script-casc26-tfa new file mode 100644 index 000000000..9f6749ed6 --- /dev/null +++ b/contrib/run-script-casc26-tfa @@ -0,0 +1,41 @@ +#!/bin/bash + +here=`dirname $0` +cvc4=$here/cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-tfa casc j8 : $bench at $2..." + +# use: trywith [params..] +# to attempt a run. If an SZS ontology result is printed, then +# the run script terminates immediately. Otherwise, this +# function returns normally. +function trywith { + limit=$1; shift; + echo "--- Run $@ at $limit..."; + (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null | + (read w1 w2 w3 result w4 w5; + case "$result" in + Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; + Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi +} +function finishwith { + echo "--- Run $@..."; + $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench +} + +trywith 10 --decision=internal --full-saturate-quant +trywith 10 --finite-model-find --decision=internal +trywith 10 --nl-ext --nl-ext-tplanes --decision=internal --full-saturate-quant +trywith 10 --purify-quant --full-saturate-quant +trywith 10 --partial-triggers --full-saturate-quant +trywith 10 --no-e-matching --full-saturate-quant +trywith 30 --cbqi-all --purify-triggers --full-saturate-quant +trywith 30 --nl-ext --fs-inst --full-saturate-quant +finishwith --nl-ext --nl-ext-tplanes --full-saturate-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-smtcomp2017 b/contrib/run-script-smtcomp2017 new file mode 100644 index 000000000..bb3425d91 --- /dev/null +++ b/contrib/run-script-smtcomp2017 @@ -0,0 +1,144 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_]*\) *) *$') + +# use: trywith [params..] +# to attempt a run. Only thing printed on stdout is "sat" or "unsat", in +# which case this run script terminates immediately. Otherwise, this +# function returns normally. +function trywith { + limit=$1; shift; + result="$(ulimit -S -t "$limit";$cvc4 -L smt2 --no-incremental --no-checking --no-interactive "$@" $bench)" + case "$result" in + sat|unsat) echo "$result"; exit 0;; + esac +} + +# use: finishwith [params..] +# to run cvc4 and let it output whatever it will to stdout. +function finishwith { + $cvc4 -L smt2 --no-incremental --no-checking --no-interactive "$@" $bench +} + +case "$logic" in + +QF_LRA) + trywith 200 --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi + finishwith --no-restrict-pivots --use-soi --new-prop --unconstrained-simp + ;; +QF_LIA) + # same as QF_LRA but add --pb-rewrites + finishwith --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites + ;; +QF_NIA) + trywith 300 --nl-ext --nl-ext-tplanes --decision=internal + trywith 1800 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cryptominisat + trywith 1800 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cryptominisat + trywith 1800 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cryptominisat + trywith 1800 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cryptominisat + finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat + ;; +QF_NRA) + trywith 300 --nl-ext --nl-ext-tplanes + ;; +ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA) + # the following is designed for a run time of 2400s (40 min). + # initial runs 1min + trywith 20 --simplification=none --full-saturate-quant + trywith 20 --no-e-matching --full-saturate-quant + trywith 20 --fs-inst --decision=internal --full-saturate-quant + # trigger selections 4min + trywith 30 --relevant-triggers --full-saturate-quant + trywith 30 --trigger-sel=max --full-saturate-quant + trywith 30 --trigger-sel=min-s-max --full-saturate-quant + trywith 30 --multi-trigger-when-single --full-saturate-quant + trywith 30 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant + trywith 30 --multi-trigger-cache --full-saturate-quant + trywith 30 --no-multi-trigger-linear --full-saturate-quant + trywith 30 --literal-match=agg --full-saturate-quant + # other 3min + trywith 30 --pre-skolem-quant --full-saturate-quant + trywith 30 --inst-when=full --full-saturate-quant + trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant + trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant + trywith 60 --nl-ext --full-saturate-quant + # finite model find 2min + trywith 30 --finite-model-find --mbqi=none + trywith 30 --finite-model-find + trywith 30 --finite-model-find --uf-ss=no-minimal + trywith 60 --finite-model-find --decision=internal + # long runs 20min + trywith 300 --decision=internal --full-saturate-quant + trywith 300 --term-db-mode=relevant --full-saturate-quant + trywith 300 --fs-inst --full-saturate-quant + trywith 300 --finite-model-find --fmf-inst-engine + # finite model find 1min + trywith 30 --finite-model-find --fmf-bound-int + trywith 30 --finite-model-find --sort-inference + # finish 9min + finishwith --full-saturate-quant + ;; +UFBV) + # many problems in UFBV are essentially BV + trywith 300 --full-saturate-quant + trywith 300 --finite-model-find + finishwith --cbqi-all --full-saturate-quant + ;; +BV) + trywith 300 --finite-model-find + finishwith --cbqi-all --full-saturate-quant + ;; +LIA|LRA|NIA|NRA) + trywith 30 --full-saturate-quant + trywith 300 --full-saturate-quant --cbqi-min-bounds + trywith 300 --full-saturate-quant --decision=internal + trywith 1800 --full-saturate-quant --cbqi-nested-qe + finishwith --full-saturate-quant --cbqi-midpoint + ;; +QF_AUFBV) + trywith 600 + finishwith --decision=justification-stoponly + ;; +QF_ABV) + trywith 50 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv + trywith 500 --arrays-weak-equiv + finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv + ;; +QF_UFBV) + finishwith --bitblast=eager --bv-sat-solver=cryptominisat + ;; +QF_BV) + exec ./pcvc4 -L smt2 --no-incremental --no-checking --no-interactive --thread-stack=1024 \ + --threads 2 \ + --thread0 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cryptominisat --bitblast-aig --no-bv-abstraction' \ + --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto --no-bv-abstraction' \ + --no-wait-to-join \ + "$bench" + #trywith 10 --bv-eq-slicer=auto --decision=justification + #trywith 60 --decision=justification + #trywith 600 --decision=internal --bitblast-eager + #finishwith --decision=justification --decision-use-weight --decision-weight-internal=usr1 + ;; +QF_AUFLIA) + finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification + ;; +QF_AX) + finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=internal + ;; +QF_AUFNIA) + finishwith --decision=justification --no-arrays-eager-index --arrays-eager-lemmas + ;; +QF_ALIA) + trywith 70 --decision=justification --arrays-weak-equiv + finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas + ;; +*) + # just run the default + finishwith + ;; + +esac + diff --git a/contrib/run-script-smtcomp2017-application b/contrib/run-script-smtcomp2017-application new file mode 100644 index 000000000..528a5deab --- /dev/null +++ b/contrib/run-script-smtcomp2017-application @@ -0,0 +1,51 @@ +#!/bin/bash + +cvc4=./cvc4-application + +read line +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 +read line +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 --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 --nl-ext --tear-down-incremental=1 + ;; +LIA|LRA) + runcvc4 --incremental --cbqi + ;; +QF_AUFLIA) + runcvc4 --no-arrays-eager-index --arrays-eager-lemmas --incremental + ;; +QF_BV) + runcvc4 --tear-down-incremental=4 --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2 + ;; +QF_LIA) + runcvc4 --tear-down-incremental=1 --unconstrained-simp + ;; +*) + # just run the default + runcvc4 --incremental + ;; + +esac diff --git a/contrib/run-script-sygusComp2017-CLIA b/contrib/run-script-sygusComp2017-CLIA new file mode 100755 index 000000000..3dc08d8c0 --- /dev/null +++ b/contrib/run-script-sygusComp2017-CLIA @@ -0,0 +1,16 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function trywith { + ($cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench) 2>/dev/null | + (read result w1; + case "$result" in + unsat) echo "$w1";cat;exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi +} + +trywith --decision=internal --cbqi-prereg-inst + diff --git a/contrib/run-script-sygusComp2017-GENERAL b/contrib/run-script-sygusComp2017-GENERAL new file mode 100755 index 000000000..0ee133ea8 --- /dev/null +++ b/contrib/run-script-sygusComp2017-GENERAL @@ -0,0 +1,33 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function runl { + limit=$1; shift; + ulimit -S -t "$limit";$cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench +} + +function trywith { + sol=$(runl $@) + status=$? + if [ $status -ne 134 ]; then + echo $sol | + (read result w1; + case "$result" in + unsat) echo "$w1";cat;exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi + fi +} + +function finishwith { + $cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench 2>/dev/null | + (read result w1; + case "$result" in + unsat) echo "$w1";cat;exit 0;; + esac) +} + +trywith 120 --cegqi-si=all-abort --cegqi-si-abort --decision=internal --cbqi-prereg-inst +finishwith --cegqi-si=none diff --git a/contrib/run-script-sygusComp2017-INV b/contrib/run-script-sygusComp2017-INV new file mode 100755 index 000000000..a25a5f5c8 --- /dev/null +++ b/contrib/run-script-sygusComp2017-INV @@ -0,0 +1,16 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function trywith { + ($cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench) 2>/dev/null | + (read result w1; + case "$result" in + unsat) echo "$w1";cat;exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi +} + +trywith --sygus-inv-templ=post + diff --git a/contrib/run-script-sygusComp2017-PBE_BitVec b/contrib/run-script-sygusComp2017-PBE_BitVec new file mode 100755 index 000000000..19d8fd891 --- /dev/null +++ b/contrib/run-script-sygusComp2017-PBE_BitVec @@ -0,0 +1,16 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function trywith { + ($cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench) 2>/dev/null | + (read result w1; + case "$result" in + unsat) echo "$w1";cat;exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi +} + +trywith --cegqi-si=none + diff --git a/contrib/run-script-sygusComp2017-PBE_Strings b/contrib/run-script-sygusComp2017-PBE_Strings new file mode 100755 index 000000000..0a845bd78 --- /dev/null +++ b/contrib/run-script-sygusComp2017-PBE_Strings @@ -0,0 +1,16 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function trywith { + ($cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench) 2>/dev/null | + (read result w1; + case "$result" in + unsat) echo "$w1";cat;exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi +} + +trywith --cegqi-si=none --strings-exp + -- 2.30.2