Java Script API bindings

[NikolajBjorner]

What are the current ways to use Z3 from Java Script?

1. What is their license?
2. Is there an interest in contributing these?

The following efforts relate to this (summarized from conversation below).

• https://github.com/ExpoSEJS/z3javascript by @jawline
• Use SWIG (suggested by @delcypher)
• @d1m0 has a project with type script
• Compile sources to WebAssembly (last tried by @cpitclaudel)

[delcypher]

@NikolajBjorner An alternative that I mentioned a while back is to use SWIG. This supports automatically generating language bindings for many different languages.

This could reduce the maintenance burden of the manually maintained language bindings. However I've never used SWIG before so I'm not sure if the bindings generated are of sufficient quality.

[d1m0]

If anyone is interested, I am working on typescript bindings for webassembly compiled libz3.so. I can contribute my progress so far?

[wintersteiger]

@cpitclaudel recently compiled all of Z3 to Javascript, which removes all the OS-dependency issues at the cost of runtime performance, but the cost was smaller than I expected.

[chriseth]

@wintersteiger I would be very interested in that! What is the size of the "binary" you got? Do you have any instructions?

[cpitclaudel]

Roughly 20MB (when compiled to WebAssembly). Compiling to javascript doesn't work, due to (I think) unaligned memory accesses. I could write things up, but probably not before the week-end after the next.

[danr]

@cpitclaudel I am very interested in seeing your build setup for compilation to webassembly.

[cpitclaudel]

I've finally packaged everything 🎉

The repo is here: https://github.com/cpitclaudel/z3.wasm
There's a live demo here: https://people.csail.mit.edu/cpitcla/z3.wasm/z3.html

The repo includes the build scripts, a binary release, some documentation, and the sources of the demo page.

The generated binaries expose Z3's command line, and a small SMT2 API.
Wrapping the full Z3 C or C++ API would likely require an extra day of work or so, using https://kripken.github.io/emscripten-site/docs/porting/connecting_cpp_and_javascript/embind.html or https://github.com/charto/nbind .

