Skip to content

Latest commit

 

History

History
55 lines (37 loc) · 1.84 KB

README.md

File metadata and controls

55 lines (37 loc) · 1.84 KB

The tests can be executed by make test from a configured build, the src or test directory and will put their intermediate and log files in the build directory. If called from outside from the build directory the last configured build directory is used.

We have four test drivers. The simplest one

./api/run.sh

is going through the API directly to test basic stand-alone functionality of the library. Next is a simple usage test for all command line options.

./usage/run.sh

The regression suite for CNF files

./cnf/run.sh

is more thorough and should catch simple bugs. It checks solutions and checks generated proofs too. The third test driver uses a regression suite and executes traces by replaying them through mobical

./traces/run.sh

Last but not least the model based tester ../src/mobical.cpp is the most effective test driver and can be run through

./mbt/run.sh

All test drivers place their intermediate and logging files into the build directory. Thus if for instance you build in a release subdirectory within the root directory of CaDiCaL

mkdir release
cd release
../configure
make test

will use the library and binaries in this release sub-directory for running all the tests. The log files including generated proofs are all put into the release subdirectory too.

For more information on external fuzz-testing see

Robert Brummayer, Florian Lonsing, Armin Biere: Automated Testing and Debugging of SAT and QBF Solvers. SAT 2010: 44-57

Model based testing of SAT solvers is described in

Cyrille Artho, Armin Biere, Martina Seidl: Model-Based Testing for Verification Back-Ends. TAP 2013: 39-55

The simple API test driver and the regression suite are executed by the default goal of the makefile. There is no need to clean up test output since it is all put into the build directory.