stp/stp — pull request #76 by delcypher (2014-03-03 10:40:39+00:00)
Title: Start fixing testing - Request for comments

This is my initial work on fixing testing. The work is far from complete but I'd like to get peoples opinions before I merge this (I see no reason not to, the testing before was even worse).

The only tests that work now are the query-files tests. I'll work on supporting API tests soon.

I've added a tool I wrote called OutputCheck as a submodule. So to run the tests (llvm-lit driven ones only right now). You need to do

```
$ git submodule init
$ git submodule update
$ cd /path/to/stp/builddir
$ make # Should trigger reconfigure and rebuild
$ make check # Run tests
```

if you want to run particular tests you can do something like

```
$ cd /path/stp/builddir/tests/query-files
$ ./llvm-lit -v unit_test/ misc-tests/no-query.cvc
```
I have automatically converted a lot of tests by using CVC4 (for .cvc files) and Z3 (for .smt and smt2 files) solvers as oracles so the testcase knows whether the answer should be ``sat``, ``unsat``, ``valid`` or ``invalid``.

A lot of the tests appear as "UNRESOLVED" because I couldn't get them to work in a reasonable amount of time or because the query files could not be parsed by the solvers. I'd like to add these as issues on our issue tracker and let someone a bit more experienced fix these.
The test suite is a still a bit messy too, there are tarballed query files which need to go somewhere.

For this reason I haven't added running tests in the Travis build. Once the ``tests/query-files`` test suite is fixed we can add running tests to the Travis build.

In ``tests/query-files`` I think we should only have query files that run quickly (e.g. say less than 5 minutes) which can be checked for the travis build.

We should have more strenuous tests but I'm not sure we should make them part of the travis build as this may take a long time. I think strenuous tests should go in a separate git repository which can be a submodule for STP which users can optionally setup if they want to run even more tests.

I also need to update the documentation on how to run/write tests... but one thing at a time.