Skip to content

Commit 0b26f7e

Browse files
authored
Add support for building Z3 using Bazel. (#7646)
Signed-off-by: Steffen Smolka <[email protected]>
1 parent f680242 commit 0b26f7e

File tree

5 files changed

+72
-3
lines changed

5 files changed

+72
-3
lines changed

.bazelrc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
# Use Bzlmod (`MODULE.bazel`) instead of `WORKSPACE.bazel`.
2+
common --enable_bzlmod
3+
common --noenable_workspace
4+
5+
# Use C++20.
6+
build --cxxopt=-std=c++20
7+
build --host_cxxopt=-std=c++20
8+
9+
# Use Clang.
10+
build --action_env=CC=clang
11+
build --action_env=CXX=clang++

.gitignore

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -111,3 +111,5 @@ dbg/**
111111
CppProperties.json
112112
genaisrc/genblogpost.genai.mts
113113
*.mts
114+
# Bazel generated files
115+
bazel-*

BUILD.bazel

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
load("@rules_foreign_cc//foreign_cc:defs.bzl", "cmake")
2+
load("@rules_license//rules:license.bzl", "license")
3+
4+
package(default_applicable_licenses = [":license"])
5+
6+
license(
7+
name = "license",
8+
license_kinds = ["@rules_license//licenses/spdx:MIT"],
9+
license_text = "LICENSE.txt",
10+
)
11+
12+
exports_files(["LICENSE.txt"])
13+
14+
filegroup(
15+
name = "all_files",
16+
srcs = glob(["**"]),
17+
)
18+
19+
cmake(
20+
name = "z3",
21+
generate_args = ["-G Ninja"],
22+
lib_source = ":all_files",
23+
out_binaries = ["z3"],
24+
out_shared_libs = ["libz3.so"],
25+
visibility = ["//visibility:public"],
26+
)

MODULE.bazel

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module(
2+
name = "z3",
3+
version = "4.14.0",
4+
bazel_compatibility = [">=7.0.0"],
5+
)
6+
7+
bazel_dep(name = "rules_foreign_cc", version = "0.14.0")
8+
bazel_dep(name = "rules_license", version = "1.0.0")
9+
10+
# Enables formatting all Bazel files (.bazel, .bzl) by running:
11+
# ```bash
12+
# bazel run -- \
13+
# @buildifier_prebuilt//:buildifier --lint=fix -r $(bazel info workspace)
14+
# ```
15+
bazel_dep(
16+
name = "buildifier_prebuilt",
17+
version = "8.0.1",
18+
dev_dependency = True,
19+
)

README.md

Lines changed: 14 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,9 @@ If you are not familiar with Z3, you can start [here](https://github.com/Z3Prove
77

88
Pre-built binaries for stable and nightly releases are available [here](https://github.com/Z3Prover/z3/releases).
99

10-
Z3 can be built using [Visual Studio][1], a [Makefile][2] or using [CMake][3]. It provides
11-
[bindings for several programming languages][4].
10+
Z3 can be built using [Visual Studio][1], a [Makefile][2], using [CMake][3],
11+
using [vcpkg][4], or using [Bazel][5].
12+
It provides [bindings for several programming languages][6].
1213

1314
See the [release notes](RELEASE_NOTES.md) for notes on various stable releases of Z3.
1415

@@ -23,7 +24,9 @@ See the [release notes](RELEASE_NOTES.md) for notes on various stable releases o
2324
[1]: #building-z3-on-windows-using-visual-studio-command-prompt
2425
[2]: #building-z3-using-make-and-gccclang
2526
[3]: #building-z3-using-cmake
26-
[4]: #z3-bindings
27+
[4]: #building-z3-using-vcpkg
28+
[5]: #building-z3-using-bazel
29+
[6]: #z3-bindings
2730

2831
## Building Z3 on Windows using Visual Studio Command Prompt
2932

@@ -115,6 +118,14 @@ git clone https://github.com/microsoft/vcpkg.git
115118
./vcpkg install z3
116119
```
117120

121+
## Building Z3 using Bazel
122+
123+
Z3 can be built using [Bazel](https://bazel.build/). This is known to work on
124+
Ubuntu with Clang (but may work elsewhere with other compilers):
125+
```
126+
bazel build //...
127+
```
128+
118129
## Dependencies
119130

120131
Z3 itself has only few dependencies. It uses C++ runtime libraries, including pthreads for multi-threading.

0 commit comments

Comments
 (0)