summaryrefslogtreecommitdiff
path: root/test/regress/run_regression
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2014-10-23 20:58:08 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2015-01-14 06:33:49 -0500
commit0042f301908763cf1edb8a2d56b3f373a0055908 (patch)
tree4f2a66c39bf5511c3f00dca9f4d1bc475435359a /test/regress/run_regression
parentba1ae20edf3f4b2321a05b39cb218940e926d436 (diff)
sygus input language and benchmark
Diffstat (limited to 'test/regress/run_regression')
-rwxr-xr-xtest/regress/run_regression23
1 files changed, 22 insertions, 1 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression
index 062458055..7b215dc2a 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -179,8 +179,29 @@ elif expr "$benchmark" : '.*\.p$' &>/dev/null; then
if grep -q '^% COMMAND-LINE: ' "$benchmark"; then
command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
fi
+elif expr "$benchmark" : '.*\.sy$' &>/dev/null; then
+ lang=sygus
+ if test -e "$benchmark.expect"; then
+ expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
+ expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'`
+ expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
+ command_line=`grep '^% COMMAND-LINE: ' "$benchmark.expect" | sed 's,^% COMMAND-LINE: ,,'`
+ if [ -z "$expected_exit_status" ]; then
+ expected_exit_status=0
+ fi
+ elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then
+ expected_output=`grep '^; EXPECT: ' "$benchmark" | sed 's,^; EXPECT: ,,'`
+ expected_error=`grep '^; EXPECT-ERROR: ' "$benchmark" | sed 's,^; EXPECT-ERROR: ,,'`
+ expected_exit_status=`grep -m 1 '^; EXIT: ' "$benchmark" | perl -pe 's,^; EXIT: ,,;s,\r,,'`
+ command_line=`grep '^; COMMAND-LINE: ' "$benchmark" | sed 's,^; COMMAND-LINE: ,,'`
+ if [ -z "$expected_exit_status" ]; then
+ expected_exit_status=0
+ fi
+ else
+ error "cannot determine expected output of \`$benchmark'"
+ fi
else
- error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2 or *.p"
+ error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2 or *.p or *.sy"
fi
command_line="${command_line:+$command_line }--lang=$lang"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback