Merge branch 'parallel-solving' of github.com:ilanashapiro/z3 into parallel-solving

CMakeLists.txt

@@ -4,7 +4,7 @@ cmake_minimum_required(VERSION 3.16)
 set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
 
 # Read version from VERSION.txt file
-file(READ "${CMAKE_CURRENT_SOURCE_DIR}/VERSION.txt" Z3_VERSION_FROM_FILE)
+file(READ "${CMAKE_CURRENT_SOURCE_DIR}/scripts/VERSION.txt" Z3_VERSION_FROM_FILE)
 string(STRIP "${Z3_VERSION_FROM_FILE}" Z3_VERSION_FROM_FILE)
 
 project(Z3 VERSION ${Z3_VERSION_FROM_FILE} LANGUAGES CXX)

MODULE.bazel

@@ -1,6 +1,6 @@
 module(
     name = "z3",
-    version = "4.16.0",  # TODO: Read from VERSION.txt - currently manual sync required
+    version = "4.15.4",  # TODO: Read from VERSION.txt - currently manual sync required
     bazel_compatibility = [">=7.0.0"],
 )
 

README-CMake.md

@@ -119,6 +119,30 @@ target_link_libraries(yourTarget libz3)
 ```
 Note that this is `libz3` not `z3` (`libz3` refers to the library target from `src/CMakeLists.txt`).
 
+#### Using system-installed Z3
+
+If you have Z3 installed on your system (e.g., via package manager or by building and installing Z3 yourself), you can use CMake's `find_package` to locate it:
+
+```cmake
+find_package(Z3 REQUIRED CONFIG)
+```
+
+Once found, you can use the Z3 include directories and libraries:
+
+```cmake
+# For C projects
+target_include_directories(yourTarget PRIVATE ${Z3_C_INCLUDE_DIRS})
+target_link_libraries(yourTarget PRIVATE ${Z3_LIBRARIES})
+
+# For C++ projects  
+target_include_directories(yourTarget PRIVATE ${Z3_CXX_INCLUDE_DIRS})
+target_link_libraries(yourTarget PRIVATE ${Z3_LIBRARIES})
+```
+
+The `find_package(Z3 CONFIG)` approach uses Z3's provided `Z3Config.cmake` file, which is installed to a standard location (typically `<prefix>/lib/cmake/z3/`). If CMake cannot automatically find Z3, you can help it by setting `-DZ3_DIR=<path>` where `<path>` is the directory containing the `Z3Config.cmake` file.
+
+**Note**: This approach requires that Z3 was built and installed using CMake. Z3 installations from the Python build system may not provide the necessary CMake configuration files.
+
 
 
 ### Ninja

scripts/mk_nuget_task.py

@@ -103,7 +103,7 @@ def mk_targets(source_root):
 def mk_icon(source_root):
     mk_dir("out/content")
     shutil.copy(f"{source_root}/resources/icon.jpg", "out/content/icon.jpg")
-#   shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md")
+    shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md")
 
 
     
@@ -124,6 +124,7 @@ Linux Dependencies:
         <copyright>&#169; Microsoft Corporation. All rights reserved.</copyright>
         <tags>smt constraint solver theorem prover</tags>
         <icon>content/icon.jpg</icon>
+        <readme>content/README.md</readme>
         <projectUrl>https://github.com/Z3Prover/z3</projectUrl>
         <license type="expression">MIT</license>
         <repository type="git" url="{1}" branch="{2}" commit="{3}" />

scripts/mk_project.py

@@ -9,7 +9,7 @@ from mk_util import *
 
 def init_version():
     # Read version from VERSION.txt file
-    version_file_path = os.path.join(os.path.dirname(os.path.dirname(__file__)), 'VERSION.txt')
+    version_file_path = os.path.join(os.path.dirname(__file__), 'VERSION.txt')
     try:
         with open(version_file_path, 'r') as f:
             version_str = f.read().strip()

scripts/nightly.yaml

@@ -1,8 +1,8 @@
 variables:
   # Version components read from VERSION.txt (updated manually when VERSION.txt changes)
   Major: '4'
-  Minor: '16'
+  Minor: '15'
-  Patch: '0'
+  Patch: '4'
   ReleaseVersion: $(Major).$(Minor).$(Patch)
   AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)
   NightlyVersion: $(AssemblyVersion)-$(Build.buildId)
@@ -254,9 +254,9 @@ stages:
       inputs:
         artifact: 'MacArm64'
         path: $(Agent.TempDirectory)\package
-    - task: NuGetToolInstaller@0
+    - task: NuGetToolInstaller@1
       inputs:
-        versionSpec: 5.x
+        versionSpec: 6.x
         checkLatest: false        
     - task: PythonScript@0
       displayName: 'Python: assemble files'
@@ -302,9 +302,9 @@ stages:
       inputs:
         artifact: 'WindowsBuild-x86'
         path: $(Agent.TempDirectory)\package
-    - task: NuGetToolInstaller@0
+    - task: NuGetToolInstaller@1
       inputs:
-        versionSpec: 5.x
+        versionSpec: 6.x
         checkLatest: false        
     - task: PythonScript@0
       displayName: 'Python: assemble files'

scripts/release.yml

@@ -6,7 +6,7 @@
 trigger: none
 
 variables:
-  ReleaseVersion: '4.16.0'  # TODO: Auto-read from VERSION.txt when Azure DevOps supports it better
+  ReleaseVersion: '4.15.4'  # TODO: Auto-read from VERSION.txt when Azure DevOps supports it better
 
 stages:
 
@@ -261,9 +261,9 @@ stages:
         artifact: 'MacArm64'
         path: $(Agent.TempDirectory)\package
 
-    - task: NuGetToolInstaller@0
+    - task: NuGetToolInstaller@1
       inputs:
-        versionSpec: 5.x
+        versionSpec: 6.x
         checkLatest: false        
     - task: PythonScript@0
       displayName: 'Python: assemble files'
@@ -305,9 +305,9 @@ stages:
       inputs:
         artifact: 'WindowsBuild-x86'
         path: $(Agent.TempDirectory)\package
-    - task: NuGetToolInstaller@0
+    - task: NuGetToolInstaller@1
       inputs:
-        versionSpec: 5.x
+        versionSpec: 6.x
         checkLatest: false        
     - task: PythonScript@0
       displayName: 'Python: assemble files'
@@ -471,7 +471,7 @@ stages:
 
      
   - job: NuGetPublish
-    condition: eq(1,0)
+    condition: eq(1,1)
     displayName: "Publish to NuGet.org"
     steps:
     - task: DownloadPipelineArtifact@2
@@ -479,9 +479,9 @@ stages:
       inputs:
         artifact: 'NuGetPackage'
         path: $(Agent.TempDirectory)
-    - task: NuGetToolInstaller@0
+    - task: NuGetToolInstaller@1
       inputs:
-        versionSpec: 5.x
+        versionSpec: 6.x
         checkLatest: false
     - task: NuGetCommand@2
       inputs:

scripts/update_version.py

@@ -16,7 +16,7 @@ import sys
 def read_version():
     """Read version from VERSION.txt file."""
     script_dir = os.path.dirname(os.path.abspath(__file__))
-    version_file = os.path.join(os.path.dirname(script_dir), 'VERSION.txt')
+    version_file = os.path.join(script_dir, 'VERSION.txt')
     
     try:
         with open(version_file, 'r') as f:

src/api/julia/CMakeLists.txt

@@ -1,5 +1,32 @@
 find_package(JlCxx REQUIRED)
 
+# Check for Windows MSVC + MinGW library compatibility issues
+if(WIN32 AND CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
+    # Get the JlCxx library path to check its format
+    get_target_property(JLCXX_LIB_PATH JlCxx::cxxwrap_julia IMPORTED_LOCATION)
+    if(NOT JLCXX_LIB_PATH)
+        get_target_property(JLCXX_LIB_PATH JlCxx::cxxwrap_julia IMPORTED_LOCATION_RELEASE)
+    endif()
+    if(NOT JLCXX_LIB_PATH)
+        get_target_property(JLCXX_LIB_PATH JlCxx::cxxwrap_julia IMPORTED_IMPLIB)
+    endif()
+    if(NOT JLCXX_LIB_PATH)
+        get_target_property(JLCXX_LIB_PATH JlCxx::cxxwrap_julia IMPORTED_IMPLIB_RELEASE)
+    endif()
+    
+    if(JLCXX_LIB_PATH AND JLCXX_LIB_PATH MATCHES "\\.dll\\.a$")
+        message(FATAL_ERROR 
+            "Julia bindings build error: Incompatible CxxWrap library format detected.\n"
+            "The found libcxxwrap_julia library (${JLCXX_LIB_PATH}) is a MinGW import library (.dll.a), "
+            "but Z3 is being built with MSVC which requires .lib format.\n\n"
+            "Solutions:\n"
+            "1. Use MinGW/GCC instead of MSVC to build Z3\n"
+            "2. Install a MSVC-compatible version of CxxWrap\n"
+            "3. Disable Julia bindings with -DZ3_BUILD_JULIA_BINDINGS=OFF\n\n"
+            "For more information, see: https://github.com/JuliaInterop/CxxWrap.jl#compiling-the-c-code")
+    endif()
+endif()
+
 add_library(z3jl SHARED z3jl.cpp)
 target_link_libraries(z3jl PRIVATE JlCxx::cxxwrap_julia libz3)
 target_include_directories(z3jl PRIVATE

src/api/python/setup.py

@@ -113,14 +113,21 @@ def _clean_native_build():
 
 def _z3_version():
     post = os.getenv('Z3_VERSION_SUFFIX', '')
+    print("z3_version", "release dir", RELEASE_DIR)   
     if RELEASE_DIR is None:
-        fn = os.path.join(SRC_DIR_REPO, 'VERSION.txt')
+        dirs = [SRC_DIR, ROOT_DIR, SRC_DIR_REPO, SRC_DIR_LOCAL, os.path.join(ROOT_DIR, '..', '..')]
-        if os.path.exists(fn):
+        for d in dirs:
-            with open(fn) as f:
+            if os.path.exists(d):
-                for line in f:
+               print(d, ": ", os.listdir(d))
-                    n = re.match(r"(.*)\.(.*)\.(.*)\.(.*)", line)
+        fns = [os.path.join(d, 'scripts', 'VERSION.txt') for d in dirs]        
-                    if not n is None:
+        for fn in fns:
-                        return n.group(1) + '.' + n.group(2) + '.' + n.group(3) + '.' + n.group(4) + post
+            print("loading version file", fn, "exists", os.path.exists(fn))
+            if os.path.exists(fn):
+                with open(fn) as f:
+                    for line in f:
+                        n = re.match(r"(.*)\.(.*)\.(.*)\.(.*)", 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]