Julia bindings for Z3 SMT solver

Specific Domains Optimization (Mathematical)
1

Recently I met the need to access Z3 from Julia program, searched a bit and found abandoned Julia bindings at zenna/Z3.jl. But they do not work with the recent versions and I asked Z3 developers themselves. As it turned out they provide Julia bindings out of the box, just didn’t announce it widely. So for anyone who is going to work with Z3 - see Julia chapter of their README. So if anyone wants to test and add an examples - Z3 project welcomes pull requests.

6 Likes
2

Thanks for this! We’re you able to get it to compile? I had some issues with cmake.

3

It would be wonderful for someone who knows how to make a package that installs the appropriate z3 binary with those Julia extensions and so makes z3 easily available for our use.

1 Like
4

I’d appreciate in advance if anyone can do this.

5

Would be nice to make it all available as a Julia package and BinaryBuilder!

4 Likes
6

Z3 is available as a jll package since November: GitHub - JuliaBinaryWrappers/z3_jll.jl :slightly_smiling_face:

4 Likes
7

Now z3_jll has also v4.8.7. However, the Julia bindings are available only in master, I’d like to wait to for a new release before building it in Yggdrasil, but maybe you can open an issue to z3 to ask for a new version :wink:

8

What is the issue that you want to share with Z3?
(please be overly specific, leave nothing to the imagination) :wink:

9

I mean, you can file a new issue to GitHub - Z3Prover/z3: The Z3 Theorem Prover and encourage the maintainer to release a new version

10

Is it that #master has stuff that is ready for release but has not been released? If so, give me one or two items to mention.

11

I don’t know z3 at all, the only thing in master I know that you could be interested in are the Julia bindings, but I didn’t even looked at how they work :slight_smile:

12

ok no problem, same here I will give it shot – after all the Julia bindings should be much easier to build (several of us have tried following the scant directions).

13

issue raised

14

from Z3:

we currently build on every commit for the MacOS. The build script is here[ (see below):@ahumenberger prepared the script and also created the bindings. He uses a MacOS, so it was easier to create the script for this environment. I am very happy to include CI builds on other platforms, but similar to you, figuring out the magic dependencies is going to take some arm-twisting. If you (or others) can see what should be done for other platforms, say Ubuntu, based on the MacOS script a pull request with an update to the CI pipeline is very welcome. In this way we can build on every push.

build script
(exerpted)

- job: "MacOSCMake"
  displayName: "MacOS build with CMake"
  pool:
    vmImage: "macOS-10.14"
  steps:
    - script: brew install ninja
    - script: brew cask install julia
    - script: |
        julia -e "using Pkg; Pkg.add(PackageSpec(name=\"libcxxwrap_julia_jll\", version=\"0.6.6\"))"
        JlCxxDir=$(julia -e "using libcxxwrap_julia_jll; println(joinpath(dirname(libcxxwrap_julia_jll.libcxxwrap_julia_path), \"cmake\", \"JlCxx\"))")
        set -e
        mkdir build
        cd build
        CC=clang CXX=clang++ cmake -DJlCxx_DIR=$JlCxxDir -DZ3_BUILD_JULIA_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -DZ3_BUILD_DOTNET_BINDINGS=False -G "Ninja" ../
        ninja
        ninja test-z3
        cd ..
    - template: scripts/test-z3.yml
    - template: scripts/test-examples-cmake.yml
    - template: scripts/test-regressions.yml
15

As you can see the Julia bindings for Z3 sit on top of the C++ API and use CxxWrap.jl. There is currently a pull request pending which updates the bindings to libcxxwrap 0.7. After that we would need a new release of Z3 to update z3_jll. The package ahumenberger/Z3.jl would then use z3_jll.
Right now, ahumenberger/Z3.jl builds an older version of Z3 on the fly. Updating the package to use z3_jll (once we have new Z3 release) should be easy.

2 Likes
16

Thank you. I provided Z3 with those additional specifics.

17

for someone who knows who knows and probably @viralbshah:
would you bring the person(s) who know how to help him do this into that thread

18

Z3.jl v0.4.0 is released. It now uses z3_jll v4.8.8. Thanks to everyone involved!

8 Likes
19

Has anyone been able to run the examples on a Intel Mac? I keep getting a segmentation fault whenever the example tries to create the solver.

1 Like
20

I run into the same issue. A bit frustrating.