diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-24 19:58:37 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-11 17:15:59 -0400 |
| commit | e80b93ca958bdbeb28959029868f6193b39a3f19 (patch) | |
| tree | 92218adf47348cb8011a41599e158b371f5659de /test/regress/run_regression | |
| parent | b76afedab3a23525da478ba4a8687c882793ea81 (diff) | |
Support for TPTP's TFF0 (with arithmetic)
This commit reverses an "SZS ontology compliance hack" that was
done for CASC-24 this year, and adds a TPTP pretty-printer which
is capable of outputting results in the TPTP way (rather than the
SMT way).
This commit includes minor changes to the Expr package to add
obvious missing functionality, and to fix the way expressions
with builtin operators are made. These changes are truly a
_fix_, the implementation had not been properly aligned with
the design vision for some corner cases.
Diffstat (limited to 'test/regress/run_regression')
| -rwxr-xr-x | test/regress/run_regression | 26 |
1 files changed, 20 insertions, 6 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression index 084df6ac9..b740e8486 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -164,21 +164,35 @@ elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then fi command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'` elif expr "$benchmark" : '.*\.p$' &>/dev/null; then - proof_command=PROOFS-NOT-SUPPORTED-IN-SMTLIB-V1; + proof_command=PROOFS-NOT-SUPPORTED-IN-TPTP; lang=tptp + command_line=--finite-model-find expected_proof=`grep '^% PROOF' "$benchmark" &>/dev/null && echo yes` expected_output=$(grep '^% EXPECT: ' "$benchmark") expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` if [ -z "$expected_output" -a -z "$expected_error" ]; then - error "cannot determine expected output of \`$benchmark': " \ - "please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures" + if grep -q '^% Status *: ' "$benchmark"; then + expected_output="$(grep '^% *Status *: ' "$benchmark" | head -1 | awk '{print$NF}')" + case "$expected_output" in + Theorem|Unsatisfiable) expected_exit_status=20 ;; + CounterSatisfiable|Satisfiable) expected_exit_status=10 ;; + GaveUp) expected_exit_status=0 ;; + esac + expected_output="% SZS status $expected_output for $(basename "$benchmark" | sed 's,\.p$,,')" + else + error "cannot determine expected output of \`$benchmark': " \ + "please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures" + fi + else + expected_output=$(echo "$expected_output" | perl -pe 's,^% EXPECT: ,,;s,\r,,') + expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'` fi - expected_output=$(echo "$expected_output" | perl -pe 's,^% EXPECT: ,,;s,\r,,') - expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'` if [ -z "$expected_exit_status" ]; then error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" fi - command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'` + if grep -q '^% COMMAND-LINE: ' "$benchmark"; then + command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'` + fi else error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2 or *.p" fi |