Link z3 from z3py (#561)

* Link z3 from z3py

* Update CodeQL build flow

.github/workflows/codeql.yml

@@ -33,7 +33,8 @@ jobs:
         if: ${{ matrix.language == 'cpp' }}
         run: |
           sudo apt-get update
-          sudo apt-get install --yes g++-11 libgmp-dev ninja-build
+          sudo apt-get install --yes g++-11 libgmp-dev ninja-build python3-pip
+          sudo pip3 install z3-solver
 
       - name: Configure (cpp)
         if: ${{ matrix.language == 'cpp' }}

.gitmodules

@@ -9,9 +9,6 @@
 [submodule "3rd-party/isl"]
     path = 3rd-party/isl
     url = git://repo.or.cz/isl.git
-[submodule "3rd-party/z3"]
-    path = 3rd-party/z3
-    url = ../../Z3Prover/z3.git
 [submodule "3rd-party/cuda-samples"]
     path = 3rd-party/cuda-samples
     url = ../../NVIDIA/cuda-samples.git

3rd-party/README.md

@@ -4,4 +4,4 @@ We use a custom pybind11 to avoid a typing error prior to Python 3.10 (https://g
 
 Since there is no easy way to install ANTLR (ANTLR4 is missing from Spack), we include it in `antlr/`. `antlr/antlr4` is the ANTLR repo, where its C++ runtime is needed. `antlr/*.jar` is the ANTLR generator binary.
 
-cppitertools can be replaced once there are enough supports from STL, maybe after C++23
+range-v3 can be replaced once there are enough supports from STL, maybe after C++23

CMakeLists.txt

@@ -25,7 +25,7 @@ if (CMAKE_CXX_COMPILER_ID STREQUAL "GNU")
 endif()
 
 # Check whther 3rd-party modules exist
-foreach(MODULE IN ITEMS antlr/antlr4 range-v3 cuda-samples isl pybind11 z3)
+foreach(MODULE IN ITEMS antlr/antlr4 range-v3 cuda-samples isl pybind11)
     file(GLOB RESULT ${CMAKE_CURRENT_SOURCE_DIR}/3rd-party/${MODULE}/*)
     list(LENGTH RESULT RES_LEN)
     if(RES_LEN EQUAL 0)
@@ -59,8 +59,11 @@ target_link_libraries(isl::isl INTERFACE ${ISL_DIR}/install/lib/libisl.so)
 add_dependencies(isl::isl ISL)
 
 # Z3
-set(SUBMODULE_DIR_NAME "3rd-party") # Z3 PR #4959
-add_subdirectory(${CMAKE_CURRENT_SOURCE_DIR}/3rd-party/z3)
+execute_process(
+    COMMAND "${Python_EXECUTABLE}" -c "import z3; import os; print(os.path.dirname(z3.__file__))"
+    OUTPUT_VARIABLE Z3_PATH)
+string(STRIP "${Z3_PATH}" Z3_PATH)
+message(STATUS "Looking for Z3 in ${Z3_PATH}")
 
 # ANTLR
 # 1. Runtime
@@ -230,13 +233,13 @@ add_library(freetensor SHARED ${SRC})
 add_dependencies(freetensor ISL)
 target_link_libraries(freetensor PUBLIC
     isl::isl
-    libz3 # See 3rd-party/z3/src/CMakeLists.txt
+    ${Z3_PATH}/lib/libz3.so
     antlr4_shared # See 3rd-party/antlr/antlr4/runtime/Cpp/runtime/CMakeLists.txt
     OpenMP::OpenMP_CXX
     ${CUDA_LIBRARIES} ${CUDA_CUBLAS_LIBRARIES})
 target_include_directories(freetensor PUBLIC
     ${CUDA_INCLUDE_DIRS}
-    ${CMAKE_CURRENT_SOURCE_DIR}/3rd-party/z3/src/api/c++
+    ${Z3_PATH}/include
     ${CMAKE_CURRENT_SOURCE_DIR}/include
     ${CMAKE_CURRENT_SOURCE_DIR}/3rd-party/range-v3/include)
 target_include_directories(freetensor PRIVATE ${ANTLR_INCLUDES})

docs/guide/build-and-run.md

@@ -15,7 +15,7 @@
 Other Python dependencies:
 
 ```sh
-pip3 install --user numpy sourceinspect astor Pygments
+pip3 install --user numpy sourceinspect astor Pygments z3-solver
 ```
 
 !!! note "Note on Python version"

pyproject.toml

@@ -11,6 +11,7 @@ dependencies = [
     "sourceinspect",
     "astor",
     "Pygments",
+    "z3-solver",
 ]
 
 [project.optional-dependencies]
@@ -24,7 +25,7 @@ doc = [
 ]
 
 [build-system]
-requires = ["py-build-cmake~=0.1.8"]
+requires = ["py-build-cmake~=0.1.8", "z3-solver"]
 build-backend = "py_build_cmake.build"
 
 [tool.py-build-cmake.module] # Where to find the Python module to package

requirements.txt

@@ -38,4 +38,5 @@ torch==2.0.0+cu118
 triton==2.0.0
 typing-extensions==4.5.0
 watchdog==3.0.0
+z3-solver==4.12.2.0
 zipp==3.15.0