--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
--- /dev/null
+#!/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
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
--- /dev/null
+#!/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
--- /dev/null
+#!/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
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
--- /dev/null
+#!/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
--- /dev/null
+#!/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
--- /dev/null
+#!/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
--- /dev/null
+#!/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
--- /dev/null
+#!/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
--- /dev/null
+#!/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
--- /dev/null
+#!/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
--- /dev/null
+#!/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
--- /dev/null
+#!/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
--- /dev/null
+#!/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
--- /dev/null
+#!/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
+
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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"
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
-
projects / cvc5.git / commitdiff