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"],
 )
 

PARALLEL_PROJECT_NOTES.md

@@ -302,6 +302,13 @@ threads-4-cube
 threads-4-cube-shareconflicts
 -T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=false smt_parallel.frugal_cube_only=false smt_parallel.share_conflicts=true smt_parallel.share_units=false 
 
+
+threads-4-cube-maxdepth-10
+-T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.share_conflicts=false smt_parallel.share_units=false smt_parallel.max_cube_depth=10
+
+threads-4-cube-shareconflicts
+-T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.share_conflicts=true smt_parallel.share_units=false smt_parallel.frugal_depth_splitting_only=true
+
 </pre>
 
 Ideas for other knobs that can be tested

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 @@ def create_nuget_spec(version, repo, branch, commit, symbols, arch):
         <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 @@
 
 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'
-  Patch: '0'
+  Minor: '15'
+  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,17 +471,17 @@ stages:
 
 
   - job: NuGetPublish
-    condition: eq(1,0)
+    condition: eq(1,1)
     displayName: "Publish to NuGet.org"
     steps:
     - task: DownloadPipelineArtifact@2
       displayName: 'Download NuGet Package'
       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 @@
 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')
-        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
+        dirs = [SRC_DIR, ROOT_DIR, SRC_DIR_REPO, SRC_DIR_LOCAL, os.path.join(ROOT_DIR, '..', '..')]
+        for d in dirs:
+            if os.path.exists(d):
+               print(d, ": ", os.listdir(d))
+        fns = [os.path.join(d, 'scripts', 'VERSION.txt') for d in dirs]        
+        for fn in fns:
+            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]

src/params/smt_parallel_params.pyg

@@ -11,4 +11,7 @@ def_module_params('smt_parallel',
                         ('share_units_initial_only', BOOL, False, 'share only initial Boolean atoms as units'),
                         ('cube_initial_only', BOOL, False, 'cube only on initial Boolean atoms'),
                         ('max_cube_size', UINT, 20, 'maximum size of a cube to share'),
+                        ('max_greedy_cubes', UINT, 1000, 'maximum number of cube to greedily share before switching to frugal'),
+                        ('num_split_lits', UINT, 2, 'how many literals, k, we split on to create 2^k cubes'),
+                        ('frugal_deepest_cube_only', BOOL, False, 'only apply frugal cube strategy, and only on a deepest (biggest) cube from the batch manager'),
               ))

src/smt/smt_context.h

@@ -191,15 +191,14 @@ namespace smt {
         unsigned_vector             m_lit_occs;    //!< occurrence count of literals
         svector<bool_var_data>      m_bdata;       //!< mapping bool_var -> data
         svector<double>             m_activity;
-        updatable_priority_queue::priority_queue<bool_var, double> m_pq_scores;
+        // updatable_priority_queue::priority_queue<bool_var, double> m_pq_scores;
 
         struct lit_node : dll_base<lit_node> {
             literal lit;
             lit_node(literal l) : lit(l) { init(this); }
         };
         lit_node* m_dll_lits;
 
-        // svector<std::array<double, 2>> m_lit_scores; 
         svector<double> m_lit_scores[2];
 
         clause_vector               m_aux_clauses;
@@ -952,7 +951,7 @@ namespace smt {
                 e = 0;
             for (auto& e : m_lit_scores[1])
                 e = 0;
-            m_pq_scores.clear();  // Clear the priority queue heap as well
+            // m_pq_scores.clear();  // Clear the priority queue heap as well
         }
         double get_score(literal l) const {
             return m_lit_scores[l.sign()][l.var()];

src/smt/smt_internalizer.cpp

@@ -1532,23 +1532,15 @@ namespace smt {
         }} 
     }
 
-    // void context::add_scores(unsigned n, literal const* lits) {
-    //     for (unsigned i = 0; i < n; ++i) {
-    //         auto lit = lits[i];
-    //         unsigned v = lit.var();
-    //         m_lit_scores[v][lit.sign()] += 1.0 / n;
-    //     }
-    // }
-
     void context::add_scores(unsigned n, literal const* lits) {
         for (unsigned i = 0; i < n; ++i) {
             auto lit = lits[i];
             unsigned v = lit.var(); // unique key per literal
 
             m_lit_scores[lit.sign()][v] += 1.0 / n;
 
-            auto new_score = m_lit_scores[0][v] * m_lit_scores[1][v];
-            m_pq_scores.set(v, new_score);
+            // auto new_score = m_lit_scores[0][v] * m_lit_scores[1][v];
+            // m_pq_scores.set(v, new_score);
 
         }
     }