diff options
Diffstat (limited to 'test/regress/run_regression')
| -rwxr-xr-x | test/regress/run_regression | 79 |
1 files changed, 24 insertions, 55 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression index 4d23e796b..ef2bb9a35 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -71,10 +71,8 @@ function gettemp { tmpbenchmark= if expr "$benchmark" : '.*\.smt$' &>/dev/null; then - proof_command=PROOFS-NOT-SUPPORTED-IN-SMTLIB-V1 lang=smt1 if test -e "$benchmark.expect"; then - expected_proof=`grep '^% PROOF' "$benchmark.expect" &>/dev/null && echo yes` 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,,'` @@ -83,7 +81,6 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then expected_exit_status=0 fi elif grep '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then - expected_proof=`grep '^% PROOF' "$benchmark" &>/dev/null && echo yes` 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,,'` @@ -97,12 +94,10 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then fi benchmark=$tmpbenchmark elif grep '^ *:status *sat' "$benchmark" &>/dev/null; then - expected_proof= expected_output=sat expected_exit_status=0 command_line= elif grep '^ *:status *unsat' "$benchmark" &>/dev/null; then - expected_proof= expected_output=unsat expected_exit_status=0 command_line= @@ -110,10 +105,8 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then error "cannot determine status of \`$benchmark'" fi elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then - proof_command='(get-proof)' lang=smt2 if test -e "$benchmark.expect"; then - expected_proof=`grep '^[%;] PROOF' "$benchmark.expect" &>/dev/null && echo yes` 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,,'` @@ -122,7 +115,6 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then expected_exit_status=0 fi elif grep '^\(%\|;\) \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then - expected_proof=`grep '^[%;] PROOF' "$benchmark" &>/dev/null && echo yes` 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,,'` @@ -136,12 +128,10 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then fi benchmark=$tmpbenchmark elif grep '^ *( *set-info *:status *sat' "$benchmark" &>/dev/null; then - expected_proof= expected_output=sat expected_exit_status=0 command_line= elif grep '^ *( *set-info *:status *unsat' "$benchmark" &>/dev/null; then - expected_proof=`grep '^; PROOF' "$benchmark" &>/dev/null && echo yes` expected_output=unsat expected_exit_status=0 command_line= @@ -149,9 +139,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then error "cannot determine status of \`$benchmark'" fi elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then - proof_command='DUMP_PROOF;' lang=cvc4 - 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 @@ -165,10 +153,8 @@ 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-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 @@ -213,14 +199,28 @@ if [ -z "$expected_output" ]; then else echo "$expected_output" >"$expoutfile" fi + check_models=false if grep '^sat$' "$expoutfile" &>/dev/null || grep '^invalid$' "$expoutfile" &>/dev/null || grep '^unknown$' "$expoptfile" &>/dev/null; then - if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-models' &>/dev/null && - ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-models' &>/dev/null; then + if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-models\>' &>/dev/null && + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-models\>' &>/dev/null; then # later on, we'll run another test with --check-models on check_models=true fi fi +check_proofs=false +if [ "$proof" = yes ]; then + # proofs not currently supported in incremental mode, turn it off + if grep '^unsat$' "$expoutfile" &>/dev/null || grep '^valid$' "$expoutfile" &>/dev/null &>/dev/null; then + if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-proofs\>' &>/dev/null && + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-proofs\>' &>/dev/null && + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental\>' &>/dev/null && + ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null; then + # later on, we'll run another test with --check-proofs on + check_proofs=true + fi + fi +fi if [ -z "$expected_error" ]; then # in case expected stderr output is empty, make sure we don't differ # by a newline, which we would if we echo "" >"$experrfile" @@ -275,47 +275,16 @@ if [ "$exit_status" != "$expected_exit_status" ]; then exitcode=1 fi -if [ "$proof" = yes -a "$expected_proof" = yes ]; then - gettemp pfbenchmark cvc4_pfbenchmark.$$.XXXXXXXXXX - # remove exit command to add proof command for smt2 benchmarks - if expr "$benchmark" : '.*\.smt2$' &>/dev/null; then - head -n -0 "$benchmark" > "$pfbenchmark"; - echo "$proof_command" >>"$pfbenchmark"; - echo "(exit)" >> "$pfbenchmark"; - else - cp $benchmark $pfbenchmark - echo "$proof_command" >>"$pfbenchmark"; +if $check_models || $check_proofs; then + check_cmdline= + if $check_models; then + check_cmdline="$check_cmdline --check-models" fi - echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof `basename "$pfbenchmark"` [from working dir `dirname "$pfbenchmark"`] - time ( :; \ - ( cd `dirname "$pfbenchmark"`; - $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --proof `basename "$pfbenchmark"`; - echo $? >"$exitstatusfile" - ) > "$outfile" 2> "$errfile" ) - - gettemp pfoutfile cvc4_proof.$$.XXXXXXXXXX - - diff --unchanged-group-format='' \ - --old-group-format='' \ - --new-group-format='%>' \ - "$expoutfile" "$outfile" > "$pfoutfile" - if [ ! -s "$pfoutfile" ]; then - echo "$prog: error: proof generation failed with empty output (stderr follows)" - cat "$errfile" - exitcode=1 - else - echo running $LFSC "$pfoutfile" [from working dir `dirname "$pfbenchmark"`] - if ! $LFSC "$pfoutfile" &> "$errfile"; then - echo "$prog: error: proof checker failed (output follows)" - cat "$errfile" - exitcode=1 - fi + if $check_proofs; then + check_cmdline="$check_cmdline --check-proofs" fi -fi - -if $check_models; then - # at least one sat/invalid response: run an extra model-checking pass - if ! CVC4_REGRESSION_ARGS="$CVC4_REGRESSION_ARGS --check-models" "$0" $wrapper "$cvc4" "$benchmark_orig"; then + # at least one sat/invalid response: run an extra model/proof-checking pass + if ! CVC4_REGRESSION_ARGS="$CVC4_REGRESSION_ARGS$check_cmdline" "$0" $wrapper "$cvc4" "$benchmark_orig"; then exitcode=1 fi fi |