| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-08-10 | Disable external initialization of `thread_local` variables (#7004) | Andres Noetzli | |
| This commit adds `-fno-extern-tls-init` to the list of compiler flags to tell the compiler that it can assume that there is no dynamic initialization of thread-local variables in non-defining translation units. This option should result in better performance and works around crashing issues with our Windows build. | |||
| 2021-07-23 | Configuration: Indicate dependencies being built (#6921) | Andres Noetzli | |
| This commit changes the output of our configuration to show which dependencies are being built as part of the cvc5 build. For example: ``` ABC : off CryptoMiniSat : off GLPK : off Kissat : off LibPoly : on (local) CoCoALib : off Build libcvc5 only : off MP library : gmp (system) Editline : off ``` Indicates that `LibPoly` was not found in the system and is thus built as part of the cvc5 build and GMP was found in the system. | |||
| 2021-06-24 | cmake: Add new code coverage targets. (#6796) | Mathias Preiner | |
| This commit adds the following new code coverage targets: - coverage-reset: Resets the code coverage counters - coverage: Generates code coverage report for all cvc5 executions since the last coverage-reset - coverage-test: This was previously the coverage target that runs the tests and generates the coverage report (as used for nightlies). By using `make coverage-reset` and `make coverage` it is now possible to generate coverage reports for arbitrary executions of cvc5. | |||
| 2021-06-21 | Make CaDiCaL a required dependency. (#6761) | Mathias Preiner | |
| Since the new BV solver is enabled by default and uses CaDiCaL (and optionally CryptoMiniSat) we make CaDiCaL a required dependency. | |||
| 2021-06-16 | Make symfpu a required dependency. (#6749) | Aina Niemetz | |
| 2021-06-15 | Add cocoalib (#6731) | Gereon Kremer | |
| This PR adds CoCoALib as an optional dependency. It will be used in the CAD-based nonlinear solver for computer algebra routines beyond the capabilities of libpoly like quotient rings and polynomial factorization. | |||
| 2021-05-25 | [Unit tests] Fix path of Java bindings (#6616) | Andres Noetzli | |
| Currently, when configuring cvc5 with Java bindings, CMake complains about `get_filename_component(CVC5_JNI_PATH ${CVC5_JAR_PATH} DIRECTORY)` not using the correct number of arguments in the Java unit tests. The issue is that `${CVC5_JAR_PATH}` is empty. The value of `${CVC5_JAR_PATH}` was computed in the Java API bindings but then not shared with the rest of the build system. Because `${CVC5_JAR_PATH}` is not used anywhere else, this commit moves the computation of `${CVC5_JAR_PATH}` to the unit tests. The commit also ensures that the API subdirectories are processed before the test subdirectories. | |||
| 2021-04-22 | cmake: Do not require --auto-download for already downloaded dependencies. ↵ | Mathias Preiner | |
| (#6417) This will look for already downloaded dependencies in the build directory and therefore will not require --auto-download if the dependencies were already downloaded in a previous build. | |||
| 2021-04-22 | Remove unused stuff from options setup (#6422) | Gereon Kremer | |
| This PR removes some old stuff from our options setup that has not been used in a long time. Most prominently, this includes the man pages that were still generated, and the alias and links options, which no longer worked anyway. | |||
| 2021-04-21 | Goodbye CVC4, hello cvc5! (#6371) | Mathias Preiner | |
| This commits changes the build system to cvc5 and removes the remaining occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/. | |||
| 2021-04-16 | Refactor cmake: auto-download and default-on dependencies (#6355) | Gereon Kremer | |
| This PR changes a few things in how dependencies are handled during configuration: - --x-dir are removed for most dependencies, use the generic --dep-path instead - the cmake ENABLE_AUTO_DOWNLOAD determines whether we attempt to download missing dependencies ourselves - external projects check this option and send an error if it is OFF - some optional dependencies are enabled by default (CaDiCaL, Poly, SymFPU) This will essentially fail every call to ./configure.sh until the user specifies --auto-download. | |||
| 2021-04-12 | Only require GMP 6.1 (#6332) | Gereon Kremer | |
| The recent refactoring of the dependencies raised the required GMP version to 6.2 for no particular reason. This PR reverts this change to only require GMP 6.1 again. | |||
| 2021-04-12 | Refactor and update copyright headers. (#6316) | Aina Niemetz | |
| 2021-04-09 | Rename CVC4_ macros to CVC5_. (#6327) | Aina Niemetz | |
| 2021-04-07 | New C++ Api: Initial setup of Api documentation. (#6295) | Aina Niemetz | |
| This configures the initial setup for generating Api documentation with Sphinx via Breathe and Doxygen. All fixes in the documentation of the cvc5.h header are for the purpose of eliminating warnings. This PR does not check for completeness of the documentation, and does not yet tweak the documentation to be nice, beautiful and consistent, which is postponed to future PRs. Configure with `--docs`, and then make. This will generate a `docs` directory in the build directory. The Sphinx documentation can be found at `build/docs/sphinx/index.html`. Doxygen documentation is only generated as xml under `build/docs/doxygen`. This PR further proposes a new style for copyright headers. If this style is approved, I will submit a PR to update the update_copyright.pl script. | |||
| 2021-04-01 | Refactor CLN dependency & Cleanup (#6251) | Gereon Kremer | |
| This PR migrates CLN to a new Find script and adds the possibility to install CLN if not found in the system. Also, it does a bit of cleanup. | |||
| 2021-03-29 | Fix configuration printing. (#6236) | Aina Niemetz | |
| 2021-03-27 | Refactor ANTLR3 dependency (#6202) | Gereon Kremer | |
| This PR refactors our first, and arguably most fragile, dependency. Right now all dependencies need to be manually installed (by calling the appropriate contrib/get-X script). For optional dependencies, we additionally need to enable them when calling the configure script (or via ccmake). This PR is the first step in refactoring all dependencies to be automatically build (if required) as an external project. Note that this not only eliminates the need to call contrib scripts, but also simplifies cross compilation: as all dependencies are now built within the build folders, every build folder has its own copy which may use different toolchains. | |||
| 2021-03-26 | Use color output to print configuration. (#6219) | Aina Niemetz | |
| 2021-03-23 | Removing unused build options and deprecated proof compile flag (#6195) | Haniel Barbosa | |
| 2021-03-20 | Generate cvc/Kind.java for the java API (#6143) | mudathirmahgoub | |
| PR changes: Refactor python/genkinds.py by separating parsing from file generation. Add java/genkinds.py to generate file Kind.java. Enable java API in ./configure.sh with "under development" warning. | |||
| 2021-03-16 | ci: Enable checking of proofs + unsat cores. (#6088) | Mathias Preiner | |
| This commit refactors the run_regression.py script and adds options for enabling/disabling checking of proofs and unsat cores. Both options are enabled by default and disabled for each corresponding CI build. | |||
| 2021-03-16 | cmake: Generate cvc4_export.h and set visibility to hidden. (#6139) | Mathias Preiner | |
| The build system (cmake) will automatically generate an export header cvc4_export.h, which makes sure that the correct export features are defined depending on the compiler and target platform. The macro CVC4_EXPORT replaces CVC4_PUBLIC and its usage is reduced by 2/3. Co-authored-by: Gereon Kremer <nafur42@gmail.com> | |||
| 2021-03-10 | cmake: Fix optimization level for debug builds. (#6097) | Mathias Preiner | |
| Further cleans up some unused variables and moves the configuration of best to configure.sh. | |||
| 2021-03-09 | Update copyright headers to 2021. (#6081) | Aina Niemetz | |
| 2021-03-04 | Add cmake scripts for iwyu targets. (#6042) | Gereon Kremer | |
| This PR adds some utility targets that simplify the usage of iwyu (include-what-you-use) on our code base. | |||
| 2021-03-03 | Remove obsolete gcc check. (#6041) | Gereon Kremer | |
| This PR removes a cmake check for gcc 4.5.1. As this version is more than a decade old and would not work anyway, as it does not fully support C++11, not to mention C++17. | |||
| 2021-03-02 | Remove obsolete dependency on CxxTest. (#6038) | Aina Niemetz | |
| 2021-03-01 | Make -Werror optional but enable it for CI. (#6032) | Mathias Preiner | |
| 2021-02-24 | Enable -Werror. (#5969) | Mathias Preiner | |
| 2021-02-23 | Switch to C++17. (#5959) | Mathias Preiner | |
| Co-authored-by: Gereon Kremer <nafur42@gmail.com> | |||
| 2021-02-09 | cmake: Make Python3 default and improve toml error messages. (#5884) | Mathias Preiner | |
| ./configure.sh will now fail if Python3 is not installed on the system. Since Python2 is now deprecated the user has to explicitly enable it via --python2. This commit also removes the --python3 configure flag. | |||
| 2020-12-01 | google test: Infrastructure and first api test. (#5548) | Aina Niemetz | |
| This sets up the infrastructure for migrating unit tests from CxxTest to Google Test. It further migrates api/datatype_api_black to the new infrastructure. | |||
| 2020-10-05 | cmake: Add warning when unit testing is disabled due to assertions being ↵ | Aina Niemetz | |
| disabled. (#5204) This further fixes the testing instructions for API tests (formerly known as system tests) in INSTALL.md. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com> | |||
| 2020-09-22 | Update 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-17 | Do not allow to build Python bindings if building statically (#4784) | Andrew V. Jones | |
| This PR disables building the Python bindings if you're doing a static build (which makes sense, because there's no such thing as a "static" Python module). Signed-off-by: Andrew V. Jones andrew.jones@vector.com | |||
| 2020-09-02 | Drop {INCLUDE,LIBRARY,RUNTIME}_INSTALL_DIR variables in CMakeLists.txt (#4979) | FabianWolff | |
| On Debian (for instance), libraries aren't installed into `/usr/lib/`, but into something like `/usr/lib/x86_64-linux-gnu/`. In particular, this means that setting the `LIBRARY_INSTALL_DIR` to `lib` in the top-level `CMakeLists.txt` file is wrong. Luckily, there is a simple solution: CMake provides [`CMAKE_INSTALL_LIBDIR`](https://cmake.org/cmake/help/v3.0/module/GNUInstallDirs.html) for this very purpose, which has sensible defaults and can be set by the user. In particular, since `CMAKE_INSTALL_LIBDIR` is a standardized variable, tools like the ones used for building Debian packages can set it to what they want it to be, whereas using a custom variable like `LIBRARY_INSTALL_DIR` wouldn't work in this setting. Signed-off-by: Fabian Wolff <fabi.wolff@arcor.de> | |||
| 2020-09-02 | Use SMT-COMP configuration for competition build (#4995) | Andres Noetzli | |
| This commit changes our `competition` build to include the libraries that we have used for SMT-COMP by default. This makes it easier for users to reproduce our SMT-COMP configuration for performance measurements. We are using GPL libraries for this build type, so the commit adds color to highlight the fact that this build type produces a GPL build. | |||
| 2020-09-01 | [API] Fix Python Examples (#4943) | Andres Noetzli | |
| When testing the API examples, Python examples were not included. This commit changes that and fixes multiple minor issues that came up once the tests were enabled: - It adds `Solver::supportsFloatingPoint()` as an API method that returns whether CVC4 is configured to support floating-point numbers or not (this is useful for failing gracefully when floating-point support is not available, e.g. in the case of our floating-point example). - It updates the `expections.py` example to use the new API. - It fixes the `sygus-fun.py` example. The example was passing a _set_ of non-terminals to `Solver::mkSygusGrammar()` but the order in which the non-terminals are passed in matters because the first non-terminal is considered to be the starting terminal. The commit also updates the documentation of that function. - It fixes the Python API for datatypes. The `__getitem__` function had a typo and the `datatypes.py` example was crashing as a result. | |||
| 2020-08-12 | Add 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-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 | |
 |
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