blob: c141cf43a22b8a16ed43f92baf2017aae1b8436b (
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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
#!/bin/bash
#
# Morgan Deters <mdeters@cs.nyu.edu>
# for the CVC4 project
#
# usage:
#
# run_regression cvc4-binary [ benchmark.cvc | benchmark.smt ]
#
# Runs benchmark and checks for correct exit status and output.
#
prog=`basename "$0"`
if [ $# != 2 ]; then
echo "usage: $prog cvc4-binary [ benchmark.cvc | benchmark.smt ]" >&2
exit 1
fi
cvc4=$1
benchmark=$2
function error {
echo "$prog: error: $*"
exit 1
}
if ! [ -x "$cvc4" ]; then
error "\`$cvc4' doesn't exist or isn't executable" >&2
fi
if ! [ -r "$benchmark" ]; then
error "\`$benchmark' doesn't exist or isn't readable" >&2
fi
if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
if grep '^ *:status *sat' "$benchmark" &>/dev/null; then
expected_output=SAT
expected_exit_status=10
elif grep '^ *:status *unsat' "$benchmark" &>/dev/null; then
expected_output=UNSAT
expected_exit_status=20
else
error "cannot determine status of \`$benchmark'"
fi
elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then
expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'`
if [ -z "$expected_output" ]; then
error "cannot determine status of \`$benchmark'"
fi
expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,'`
else
error "benchmark \`$benchmark' must be *.cvc or *.smt"
fi
expfile=`mktemp -t cvc4_expected.XXXXXXXXXX`
outfile=`mktemp -t cvc4_output.XXXXXXXXXX`
echo "$expected_output" >"$expfile"
echo "$cvc4" --segv-nospin "$benchmark"
"$cvc4" --segv-nospin "$benchmark" | tee "$outfile"
diffs=`diff -u "$expfile" "$outfile"`
diffexit=$?
rm -f "$expfile"
rm -f "$outfile"
if [ $diffexit -ne 0 ]; then
echo "$prog: error: differences between expected and actual output"
echo "$diffs"
exit 1
fi
if [ -n "$expected_exit_status" ]; then
:
#if [ $exit_status != "$expected_exit_status" ]; then
# error "expected exit status \`$expected_exit_status' but got \`$exit_status'"
#fi
fi
|
