diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-09 21:39:03 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-09 21:39:03 -0500 |
commit | 20cde072ebef5eddfc1562bebdd9438c77a22c8e (patch) | |
tree | ddb2b5e0d5fe8d4e37d05af6c947298d030fd91d /contrib | |
parent | 83ecbc2357ffbb7d0772804c360302ca1daa2400 (diff) |
Add simplification option --fo-prop-quant. Add model support for new model-checking procedure. Add run script for casc24-fnt.
Diffstat (limited to 'contrib')
-rwxr-xr-x | contrib/run-script-casc24-fnt | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/contrib/run-script-casc24-fnt b/contrib/run-script-casc24-fnt new file mode 100755 index 000000000..0230b8e13 --- /dev/null +++ b/contrib/run-script-casc24-fnt @@ -0,0 +1,27 @@ +#!/bin/bash + +cvc4=cvc4 +bench="$1" + +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="$($cvc4 -L tptp --no-checking --no-interactive "$@" $bench)" + case "$result" in + sat) echo "SZS Satisfiable for $filename"; exit 0;; + unsat) echo "SZS Unsatisfiable for $filename"; exit 0;; + esac +} + + +trywith --finite-model-find --uf-ss-totality --tlimit-per=10000 +trywith --finite-model-find --decision=justification --tlimit-per=10000 +trywith --finite-model-find --decision=justification --fmf-fmc +;; + + |