Add support for building Z3 using Bazel.

Signed-off-by: Steffen Smolka <[email protected]>

Author: smolkaj

.bazelrc

@@ -0,0 +1,11 @@
+# Use Bzlmod (`MODULE.bazel`) instead of `WORKSPACE.bazel`.
+common --enable_bzlmod
+common --noenable_workspace
+
+# Use C++20.
+build --cxxopt=-std=c++20
+build --host_cxxopt=-std=c++20
+
+# Use Clang.
+build --action_env=CC=clang
+build --action_env=CXX=clang++

.github/workflows/bazel-build.yml

@@ -0,0 +1,75 @@
+name: Bazel Build
+
+on:
+  push:
+  pull_request:
+
+jobs:
+  build:
+
+    strategy:
+      matrix:
+        # We only test on the oldest version we want to support and latest.
+        # We trust that things also work for versions in the middle.
+        os: [ubuntu-22.04, ubuntu-latest]
+        # See Bazelisk README for legal values.
+        bazel_version: [7.x, latest]
+      # Don't abort other runs when one of them fails, to ease debugging.
+      fail-fast: false
+
+    runs-on: ${{ matrix.os }}
+
+    env:
+      # This tells Bazelisk (installed as `bazel`) to use specified version.
+      # https://github.com/bazelbuild/bazelisk?tab=readme-ov-file#how-does-bazelisk-know-which-bazel-version-to-run
+      USE_BAZEL_VERSION: ${{ matrix.bazel_version }}
+      CACHE_KEY: bazel-${{ matrix.bazel_version }}
+
+    steps:
+    - uses: actions/checkout@v4
+
+    - name: Mount bazel cache
+      uses: actions/cache/restore@v4
+      with:
+        path: "~/.cache/bazel"
+        key: ${{ env.CACHE_KEY }}-${{ hashFiles('**/*.bazel*', '**/*.bzl') }}
+        restore-keys: |
+          ${{ env.CACHE_KEY }}
+
+    - name: Save start time
+      uses: josStorer/get-current-time@v2
+      id: start-time
+      with:
+        format: X  # https://momentjs.com/docs/#/displaying/format/
+
+    - run: bazel build //...
+
+    - name: Save end time
+      # Needed to save cache regardless of build failures.
+      if: always()
+      uses: josStorer/get-current-time@v2
+      id: end-time
+      with:
+        format: X  # https://momentjs.com/docs/#/displaying/format/
+
+    - name: Calculate build duration
+      # Needed to save cache regardless of build failures.
+      if: always()
+      run: |
+        START=${{ steps.start-time.outputs.formattedTime }}
+        END=${{ steps.end-time.outputs.formattedTime }}
+        DURATION=$(( $END - $START ))
+        echo "duration=$DURATION" | tee "$GITHUB_ENV"
+
+    - name: Compress cache
+      # Needed to save cache regardless of build failures.
+      if: always()
+      run: rm -rf $(bazel info repository_cache)
+
+    - name: Save bazel cache
+      uses: actions/cache/save@v4
+      # Create new cache entry if on master branch or build takes >3mins.
+      if: always() && (github.ref_name == 'master' || env.duration > 180)
+      with:
+        path: "~/.cache/bazel"
+        key: ${{ env.CACHE_KEY }}-${{ hashFiles('**/*.bazel*', '**/*.bzl') }}-${{ github.run_id }}

.gitignore

@@ -109,3 +109,6 @@ CMakeSettings.json
 dbg/**
 *.wsp
 CppProperties.json
+# Bazel generated files
+bazel-*
+*.lock

BUILD.bazel

@@ -0,0 +1,37 @@
+load("@rules_foreign_cc//foreign_cc:defs.bzl", "configure_make")
+load("@rules_license//rules:license.bzl", "license")
+
+package(default_applicable_licenses = [":license"])
+
+license(
+    name = "license",
+    license_kinds = ["@rules_license//licenses/spdx:MIT"],
+    license_text = "LICENSE.txt",
+)
+
+exports_files(["LICENSE.txt"])
+
+filegroup(
+    name = "all_files",
+    srcs = glob(["**"]),
+)
+
+configure_make(
+    name = "z3",
+    args = [
+        "--directory build",
+        # "-j8",
+    ],
+    configure_in_place = True,
+    env = {
+        # See https://github.com/bazelbuild/rules_foreign_cc/issues/239.
+        "CFLAGS": "-Dredacted=0",
+        "CXXFLAGS": "-Dredacted=0",
+        "PYTHON": "python3",
+    },
+    lib_source = ":all_files",
+    out_binaries = ["z3"],
+    out_shared_libs = ["libz3.so"],
+    targets = ["install"],
+    visibility = ["//visibility:public"],
+)

MODULE.bazel

@@ -0,0 +1,18 @@
+module(
+    name = "z3",
+    version = "4.14.0",
+    bazel_compatibility = [">=7.0.0"],
+)
+
+bazel_dep(name = "rules_foreign_cc", version = "0.14.0")
+bazel_dep(name = "rules_license", version = "1.0.0")
+
+# Enables formatting all Bazel files (.bazel, .bzl) by running:
+# ```bash
+# bazel run -- @buildifier_prebuilt//:buildifier --lint=fix -r .
+# ```
+bazel_dep(
+    name = "buildifier_prebuilt",
+    version = "8.0.1",
+    dev_dependency = True,
+)

README.md

@@ -7,8 +7,9 @@ If you are not familiar with Z3, you can start [here](https://github.com/Z3Prove
 
 Pre-built binaries for stable and nightly releases are available [here](https://github.com/Z3Prover/z3/releases).
 
-Z3 can be built using [Visual Studio][1], a [Makefile][2] or using [CMake][3]. It provides
-[bindings for several programming languages][4]. 
+Z3 can be built using [Visual Studio][1], a [Makefile][2], using [CMake][3],
+using [vcpkg][4], or using [Bazel][5] on Ubuntu. It provides
+[bindings for several programming languages][6].
 
 See the [release notes](RELEASE_NOTES.md) for notes on various stable releases of Z3.
 
@@ -25,7 +26,9 @@ See the [release notes](RELEASE_NOTES.md) for notes on various stable releases o
 [1]: #building-z3-on-windows-using-visual-studio-command-prompt
 [2]: #building-z3-using-make-and-gccclang
 [3]: #building-z3-using-cmake
-[4]: #z3-bindings
+[4]: #building-z3-using-vcpkg
+[5]: #building-z3-using-bazel
+[6]: #z3-bindings
 
 ## Building Z3 on Windows using Visual Studio Command Prompt
 
@@ -106,6 +109,7 @@ Z3 has a build system using CMake. Read the [README-CMake.md](README-CMake.md)
 file for details. It is recommended for most build tasks, 
 except for building OCaml bindings.
 
+
 ## Building Z3 using vcpkg
 
 vcpkg is a full platform package manager. To install Z3 with vcpkg, execute:
@@ -117,6 +121,14 @@ git clone https://github.com/microsoft/vcpkg.git
 ./vcpkg install z3
 ```
 
+## Building Z3 using Bazel
+
+Z3 can be built using [Bazel](https://bazel.build/). This is known to work on
+Ubuntu with Clang (but may work elsewhere with other compilers):
+```
+bazel build //...
+```
+
 ## Dependencies
 
 Z3 itself has only few dependencies. It uses C++ runtime libraries, including pthreads for multi-threading.