blob: 0230b8e137b1bb89e1fdddaa0cc88dfed7c56fd8 (
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
|
#!/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
;;
|
