diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-28 02:28:39 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-28 02:28:39 -0500 |
| commit | b8bd234936a499d72cb5a9444f8cfd82d980fe8f (patch) | |
| tree | bd2971ad0f7a5239c89f05abba52ebe3b8da2245 /contrib | |
| parent | 3b49d2e6938fbee46737bbd71419febca2ec318d (diff) | |
Add option to avoid dumping partial models/proofs.
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/run-script-cascj7-fnt | 8 | ||||
| -rwxr-xr-x | contrib/run-script-cascj7-fof | 4 |
2 files changed, 6 insertions, 6 deletions
diff --git a/contrib/run-script-cascj7-fnt b/contrib/run-script-cascj7-fnt index 9e754ffc7..ce54fe5ae 100755 --- a/contrib/run-script-cascj7-fnt +++ b/contrib/run-script-cascj7-fnt @@ -15,7 +15,7 @@ echo "------- cvc4-fnt casc j7 : $bench at $2..." function trywith { limit=$1; shift; echo "--- Run $@ at $limit..."; - (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-models --produce-models "$@" $bench) 2>/dev/null | + (ulimit -t "$limit";$cvc4 --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;; @@ -25,12 +25,12 @@ function trywith { } function finishwith { echo "--- Run $@..."; - $cvc4 --no-checking --no-interactive --dump-models --produce-models "$@" $bench + $cvc4 --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 10 --finite-model-find --disable-uf-ss-min-model --sort-inference --uf-ss-fair -trywith 30 --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair +trywith 15 --finite-model-find --disable-uf-ss-min-model --sort-inference --uf-ss-fair +trywith 60 --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair finishwith --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair --mbqi-one-inst-per-round # echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-cascj7-fof b/contrib/run-script-cascj7-fof index 2e4f4d0b9..783eca17e 100755 --- a/contrib/run-script-cascj7-fof +++ b/contrib/run-script-cascj7-fof @@ -15,7 +15,7 @@ echo "------- cvc4-fof casc j7 : $bench at $2..." function trywith { limit=$1; shift; echo "--- Run $@ at $limit..."; - (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs "$@" $bench) 2>/dev/null | + (ulimit -t "$limit";$cvc4 --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;; @@ -25,7 +25,7 @@ function trywith { } function finishwith { echo "--- Run $@..."; - $cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs "$@" $bench + $cvc4 --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 |