I've tested this on small examples, and I'm using this as the SMT solver backend for my JavaScript build of F* (https://people.csail.mit.edu/cpitcla/fstar.js/stlc.html)

[NikolajBjorner]

This is great! I added a link to the repository from the readme.md file.

[jawline]

There is also https://github.com/babelsberg/z3.js which is a set of build-scripts I've used previously to compiled Z3 into native JavaScript.

Our approach (z3javascript) works well from Node / Electron but I think as WebAssembly matures that would probably be a better long term target (compatability). I experimented with ASM.js two years ago and it compiled fine but was too slow for practical usage.

A big issue we've found is that JavaScripts lack of destructors can make memory management very difficult.

Is Z3 going to get official JavaScript bindings or is this just for documentation?

[sb98052]

I would like to make an attempt to contribute something here. Besides SWIG and Native C++ add ons for Node (https://nodejs.org/api/addons.html), another option is to wrap the C API using http://grpc.io. In addition to opening up the languages supported by it, using gRPC would bring the benefit of being able to integrate with a remote Z3 server. I would love to hear feedback on this option.

[NikolajBjorner]

Sounds very nice.
Note that there are a few different use cases for what it means to be a remote server, so it will depend on your application what makes sense.

With Miguel Neves we have an internal scale out version of Z3 that runs in Azure.
It uses the public API from C# and uses Azure queues and tables to store state in the form of SMT-LIB text files. This makes reproducing any potential issue transparent as it becomes a question of downloading text files and rerunning Z3 locally on those.

For ecma script integration, I have no real understanding of what is the better approach.
Keeping server side state and wrapping API calls over REST or similar could be useful for some cases. They would have to protect the services from vandalism by some means of authentication as sooner or later someone finds it "fun" to poke holes.
We will not be able to maintain or support these features, so maintaining them as external contributions is probably the better approach and I will be very happy to work with you and others on linking to them.

[d1m0]

I have a working (for simple programs at least) TypeScript bindings around libz3 compiled with WASM. Repo is here: https://github.com/d1m0/z3.ts. Here is an example of code using the bindings:

var lib: LibZ3 = new LibZ3(wasmInstance)
var config: Z3_config = lib.Z3_mk_config()
var context: Z3_context = lib.Z3_mk_context(config)
var solver: Z3_solver = lib.Z3_mk_solver(context)
var int_sort: Z3_sort = lib.Z3_mk_int_sort(context)

var s1: Z3_symbol = lib.Z3_mk_int_symbol(context, new Sint32(1))
var c1: Z3_ast = lib.Z3_mk_const(context, s1, int_sort)
var s2: Z3_symbol = lib.Z3_mk_int_symbol(context, new Sint32(2))
var c2: Z3_ast = lib.Z3_mk_const(context, s2, int_sort)

var eq: Z3_ast = lib.Z3_mk_eq(context, c1, c2)
var neq: Z3_ast = lib.Z3_mk_not(context, eq)

lib.Z3_solver_assert(context, solver, eq)
lib.Z3_solver_assert(context, solver, neq)
var res: Z3_lbool = lib.Z3_solver_check(context, solver)

The bindings were auto-generated from the Pyhton bindings in z3.z3core.

[NikolajBjorner]

Looks pretty slick.
There are a few hard-wired dependencies. Perhaps we can remove them by updating
scripts/update_api.py?

For example, the code that does not produce any attribute when the return value is VOID is

  def mk_py_binding(name, result, params):
        ....
        if result != VOID:
             core_py.write("_lib.%s.restype = %s\n" % (name, type2pystr(result)))

Your bindings will too easily bit-rot (I am going to change a lot in the next couple of months so it is going to be quite busy).

[d1m0]

Sure! If it would not be too much work for you! Also if you see a way to just fold some of this code into the main repo, I would love to help.

[sb98052]

Thanks for your feedback, @NikolajBjorner

FYI, I gave SWIG a try and it while it seems very nice, the Javascript backend does not seem to be actively maintained (e.g. swig/swig#804). It's possible to patch the issues, but it will probably require continuous maintenance.

[sb98052]

I've built a native N-API binding for Z3. Rather than compiling Z3 into Javascript, it defines an FFI from Javascript into Z3 compiled natively. It is still work-in-progress and has not been integrated with Z3's build system. I am putting it up early for other people who are looking for this functionality, and who would be willing to help harden it.

It can be found here: https://github.com/sb98052/z3/tree/master/src/api/n-api

I plan on submitting this extension as a pull request when I am convinced that it is stable and has test coverage equalling the other APIs.

[sim642]

I've been interested in this for a while for browser usage in an actual application. I have now created my own library build to WASM via emscripten as well: https://github.com/sim642/z3em. There's nothing revolutionary there except that it's packaged and published on npm unlike other similar attempts: https://www.npmjs.com/package/z3em. My goal is to integrate Z3 into an actual logic game of mine (https://github.com/sim642/einstein-js/tree/z3) and have Z3 as an independent and reusable module. I haven't focused on API but have just exposed the bare minimum to evaluate smtlib2 interactively.

I encountered an issue with compiling Z3 via emscripten: sim642/z3em#1. The mk_make.py script configures OS as _LINUX_ even under emconfigure. That causes scoped_timer to attempt to use pthread but that's not possible in WASM. I've worked around this by modifying config.mk afterwards to make scoped_timer use an empty implementation instead. I'll try to replace the implementation with an emscripten compatible one soon (sim642/z3em#2).

I think currently there's no means for cross-compilation as mk_make.py works based on the host OS. In broader perspective it may be useful to allow manually overriding certain parts of the configuration script to allow cross-compilation, including compilation via emscripten, which would be like Linux but shouldn't pretend to be actual Linux but be aware of the fact that emscripten is being used instead.

[NikolajBjorner]

Commit f306f75 starts the process of providing js bindings adapting the style of @sb98052 using the python build scripts for creating the json manifest and bypassing dependencies on cli/ocaml for the build.

[sb98052]

Thanks! Commit c247abf provides enough scaffolding for me to transition my changes over to your build system. I should have a PR for your review soon.

[mjyc]

Hello. I prototyped z3js, a utility library for transpiling a tiny subset of javascript into smt and vice versa. The main idea of z3js is using it with @cpitclaudel's z3.wasm to use z3 in (a tiny subset of) javascript (even inbrowser) and hence act as javascript-binding for z3. z3js is far far far away from being actually useful but would like to hear z3 experts' feedback on it. Thanks in advance.

[mgree]

I've been using @cpitclaudel's z3.wasm, but I haven't yet found a way to set the timeout without either a pthread issue or a crash: building --single-threaded leads to crashes when I give -T:2 or -t:2000 or what-have-you. (See cpitclaudel/z3.wasm#2 (comment).) Do any of the other solutions support timeouts?

[stahlbauer]

Hey :)

it is great to see that there is effort to get Z3 running in the browser. Are there news regarding the current status of this?(compiled into WASM? @cpitclaudel )?. I would love to use the TypeScript bindings by @d1m0 and facing some compilation issues such as ../src/util/lp/permutation_matrix.h:135:44: error: no viable conversion from returned value of type 'const vector<unsigned int>' to function return type 'unsigned int *' unsigned * values() const { return m_permutation; }.

Are there pre-built releases of both Z3.wasm and the TypeScript (or JavaScript) bindings that work with the WASM?

EDIT: I have fixed the compilation issues by using specific versions of Emscripten and Z3.

[mgree]

I don't have TS bindings, but you can see an example of use by an Elm app in https://github.com/mgree/crossbars/, using a WebWorker via an elm port.

[stahlbauer]

@mgree: Thanks a lot. Great project :)

[cd1m0]

@stahlbauer hey! I haven't touched the .ts bindings in a long time, but if they may be useful to you, I can resurrect them over a weekend. Let me know if you would be interesting in maintaining/contributing to those as well!

[stahlbauer]

@cd1m0: Hey, I have fixed the TS bindings and got them working. At the moment, the adjustments are in my fork (on Github) of the bindings. I am also working on a more user-friendly API to Z3 in TS that builds on this bindings. Should be finished within the next two weeks.

[bakkot]

There's now TypeScript bindings published on npm: https://www.npmjs.com/package/z3-solver