Testing with CTest and vtest

Vampire now has units tests which can run with CTest.

Running tests

tl;dr: (test are only compiled in Debug mode)

mkdir cmake-build
cd cmake-build 
cmake -DCMAKE_BUILD_TYPE=Debug ..
make 
ctest --output-on-failure

Unit test binaries are automatically built when building with cmake. They can be run by calling ctest in the build directory.

Options you will probably find useful are the following:

• --output-on-failure
• --rerun-failed
• -R <regex> run only tests with names matching <regex>
• -E <regex> do not run tests with names matching <regex>

Every test unit consists of multiple test cases, which will be run each as a separate process. This can be annoying if one wants to debug a single test case using lldb or similar tools. Therefore you can also run a single test case without launching a separarate process:

mkdir cmake-build
cd cmake-build
cmake ..
make 
./vtest run <unit_id> <test_case>

All available test cases and test units can be listed with

./vtest ls

Compiling tests can also slow down compile times. Compiling them can be circumvented by calling make vampire instead of make in your cmake directory.

Creating new unit tests

tl;dr:

# choose a name
MY_TEST_NAME=...

# create test file
cp UnitTests/tSyntaxSugar.cpp UnitTests/t${MY_TEST_NAME}.cpp

# alter CMakeLists.txt
sed -e "{/tSyntaxSugar.cpp/p;s/tSyntaxSugar.cpp/t${MY_TEST_NAME}.cpp/;}" \
    -i '' CMakeLists.txt

# write the unit test
vim UnitTests/t${MY_TEST_NAME}.cpp

The unit tests are located in the directory UnitTests/. The tests are expected to be cpp files, and are prefixed with a t (e.g.: UnitTests/tSyntaxSugar.cpp). Each new test file must be added to the source list UNIT_TEST in CMakeLists.txt.

A test file must include Test/UnitTesting.hpp contain the following statements to initalize unit testing.

#include "Test/UnitTesting.hpp"

After this test functions can be defined:

TEST_FUN(<test_name>) {
  /* testing code goes here */
}

Every test function will be run as its own process. It is considered successful if the process exits with code 0, or the test function returns void, and considered a failure when the process throws an exception, violates an assertion, or exits with code -1.

Consider the following guide-lines for writing unit tests:

• what every individual test case does should be visible at first sight
• keep them short and concise
• don't test multiple things in one test
• don't rely on stdout printing of your unit tests. their success is meant to be machine checked.
• for that use and extend the test utilities mentioned in the next section.

Test utilities

Testing utilities can be found in Test/. The most notable are currently (all not yet merged):

• Test/TestUtils.hpp, containing utilites like checking equality of terms, literals and clauses modulo AC
• Test/SyntaxSugar.hpp, containing utilities to create terms, literals and clauses in a nicely read and writable way
• Test/GenerationTester.hpp, framework for writing tests for SimplifyingGeneratingInferences and GeneratingInferenceEngines. An example for these tests is given in UnitTests/tEqalityResolution.cpp. Pitfully we do not have unit-test for all our old inference rules, as these were not written with unit testing in mind, and are tightly bound to the Saturation/SaturationAlgorithm.hpp framework, which will hopefully be resolved by refactoring in the future.
• Test/SimplificationTester.hpp, framework for testing SimplifyingInferenceEngines. An example for these tests if given by UnitTests/tGaussianElimination.cpp