diff --git a/src/api/python/pyproject.toml b/src/api/python/pyproject.toml index 380744c87..71de3dcb6 100644 --- a/src/api/python/pyproject.toml +++ b/src/api/python/pyproject.toml @@ -1,3 +1,52 @@ [build-system] requires = ["setuptools>=70"] build-backend = "setuptools.build_meta" + +[project] +name = "z3-solver" +description = "an efficient SMT solver library" +readme = "README.txt" +requires-python = ">=3.8" +license = "MIT" +authors = [ + {name = "The Z3 Theorem Prover Project"} +] +maintainers = [ + {name = "Audrey Dutcher and Nikolaj Bjorner", email = "audrey@rhelmot.io"} +] +keywords = ["z3", "smt", "sat", "prover", "theorem"] +classifiers = [ + "Development Status :: 5 - Production/Stable", + "Intended Audience :: Developers", + "Intended Audience :: Science/Research", + "Operating System :: OS Independent", + "Programming Language :: Python :: 3", + "Programming Language :: Python :: 3.8", + "Programming Language :: Python :: 3.9", + "Programming Language :: Python :: 3.10", + "Programming Language :: Python :: 3.11", + "Programming Language :: Python :: 3.12", + "Topic :: Scientific/Engineering", + "Topic :: Scientific/Engineering :: Mathematics", + "Topic :: Software Development :: Libraries :: Python Modules", +] +dependencies = [ + "importlib-resources; python_version < '3.9'" +] +dynamic = ["version"] + +[project.urls] +Homepage = "https://github.com/Z3Prover/z3" +"Bug Reports" = "https://github.com/Z3Prover/z3/issues" +Repository = "https://github.com/Z3Prover/z3" +Documentation = "http://z3prover.github.io/api/html/z3.html" + +[tool.setuptools] +packages = ["z3"] +include-package-data = true + +[tool.setuptools.package-data] +z3 = ["lib/*", "include/*.h", "include/c++/*.h"] + +[tool.setuptools.dynamic] +version = {attr = "z3_version.__version__"} diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 4d26367b3..49adc8e49 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -112,21 +112,27 @@ def _clean_native_build(): rmtree(BUILD_DIR) def _z3_version(): - post = os.getenv('Z3_VERSION_SUFFIX', '') - if RELEASE_DIR is None: - fn = os.path.join(SRC_DIR, 'scripts', 'mk_project.py') - if os.path.exists(fn): - with open(fn) as f: - for line in f: - n = re.match(r".*set_version\((.*), (.*), (.*), (.*)\).*", line) - if not n is None: - return n.group(1) + '.' + n.group(2) + '.' + n.group(3) + '.' + n.group(4) + post - return "?.?.?.?" - else: - version = RELEASE_METADATA[0] - if version.count('.') == 2: - version += '.0' - return version + post + # Import version from z3_version module for consistency + try: + from z3_version import get_version + return get_version() + except ImportError: + # Fallback to original implementation + post = os.getenv('Z3_VERSION_SUFFIX', '') + if RELEASE_DIR is None: + fn = os.path.join(SRC_DIR, 'scripts', 'mk_project.py') + if os.path.exists(fn): + with open(fn) as f: + for line in f: + n = re.match(r".*set_version\((.*), (.*), (.*), (.*)\).*", line) + if not n is None: + return n.group(1) + '.' + n.group(2) + '.' + n.group(3) + '.' + n.group(4) + post + return "?.?.?.?" + else: + version = RELEASE_METADATA[0] + if version.count('.') == 2: + version += '.0' + return version + post def _configure_z3(): global IS_SINGLE_THREADED @@ -284,7 +290,7 @@ class sdist(_sdist): # The Azure Dev Ops pipelines use internal OS version tagging that don't correspond # to releases. -internal_build_re = re.compile("(.+)\_7") +internal_build_re = re.compile(r"(.+)\_7") class bdist_wheel(_bdist_wheel): diff --git a/src/api/python/test_dist_info.py b/src/api/python/test_dist_info.py new file mode 100755 index 000000000..13337419a --- /dev/null +++ b/src/api/python/test_dist_info.py @@ -0,0 +1,129 @@ +#!/usr/bin/env python3 +""" +Test script to validate that z3-solver creates dist-info when installed from source. +This test ensures that downstream packages can detect z3-solver properly. +""" + +import subprocess +import sys +import tempfile +import os +import shutil +from pathlib import Path + +def test_source_install_creates_dist_info(): + """Test that installing z3-solver from source creates dist-info directory.""" + print("Testing that source installation creates dist-info...") + + # Create a temporary virtual environment + with tempfile.TemporaryDirectory() as tmpdir: + venv_path = Path(tmpdir) / "test_venv" + + # Create virtual environment + result = subprocess.run([sys.executable, "-m", "venv", str(venv_path)], + capture_output=True, text=True) + if result.returncode != 0: + print(f"Failed to create venv: {result.stderr}") + return False + + # Determine the path to pip in the virtual environment + if sys.platform == "win32": + pip_path = venv_path / "Scripts" / "pip.exe" + python_path = venv_path / "Scripts" / "python.exe" + else: + pip_path = venv_path / "bin" / "pip" + python_path = venv_path / "bin" / "python" + + # Upgrade pip and setuptools + result = subprocess.run([str(pip_path), "install", "--upgrade", "pip", "setuptools"], + capture_output=True, text=True) + if result.returncode != 0: + print(f"Failed to upgrade pip/setuptools: {result.stderr}") + return False + + # Get the path to the z3 python package + z3_python_path = Path(__file__).parent.absolute() + + # Install z3-solver in editable mode without deps to avoid building C++ components + result = subprocess.run([str(pip_path), "install", "--no-deps", "--no-build-isolation", + "-e", str(z3_python_path)], + capture_output=True, text=True) + if result.returncode != 0: + print(f"Failed to install z3-solver: {result.stderr}") + return False + + # Check that dist-info directory was created + site_packages = venv_path / "lib" / f"python{sys.version_info.major}.{sys.version_info.minor}" / "site-packages" + if sys.platform == "win32": + site_packages = venv_path / "Lib" / "site-packages" + + dist_info_dirs = list(site_packages.glob("z3_solver*.dist-info")) + if not dist_info_dirs: + print(f"ERROR: No dist-info directory found in {site_packages}") + print("Available directories:") + for item in site_packages.iterdir(): + if item.is_dir(): + print(f" {item.name}") + return False + + dist_info_dir = dist_info_dirs[0] + print(f"SUCCESS: Found dist-info directory: {dist_info_dir.name}") + + # Check that the METADATA file exists and has proper content + metadata_file = dist_info_dir / "METADATA" + if not metadata_file.exists(): + print(f"ERROR: METADATA file not found in {dist_info_dir}") + return False + + metadata_content = metadata_file.read_text() + if "Name: z3-solver" not in metadata_content: + print(f"ERROR: METADATA file doesn't contain expected package name") + return False + + print("SUCCESS: METADATA file contains correct package information") + + # Test that the package can be detected by pip + result = subprocess.run([str(pip_path), "show", "z3-solver"], + capture_output=True, text=True) + if result.returncode != 0: + print(f"ERROR: pip show z3-solver failed: {result.stderr}") + return False + + if "Name: z3-solver" not in result.stdout: + print(f"ERROR: pip show output doesn't contain expected package name") + return False + + print("SUCCESS: pip can detect the installed package") + + # Test that Python can detect the package + python_test_script = ''' +import sys +try: + import importlib.metadata as metadata + dist = metadata.distribution("z3-solver") + print(f"Found package: {dist.name} {dist.version}") + sys.exit(0) +except metadata.PackageNotFoundError: + print("ERROR: Package not found by importlib.metadata") + sys.exit(1) +''' + + result = subprocess.run([str(python_path), "-c", python_test_script], + capture_output=True, text=True) + if result.returncode != 0: + print(f"ERROR: Python package detection failed: {result.stderr}") + return False + + print("SUCCESS: Python can detect the installed package") + print(f"Detection output: {result.stdout.strip()}") + + return True + +if __name__ == "__main__": + success = test_source_install_creates_dist_info() + if success: + print("\n✓ All tests passed! Source installation creates proper dist-info.") + sys.exit(0) + else: + print("\n✗ Test failed! Source installation does not create proper dist-info.") + sys.exit(1) \ No newline at end of file diff --git a/src/api/python/z3_version.py b/src/api/python/z3_version.py new file mode 100644 index 000000000..debb328e4 --- /dev/null +++ b/src/api/python/z3_version.py @@ -0,0 +1,40 @@ +""" +Version detection for z3-solver package. +""" +import os +import re + +def get_version(): + """Get the z3 version from the source tree.""" + post = os.getenv('Z3_VERSION_SUFFIX', '') + + # Determine where the source directory is located + ROOT_DIR = os.path.abspath(os.path.dirname(__file__)) + SRC_DIR_LOCAL = os.path.join(ROOT_DIR, 'core') + SRC_DIR_REPO = os.path.join(ROOT_DIR, '..', '..', '..') + SRC_DIR = SRC_DIR_LOCAL if os.path.exists(SRC_DIR_LOCAL) else SRC_DIR_REPO + + # Check if we're using a release directory + RELEASE_DIR = os.environ.get('PACKAGE_FROM_RELEASE', None) + + if RELEASE_DIR is None: + fn = os.path.join(SRC_DIR, 'scripts', 'mk_project.py') + if os.path.exists(fn): + with open(fn) as f: + for line in f: + n = re.match(r".*set_version\((.*), (.*), (.*), (.*)\).*", line) + if not n is None: + return n.group(1) + '.' + n.group(2) + '.' + n.group(3) + '.' + n.group(4) + post + return "4.15.3.0" + post # fallback version + else: + RELEASE_METADATA = os.path.basename(RELEASE_DIR).split('-') + if RELEASE_METADATA[0] == 'z3' and len(RELEASE_METADATA) >= 4: + RELEASE_METADATA.pop(0) + version = RELEASE_METADATA[0] + if version.count('.') == 2: + version += '.0' + return version + post + return "4.15.3.0" + post # fallback version + +# Make version available at module level +__version__ = get_version() \ No newline at end of file