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 updates the cvc5 Java API documentation to explain how to use
the cvc5 Java bindings in a Maven project. It also updates the output
obtained when building the Java bindings from source.
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.
The `Length` function in the Pythonic API applies to both strings and
sequences, so its documentation appears in `strings.rst` and
`sequences.rst`. To avoid duplicate entries in the index, one occurrence
is marked with `:noindex:`.
This PR addresses two issues reported by Sphinx. First, the
`docs/api/python/base/modes.rst` document was not included in any
toctree. Second, the `proofrule.rst` and `cvc5proofrule.rst` documents
were included in multiple toctrees. The latter is resolved by including
each document in only one toctree and referencing it elsewhere in the
documentation using cross-references.
This PR updates the Doxyfile using the `doxygen -u` command, removing
several obsolete tags from the configuration file as detected by the
Doxygen version used in CI.
This PR raises the quality standard for the cvc5 Java API documentation
by treating all warnings reported by Javadoc (in Java 21) as errors and
by addressing the remaining warnings in the source code. Since newer
versions of Javadoc catch more issues than older ones, this PR uses the
current Long-Term Support (LTS) release of Java (version 21) to generate
the documentation. However, it continues to use Java 8 in the workflow
jobs that build the JAR files for releases in order to maintain backward
compatibility with the older Java version.
---------
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
This PR introduces the new C++ methods `Term TermManager::mkString(const
std::u32string& s)` and `std::u32string Term::getU32StringValue()` to
replace old methods `Term TermManager::mkString(const std::wstring& s)`
and `std::wstring Term::getStringValue()`.
The reason for this change is that `wchar_t` has a platform-dependent
size: on Windows, it is 16-bit (UTF-16), while on Linux and macOS, it is
32-bit (UTF-32). However, the current implementation assumes that
`wchar_t` is always 32 bits. In contrast, `char32_t` and
`std::u32string` are explicitly designed for Unicode and have consistent
32-bit size across platforms.
Similarly, this PR also introduces C functions
`cvc5_mk_string_from_char32` and `cvc5_term_get_u32string_value`
to replace old functions `cvc5_mk_string_from_wchar` and
`cvc5_term_get_string_value`.
Although `char32_t` is part of the C11 standard, the `<uchar.h>` header
(which should define `char32_t`) is missing in Apple Clang. Therefore,
we explicitly provide a definition in such cases.
---------
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
After this change, the Java API first attempts to locate native
libraries as resources within a JAR before searching system paths. If
the Java API is packaged in a self-contained JAR, it will prioritize the
native libraries within the JAR, as they are more likely to be
compatible with the API version included in the JAR.
This PR also fixes and enhances error handling when searching for and
loading the native libraries.
It also replaces calls to deprecated functions of `Solver` with the
corresponding function of `TermManager`.
---------
Co-authored-by: mudathirmahgoub <mudathirmahgoub@gmail.com>
