blob: a189c10bde920ff44635f3fc956cb530e6add445 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
#!/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 Satisfiable for $filename"; exit 0;;
unsat) echo "% SZS Unsatisfiable for $filename"; exit 0;;
conjecture-sat) echo "% SZS CounterSatisfiable for $filename"; exit 0;;
conjecture-unsat) echo "% SZS 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 Satisfiable for $filename"; exit 0;;
unsat) echo "% SZS Unsatisfiable for $filename"; exit 0;;
conjecture-sat) echo "% SZS CounterSatisfiable for $filename"; exit 0;;
conjecture-unsat) echo "% SZS 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 GaveUp for $filename"
|
