diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-12 14:15:40 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-12 14:15:58 -0500 |
| commit | 3013db0a0cf330ebd8d09a4d9c0b4d5dd3312068 (patch) | |
| tree | f6db2044d637a74a801f15cbfe3fddd6bb4f9dbc /contrib/run-script-cascj7-tff | |
| parent | 2550b6de915e6937ca145dae68ee04fc58680bce (diff) | |
Minor updates/fix to --cbqi-recurse
Diffstat (limited to 'contrib/run-script-cascj7-tff')
| -rwxr-xr-x | contrib/run-script-cascj7-tff | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/contrib/run-script-cascj7-tff b/contrib/run-script-cascj7-tff index 893b69572..8033bed1f 100755 --- a/contrib/run-script-cascj7-tff +++ b/contrib/run-script-cascj7-tff @@ -2,11 +2,12 @@ cvc4=cvc4 bench="$1" -let "to = $2 - 170" file=${bench##*/} filename=${file%.*} +echo "------- cvc4-tff $bench at $2..." + # 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 @@ -22,11 +23,16 @@ function trywith { esac; exit 1) if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi } +function finishwith { + echo "--- Run $@ at $limit..."; + $cvc4 --no-checking --no-interactive --dump-instantiations "$@" $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 90 --full-saturate-quant -trywith $to --cbqi-recurse --full-saturate-quant --pre-skolem-quant +trywith 30 --full-saturate-quant +trywith 60 --quant-cf --full-saturate-quant +finishwith --cbqi-recurse --full-saturate-quant --pre-skolem-quant echo "% SZS status" "GaveUp for $filename" |