Python regression script (#1662)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 6 Apr 2018 04:45:17 +0000 (21:45 -0700)
committerGitHub <noreply@github.com>
Fri, 6 Apr 2018 04:45:17 +0000 (21:45 -0700)
commitefc6163629c6c5de446eccfe81777c93829995d5
tree8681a332d409e94fc4ab7259513bc7935e5568b5
parentcf73e3ceb3f93fef830349bd44afec99404b5038
 Python regression script (#1662)

Until now, we have been using a bash script for the running the
regressions. That script had several issues, e.g. it was creating many
temprorary files and it was calling itself recursively, making it
difficult to maintain. This commit replaces the script with a Python
script. The Python script uses the TAP protocol, which allows us to
display the results of multiple tests per file (e.g. with --check-models
and without) separately and with more details. It also outputs whenever it starts running
a test, which allows finding "stuck" regression tests on Travis. As recommended in the
automake documentation [0], the commit copies the TAP driver to enable
TAP support for the test driver.

Note: the commit also changes some of the regressions slightly because
we were using "%" for the test directives in SMT files which does not
correspond to the comment character ";". Using the comment character
simplifies the handling and makes it easier for users to reproduce a
failure (they can simply run CVC4 on the regression file).

[0]
https://www.gnu.org/software/automake/manual/html_node/Use-TAP-with-the-Automake-test-harness.html
config/tap-driver.sh [new file with mode: 0755]
configure.ac
test/regress/Makefile.am
test/regress/regress0/arrays/incorrect10.smt
test/regress/regress0/expect/scrub.02.smt
test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt
test/regress/regress0/fmf/QEpres-uf.855035.smt
test/regress/regress1/fmf/Hoare-z3.931718.smt
test/regress/run_regression [deleted file]
test/regress/run_regression.py [new file with mode: 0755]