From 839b8f788f1d240380ca72c6d245c62e8e47501b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 15 May 2014 12:51:35 -0500 Subject: [PATCH] Minor fixes. Add SMTCOMP 2014 script. --- contrib/run-script-cascj7-fnt | 4 +- contrib/run-script-cascj7-fof | 4 +- contrib/run-script-cascj7-tff | 4 +- contrib/run-script-smtcomp2014 | 82 ++++++++++++++++++++++++++++++++++ src/smt/smt_engine.cpp | 4 +- 5 files changed, 90 insertions(+), 8 deletions(-) create mode 100755 contrib/run-script-smtcomp2014 diff --git a/contrib/run-script-cascj7-fnt b/contrib/run-script-cascj7-fnt index 073a9f297..5309fc93b 100755 --- a/contrib/run-script-cascj7-fnt +++ b/contrib/run-script-cascj7-fnt @@ -6,7 +6,7 @@ bench="$1" file=${bench##*/} filename=${file%.*} -echo "------- cvc4-fnt $bench at $2..." +echo "------- cvc4-fnt casc j7 : $bench at $2..." # use: trywith [params..] # to attempt a run. If an SZS ontology result is printed, then @@ -24,7 +24,7 @@ function trywith { if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi } function finishwith { - echo "--- Run $@ at $limit..."; + echo "--- Run $@..."; $cvc4 --no-checking --no-interactive --dump-models --produce-models "$@" $bench } diff --git a/contrib/run-script-cascj7-fof b/contrib/run-script-cascj7-fof index be656b57a..a863f70b5 100755 --- a/contrib/run-script-cascj7-fof +++ b/contrib/run-script-cascj7-fof @@ -6,7 +6,7 @@ bench="$1" file=${bench##*/} filename=${file%.*} -echo "------- cvc4-fof $bench at $2..." +echo "------- cvc4-fof casc j7 : $bench at $2..." # use: trywith [params..] # to attempt a run. If an SZS ontology result is printed, then @@ -24,7 +24,7 @@ function trywith { if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi } function finishwith { - echo "--- Run $@ at $limit..."; + echo "--- Run $@..."; $cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs "$@" $bench } diff --git a/contrib/run-script-cascj7-tff b/contrib/run-script-cascj7-tff index 4506e511d..41aec1335 100755 --- a/contrib/run-script-cascj7-tff +++ b/contrib/run-script-cascj7-tff @@ -6,7 +6,7 @@ bench="$1" file=${bench##*/} filename=${file%.*} -echo "------- cvc4-tff $bench at $2..." +echo "------- cvc4-tff casc j7 : $bench at $2..." # use: trywith [params..] # to attempt a run. If an SZS ontology result is printed, then @@ -24,7 +24,7 @@ function trywith { if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi } function finishwith { - echo "--- Run $@ at $limit..."; + echo "--- Run $@..."; $cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs "$@" $bench } diff --git a/contrib/run-script-smtcomp2014 b/contrib/run-script-smtcomp2014 new file mode 100755 index 000000000..b121c6956 --- /dev/null +++ b/contrib/run-script-smtcomp2014 @@ -0,0 +1,82 @@ +#!/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) + # 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 + ;; +LRA) + 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 --tlimit-per=600000 + finishwith --decision=justification-stoponly + ;; +QF_BV) + trywith --bv-core --decision=justification --tlimit-per=10000 + trywith --decision=justification --tlimit-per=60000 + trywith --decision=internal --bitblast-eager --tlimit-per=600000 + finishwith --decision=justification --decision-use-weight --decision-weight-internal=usr1 + ;; +QF_AX) + trywith --tlimit-per=2000 + finishwith --no-arrays-model-based + ;; +*) + # just run the default + finishwith + ;; + +esac + diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c6b76e850..8ef1d1543 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3803,13 +3803,13 @@ Proof* SmtEngine::getProof() throw(ModalException) { void SmtEngine::printInstantiations( std::ostream& out ) { SmtScope smts(this); if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){ - out << "% SZS CNF output start CNFRefutation for " << d_filename.c_str() << std::endl; + out << "% SZS output start Proof for " << d_filename.c_str() << std::endl; } if( d_theoryEngine ){ d_theoryEngine->printInstantiations( out ); } if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){ - out << "% SZS CNF output end CNFRefutation for " << d_filename.c_str() << std::endl; + out << "% SZS output end Proof for " << d_filename.c_str() << std::endl; } } -- 2.30.2