From 0b26f7e0ee4a3a94eac2041c4b0831d8e5d8736d Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolkaj@google.com>
Date: Thu, 15 May 2025 09:47:29 -0600
Subject: [PATCH] Add support for building Z3 using Bazel. (#7646)

Signed-off-by: Steffen Smolka <smolkaj@google.com>
---
 .bazelrc     | 11 +++++++++++
 .gitignore   |  2 ++
 BUILD.bazel  | 26 ++++++++++++++++++++++++++
 MODULE.bazel | 19 +++++++++++++++++++
 README.md    | 17 ++++++++++++++---
 5 files changed, 72 insertions(+), 3 deletions(-)
 create mode 100644 .bazelrc
 create mode 100644 BUILD.bazel
 create mode 100644 MODULE.bazel

diff --git a/.bazelrc b/.bazelrc
new file mode 100644
index 000000000..b31c49c40
--- /dev/null
+++ b/.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++
diff --git a/.gitignore b/.gitignore
index 8c149afc5..dde5ac47b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -111,3 +111,5 @@ dbg/**
 CppProperties.json
 genaisrc/genblogpost.genai.mts
 *.mts
+# Bazel generated files
+bazel-*
diff --git a/BUILD.bazel b/BUILD.bazel
new file mode 100644
index 000000000..51ff02b11
--- /dev/null
+++ b/BUILD.bazel
@@ -0,0 +1,26 @@
+load("@rules_foreign_cc//foreign_cc:defs.bzl", "cmake")
+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(["**"]),
+)
+
+cmake(
+    name = "z3",
+    generate_args = ["-G Ninja"],
+    lib_source = ":all_files",
+    out_binaries = ["z3"],
+    out_shared_libs = ["libz3.so"],
+    visibility = ["//visibility:public"],
+)
diff --git a/MODULE.bazel b/MODULE.bazel
new file mode 100644
index 000000000..58aa2520f
--- /dev/null
+++ b/MODULE.bazel
@@ -0,0 +1,19 @@
+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 info workspace)
+# ```
+bazel_dep(
+    name = "buildifier_prebuilt",
+    version = "8.0.1",
+    dev_dependency = True,
+)
diff --git a/README.md b/README.md
index 2797c2da2..b99c9e6b5 100644
--- a/README.md
+++ b/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].
+It provides [bindings for several programming languages][6].
 
 See the [release notes](RELEASE_NOTES.md) for notes on various stable releases of Z3.
 
@@ -23,7 +24,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
 
@@ -115,6 +118,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.