mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
e0ec61e050
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.
82 lines
2.3 KiB
ReStructuredText
82 lines
2.3 KiB
ReStructuredText
Python API
|
|
==========
|
|
|
|
.. only:: not bindings_python
|
|
|
|
.. warning::
|
|
|
|
This documentation was built while python bindings were disabled. This part of the documentation is likely either empty or outdated. Please enable :code:`BUILD_BINDINGS_PYTHON` in :code:`cmake` and build the documentation again.
|
|
|
|
cvc5 offers two separate APIs for Python users.
|
|
The :doc:`base Python API <base/python>` is an almost exact copy of the
|
|
:doc:`C++ API <../cpp/cpp>`.
|
|
Alternatively, the :doc:`pythonic API <pythonic/pythonic>` is a more pythonic
|
|
API that aims to be fully compatible with `Z3s Python API
|
|
<https://z3prover.github.io/api/html/namespacez3py.html>`_ while adding
|
|
functionality that Z3 does not support.
|
|
|
|
.. toctree::
|
|
:maxdepth: 1
|
|
|
|
pythonic/pythonic
|
|
base/python
|
|
|
|
|
|
Which Python API should I use?
|
|
------------------------------
|
|
|
|
If you are a new user, or already have an application that uses Z3's python
|
|
API, use the :doc:`pythonic API <pythonic/pythonic>`.
|
|
If you would like a more feature-complete---yet verbose---python API, with the
|
|
ability to do almost everything that the cpp API allows, use the :doc:`base
|
|
Python API <base/python>`.
|
|
|
|
You can compare examples using the two APIs by visiting the :doc:`examples page
|
|
<../../examples/quickstart>`.
|
|
|
|
|
|
Installation (from PyPi)
|
|
------------------------
|
|
|
|
The base and pythonic Python API can be installed via `pip` as follows:
|
|
|
|
.. code:: bash
|
|
|
|
pip install cvc5
|
|
|
|
|
|
Installation (from source)
|
|
--------------------------
|
|
|
|
The base and pythonic Python API can also be installed from source following
|
|
these steps:
|
|
|
|
.. code:: bash
|
|
|
|
git clone https://github.com/cvc5/cvc5.git
|
|
cd cvc5
|
|
./configure.sh --python-bindings --auto-download
|
|
cd build
|
|
make # add -jN for parallel build using N threads
|
|
make install
|
|
|
|
The last step installs both the cvc5 binary and the Python bindings.
|
|
If you want to install only the Python bindings, run the following
|
|
command instead of ``make install``:
|
|
|
|
.. code:: bash
|
|
|
|
cmake --install . --component python-api
|
|
|
|
For Windows, the steps above must be executed in
|
|
a MINGW64 or CLANGARM64 environment with the required
|
|
dependencies installed
|
|
(see the :doc:`installation instructions <../../installation/installation>`).
|
|
|
|
Finally, you can make sure that it works by running:
|
|
|
|
.. code:: bash
|
|
|
|
python3
|
|
import cvc5
|