| Age | Commit message (Collapse) | Author |
|---|
|
If building with python bindings, check the pytest is installed, and adds a command to run pytest after the existing make check tests. If built without python bindings, it just uses a null command. Note: the current semantics are such that the pytest tests will not run if the ctest run fails (unless you pass the correct flag to make to continue --ignore-errors I believe). I can look into changing this semantics if that would be preferred.
|
|
|
|
|
|
GH introduced a new workflow event pull_request_target that now makes it
possible to cancel builds on the base repository.
|
|
Commit e969318 introduced the ICP-based
solver for nonlinear arithmetic. That code, however, depends on LibPoly.
When configuring CVC4 without LibPoly, the code doesn't compile because
the class ICPSolver is missing. This commit adds a dummy version if
ICPSolver to remedy the issue.
|
|
Cython has been causing issues recently, see e.g.
https://github.com/CVC4/CVC4/pull/4982/checks?check_run_id=1052433862.
It looks like the issue is that globally installed packages can't be
found by Python (maybe the global site-package directories changed/are
not included in the search paths anymore?). This commit changes the
installation of Cython to install it locally to the user instead of
globally. It also adds `bin` in the user base directory to `PATH` s.t.
CMake is able to find the `cython` binary.
|
|
|
|
Since
https://github.com/CVC4/LFSC/commit/1d1c55fa17b08e2bc8cb686b9d07ec63bf0dd4a2
LFSC requires Flex, so we need to install the corresponding packages in
our CI environment. This commit also removes SWIG from the list of
packages to install since we do not use it anymore.
|
|
The previously introduced action to cancel running builds is not able to
cancel builds on other branches, only on the same branch. As a consequence,
when pushing to a branch for which a PR has been submitted, builds on the
main repository are not cancelled.
This removes the cancel build. If we want behavior similar to how it was
on Travis, we need a workaround / more sophisticated solution since GH
Actions doesn't really allow / support this (due to permission issues).
|
|
dependencies (#4809)
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.
|
|
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.
|
|
I noticed recently that getKind for Op and Term was not correct in the python bindings. This PR would add maps to keep track of the Kind objects and the Python names (which are different from the C++ Kind names). Then a Python `kind` only needs the integer representation of a `Kind` to be constructed. Now, in `getKind` it can just pass the integer representation when constructing a `kind`.
|
|
|
|
|
|
Enable CI with GitHub actions, add macOS builds and disable Travis CI.
|
