Age | Commit message (Collapse) | Author |
|
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.
|
|
Since the new BV solver is enabled by default and uses CaDiCaL
(and optionally CryptoMiniSat) we make CaDiCaL a required dependency.
|
|
|
|
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.
|
|
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.
|
|
(#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.
|
|
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.
|
|
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
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.
|
|
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.
|
|
|
|
|
|
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.
|
|
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.
|
|
|
|
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.
|
|
|
|
|
|
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.
|
|
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.
|
|
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>
|
|
Further cleans up some unused variables and moves the configuration of
best to configure.sh.
|
|
|
|
This PR adds some utility targets that simplify the usage of iwyu (include-what-you-use) on our code base.
|
|
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.
|
|
|
|
|
|
|
|
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
|
|
./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.
|
|
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.
|
|
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>
|
|
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.
|
|
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
|
|
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>
|
|
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.
|
|
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.
|
|
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.
|
|
|
|
## 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>
|
|
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
|
|
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.
|
|
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.
|
|
strings (#4702)
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
|
|
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.
|
|
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.
|
|
|
|
|
|
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.
|
|
## 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>
|