blob: eb8e91310b6467f4d904b9ffed1c7236ee727557 (
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
37
|
#!/bin/bash
cvc4=./cvc4
bench="$1"
let "to = $2 - 75"
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
trywith 15 --finite-model-find --fmf-inst-engine
trywith 30 --finite-model-find --decision=justification --fmf-fmc
trywith $to --decision=justification
echo "SZS GaveUp for $filename"
|
