| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-12-06 | contrib: Setup all dependencies in deps/ directory. (#3534) | Mathias Preiner | |
| 2019-11-18 | Use -Wimplicit-fallthrough (#3464) | Andres Noetzli | |
| This commit enables compiler warnings for implicit fallthroughs in switch statements that are not explicitly marked as such. The commit introduces a new macro `CVC4_FALLTHROUGH` that can be used to indicate that a fallthrough is intentional. The commit fixes existing warnings and a bug in the arithmetic rewriter for `abs` (the bug likely couldn't be triggered easily because we rewrite `abs` to an `ite` while expanding definitions). To have the new macro also available in the parser, the commit changes `src/base/check.h` to be visible to the parser (it includes `cvc4_private_library.h` now instead of `cvc4_private.h`). | |||
| 2019-11-16 | Add support for ThreadSanitizer instrumentation (#3467) | Andres Noetzli | |
| This commit adds support for compiling CVC4 with ThreadSanitizer instrumentation. This is useful for debugging issues when CVC4 is used in a multi-threaded context (e.g. #3292). | |||
| 2019-11-08 | cmake: Disable C++ GNU extensions. (#3446) | Mathias Preiner | |
| Fixes #971. | |||
| 2019-10-15 | Remove remaining references to Boost and Autotools (#3390) | Andres Noetzli | |
| This commit removes references to Boost and Autotools in the copyright information and CMakeLists.txt. | |||
| 2019-10-11 | Add support for UBSan instrumentation (#3382) | Andres Noetzli | |
| This commit adds support for compiling CVC4 with UBSan instrumentation. The commit also adds a dummy version of `AigBitblaster`. Previously, when CVC4 was built without ABC, `AigBitblaster` was not fully defined (the class was declared but the implementation was not being compiled). This lead to missing RTTI information when compiling with UBSan instrumentation. | |||
| 2019-10-07 | Build system: Add build type for incremental competition builds. (#3365) | Aina Niemetz | |
| Previously, competition builds for incremental tracks required to manually pass in -DCVC4_SMTCOMP_APPLICATION_TRACK as compiler flag. This introduces an additional build type for incremental competition builds to simplify configuration for such builds. | |||
| 2019-09-25 | Use separate CMake project for CVC4 examples. (#3196) | Mathias Preiner | |
| 2019-09-06 | Remove portfolio (#3236) | Andrew Reynolds | |
| 2019-08-15 | cmake: Use ExactVersion instead of SameMinorVersion. (#3191) | Mathias Preiner | |
| 2019-08-14 | cmake: Export CVC4 library interface. (#3179) | Mathias Preiner | |
| 2019-08-08 | Fix issues with Ninja build system and add configure option. (#3166) | Mathias Preiner | |
| Adds option --ninja to configure.sh. | |||
| 2019-04-12 | Referring to prerelease 1.8 (#2943) | Haniel Barbosa | |
| 2019-04-05 | prerelease -> release (#2941) | Haniel Barbosa | |
| 2019-04-03 | Update release notes and lib version (#2933) | Haniel Barbosa | |
| 2019-01-15 | CMake: Fix search for static libraries (#2798) | Andres Noetzli | |
| When configuring CVC4 with `--static`, we change `CMAKE_FIND_LIBRARY_SUFFIXES` to prefer static libraries (`*.a`) over shared ones. However, instead of prepending `.a` to the list of `CMAKE_FIND_LIBRARY_SUFFIXES`, we created a single element with `.a` and the previous list. Output of `message("${CMAKE_FIND_LIBRARY_SUFFIXES}")` before the change: ``` .a .tbd;.dylib;.so;.a ``` After the change: ``` .a;.tbd;.dylib;.so;.a ``` On macOS, both the static and the shared library of GMP are available (when installed via homebrew) and before the change, CMake would pick the shared library when compiling with `--static --no-static-binary`. This commit fixes that issue. | |||
| 2019-01-04 | cmake: Disable unit tests for static builds. (#2775) | Mathias Preiner | |
| --static now implies --no-unit-testing. Fixes #2672. | |||
| 2018-12-17 | Configured for linking against drat2er (#2754) | Alex Ozdemir | |
| drat2er is a C/C++ project which includes support for * Checking DRAT proofs * Converting DRAT proofs to LRAT proofs * Converting DRAT proofs to ER proofs It does the first 2 by using drat-trim under the hood. I've modified our CMake configuration to allow drat2er to be linked into CVC4, and I added a contrib script. | |||
| 2018-11-08 | cmake: Add option to explicitely enable/disable static binaries. (#2698) | Mathias Preiner | |
| 2018-10-23 | CMake: Set RPATH on installed binary (#2671) | Andres Noetzli | |
| Currently, when installing CVC4 with a custom installation directory on macOS, the resulting binary cannot be executed because the linker cannot find the required libraries (e.g. our parser). This commit changes our build system to use the `CMAKE_INSTALL_RPATH` variable to add the installation directory to the RPATH list in the exectuable. | |||
| 2018-10-19 | Remove autotools build system. (#2639) | Mathias Preiner | |
| 2018-10-10 | cmake: Use gcovr instead lcov for coverage report generation. (#2617) | Mathias Preiner | |
| 2018-10-02 | cmake: Add examples to build-tests, add warning for disabling static build. ↵ | Mathias Preiner | |
| (#2562) | |||
| 2018-10-01 | cmake: Generate compile_commands.json on configure. (#2559) | Mathias Preiner | |
| 2018-10-01 | cmake: Add build target build-tests to build all test dependencies. (#2558) | Mathias Preiner | |
| 2018-09-29 | cmake: Ignore ctest exit code for coverage reports. | Mathias Preiner | |
| 2018-09-27 | cmake: Add CxxTest finder module to allow custom paths. (#2542) | Mathias Preiner | |
| 2018-09-26 | cmake: Fix test target dependency issues. (#2540) | Mathias Preiner | |
| 2018-09-25 | cmake: Exclude examples for coverage target. (#2535) | Mathias Preiner | |
| 2018-09-25 | cmake: Add check for GCC 4.5.1 and warn user. (#2533) | Mathias Preiner | |
| 2018-09-24 | cmake: Add program prefix option. (#2515) | Mathias Preiner | |
| 2018-09-22 | cmake: Add python3 option. | Mathias Preiner | |
| 2018-09-22 | cmake: Enable -Wall. | Mathias Preiner | |
| 2018-09-22 | cmake: Build fully static binaries with option --static. | Mathias Preiner | |
| 2018-09-22 | cmake: Run make coverage in parallel by default. | Mathias Preiner | |
| 2018-09-22 | cmake: Add more documentation, some fixes and cleanup. | Mathias Preiner | |
| 2018-09-22 | cmake: Move PACKAGE_NAME to ConfigureCVC4, more cleanup. | Mathias Preiner | |
| 2018-09-22 | cmake: Do not allow dumping with portfolio build. | Aina Niemetz | |
| 2018-09-22 | cmake: Move extracting git information to src/base cmake config file. | Aina Niemetz | |
| 2018-09-22 | cmake: Disable unit tests if assertions are not enabled. | Mathias Preiner | |
| 2018-09-22 | cmake: Do not build examples and unit and system tests by default. | Aina Niemetz | |
| 2018-09-22 | cmake: Add some more documentation, cleanup. | Mathias Preiner | |
| 2018-09-22 | cmake: Move helper functions to cmake/Helpers.cmake. | Mathias Preiner | |
| 2018-09-22 | cmake: Added target examples (currently .cpp examples only) | Aina Niemetz | |
| 2018-09-22 | cmake: Simplify build type configuration. | Mathias Preiner | |
| 2018-09-22 | cmake: Refactor and clean up build profile printing. | Aina Niemetz | |
| 2018-09-22 | cmake: Added target check | Aina 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-22 | cmake: Add make install rule. | Mathias Preiner | |
| 2018-09-22 | cmake: configure.sh wrapper: Fix handling of options with arguments. | Aina Niemetz | |
| 2018-09-22 | cmake: Add module finder for Valgrind. | Mathias Preiner | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
path: root/CMakeLists.txt
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback