Z3 Theorem Prover

The high-level API is designed to be similar to Z3Py. Most operations require a Context. When you create a Context, TypeScript uses the provided name to narrow types, preventing you from accidentally mixing objects from different contexts at compile time.

Note: The high-level API is not thread-safe; long-running functions are queued and executed one after another.

const { init } = require('z3-solver');
const { Context } = await init();
const { Solver, Int, And } = new Context('main');

const x = Int.const('x');
const solver = new Solver();
solver.add(And(x.ge(0), x.le(9)));
console.log(await solver.check());
// sat

Z3 handles recursive functions by 'unfolding' function definitions into auxiliary clauses. For a function definition f(x1…xn) := rhs[x1…xn], the engine compiles it into:

1. Case Clauses: A_f_i[x1…xn] => f(x1…xn) = rhs_i[x1…xn]. These are added as auxiliary clauses only when the condition A_f_i becomes true in the current model.
2. Constraint Clauses: Γ_f_i[x1…xn] <=> A_f_i[x1…xn]. These define the conditions under which a specific case of the function applies and are added as soon as the function is internalized.

Example: The definition fact(n) := if n < 2 then 1 else n * fact(n-1) is compiled into:

• A_fact_0[n] => fact(n) = 1
• A_fact_1[n] => fact(n) = n * fact(n-1)
• A_fact_0[n] <=> n < 2
• A_fact_1[n] <=> ¬(n < 2)

This mechanism allows Z3 to support recursive functions in QF_* fragments and enables the direct analysis of functional programs.

When building with Microsoft Visual C++ (MSVC), Z3 enables security features by default to protect against control flow redirection attacks.

Control Flow Guard (CFG)

• Option: Z3_ENABLE_CFG (Defaults to ON for MSVC).
• Function: Analyzes control flow for indirect call targets and inserts runtime verification.
• Incompatibilities: CFG is incompatible with /ZI (Edit and Continue) and /clr (Common Language Runtime). If these are detected, CFG is automatically disabled with a warning.
• Disabling: To turn it off, set Z3_ENABLE_CFG=OFF.

Address Space Layout Randomization (ASLR)

• Mechanism: Enabled via the /DYNAMICBASE linker flag.
• Dependency: Automatically enabled when Control Flow Guard is active.

cmake -DZ3_ENABLE_CFG=OFF ../

Z3 contexts are not thread-safe. To avoid race conditions, you should either:

1. Use a unique context for each goroutine.
2. Use appropriate synchronization (e.g., mutexes) when sharing a context across goroutines.

The Go bindings use runtime.SetFinalizer to automatically manage Z3 reference counts. You do not need to manually call inc_ref or dec_ref.

Note: Because finalizers run during garbage collection, resources may not be freed immediately. To ensure safety with concurrent GC, the bindings enable Z3_enable_concurrent_dec_ref when creating contexts.

Z3 supports standard installation and uninstallation targets. Use CMAKE_INSTALL_PREFIX to define the installation directory.

For staged installs (e.g., for packaging), use the DESTDIR environment variable.

# Standard install
make install

# Standard uninstall
make uninstall

# Staged install (using DESTDIR)
mkdir staged
make install DESTDIR=/full/path/to/staged/

# Staged uninstall
make uninstall DESTDIR=/full/path/to/staged

To use the Z3 Go bindings on Windows, build Z3 using CMake and configure your environment variables to ensure the Go compiler can find the Z3 DLLs and headers.

1. Build Z3: Use cmake --build . --config Release in the build directory.
2. Configure Environment: Add the build\Release directory to your PATH, set CGO_CFLAGS to the Z3 API header directory, and set CGO_LDFLAGS to the library path and -lz3.
3. Run: Execute your Go files using go run.

REM Build Z3 first
cd ..\..
mkdir build
cd build
cmake ..
cmake --build . --config Release

REM Set up environment
cd ..\examples\go
set PATH=..\..\build\Release;%PATH%
set CGO_CFLAGS=-I..\..\src\api
set CGO_LDFLAGS=-L..\..\build\Release -lz3

REM Run examples
go run basic_example.go

Alternatively, you can use the Python-based build script to generate the makefiles for the Go bindings.

python scripts/mk_make.py --go
cd build
make

Go bindings are built using CGO to wrap the Z3 C API.

Requirements:

• Go 1.20 or later.
• Z3_BUILD_LIBZ3_SHARED=ON (Shared library is required).

Build Targets: If a Go installation is detected in your PATH, CMake provides:

• go-bindings: Builds the Go bindings (installed as source files).
• test-go-examples: Runs the Go examples.

Usage: Since Go packages are distributed as source, you must set the following CGO flags to use the installed bindings:

# Build command
mkdir build
cd build
cmake -DZ3_BUILD_GO_BINDINGS=ON -DZ3_BUILD_LIBZ3_SHARED=ON ../
make

# Environment variables for usage
export CGO_CFLAGS="-I/path/to/z3/include"
export CGO_LDFLAGS="-L/path/to/z3/lib -lz3"
export LD_LIBRARY_PATH="/path/to/z3/lib:$LD_LIBRARY_PATH"  # Linux/macOS

To use Z3 in Java, you need two components: the Java API library (com.microsoft.z3.jar) and the native libraries (libz3 and libz3java with platform-specific extensions).

Option 1: Download Pre-built Binaries (Recommended)

1. Download the appropriate release from the Z3 Releases page.
2. Extract to a location (e.g., C:\z3 or /opt/z3).
3. Ensure the bin folder contains:
   • com.microsoft.z3.jar (Java API)
   • libz3.dll / .so / .dylib (Native Z3)
   • libz3java.dll / .so / .dylib (JNI bridge)

# If building from source to enable Java bindings:
python scripts/mk_make.py --java
cd build
make

Before running Python examples (such as example.py) on Linux or macOS, you must install the Python bindings. Run the following command from the Z3 root directory:

sudo make install-z3py

Visual Studio 19 and later have integrated CMake support. You can simply open the Z3 folder containing the root CMakeLists.txt directly in Visual Studio.

For legacy versions (using cmake-gui):

1. Create an empty build directory.
2. Use cmake-gui to set the source directory (Z3 root) and build directory.
3. Click Configure and select the appropriate Visual Studio generator (e.g., Visual Studio 16 2019 Win64).
4. Adjust configuration options and click Generate.
5. Open the generated Z3.sln file in Visual Studio.
6. Select your build type (Debug/Release) inside Visual Studio and select BUILD > Build Solution.

Note: Unlike Ninja or Make, Visual Studio generators are multi-configuration generators. You do not set the build type during the CMake configuration step; you set it within the Visual Studio IDE.