z3-gradle-plugin

This Gradle plugin extracts and provides the necessary Z3 native binaries and JAR sources at build time, eliminating the need for runtime extraction. By selecting the correct Z3 native binaries for your system architecture (x64, arm64) and operating system (glibc, osx, win) during the build, it significantly improves startup performance compared to wrappers that extract natives at runtime (e.g. z3-turnkey). It supports both JVM and GraalVM native image builds.

Features

• Automatic selection of Z3 native binaries for your architecture and OS.
• Copies Z3 binaries to distribution libs and native directories.
• Supports overriding the Z3 version.
• Compatible with gradlew installDist and GraalVM's nativeCompile.
• Provides a runtime bootstrap component for explicit library loading.

Usage

Add the plugin to your build.gradle.kts:

plugins {
    id("io.github.rascmatt.z3") version "1.0.2"
}

Optionally, override the Z3 version:

z3 {
    version = "4.15.3"
}

The specified version corresponds to the z3-bundle version (e.g. arm64 osx bundle).

Runtime Initialization

To explicitly load the Z3 library, add the bootstrap dependency:

implementation("io.github.rascmatt:z3-bootstrap:1.0.0")

Call the bootstrap method at runtime:

import com.microsoft.z3.Context
import io.github.rascmatt.z3.Z3Bootstrap
import kotlin.system.exitProcess
import kotlin.system.measureTimeMillis

fun main() {

    var initialized: Boolean
    val time = measureTimeMillis {
        initialized = Z3Bootstrap.init()
    }

    if (!initialized) {
        println("Failed to initialize Z3!")
        exitProcess(1)
    }

    println("Initialized Z3 (Took $time ms)")

    Context().use { ctx ->

        val solver = ctx.mkSolver()
        solver.add(ctx.mkFalse())

        val result = solver.check()

        println(result)
    }
}

License

Apache-2.0

Links

• Plugin Repository
• Z3