Can Python bindings use external libz3.so?

[yurivict]

In the version 4.8.17 the distutils build in src/api/python rebuilds z3 binaries but then it only installs Python's platform independent files.

How to reuse the pre-installed libz3.so?

The build should either build and install binaries, or it should not build and not install them. The way how it is now, when they are built and not installed, is wasteful and inconsistent.

FreeBSD 14.1

[NikolajBjorner]

It isn't possible to respond to issues for downlevel z3. Maybe the same issue holds for 4.13.1. You can build with cmake where the installation logic is going to be more streamlined than the python build.

[yurivict]

@NikolajBjorner

In the version 4.13.2 cmake based build fails:

===>  Building for py311-z3-solver-4.13.2
[  0% 2/3] cd /usr/ports/math/py-z3-solver/work-py311/.build && /usr/local/bin/python3.11 /usr/ports/math/py-z3-solver/work-py311/z3-z3-4.13.2/src/api/python/scripts/update_api.py --z3py-output-dir /usr/ports/math/py-z3-solver/work-py311/.build/python
usage: update_api.py [-h] [--api_output_dir API_OUTPUT_DIR] [--z3py-output-dir Z3PY_OUTPUT_DIR] [--dotnet-output-dir DOTNET_OUTPUT_DIR] [--java-input-dir JAVA_INPUT_DIR]
                     [--java-output-dir JAVA_OUTPUT_DIR] [--java-package-name JAVA_PACKAGE_NAME] [--ml-src-dir ML_SRC_DIR] [--ml-output-dir ML_OUTPUT_DIR]
                     api_files [api_files ...]
update_api.py: error: the following arguments are required: api_files

The "api_files" argument is expected by update_api.py but the cmake script that calls update_api.py doesn't supply this argument.

In the above I am running cmake in the src/api/python subdirectory because I need to build the Python extension, and not the rest of the Z3 project.

[NikolajBjorner]

In the above I am running cmake in the src/api/python subdirectory because I need to build the Python extension, and not the rest of the Z3 project.

I don't understand this.

1. What precisely are the repro steps for what you are doing?
2. Are you trying to build z3 python bindings in a non-standard way? If the standard way works, then why should the non-standard way be supported?

[yurivict]

I don't understand this.

1. What precisely are the repro steps for what you are doing?

I do this: cd src/api/python && cmake . && gmake

Are you trying to build z3 python bindings in a non-standard way?

We have the Z3 project (C++ code) in a separate port/package. Now we need to build the Python part based on the C++ part. The Python part should just link to libz3.so that is pre-installed. This is the standard way of handling Python bindings.

[NikolajBjorner]

The CMakeLists.txt isn't set up for this:

cd src/api/python && cmake .

C:\z3\src\api\python>cmake .
CMake Warning (dev) in CMakeLists.txt:
  No project() command is present.  The top-level CMakeLists.txt file must
  contain a literal, direct call to the project() command.  Add a line of
  code such as

    project(ProjectName)

  near the top of the file, but after cmake_minimum_required().

  CMake is pretending there is a "project(Project)" command on the first
  line.

[yurivict]

The CMakeLists.txt isn't set up for this:

How can multiple python bindings for multiple Python versions be built? Do we have to always also rebuild the whole Z3 project just to build Python bindings for a different Python version?