This PR replaces the MSYS2 MINGW64 environment with the CLANG64
environment for compiling cvc5 natively on Windows x86_64. The main
difference between the two is that MINGW64 uses GCC and links against
libstdc++ and the MSVCRT runtime, whereas CLANG64 uses Clang and links
against libc++ and the UCRT runtime (see the MSYS2 [environment
documentation](https://www.msys2.org/docs/environments/) for details).
This ensures compatibility for statically linking cvc5 with Lean
binaries that use libc++ on Windows x86_64, thus facilitating the
integration of cvc5 into
[lean-cvc5](https://github.com/abdoo8080/lean-cvc5).
---------
Co-authored-by: Abdalrhman Mohamed <abdoo8080@outlook.com>
This PR applies several changes required to compile cvc5 on Windows
ARM64 using MSYS2 CLANGARM64. In particular, `thread_local` class fields
and local function variables in classes and functions exported in the
API are not allowed, so they have been converted into global variables
within the compilation unit. Moreover, some functions in the cvc5 parser
library were using non-exported functions from the cvc5 base library.
This PR exports these functions and converts the ones that were inlined
into non-inlined functions to make them exportable.
Here is a summary of the results of running the cvc5 version in main and
in this branch:
```
config status total solved sat unsat best timeout memout error uniq dis time_cpu memory
main ee 450474 385375 173928 211447 256627 57617 719 5 36 0 18909500.3 42742499.9
pr ee 450474 385370 173923 211447 192564 57621 720 5 31 0 18914388.1 42779989.7
```
It seems that the Windows ARM64 changes do not significantly affect
solver performance compared to the main branch.
I always forget what packages I need to install inside of a venv to build cvc5. This PR adds two requirements.txt files:
requirements_build.txt for the Python packages you need to install to build cvc5
requirements_python_dev.txt for the Python packages you need to build cvc5's Python bindings
Signed-off-by: Andrew V. Teylu andrew@tey.lu
The toml module does not support the latest TOML standard and has not released a new version since 2020. This PR moves from toml to tomli for python < 3.11.0. For 3.11.0 and later, python ships with a tomllib module, based on tomli.
Signed-off-by: Jerry James <loganjerry@gmail.com>
This PR does multiple things:
- the kinds are changed from custom objects to a proper enum.Enum class
(including according changes to the cython code and the kind generation scripts)
- all examples and tests are modified to account for the change how to use kinds
(Kind instead of kinds)
- add docstrings to the kind enum values
- add a custom documenter that properly renders enums via autodoc
- extend doxygen setup so that we can write comments as rst (allowing us to copy
the documentation for kinds from the cpp api to the other apis)
This PR includes documentation for the z3py compatibility API into our general API.
It does so by adding the z3py compatibility API as an external project to download it and then have sphinx document it via the autodoc extension that we already use for our regular python API.
Right now we simply show everything on one page, which should be refactored in the future.
This PR adds documentation to the python class Op, Grammar, Result, and for API enums.
Additionally, documentation for isNull functions in the datatype classes is added for the python API, and a small change in the cpp API documentation is introduced.
