diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-23 20:58:08 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2015-01-14 06:33:49 -0500 |
commit | 0042f301908763cf1edb8a2d56b3f373a0055908 (patch) | |
tree | 4f2a66c39bf5511c3f00dca9f4d1bc475435359a /test/regress/run_regression | |
parent | ba1ae20edf3f4b2321a05b39cb218940e926d436 (diff) |
sygus input language and benchmark
Diffstat (limited to 'test/regress/run_regression')
-rwxr-xr-x | test/regress/run_regression | 23 |
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" |