| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 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. | |||
 |
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