| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-08-04 | Add documentation and build instructions for recompilation (LGPL). (#4844) | Mathias Preiner | |
| 2020-08-01 | Ensure that we only find '.a's when building statically (#4785) | Andrew V. Jones | |
| ## Issue When trying to building statically, and if your machine *does not* have static libraries (e.g., there is [no static GMP on CentOS 8](https://access.redhat.com/documentation/en-us/red_hat_enterprise_linux/8/html-single/considerations_in_adopting_rhel_8/index#removed-packages_changes-to-packages)), then CVC4's CMake does not detect this: ``` FAILED: bin/cvc4 : && /usr/bin/c++ -O3 -Wall -Wno-deprecated -Wsuggest-override -Wnon-virtual-dtor -Wimplicit-fallthrough -Wshadow -Wno-class-memaccess -fuse-ld=gold -static src/main/CMakeFiles/main.dir/command_executor.cpp.o src/main/CMakeFiles/main.dir/interactive_shell.cpp.o src/main/CMakeFiles/main.dir/signal_handlers.cpp.o src/main/CMakeFiles/main.dir/time_limit.cpp.o src/main/CMakeFiles/cvc4-bin.dir/driver_unified.cpp.o src/main/CMakeFiles/cvc4-bin.dir/main.cpp.o -o bin/cvc4 src/libcvc4.a src/parser/libcvc4parser.a src/libcvc4.a -Wl,-Bdynamic /usr/lib64/libgmp.so -Wl,-Bstatic ../deps/install/lib/libantlr3c.a && : /usr/bin/ld.gold: error: cannot mix -static with dynamic object /usr/lib64/libgmp.so ``` ## Resolution This PR changes CVC4's CMakeLists such that, if you're building statically, it *only* allows for linking against `.a`s (or `.a`s + `.lib`s on Windows). Signed-off-by: Andrew V. Jones <andrew.jones@vector.com> | |||
| 2020-07-17 | Support for using 'libedit' over 'readline' #4571 (#4579) | Andrew V. Jones | |
| Signed-off-by: Andrew V. Jones <andrew.jones@vector.com> | |||
| 2020-07-17 | Integration of libpoly (#4679) | Gereon Kremer | |
| This commit integrates LibPoly into CVC4. It adds `contrib/get-poly`, adds it to the configure script, cmake and places where CVC4 inspects its own build configuration. Furthermore, it adds `CVC4::RealAlgebraicNumber` (which wraps `poly::AlgebraicNumber`) including some basic unit tests and some utilities. | |||
| 2020-07-10 | Add deps/install/lib to RPATH and warn user when using dynamic libs. (#4684) | Gereon Kremer | |
| Installing the cvc4 binary does not work right now if it links against a shared library obtained via one of the contrib scripts. This PR thus adds deps/install/lib to the RPATH so that the installed binary works at all in this case. This change however paves the way to more problems: If one install such a dynamically linked binary and then removes (or updates) one the shared libraries in deps/install/lib, the installed binary most probably stops working. Hence, this PR checks whether this may happen (whether we link dynamically and link against a shared library from deps/install/lib) and, if this is the case, informs and warns the user about this issue. If the user tries to install to the default install prefix (/usr/local) we disallow installation entirely. | |||
| 2020-07-07 | Increase the minimum version of CMake due to the use of 'APPEND' with ↵ | Andrew V. Jones | |
| strings (#4702) Signed-off-by: Andrew V. Jones <andrew.jones@vector.com> | |||
| 2020-07-02 | Remove SWIG bindings (#4683) | Andres Noetzli | |
| This commit removes support for SWIG bindings for the legacy API. The bindings were already broken by 19054b3b1d427e662d30d4322df2b2f2361353da and we are not planning on using SWIG for the Java API for the new API. | |||
| 2020-06-24 | Fix CVC4_EXTRAVERSION variable (#4653) | Andres Noetzli | |
| When I created the PR for 733083c, it did not contain the change from "" -> "-prerelease" because at the time master still had CVC4_EXTRAVERSION set to "-prerelease". This commit fixes CVC4_EXTRAVERSION. | |||
| 2020-06-19 | Update version information post 1.8 release (#4635) | Andres Noetzli | |
| 2020-06-19 | Update info for 1.8 release (#4633) | Andres Noetzli | |
| 2020-06-11 | Fix install of static builds (#4604) | Andres Noetzli | |
| We use CMAKE_INSTALL_PATH to set the installation prefix as an RPATH in the executable. However, for static builds, changing the RPATH fails. This commit changes our build system to only change the CMAKE_INSTALL_PATH if we are doing a shared library build. | |||
| 2020-06-04 | If using 'ninja', tell the user to run 'ninja' not 'make' (#4568) | Andrew V. Jones | |
| ## Issue If you call CVC4's `configure` script with `--ninja`, then you get a misleading status message: ``` [avj@tempvm CVC4]$ ./configure.sh --ninja --python3 | tail -n 5 Now change to 'build' and type make, followed by make check or make install. -- Configuring done -- Generating done -- Build files have been written to: /home/avj/working/CVC4/build ``` ## Solution This commit simply fixes the status message to tell the user to run the correct command based on the specified generator: ``` [avj@tempvm CVC4]$ ./configure.sh --ninja --python3 | tail -n 5 Now change to 'build' and type 'ninja', followed by 'ninja check' or 'ninja install'. -- Configuring done -- Generating done -- Build files have been written to: /home/avj/working/CVC4/build ``` Signed-off-by: Andrew V. Jones <andrew.jones@vector.com> | |||
| 2020-05-22 | Add support for SAT solver Kissat. (#4514) | Aina Niemetz | |
| 2020-03-31 | Remove replay and use-theory options and idl (#4186) | Andrew Reynolds | |
| Towards disentangling Options / NodeManager / SmtEngine. This PR removes options --use-theory=NAME and --replay/--replay-log. Both of these options are highly complex, unused, and lead to complications when implementing the way options and our build system work. The first is motivated by making TheoryEngine use an "alternate" theory, which appears to e.g. make it so that TheoryIdl could entirely replace TheoryArith. I believe this is too heavy handed of a solution: there should a consistent TheoryArith class, and options should be used to enable/disable alternate modules within it. The second attempts to replay low level decisions from the SAT solver. It is documented as not working (in 1.0). I do not believe this is worth salvaging. It also removes the solver in src/theory/idl, which cannot be enabled after this commit. | |||
| 2020-03-09 | Increase stack size for Windows builds to 100 MB (#3943) | Andres Noetzli | |
| Fixes #3528. The default stack size for Windows builds is very limited (it seems to be 1 MB). This leads to problems for some of our users' benchmarks (see the previously mentioned issue and another email that we've received recently). Bumping the stack size to 100 MB seems to solve the issues for the benchmarks that we have received. This of course does not mean that we shouldn't continue working towards making less of our code recursive. | |||
| 2020-03-05 | Enable -Wshadow and fix warnings. (#3909) | Mathias Preiner | |
| Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally. Co-authored-by: Clark Barrett <barrett@cs.stanford.edu> Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com> Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com> Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu> Co-authored-by: makaimann <makaim@stanford.edu> Co-authored-by: yoni206 <yoni206@users.noreply.github.com> Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com> Co-authored-by: AleksandarZeljic <zeljic@stanford.edu> Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com> Co-authored-by: Amalee <amaleewilson@gmail.com> Co-authored-by: Scott Kovach <dskovach@gmail.com> Co-authored-by: ntsis <nekuna@gmail.com> | |||
| 2020-02-19 | Add Python bindings using Cython -- see below for more details (#2879) | makaimann | |
| 2020-02-11 | cmake: Remove unused ENABLE_OPTIMIZED option. (#3749) | Mathias Preiner | |
| 2020-02-10 | cmake: Use ld.gold if available for faster link times. (#3738) | Mathias Preiner | |
| 2019-12-19 | Define all options modified by ENABLE_BEST using cvc4_option (#3578) | Simon Dierl | |
| Signed-off-by: Simon Dierl <simon.dierl@cs.tu-dortmund.de> | |||
| 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 | |
 |
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