diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-08 15:16:41 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-08 15:16:41 -0500 |
commit | a56575f413499d256e81f6ca1a64ffe1413ed3c7 (patch) | |
tree | 03ea560fb5b45eb0877e1df4bdfe410ea9de79dd /contrib/competitions | |
parent | 63a6e17196d849ad6e57bce7490eafb5b7f7f3ec (diff) |
Add subdirectories to contrib for competition scripts (#3164)
Diffstat (limited to 'contrib/competitions')
70 files changed, 3341 insertions, 0 deletions
diff --git a/contrib/competitions/casc/run-script-casc24-fnt b/contrib/competitions/casc/run-script-casc24-fnt new file mode 100755 index 000000000..b10d7324a --- /dev/null +++ b/contrib/competitions/casc/run-script-casc24-fnt @@ -0,0 +1,38 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" +let "to = $2 - 60" + +file=${bench##*/} +filename=${file%.*} + +# 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; + (ulimit -t "$limit";$cvc4 -L tptp --szs-compliant --no-checking --no-interactive --dump-models --produce-models "$@" $bench) 2>/dev/null | + (read result; + case "$result" in + sat) echo "% SZS status" "Satisfiable for $filename"; + echo "% SZS output" "start FiniteModel for $filename"; + cat; + echo "% SZS output" "end FiniteModel for $filename"; + exit 0;; + unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;; + conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename"; + echo "% SZS output" "start FiniteModel for $filename"; + cat; + echo "% SZS output" "end FiniteModel for $filename"; + exit 0;; + conjecture-unsat) echo "% SZS status" "Theorem for $filename"; exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi +} + +trywith 30 --finite-model-find --uf-ss-totality +trywith 30 --finite-model-find --decision=justification --fmf-fmc +trywith $to --finite-model-find --decision=justification +echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-casc24-fnt-no-models b/contrib/competitions/casc/run-script-casc24-fnt-no-models new file mode 100755 index 000000000..3b4d5e320 --- /dev/null +++ b/contrib/competitions/casc/run-script-casc24-fnt-no-models @@ -0,0 +1,36 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" +let "to = $2 - 60" + +file=${bench##*/} +filename=${file%.*} + +# 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 { + result="$( ulimit -t "$1";shift;$cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)" + case "$result" in + sat) echo "% SZS status" "Satisfiable for $filename"; exit 0;; + unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;; + conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename"; exit 0;; + conjecture-unsat) echo "% SZS status" "Theorem for $filename"; exit 0;; + esac +} +function finishwith { + result="$( $cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)" + case "$result" in + sat) echo "% SZS status" "Satisfiable for $filename"; exit 0;; + unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;; + conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename"; exit 0;; + conjecture-unsat) echo "% SZS status" "Theorem for $filename"; exit 0;; + esac +} + +trywith 30 --finite-model-find --uf-ss-totality +trywith 30 --finite-model-find --decision=justification --fmf-fmc +trywith $to --finite-model-find --decision=justification +echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-casc24-fof b/contrib/competitions/casc/run-script-casc24-fof new file mode 100755 index 000000000..b3ede0dfa --- /dev/null +++ b/contrib/competitions/casc/run-script-casc24-fof @@ -0,0 +1,37 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" +let "to = $2 - 75" + +file=${bench##*/} +filename=${file%.*} + +# 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 { + result="$( ulimit -t "$1";shift;$cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)" + case "$result" in + sat) echo "% SZS status" "Satisfiable for $filename"; exit 0;; + unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;; + conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename"; exit 0;; + conjecture-unsat) echo "% SZS status" "Theorem for $filename"; exit 0;; + esac +} +function finishwith { + result="$( $cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)" + case "$result" in + sat) echo "% SZS status" "Satisfiable for $filename"; exit 0;; + unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;; + conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename"; exit 0;; + conjecture-unsat) echo "% SZS status" "Theorem for $filename"; exit 0;; + esac +} + +trywith 30 +trywith 15 --finite-model-find --fmf-inst-engine +trywith 30 --finite-model-find --decision=justification --fmf-fmc +trywith $to --decision=justification +echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-casc25-fnt b/contrib/competitions/casc/run-script-casc25-fnt new file mode 100755 index 000000000..7f007186c --- /dev/null +++ b/contrib/competitions/casc/run-script-casc25-fnt @@ -0,0 +1,38 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-fnt casc 25 : $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 30 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair --mbqi=gen-ev +trywith 20 --finite-model-find --uf-ss=no-minimal --sort-inference --uf-ss-fair +trywith 20 --finite-model-find --decision=internal --sort-inference --uf-ss-fair +trywith 20 --finite-model-find --uf-ss-totality --sort-inference --uf-ss-fair --mbqi=gen-ev +trywith 60 --finite-model-find --quant-cf --sort-inference --uf-ss-fair --mbqi=abs +finishwith --finite-model-find --sort-inference --uf-ss-fair --mbqi=abs +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-casc25-fof b/contrib/competitions/casc/run-script-casc25-fof new file mode 100755 index 000000000..26c544062 --- /dev/null +++ b/contrib/competitions/casc/run-script-casc25-fof @@ -0,0 +1,46 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-fof casc 25 : $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 15 --relevant-triggers --clause-split --full-saturate-quant +trywith 15 --clause-split --no-e-matching --full-saturate-quant +trywith 15 --finite-model-find --quant-cf --qcf-all-conflict --sort-inference --uf-ss-fair +trywith 5 --trigger-sel=max --full-saturate-quant +trywith 5 --relevant-triggers --clause-split --multi-trigger-when-single --full-saturate-quant +trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant +trywith 5 --pre-skolem-quant --no-pre-skolem-quant-nested --full-saturate-quant +trywith 15 --relevant-triggers --decision=internal --full-saturate-quant +trywith 15 --clause-split --no-quant-cf --full-saturate-quant +trywith 15 --clause-split --trigger-sel=min --full-saturate-quant +trywith 30 --prenex-quant=none --full-saturate-quant +trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant +trywith 30 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair --mbqi=gen-ev +finishwith --term-db-mode=relevant --full-saturate-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-casc25-tfa b/contrib/competitions/casc/run-script-casc25-tfa new file mode 100755 index 000000000..40ed76df5 --- /dev/null +++ b/contrib/competitions/casc/run-script-casc25-tfa @@ -0,0 +1,41 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-tfa casc 25 : $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 --cbqi2 --decision=internal --full-saturate-quant +trywith 10 --relevant-triggers --full-saturate-quant --partial-triggers --purify-triggers +trywith 10 --cbqi --full-saturate-quant +trywith 10 --cbqi2 --e-matching --partial-triggers --purify-triggers +trywith 30 --qcf-tconstraint --full-saturate-quant +trywith 60 --cbqi --cbqi-recurse --full-saturate-quant +trywith 10 --full-saturate-quant --partial-triggers --purify-triggers +trywith 10 --no-e-matching --full-saturate-quant +trywith 10 --fmf-bound-int +finishwith --cbqi2 --cbqi-recurse --full-saturate-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-casc25-tfn b/contrib/competitions/casc/run-script-casc25-tfn new file mode 100755 index 000000000..6888d7b49 --- /dev/null +++ b/contrib/competitions/casc/run-script-casc25-tfn @@ -0,0 +1,36 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-tfn casc 25 : $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 -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" "$@" $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 --force-logic="UFNIRA" "$@" $bench +} + +trywith 30 --cbqi2 --decision=internal --full-saturate-quant +trywith 30 --cbqi --full-saturate-quant +trywith 60 --cbqi --cbqi-recurse --full-saturate-quant +trywith 60 --fmf-bound-int --macros-quant +finishwith --cbqi2 --cbqi-recurse --full-saturate-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-casc26-fnt b/contrib/competitions/casc/run-script-casc26-fnt new file mode 100644 index 000000000..c89d3eb0a --- /dev/null +++ b/contrib/competitions/casc/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 26 : $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 --macros-quant --macros-quant-mode=all --sort-inference --uf-ss-fair +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-casc26-fof b/contrib/competitions/casc/run-script-casc26-fof new file mode 100644 index 000000000..5ec312cb7 --- /dev/null +++ b/contrib/competitions/casc/run-script-casc26-fof @@ -0,0 +1,50 @@ +#!/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 26 : $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 --uf-ss=no-minimal +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 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 --decision=internal --full-saturate-quant +trywith 30 --qcf-vo-exp --full-saturate-quant +trywith 30 --no-quant-cf --full-saturate-quant +finishwith --macros-quant --macros-quant-mode=all --full-saturate-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-casc26-tfa b/contrib/competitions/casc/run-script-casc26-tfa new file mode 100644 index 000000000..74147e529 --- /dev/null +++ b/contrib/competitions/casc/run-script-casc26-tfa @@ -0,0 +1,37 @@ +#!/bin/bash + +here=`dirname $0` +cvc4=$here/cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-tfa casc 26 : $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 15 --finite-model-find --decision=internal +trywith 15 --multi-trigger-when-single --multi-trigger-priority --nl-ext-tplanes --full-saturate-quant +trywith 15 --no-e-matching --full-saturate-quant +trywith 15 --cbqi-all --purify-triggers --full-saturate-quant +finishwith --macros-quant --macros-quant-mode=all --nl-ext-tplanes --full-saturate-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-casc27-fnt b/contrib/competitions/casc/run-script-casc27-fnt new file mode 100755 index 000000000..301b03a2b --- /dev/null +++ b/contrib/competitions/casc/run-script-casc27-fnt @@ -0,0 +1,35 @@ +#!/bin/bash + +here=`dirname $0` +cvc4=$here/cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-fnt casc 27 : $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 30 --finite-model-find --uf-ss=no-minimal --sort-inference +finishwith --finite-model-find --macros-quant --macros-quant-mode=all --sort-inference +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-casc27-fof b/contrib/competitions/casc/run-script-casc27-fof new file mode 100755 index 000000000..c95266367 --- /dev/null +++ b/contrib/competitions/casc/run-script-casc27-fof @@ -0,0 +1,50 @@ +#!/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 27 : $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 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant +trywith 20 --no-e-matching --full-saturate-quant +trywith 15 --finite-model-find --uf-ss=no-minimal +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 15 --prenex-quant=none --full-saturate-quant +trywith 15 --fs-interleave --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 --pre-skolem-quant --full-saturate-quant +trywith 30 --qcf-vo-exp --full-saturate-quant +trywith 30 --no-quant-cf --full-saturate-quant +finishwith --macros-quant --macros-quant-mode=all --full-saturate-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-casc27-tfa b/contrib/competitions/casc/run-script-casc27-tfa new file mode 100755 index 000000000..ec4c76685 --- /dev/null +++ b/contrib/competitions/casc/run-script-casc27-tfa @@ -0,0 +1,37 @@ +#!/bin/bash + +here=`dirname $0` +cvc4=$here/cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-tfa casc 27 : $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 15 --finite-model-find --decision=internal +trywith 15 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant +trywith 15 --no-e-matching --full-saturate-quant +trywith 15 --cbqi-all --purify-triggers --full-saturate-quant +finishwith --macros-quant --macros-quant-mode=all --nl-ext-tplanes --full-saturate-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-casc27-thf b/contrib/competitions/casc/run-script-casc27-thf new file mode 100755 index 000000000..5db5527ed --- /dev/null +++ b/contrib/competitions/casc/run-script-casc27-thf @@ -0,0 +1,44 @@ +#!/bin/bash + +# script is used for THF division + +here=`dirname $0` +cvc4=$here/cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-thf casc 27 : $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 --uf-ho --ho-elim --no-ho-elim-store-ax --full-saturate-quant +trywith 20 --uf-ho --ho-elim --full-saturate-quant +trywith 5 --uf-ho --ho-elim --finite-model-find --uf-ss=no-minimal +trywith 5 --uf-ho --no-ho-matching --finite-model-find --uf-ss=no-minimal +trywith 30 --uf-ho --no-ho-matching --full-saturate-quant --fs-interleave --ho-elim-store-ax +trywith 20 --uf-ho --no-ho-matching --full-saturate-quant --macros-quant-mode=all +trywith 30 --uf-ho --ho-elim --full-saturate-quant --fs-interleave +trywith 30 --uf-ho --no-ho-matching --full-saturate-quant --ho-elim-store-ax +finishwith --uf-ho --ho-elim --no-ho-elim-store-ax --full-saturate-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-cascj7-fnt b/contrib/competitions/casc/run-script-cascj7-fnt new file mode 100755 index 000000000..e3ad1a2ff --- /dev/null +++ b/contrib/competitions/casc/run-script-cascj7-fnt @@ -0,0 +1,36 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-fnt casc j7 : $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 +} + +trywith 30 --finite-model-find --sort-inference --uf-ss-fair +trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality --decision=internal --sort-inference --uf-ss-fair +trywith 15 --finite-model-find --disable-uf-ss-min-model --sort-inference --uf-ss-fair +trywith 60 --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair +finishwith --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair --mbqi-one-inst-per-round +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-cascj7-fof b/contrib/competitions/casc/run-script-cascj7-fof new file mode 100755 index 000000000..fb2ca33eb --- /dev/null +++ b/contrib/competitions/casc/run-script-cascj7-fof @@ -0,0 +1,38 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-fof casc j7 : $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 +} + +trywith 15 --quant-cf --pre-skolem-quant --full-saturate-quant +trywith 30 --full-saturate-quant +trywith 30 --finite-model-find --fmf-inst-engine --mbqi=gen-ev +trywith 30 --relevant-triggers --full-saturate-quant +trywith 15 --finite-model-find --decision=justification-stoponly +trywith 30 --pre-skolem-quant --full-saturate-quant +finishwith --quant-cf --full-saturate-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-cascj7-tff b/contrib/competitions/casc/run-script-cascj7-tff new file mode 100755 index 000000000..11350cd7e --- /dev/null +++ b/contrib/competitions/casc/run-script-cascj7-tff @@ -0,0 +1,38 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-tff casc j7 : $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 -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive "$@" $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 "$@" $bench +} + +trywith 15 --cbqi-recurse --full-saturate-quant +trywith 15 --decision=internal --full-saturate-quant +trywith 30 --quant-cf --qcf-tconstraint --full-saturate-quant +trywith 20 --finite-model-find +trywith 30 --fmf-bound-int +trywith 60 --quant-cf --full-saturate-quant +finishwith --cbqi-recurse --full-saturate-quant --pre-skolem-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-cascj8-fnt b/contrib/competitions/casc/run-script-cascj8-fnt new file mode 100755 index 000000000..bc37180a6 --- /dev/null +++ b/contrib/competitions/casc/run-script-cascj8-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/competitions/casc/run-script-cascj8-fof b/contrib/competitions/casc/run-script-cascj8-fof new file mode 100755 index 000000000..fe18c3ed0 --- /dev/null +++ b/contrib/competitions/casc/run-script-cascj8-fof @@ -0,0 +1,48 @@ +#!/bin/bash + +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 --finite-model-find --uf-ss=no-minimal --sort-inference --uf-ss-fair +trywith 10 --term-db-mode=relevant --full-saturate-quant +trywith 15 --prenex-quant=none --full-saturate-quant +trywith 15 --decision=internal --full-saturate-quant +trywith 30 --relevant-triggers --full-saturate-quant +trywith 30 --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/competitions/casc/run-script-cascj8-tfa b/contrib/competitions/casc/run-script-cascj8-tfa new file mode 100755 index 000000000..da4056466 --- /dev/null +++ b/contrib/competitions/casc/run-script-cascj8-tfa @@ -0,0 +1,40 @@ +#!/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 --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 60 --cbqi-all --fs-inst --full-saturate-quant +finishwith --full-saturate-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-cascj8-tfn b/contrib/competitions/casc/run-script-cascj8-tfn new file mode 100755 index 000000000..a6fe1e23c --- /dev/null +++ b/contrib/competitions/casc/run-script-cascj8-tfn @@ -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 --sort-inference --uf-ss-fair +trywith 30 --full-saturate-quant +trywith 30 --finite-model-find --fmf-bound-int --macros-quant +finishwith --finite-model-find --decision=internal --sort-inference --uf-ss-fair +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-cascj9-fnt b/contrib/competitions/casc/run-script-cascj9-fnt new file mode 100755 index 000000000..4e52e8e91 --- /dev/null +++ b/contrib/competitions/casc/run-script-cascj9-fnt @@ -0,0 +1,35 @@ +#!/bin/bash + +here=`dirname $0` +cvc4=$here/cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-fnt casc j9 : $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 30 --finite-model-find --uf-ss=no-minimal --sort-inference +finishwith --finite-model-find --macros-quant --macros-quant-mode=all --sort-inference +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-cascj9-fof b/contrib/competitions/casc/run-script-cascj9-fof new file mode 100755 index 000000000..71107775a --- /dev/null +++ b/contrib/competitions/casc/run-script-cascj9-fof @@ -0,0 +1,50 @@ +#!/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 j9 : $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 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant +trywith 20 --no-e-matching --full-saturate-quant +trywith 15 --finite-model-find --uf-ss=no-minimal +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 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 --pre-skolem-quant --full-saturate-quant +trywith 30 --qcf-vo-exp --full-saturate-quant +trywith 30 --no-quant-cf --full-saturate-quant +finishwith --macros-quant --macros-quant-mode=all --full-saturate-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-cascj9-tfa b/contrib/competitions/casc/run-script-cascj9-tfa new file mode 100755 index 000000000..d730db922 --- /dev/null +++ b/contrib/competitions/casc/run-script-cascj9-tfa @@ -0,0 +1,37 @@ +#!/bin/bash + +here=`dirname $0` +cvc4=$here/cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-tfa casc j9 : $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 15 --finite-model-find --decision=internal +trywith 15 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant +trywith 15 --no-e-matching --full-saturate-quant +trywith 15 --cbqi-all --purify-triggers --full-saturate-quant +finishwith --macros-quant --macros-quant-mode=all --nl-ext-tplanes --full-saturate-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/casc/run-script-cascj9-tfn-nr b/contrib/competitions/casc/run-script-cascj9-tfn-nr new file mode 100644 index 000000000..8124fd6f9 --- /dev/null +++ b/contrib/competitions/casc/run-script-cascj9-tfn-nr @@ -0,0 +1,36 @@ +#!/bin/bash + +here=`dirname $0` +cvc4=$here/cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-tfn casc j9 : $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-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 --force-logic="UFNIRA" --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench +} + +# designed for 300 seconds +trywith 30 --finite-model-find --decision=internal --sort-inference --macros-quant --macros-quant-mode=all +trywith 15 --nl-ext-tplanes --full-saturate-quant --macros-quant --macros-quant-mode=all +finishwith --finite-model-find --fmf-inst-engine --sort-inference --macros-quant --macros-quant-mode=all +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2012 b/contrib/competitions/smt-comp/run-script-smtcomp2012 new file mode 100755 index 000000000..dfdd88cc6 --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smtcomp2012 @@ -0,0 +1,51 @@ +#!/bin/bash + +cat >bench-$$.smt2 +trap 'rm bench-$$.smt2' EXIT + +logic=$(expr "$(head -n 1 bench-$$.smt2)" : ' *(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 { + result="$(./cvc4 -L smt2 --no-checking --no-interactive "$@" bench-$$.smt2)" + 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-checking --no-interactive "$@" bench-$$.smt2 +} + +case "$logic" in + +QF_LRA) + # 3 minutes with default decision heuristic + trywith --tlimit-per=180000 + # switch to internal decision heuristic + finishwith --decision=internal + ;; +AUFLIA) + # 60 seconds with default decision heuristic + trywith --tlimit-per=60000 + # try simplification for 60 seconds, default decision heuristic + trywith --simplification=batch --tlimit-per=60000 + # switch to internal decision heuristic + finishwith --decision=internal + ;; +QF_AUFBV) + trywith --tlimit-per=600000 + finishwith --decision=justification-stoponly + ;; +*) + # just run the default + finishwith + ;; + +esac + diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2014 b/contrib/competitions/smt-comp/run-script-smtcomp2014 new file mode 100755 index 000000000..31ee4cf4d --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smtcomp2014 @@ -0,0 +1,96 @@ +#!/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 + ;; +ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) + # the following is designed for a run time of 1500s. + # initial runs + trywith 20 --simplification=none --decision=internal --full-saturate-quant + trywith 20 --quant-cf --pre-skolem-quant --full-saturate-quant + trywith 20 --finite-model-find --mbqi=none + # more runs... + trywith 30 --relevant-triggers --full-saturate-quant + trywith 30 --quant-cf --qcf-tconstraint --inst-when=last-call --full-saturate-quant + trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality + trywith 30 --disable-prenex-quant --full-saturate-quant + trywith 20 --simplification=none --decision=internal --pre-skolem-quant --full-saturate-quant + trywith 20 --quant-cf --quant-cf-mode=conflict --full-saturate-quant + trywith 20 --fmf-bound-int --macros-quant + # medium runs (2 min per) + trywith 120 --decision=justification-stoponly --full-saturate-quant + trywith 120 --quant-cf --qcf-tconstraint --full-saturate-quant + trywith 120 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair --mbqi=gen-ev + # last call runs (5 min per) + trywith 300 --full-saturate-quant + trywith 300 --finite-model-find --sort-inference --uf-ss-fair + finishwith --quant-cf --full-saturate-quant + ;; +LIA|LRA|NIA|NRA) + trywith 20 --enable-cbqi --full-saturate-quant + trywith 20 --full-saturate-quant + trywith 20 --cbqi-recurse --full-saturate-quant + trywith 30 --quant-cf --full-saturate-quant + trywith 60 --quant-cf --qcf-tconstraint --full-saturate-quant + trywith 120 --cbqi-recurse --disable-prenex-quant --full-saturate-quant + finishwith --cbqi-recurse --pre-skolem-quant --full-saturate-quant + ;; +QF_AUFBV) + trywith 600 + finishwith --decision=justification-stoponly + ;; +QF_ABV) + finishwith --ite-simp --simp-with-care --repeat-simp + ;; +QF_BV) + exec ./pcvc4 -L smt2 --no-incremental --no-checking --no-interactive \ + --threads 2 \ + --thread0 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --no-bv-abstraction' \ + --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto ' \ + --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|QF_AX) + finishwith --no-arrays-eager-index --arrays-eager-lemmas + ;; +*) + # just run the default + finishwith + ;; + +esac + diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2014-application b/contrib/competitions/smt-comp/run-script-smtcomp2014-application new file mode 100755 index 000000000..53df6a927 --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smtcomp2014-application @@ -0,0 +1,52 @@ +#!/bin/bash + +cvc4=./cvc4 + +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 --tear-down-incremental "$@" <&0- +} + +case "$logic" in + +QF_LRA) + runcvc4 --enable-miplib-trick --miplib-trick-subs=4 --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp + ;; +QF_LIA) + # same as QF_LRA but add --pb-rewrites + runcvc4 --enable-miplib-trick --miplib-trick-subs=4 --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --pb-rewrites + ;; +ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) + runcvc4 --simplification=none --decision=internal --full-saturate-quant + ;; +LIA|LRA|NIA|NRA) + runcvc4 --enable-cbqi --full-saturate-quant + ;; +QF_BV) + runcvc4 --unconstrained-simp --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2 + ;; +QF_AUFLIA|QF_AX) + runcvc4 --no-arrays-eager-index --arrays-eager-lemmas + ;; +*) + # just run the default + runcvc4 + ;; + +esac diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2015 b/contrib/competitions/smt-comp/run-script-smtcomp2015 new file mode 100755 index 000000000..846459f23 --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smtcomp2015 @@ -0,0 +1,106 @@ +#!/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 + ;; +ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) + # the following is designed for a run time of 1800s. + # initial runs 1min + trywith 20 --simplification=none --full-saturate-quant + trywith 20 --finite-model-find + trywith 20 --no-e-matching --full-saturate-quant + # trigger selections/special 1min + trywith 10 --multi-trigger-when-single --full-saturate-quant + trywith 10 --trigger-sel=max --full-saturate-quant + trywith 10 --relevant-triggers --full-saturate-quant + trywith 10 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant + trywith 10 --trigger-sel=min --full-saturate-quant + trywith 10 --qcf-tconstraint --full-saturate-quant + # medium runs 5min + trywith 30 --no-quant-cf --full-saturate-quant + trywith 30 --finite-model-find --fmf-inst-engine --mbqi=gen-ev + trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant + trywith 30 --pre-skolem-quant --full-saturate-quant + trywith 30 --no-inst-no-entail --no-quant-cf --full-saturate-quant + trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality + trywith 30 --inst-when=full --full-saturate-quant + #trywith 30 --fmf-bound-int --macros-quant # recently bug fixed + trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant + trywith 30 --decision=justification-stoponly --full-saturate-quant + # large runs 3min + trywith 60 --term-db-mode=relevant --full-saturate-quant + trywith 60 --finite-model-find --mbqi=none + trywith 60 --decision=internal --full-saturate-quant + # last call runs 20min + trywith 300 --finite-model-find --fmf-inst-engine --quant-cf + trywith 300 --no-inst-no-entail --full-saturate-quant + finishwith --full-saturate-quant + ;; +LIA|LRA|NIA|NRA) + trywith 180 --cbqi --no-cbqi-sat --full-saturate-quant + trywith 60 --full-saturate-quant + trywith 180 --qcf-tconstraint --full-saturate-quant + finishwith --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant + ;; +QF_AUFBV) + trywith 600 + finishwith --decision=justification-stoponly + ;; +QF_ABV) + finishwith --ite-simp --simp-with-care --repeat-simp + ;; +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 --no-bv-abstraction' \ + --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto ' \ + --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_AUFNIA) + finishwith --decision=justification --no-arrays-eager-index --arrays-eager-lemmas + ;; +QF_AUFLIA|QF_AX) + finishwith --no-arrays-eager-index --arrays-eager-lemmas + ;; +*) + # just run the default + finishwith + ;; + +esac + diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2015-application b/contrib/competitions/smt-comp/run-script-smtcomp2015-application new file mode 100755 index 000000000..3ffcc7234 --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smtcomp2015-application @@ -0,0 +1,52 @@ +#!/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 + +QF_LRA) + runcvc4 --tear-down-incremental --unconstrained-simp + ;; +QF_LIA) + # same as QF_LRA but add --pb-rewrites + runcvc4 --tear-down-incremental --unconstrained-simp + ;; +ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) + runcvc4 --tear-down-incremental + ;; +LIA|LRA|NIA|NRA) + runcvc4 --tear-down-incremental --cbqi --no-cbqi-sat + ;; +QF_BV) + runcvc4 --tear-down-incremental --unconstrained-simp --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2 + ;; +QF_AUFLIA|QF_AX) + runcvc4 --tear-down-incremental --no-arrays-eager-index --arrays-eager-lemmas + ;; +*) + # just run the default + runcvc4 --tear-down-incremental + ;; + +esac diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2015-assertions b/contrib/competitions/smt-comp/run-script-smtcomp2015-assertions new file mode 100755 index 000000000..4fa96af71 --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smtcomp2015-assertions @@ -0,0 +1,108 @@ +#!/bin/bash + +cvc4=./cvc4-assertions +# Attempt to run each benchmark 1-5 min depending on numconfigs +# quanitifers get 5 min / benchmark +# quantifier free uf, arith, arrays get 1 min / benchmark +# qf_bv gets 1 min wall (2 min user) / benchmark + +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 30 --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 + ;; +ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) + # the following is designed for a run time of 1800s. + # initial runs 1min (30) + trywith 10 --simplification=none --full-saturate-quant + trywith 10 --finite-model-find + trywith 10 --no-e-matching --full-saturate-quant + # trigger selections/special 1min (60) + trywith 10 --multi-trigger-when-single --full-saturate-quant + trywith 10 --trigger-sel=max --full-saturate-quant + trywith 10 --relevant-triggers --full-saturate-quant + trywith 10 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant + trywith 10 --trigger-sel=min --full-saturate-quant + trywith 10 --qcf-tconstraint --full-saturate-quant + # medium runs 5min (20*10 = 200) + trywith 10 --no-quant-cf --full-saturate-quant + trywith 10 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair --mbqi=gen-ev + trywith 10 --no-e-matching --no-quant-cf --full-saturate-quant + trywith 10 --pre-skolem-quant --full-saturate-quant + trywith 10 --no-inst-no-entail --no-quant-cf --full-saturate-quant + trywith 10 --finite-model-find --mbqi=gen-ev --uf-ss-totality + trywith 10 --inst-when=full --full-saturate-quant + #trywith 10 --fmf-bound-int --macros-quant # recently bug fixed + trywith 10 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant + trywith 10 --decision=justification-stoponly --full-saturate-quant + # large runs 3min + trywith 10 --term-db-mode=relevant --full-saturate-quant + trywith 10 --finite-model-find --mbqi=none + trywith 10 --decision=internal --full-saturate-quant + # last call runs 20min + trywith 20 --finite-model-find --fmf-inst-engine --quant-cf --sort-inference --uf-ss-fair + trywith 20 --no-inst-no-entail --full-saturate-quant + finishwith --full-saturate-quant + ;; +LIA|LRA|NIA|NRA) + trywith 30 --cbqi --no-cbqi-sat --full-saturate-quant + trywith 30 --full-saturate-quant + trywith 30 --qcf-tconstraint --full-saturate-quant + finishwith --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant + ;; +QF_AUFBV) + trywith 30 + finishwith --decision=justification-stoponly + ;; +QF_ABV) + finishwith --ite-simp --simp-with-care --repeat-simp + ;; +QF_BV) + exec ./pcvc4-assertions -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 --no-bv-abstraction' \ + --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto ' \ + --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|QF_AX) + finishwith --no-arrays-eager-index --arrays-eager-lemmas + ;; +*) + # just run the default + finishwith + ;; + +esac + diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2016 b/contrib/competitions/smt-comp/run-script-smtcomp2016 new file mode 100755 index 000000000..58b281b4c --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smtcomp2016 @@ -0,0 +1,134 @@ +#!/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 20 + 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 + ;; +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 2min + trywith 30 --relevant-triggers --full-saturate-quant + trywith 30 --trigger-sel=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 + # other 2min + 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 + # finite model find 2min + 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 12min + 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 + 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/competitions/smt-comp/run-script-smtcomp2016-application b/contrib/competitions/smt-comp/run-script-smtcomp2016-application new file mode 100755 index 000000000..88bbb5f53 --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smtcomp2016-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) + runcvc4 --tear-down-incremental=1 + ;; +LIA) + 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/competitions/smt-comp/run-script-smtcomp2017 b/contrib/competitions/smt-comp/run-script-smtcomp2017 new file mode 100644 index 000000000..06cd6a6e4 --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smtcomp2017 @@ -0,0 +1,152 @@ +#!/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.6 --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.6 --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 --decision=justification + finishwith --nl-ext --nl-ext-tplanes + ;; +# all logics with UF + quantifiers should either fall under this or special cases below +ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA) + # 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 3min + trywith 30 --relevant-triggers --full-saturate-quant + trywith 30 --trigger-sel=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 + # other 3min + trywith 30 --pre-skolem-quant --full-saturate-quant + trywith 30 --inst-when=full --full-saturate-quant + trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant + trywith 30 --nl-ext --full-saturate-quant + trywith 30 --full-saturate-quant --quant-ind + trywith 60 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant + # finite model find 2min + trywith 20 --finite-model-find --mbqi=none + trywith 20 --finite-model-find + trywith 20 --finite-model-find --uf-ss=no-minimal + trywith 60 --finite-model-find --fmf-inst-engine + # long runs 20min + trywith 200 --decision=internal --full-saturate-quant + trywith 200 --term-db-mode=relevant --full-saturate-quant + trywith 200 --fs-inst --full-saturate-quant + trywith 600 --finite-model-find --decision=internal + # finite model find 1min + trywith 30 --finite-model-find --fmf-bound-int + trywith 30 --finite-model-find --sort-inference + # finish 10min + finishwith --full-saturate-quant + ;; +UFBV) + # most problems in UFBV are essentially BV + trywith 300 --full-saturate-quant + trywith 300 --full-saturate-quant --no-cbqi + trywith 300 --full-saturate-quant --cbqi --decision=internal + finishwith --finite-model-find + ;; +BV) + trywith 300 --full-saturate-quant + trywith 300 --full-saturate-quant --no-cbqi + finishwith --full-saturate-quant --cbqi --decision=internal + ;; +LIA|LRA) + trywith 30 --full-saturate-quant + trywith 300 --full-saturate-quant --cbqi-midpoint + trywith 300 --full-saturate-quant --cbqi-nested-qe + finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal + ;; +NIA|NRA) + trywith 30 --full-saturate-quant + trywith 300 --full-saturate-quant --nl-ext + trywith 300 --full-saturate-quant --cbqi-nested-qe + finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal + ;; +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.6 --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/competitions/smt-comp/run-script-smtcomp2017-application b/contrib/competitions/smt-comp/run-script-smtcomp2017-application new file mode 100755 index 000000000..8a8ea7786 --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smtcomp2017-application @@ -0,0 +1,57 @@ +#!/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 --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/competitions/smt-comp/run-script-smtcomp2017-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp2017-unsat-cores new file mode 100644 index 000000000..f42f3ca30 --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smtcomp2017-unsat-cores @@ -0,0 +1,74 @@ +#!/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_LRA) + finishwith --no-restrict-pivots --use-soi --new-prop --unconstrained-simp + ;; +QF_LIA) + 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 + ;; +QF_NIA) + finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat + ;; +QF_NRA) + finishwith --nl-ext --nl-ext-tplanes + ;; +# all logics with UF + quantifiers should either fall under this or special cases below +ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA) + finishwith --full-saturate-quant + ;; +UFBV) + finishwith --finite-model-find + ;; +BV) + finishwith --full-saturate-quant --cbqi --decision=internal + ;; +LIA|LRA) + finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal + ;; +NIA|NRA) + finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal + ;; +QF_AUFBV) + finishwith --decision=justification-stoponly + ;; +QF_ABV) + finishwith --ite-simp --simp-with-care --arrays-weak-equiv + ;; +QF_UFBV) + finishwith --bitblast=eager --bv-sat-solver=cryptominisat + ;; +QF_BV) + finishwith --bv-div-zero-const --bv-eq-slicer=auto --no-bv-abstraction + ;; +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) + finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas + ;; +*) + # just run the default + finishwith + ;; + +esac + diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2018 b/contrib/competitions/smt-comp/run-script-smtcomp2018 new file mode 100644 index 000000000..849df0a6b --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smtcomp2018 @@ -0,0 +1,157 @@ +#!/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 and prints the output of the solver to stderr. +function trywith { + limit=$1; shift; + result="$(ulimit -S -t "$limit";$cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench)" + case "$result" in + sat|unsat) echo "$result"; exit 0;; + *) echo "$result" >&2;; + esac +} + +# 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_LRA) + trywith 200 --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 --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-tplanes --decision=internal + trywith 30 --no-nl-ext-tplanes --decision=internal + # this totals up to more than 20 minutes, although notice that smaller bit-widths may quickly fail + trywith 300 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction + trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction + trywith 300 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction + trywith 300 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction + finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction + ;; +QF_NRA) + trywith 300 --nl-ext-tplanes --decision=internal + trywith 300 --nl-ext-tplanes --decision=justification --no-nl-ext-factor + trywith 30 --nl-ext-tplanes --decision=internal --solve-real-as-int + finishwith --nl-ext-tplanes --decision=justification + ;; +# all logics with UF + quantifiers should either fall under this or special cases below +ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA) + # the following is designed for a run time of 20 min. + # initial runs 1min + trywith 30 --simplification=none --full-saturate-quant + trywith 30 --no-e-matching --full-saturate-quant + # trigger selections 3min + trywith 30 --relevant-triggers --full-saturate-quant + trywith 30 --trigger-sel=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 + # other 4min + trywith 30 --pre-skolem-quant --full-saturate-quant + trywith 30 --inst-when=full --full-saturate-quant + trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant + trywith 30 --full-saturate-quant --quant-ind + trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant + trywith 30 --decision=internal --full-saturate-quant + trywith 30 --term-db-mode=relevant --full-saturate-quant + trywith 30 --fs-interleave --full-saturate-quant + # finite model find 3min + trywith 30 --finite-model-find --mbqi=none + trywith 30 --finite-model-find --decision=internal + trywith 30 --finite-model-find --macros-quant --macros-quant-mode=all + trywith 30 --finite-model-find --uf-ss=no-minimal + trywith 60 --finite-model-find --fmf-inst-engine + # long runs 9min + trywith 240 --finite-model-find --decision=internal + finishwith --full-saturate-quant + ;; +ABVFP|BVFP|FP) + finishwith --full-saturate-quant + ;; +UFBV) + # most problems in UFBV are essentially BV + trywith 300 --full-saturate-quant --decision=internal + trywith 300 --full-saturate-quant --cbqi-nested-qe --decision=internal + trywith 30 --full-saturate-quant --no-cbqi-innermost --global-negate + finishwith --finite-model-find + ;; +BV) + trywith 120 --full-saturate-quant + trywith 120 --full-saturate-quant --no-cbqi-innermost + trywith 300 --full-saturate-quant --cbqi-nested-qe --decision=internal + trywith 30 --full-saturate-quant --no-cbqi-bv + trywith 30 --full-saturate-quant --cbqi-bv-ineq=eq-slack + # finish 10min + finishwith --full-saturate-quant --no-cbqi-innermost --global-negate + ;; +LIA|LRA|NIA|NRA) + trywith 30 --full-saturate-quant --nl-ext-tplanes + trywith 300 --full-saturate-quant --no-cbqi-innermost + trywith 300 --full-saturate-quant --cbqi-nested-qe + finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal + ;; +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=cadical + ;; +QF_BV) + finishwith --unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --bv-eq-slicer=auto --no-bv-abstraction + ;; +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 + ;; +QF_SLIA) + trywith 500 --strings-exp --rewrite-divk --lang=smt2.6.1 + finishwith --strings-exp --rewrite-divk --lang=smt2.6.1 --strings-fmf + ;; +QF_ABVFP) + finishwith + ;; +QF_BVFP) + finishwith + ;; +QF_FP) + finishwith + ;; +*) + # just run the default + finishwith + ;; + +esac + diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2018-application b/contrib/competitions/smt-comp/run-script-smtcomp2018-application new file mode 100755 index 000000000..58db84d36 --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smtcomp2018-application @@ -0,0 +1,84 @@ +#!/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 --tear-down-incremental=4 --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2 + ;; +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/competitions/smt-comp/run-script-smtcomp2018-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp2018-unsat-cores new file mode 100644 index 000000000..1454e7a8a --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smtcomp2018-unsat-cores @@ -0,0 +1,83 @@ +#!/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_LRA) + finishwith --no-restrict-pivots --use-soi --new-prop --unconstrained-simp + ;; +QF_LIA) + finishwith --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 + ;; +QF_NIA) + finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat + ;; +QF_NRA) + finishwith --nl-ext --nl-ext-tplanes + ;; +# all logics with UF + quantifiers should either fall under this or special cases below +ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA|ABVFP|BVFP|FP) + finishwith --full-saturate-quant + ;; +UFBV) + finishwith --finite-model-find + ;; +BV) + finishwith --full-saturate-quant --decision=internal + ;; +LIA|LRA) + finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal + ;; +NIA|NRA) + finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal + ;; +QF_AUFBV) + finishwith --decision=justification-stoponly + ;; +QF_ABV) + finishwith --ite-simp --simp-with-care --arrays-weak-equiv + ;; +QF_UFBV) + finishwith --bitblast=eager --bv-sat-solver=cryptominisat + ;; +QF_BV) + finishwith --bv-div-zero-const --bv-eq-slicer=auto --no-bv-abstraction + ;; +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) + finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas + ;; +QF_ABVFP) + finishwith + ;; +QF_BVFP) + finishwith + ;; +QF_FP) + finishwith + ;; +*) + # just run the default + finishwith + ;; + +esac + diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2019 b/contrib/competitions/smt-comp/run-script-smtcomp2019 new file mode 100755 index 000000000..a8c6b0ba4 --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smtcomp2019 @@ -0,0 +1,162 @@ +#!/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 and prints the output of the solver to stderr. +function trywith { + limit=$1; shift; + result="$(ulimit -S -t "$limit";$cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench)" + case "$result" in + sat|unsat) echo "$result"; exit 0;; + *) echo "$result" >&2;; + esac +} + +# 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_LRA) + trywith 400 --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 --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 600 --nl-ext-tplanes --decision=internal + trywith 60 --nl-ext-tplanes --decision=justification + trywith 60 --no-nl-ext-tplanes --decision=internal + # this totals up to more than 40 minutes, although notice that smaller bit-widths may quickly fail + trywith 600 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + trywith 600 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + trywith 600 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + trywith 600 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + trywith 1200 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + finishwith --nl-ext-tplanes --decision=internal + ;; +QF_NRA) + trywith 600 --nl-ext-tplanes --decision=internal + trywith 600 --nl-ext-tplanes --decision=justification --no-nl-ext-factor + trywith 60 --nl-ext-tplanes --decision=internal --solve-real-as-int + finishwith --nl-ext-tplanes --decision=justification + ;; +# all logics with UF + quantifiers should either fall under this or special cases below +ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA) + # the following is designed for a run time of 20 min. + # initial runs 2min + trywith 60 --simplification=none --full-saturate-quant + trywith 60 --no-e-matching --full-saturate-quant + # trigger selections 6min + trywith 60 --relevant-triggers --full-saturate-quant + trywith 60 --trigger-sel=max --full-saturate-quant + trywith 60 --multi-trigger-when-single --full-saturate-quant + trywith 60 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant + trywith 60 --multi-trigger-cache --full-saturate-quant + trywith 60 --no-multi-trigger-linear --full-saturate-quant + # other 8min + trywith 60 --pre-skolem-quant --full-saturate-quant + trywith 60 --inst-when=full --full-saturate-quant + trywith 60 --no-e-matching --no-quant-cf --full-saturate-quant + trywith 60 --full-saturate-quant --quant-ind + trywith 60 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant + trywith 60 --decision=internal --full-saturate-quant + trywith 60 --term-db-mode=relevant --full-saturate-quant + trywith 60 --fs-interleave --full-saturate-quant + # finite model find 6min + trywith 60 --finite-model-find --mbqi=none + trywith 60 --finite-model-find --decision=internal + trywith 60 --finite-model-find --macros-quant --macros-quant-mode=all + trywith 60 --finite-model-find --uf-ss=no-minimal + trywith 120 --finite-model-find --fmf-inst-engine + # long runs 8min + trywith 480 --finite-model-find --decision=internal + finishwith --full-saturate-quant + ;; +ABVFP|BVFP|FP) + finishwith --full-saturate-quant --fp-exp + ;; +UFBV) + # most problems in UFBV are essentially BV + trywith 600 --full-saturate-quant --decision=internal + trywith 600 --full-saturate-quant --cbqi-nested-qe --decision=internal + trywith 60 --full-saturate-quant --no-cbqi-innermost --global-negate + finishwith --finite-model-find + ;; +BV) + trywith 240 --full-saturate-quant + trywith 240 --full-saturate-quant --no-cbqi-innermost + trywith 600 --full-saturate-quant --cbqi-nested-qe --decision=internal + trywith 60 --full-saturate-quant --no-cbqi-bv + trywith 60 --full-saturate-quant --cbqi-bv-ineq=eq-slack + # finish 10min + finishwith --full-saturate-quant --no-cbqi-innermost --global-negate + ;; +LIA|LRA|NIA|NRA) + trywith 60 --full-saturate-quant --nl-ext-tplanes + trywith 600 --full-saturate-quant --no-cbqi-innermost + trywith 600 --full-saturate-quant --cbqi-nested-qe + finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal + ;; +QF_AUFBV) + trywith 1200 + finishwith --decision=justification-stoponly + ;; +QF_ABV) + trywith 100 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv + trywith 1000 --arrays-weak-equiv + finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv + ;; +QF_UFBV) + # Benchmarks with uninterpreted sorts cannot be solved with eager + # bit-blasting currently + trywith 2400 --bitblast=eager --bv-sat-solver=cadical + finishwith + ;; +QF_BV) + finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + ;; +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 140 --decision=justification --arrays-weak-equiv + finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas + ;; +QF_S|QF_SLIA) + trywith 300 --strings-exp --rewrite-divk --lang=smt2.6.1 --strings-fmf + finishwith --strings-exp --rewrite-divk --lang=smt2.6.1 + ;; +QF_ABVFP) + finishwith --fp-exp + ;; +QF_BVFP) + finishwith --fp-exp + ;; +QF_FP) + finishwith --fp-exp + ;; +*) + # just run the default + finishwith + ;; + +esac + diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2019-incremental b/contrib/competitions/smt-comp/run-script-smtcomp2019-incremental new file mode 100755 index 000000000..12c91a036 --- /dev/null +++ b/contrib/competitions/smt-comp/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/competitions/smt-comp/run-script-smtcomp2019-model-validation b/contrib/competitions/smt-comp/run-script-smtcomp2019-model-validation new file mode 100755 index 000000000..eec17294d --- /dev/null +++ b/contrib/competitions/smt-comp/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 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + ;; +*) + # just run the default + finishwith + ;; + +esac + diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2019-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp2019-unsat-cores new file mode 100755 index 000000000..795de734b --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smtcomp2019-unsat-cores @@ -0,0 +1,86 @@ +#!/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_LRA) + finishwith --no-restrict-pivots --use-soi --new-prop + ;; +QF_LIA) + finishwith --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 --use-soi + ;; +QF_NIA) + finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat + ;; +QF_NRA) + finishwith --nl-ext --nl-ext-tplanes + ;; +# all logics with UF + quantifiers should either fall under this or special cases below +ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA|ABVFP|BVFP|FP) + finishwith --full-saturate-quant --fp-exp + ;; +UFBV) + finishwith --finite-model-find + ;; +BV) + finishwith --full-saturate-quant --decision=internal + ;; +LIA|LRA) + finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal + ;; +NIA|NRA) + finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal + ;; +QF_AUFBV) + finishwith --decision=justification-stoponly + ;; +QF_ABV) + finishwith --ite-simp --simp-with-care --arrays-weak-equiv + ;; +QF_UFBV) + finishwith + ;; +QF_BV) + finishwith --bv-div-zero-const --bv-eq-slicer=auto --no-bv-abstraction + ;; +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) + finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas + ;; +QF_S|QF_SLIA) + finishwith --strings-exp --rewrite-divk --lang=smt2.6.1 + ;; +QF_ABVFP) + finishwith --fp-exp + ;; +QF_BVFP) + finishwith --fp-exp + ;; +QF_FP) + finishwith --fp-exp + ;; +*) + # just run the default + finishwith + ;; + +esac + diff --git a/contrib/competitions/smt-comp/run-script-smteval2013 b/contrib/competitions/smt-comp/run-script-smteval2013 new file mode 100755 index 000000000..2212f71c7 --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smteval2013 @@ -0,0 +1,61 @@ +#!/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 { + result="$($cvc4 --stats -L smt2 --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 --stats -L smt2 --no-checking --no-interactive "$@" $bench +} + +case "$logic" in + +QF_LRA) + finishwith --no-restrict-pivots --enable-miplib-trick --miplib-trick-subs=2 --fc-penalties --collect-pivot-stats --use-soi --new-prop --dio-decomps --unconstrained-simp --fancy-final + ;; +AUFLIA|AUFLIRA|AUFNIRA|UFLRA|UFNIA) + # 60 seconds with default decision heuristic + trywith --simplification=none --tlimit-per=60000 + # try simplification for 60 seconds, default decision heuristic + trywith --tlimit-per=60000 + # switch to internal decision heuristic + finishwith --simplification=none --decision=internal + ;; +LRA) + finishwith --enable-cbqi + ;; +QF_AUFBV) + trywith --tlimit-per=600000 + finishwith --decision=justification-stoponly + ;; +QF_BV) + trywith --bv-core --decision=justification --tlimit-per=10000 + trywith --decision=justification --tlimit-per=60000 + trywith --decision=internal --bitblast-eager --tlimit-per=600000 + finishwith --decision=justification --decision-use-weight --decision-weight-internal=usr1 + ;; +QF_AX) + trywith --tlimit-per=2000 + finishwith --no-arrays-model-based + ;; +*) + # just run the default + finishwith + ;; + +esac + diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2016-CLIA b/contrib/competitions/sygus-comp/run-script-sygusComp2016-CLIA new file mode 100755 index 000000000..3dc08d8c0 --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2016-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/competitions/sygus-comp/run-script-sygusComp2016-GENERAL b/contrib/competitions/sygus-comp/run-script-sygusComp2016-GENERAL new file mode 100755 index 000000000..0ee133ea8 --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2016-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/competitions/sygus-comp/run-script-sygusComp2016-INV b/contrib/competitions/sygus-comp/run-script-sygusComp2016-INV new file mode 100755 index 000000000..a25a5f5c8 --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2016-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/competitions/sygus-comp/run-script-sygusComp2016-PBE b/contrib/competitions/sygus-comp/run-script-sygusComp2016-PBE new file mode 100755 index 000000000..19d8fd891 --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2016-PBE @@ -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/competitions/sygus-comp/run-script-sygusComp2017-CLIA b/contrib/competitions/sygus-comp/run-script-sygusComp2017-CLIA new file mode 100755 index 000000000..3dc08d8c0 --- /dev/null +++ b/contrib/competitions/sygus-comp/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/competitions/sygus-comp/run-script-sygusComp2017-GENERAL b/contrib/competitions/sygus-comp/run-script-sygusComp2017-GENERAL new file mode 100755 index 000000000..0ee133ea8 --- /dev/null +++ b/contrib/competitions/sygus-comp/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/competitions/sygus-comp/run-script-sygusComp2017-INV b/contrib/competitions/sygus-comp/run-script-sygusComp2017-INV new file mode 100755 index 000000000..a21792fb9 --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2017-INV @@ -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 60 --sygus-inv-templ=pre +finishwith --sygus-inv-templ=post diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2017-PBE_BitVec b/contrib/competitions/sygus-comp/run-script-sygusComp2017-PBE_BitVec new file mode 100755 index 000000000..19d8fd891 --- /dev/null +++ b/contrib/competitions/sygus-comp/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/competitions/sygus-comp/run-script-sygusComp2017-PBE_Strings b/contrib/competitions/sygus-comp/run-script-sygusComp2017-PBE_Strings new file mode 100755 index 000000000..849835b28 --- /dev/null +++ b/contrib/competitions/sygus-comp/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 --sygus-fair=direct + diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2018-CLIA b/contrib/competitions/sygus-comp/run-script-sygusComp2018-CLIA new file mode 100644 index 000000000..b4e00423c --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2018-CLIA @@ -0,0 +1,37 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function runl { + limit=$1; shift; + ulimit -S -t "$limit";$cvc4 --lang=sygus --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null +} + +function trywith { + sol=$(runl $@) + status=$? + if [ $status -ne 134 ]; then + echo $sol |& + (read result w1 w2; + case "$result" in + unsat) + case "$w1" in + "(define-fun") echo "$w1 $w2";cat;exit 0;; + esac; exit 1;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi + fi +} + +function finishwith { + $cvc4 --lang=sygus --no-checking --no-interactive --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 --cegqi-si-abort --decision=internal --cbqi --cbqi-prereg-inst +trywith 10 --cegqi-si=none +finishwith --cegqi-si=none --no-sygus-repair-const diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2018-GENERAL b/contrib/competitions/sygus-comp/run-script-sygusComp2018-GENERAL new file mode 100644 index 000000000..8419e6841 --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2018-GENERAL @@ -0,0 +1,37 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function runl { + limit=$1; shift; + ulimit -S -t "$limit";$cvc4 --lang=sygus --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null +} + +function trywith { + sol=$(runl $@) + status=$? + if [ $status -ne 134 ]; then + echo $sol |& + (read result w1 w2; + case "$result" in + unsat) + case "$w1" in + "(define-fun") echo "$w1 $w2";cat;exit 0;; + esac; exit 1;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi + fi +} + +function finishwith { + $cvc4 --lang=sygus --no-checking --no-interactive --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 --cegqi-si-abort --decision=internal --cbqi --cbqi-prereg-inst +trywith 5 --cegqi-si=none --sygus-crepair-abort +finishwith --cegqi-si=none --no-sygus-repair-const diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2018-INV b/contrib/competitions/sygus-comp/run-script-sygusComp2018-INV new file mode 100644 index 000000000..57870a5af --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2018-INV @@ -0,0 +1,37 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function runl { + limit=$1; shift; + ulimit -S -t "$limit";$cvc4 --lang=sygus --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null +} + +function trywith { + sol=$(runl $@) + status=$? + if [ $status -ne 134 ]; then + echo $sol |& + (read result w1 w2; + case "$result" in + unsat) + case "$w1" in + "(define-fun") echo "$w1 $w2";cat;exit 0;; + esac; exit 1;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi + fi +} + +function finishwith { + $cvc4 --lang=sygus --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null | + (read result w1; + case "$result" in + unsat) echo "$w1";cat;exit 0;; + esac) +} + +trywith 10 +trywith 120 --sygus-unif +finishwith --no-sygus-repair-const diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2018-PBE_BitVec b/contrib/competitions/sygus-comp/run-script-sygusComp2018-PBE_BitVec new file mode 100644 index 000000000..ee5035e59 --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2018-PBE_BitVec @@ -0,0 +1,16 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function finishwith { + ($cvc4 --lang=sygus --no-checking --no-interactive --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 +} + +finishwith --cegqi-si=none + diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2018-PBE_Strings b/contrib/competitions/sygus-comp/run-script-sygusComp2018-PBE_Strings new file mode 100644 index 000000000..a9e05bf76 --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2018-PBE_Strings @@ -0,0 +1,16 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function finishwith { + ($cvc4 --lang=sygus --no-checking --no-interactive --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 +} + +finishwith --cegqi-si=none --sygus-fair=direct + diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-CLIA b/contrib/competitions/sygus-comp/run-script-sygusComp2019-CLIA new file mode 100755 index 000000000..97bb2175b --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-CLIA @@ -0,0 +1,37 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function runl { + limit=$1; shift; + ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null +} + +function trywith { + sol=$(runl $@) + status=$? + if [ $status -ne 134 ]; then + echo $sol |& + (read result w1 w2; + case "$result" in + unsat) + case "$w1" in + "(define-fun") echo "$w1 $w2";cat;exit 0;; + esac; exit 1;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi + fi +} + +function finishwith { + $cvc4 --lang=sygus2 --no-checking --no-interactive --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 --cegqi-si-abort --cbqi --cbqi-prereg-inst +trywith 10 --cegqi-si=none --sygus-repair-const +finishwith --cegqi-si=none diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-GENERAL-auto b/contrib/competitions/sygus-comp/run-script-sygusComp2019-GENERAL-auto new file mode 100755 index 000000000..36afb0790 --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-GENERAL-auto @@ -0,0 +1,37 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function runl { + limit=$1; shift; + ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null +} + +function trywith { + sol=$(runl $@) + status=$? + if [ $status -ne 134 ]; then + echo $sol |& + (read result w1 w2; + case "$result" in + unsat) + case "$w1" in + "(define-fun") echo "$w1 $w2";cat;exit 0;; + esac; exit 1;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi + fi +} + +function finishwith { + $cvc4 --lang=sygus2 --no-checking --no-interactive --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 --cegqi-si-abort --cbqi --cbqi-prereg-inst +trywith 5 --cegqi-si=none --sygus-crepair-abort --sygus-repair-const +finishwith --cegqi-si=none diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-GENERAL-f b/contrib/competitions/sygus-comp/run-script-sygusComp2019-GENERAL-f new file mode 100755 index 000000000..5c5e5e9e7 --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-GENERAL-f @@ -0,0 +1,36 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function runl { + limit=$1; shift; + ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null +} + +function trywith { + sol=$(runl $@) + status=$? + if [ $status -ne 134 ]; then + echo $sol |& + (read result w1 w2; + case "$result" in + unsat) + case "$w1" in + "(define-fun") echo "$w1 $w2";cat;exit 0;; + esac; exit 1;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi + fi +} + +function finishwith { + $cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null | + (read result w1; + case "$result" in + unsat) echo "$w1";cat;exit 0;; + esac) +} + +trywith 5 --sygus-active-gen=enum --cegqi-si=none --sygus-crepair-abort --sygus-repair-const +finishwith --sygus-active-gen=enum --cegqi-si=none diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-GENERAL-s b/contrib/competitions/sygus-comp/run-script-sygusComp2019-GENERAL-s new file mode 100755 index 000000000..2a19a14b5 --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-GENERAL-s @@ -0,0 +1,36 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function runl { + limit=$1; shift; + ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null +} + +function trywith { + sol=$(runl $@) + status=$? + if [ $status -ne 134 ]; then + echo $sol |& + (read result w1 w2; + case "$result" in + unsat) + case "$w1" in + "(define-fun") echo "$w1 $w2";cat;exit 0;; + esac; exit 1;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi + fi +} + +function finishwith { + $cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null | + (read result w1; + case "$result" in + unsat) echo "$w1";cat;exit 0;; + esac) +} + +trywith 5 --sygus-active-gen=none --cegqi-si=none --sygus-crepair-abort --sygus-repair-const +finishwith --sygus-active-gen=none --cegqi-si=none diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-INV-f b/contrib/competitions/sygus-comp/run-script-sygusComp2019-INV-f new file mode 100755 index 000000000..21120c0a4 --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-INV-f @@ -0,0 +1,37 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function runl { + limit=$1; shift; + ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null +} + +function trywith { + sol=$(runl $@) + status=$? + if [ $status -ne 134 ]; then + echo $sol |& + (read result w1 w2; + case "$result" in + unsat) + case "$w1" in + "(define-fun") echo "$w1 $w2";cat;exit 0;; + esac; exit 1;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi + fi +} + +function finishwith { + $cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null | + (read result w1; + case "$result" in + unsat) echo "$w1";cat;exit 0;; + esac) +} + +trywith 10 --sygus-active-gen=enum --sygus-repair-const +trywith 120 --sygus-unif +finishwith --sygus-active-gen=enum diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-INV-s b/contrib/competitions/sygus-comp/run-script-sygusComp2019-INV-s new file mode 100755 index 000000000..e835ba91a --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-INV-s @@ -0,0 +1,37 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function runl { + limit=$1; shift; + ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null +} + +function trywith { + sol=$(runl $@) + status=$? + if [ $status -ne 134 ]; then + echo $sol |& + (read result w1 w2; + case "$result" in + unsat) + case "$w1" in + "(define-fun") echo "$w1 $w2";cat;exit 0;; + esac; exit 1;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi + fi +} + +function finishwith { + $cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null | + (read result w1; + case "$result" in + unsat) echo "$w1";cat;exit 0;; + esac) +} + +trywith 10 --sygus-active-gen=none --sygus-repair-const +trywith 120 --sygus-unif +finishwith --sygus-active-gen=none diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-INV-su b/contrib/competitions/sygus-comp/run-script-sygusComp2019-INV-su new file mode 100755 index 000000000..b3e056d7c --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-INV-su @@ -0,0 +1,37 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function runl { + limit=$1; shift; + ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null +} + +function trywith { + sol=$(runl $@) + status=$? + if [ $status -ne 134 ]; then + echo $sol |& + (read result w1 w2; + case "$result" in + unsat) + case "$w1" in + "(define-fun") echo "$w1 $w2";cat;exit 0;; + esac; exit 1;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi + fi +} + +function finishwith { + $cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null | + (read result w1; + case "$result" in + unsat) echo "$w1";cat;exit 0;; + esac) +} + +trywith 30 --sygus-unif-boolean-heuristic-dt --sygus-active-gen=var-agnostic --sygus-add-const-grammar --decision=justification +trywith 10 --sygus-active-gen=none --sygus-repair-const +finishwith --sygus-active-gen=none diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_BitVec-f b/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_BitVec-f new file mode 100755 index 000000000..7fd203238 --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_BitVec-f @@ -0,0 +1,15 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function finishwith { + ($cvc4 --lang=sygus2 --no-checking --no-interactive --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 +} + +finishwith --cegqi-si=none diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_BitVec-s b/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_BitVec-s new file mode 100755 index 000000000..27d72f7a0 --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_BitVec-s @@ -0,0 +1,15 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function finishwith { + ($cvc4 --lang=sygus2 --no-checking --no-interactive --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 +} + +finishwith --sygus-active-gen=none --cegqi-si=none diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_Strings-f b/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_Strings-f new file mode 100755 index 000000000..f60263e05 --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_Strings-f @@ -0,0 +1,15 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function finishwith { + ($cvc4 --lang=sygus2 --no-checking --no-interactive --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 +} + +finishwith --cegqi-si=none --sygus-fair=direct diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_Strings-s b/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_Strings-s new file mode 100755 index 000000000..42c7c40e7 --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_Strings-s @@ -0,0 +1,15 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function finishwith { + ($cvc4 --lang=sygus2 --no-checking --no-interactive --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 +} + +finishwith --sygus-active-gen=none --cegqi-si=none --sygus-fair=direct diff --git a/contrib/competitions/sygus-comp/run-script-syguscomp2015 b/contrib/competitions/sygus-comp/run-script-syguscomp2015 new file mode 100755 index 000000000..aab6851e1 --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-syguscomp2015 @@ -0,0 +1,17 @@ +#!/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 --cegqi-si-multi-inst-abort --cegqi-si-abort --decision=internal +trywith --cegqi --no-cegqi-si + |