summaryrefslogtreecommitdiff
path: root/test/CMakeLists.txt
AgeCommit message (Collapse)Author
2021-04-05A proposal for python api unit tests (#6255)yoni206
This PR introduces two unit tests for the python api, translated directly from the unit tests for the cpp api. The goal is to get feedback in order to reach some kind of a pattern/style for python API tests. Also, i'd be happy to hear if there is any specific cpp api unit test I should translate for this initial attempt (e.g., a test that is more representative or might raise difficulties). For now i just picked the first two solver tests.
2021-03-23Removing unused build options and deprecated proof compile flag (#6195)Haniel Barbosa
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
2020-09-14Rename system tests to api tests and remove obsolete Java test. (#5066)Aina Niemetz
2020-08-12Add option to only build library (#4801)makaimann
This PR would add an option to only build the CVC4 library and not the parser or executable. This can be used for projects that only intend to use CVC4 through the API. It seems to be working now, but it's not necessarily the cleanest solution. In particular, if you'd like the polarity to be different I'm happy to change that. Polarity meaning something like "${WITH_BINARY}" STREQUAL "YES" instead of NOT "${LIB_ONLY} STREQUAL "YES" which is admittedly a little strange.
2020-07-01Add testing infrastructure for LFSC signatures (#4678)Andres Noetzli
This commit adds testing infrastructure for LFSC signatures that is enabled when CVC4 is configured with LFSC. The testing infrastructure adopts run_test.py from https://github.com/CVC4/LFSC with minor modifications (mainly adding support for a list of include directories that are searched to resolve *.plf dependencies). The commit uses the existing examples and test files from proofs/signatures as the initial set of tests. Co-authored-by: Alex Ozdemir aozdemir@hmc.edu
2020-02-19Add Python bindings using Cython -- see below for more details (#2879)makaimann
2019-09-25Use separate CMake project for CVC4 examples. (#3196)Mathias Preiner
2019-08-08Fix issues with Ninja build system and add configure option. (#3166)Mathias Preiner
Adds option --ninja to configure.sh.
2018-10-18cmake: Run regression level 2 for make check. (#2645)Mathias Preiner
2018-10-02cmake: Add examples to build-tests, add warning for disabling static build. ↵Mathias Preiner
(#2562)
2018-10-01cmake: Add build target build-tests to build all test dependencies. (#2558)Mathias Preiner
2018-09-28cmake: Only do Java tests when unit testing on (#2551)Andres Noetzli
Right now, we are adding the Java tests even when we are not building unit tests. This commit changes the build system to only add the Java tests when unit tests are enabled. There are two reasons for this change: - building a production version of CVC4 should not require JUnit - it seems more intuitive (to me at least) to disable JUnit tests when unit tests are disabled This change also simplifies building the Java bindings in our homebrew formula.
2018-09-26cmake: Fix test target dependency issues. (#2540)Mathias Preiner
2018-09-22cmake: Run make coverage in parallel by default.Mathias Preiner
2018-09-22cmake: Disable unit tests if assertions are not enabled.Mathias Preiner
2018-09-22cmake: Do not build examples and unit and system tests by default.Aina Niemetz
2018-09-22cmake: Added target checkAina Niemetz
Targets 'check', 'units', 'systemtests' and 'regress' are now run in parallel with the number of available cores by default. This can be overriden by passing ARGS=-jN.
2018-09-22cmake: Removed obsolete CMakeLists file in test.Aina Niemetz
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback