Calling SMT solver from JavaScript

Question

Is there a way to run Z3 solver from javascript? Or is there a better SMT solver that I can be used in JavaScript?

Prowel

Answer 1

There is an implementation of the Alt-Ergo SMT solver in JavaScript, which was compiled into JavaScript using the dune build system. It may also be possible to embed a Prolog SMT solver in JavaScript using Tau-Prolog.

Annuity

Answer 2

Depending on how performance-critical your application is, you may be able to implement the functionality you need by creating a new z3 process with z3 -in so that it reads commands from standard input, then use (push) and (pop) smtlib commands to do incremental queries. I have had a decent amount of success with this in other languages when I didn't want to depend on native bindings, although of course it does suffer from increased overhead compared to a directly-exposed API, because you are spending time creating a new process and then parsing smtlib expressions. But in practice it's still extremely fast unless you need every single millisecond you can squeeze out.

Of course, this assumes you are running javascript as a process on a system via e.g. node.js and have access to the ability to create new processes. If you are running in a browser, it is highly unlikely that you could get this to work at all. Even something like emscripten, if you could even get it to work, would likely have completely intractable performance on any real-world problems.

Sworn

Answer 3

Z3 comes with a Java API, but the implementation of all functionality is within a native code .dll/.so/.dylib, but as long as you have other means of making sure that the native library is on the client machine and it's accessible, I think the Java API should be enough. Of course, there may be security problems with running native code on client machines, those would have to be resolved first.

Skep

Thanks, but what I mean is JavaScript rather than Java, they are two different animals :) – Prowel

Yes, still it's the closest one. E.g., that Java wrappers should translate nicely into JavaScript (at non-zero but small effort), but the native code problem will remain. – Skep

@ChristophWintersteiger Would it be possible to port the native code to JavaScript using Emscripten? – Annuity

@AndersonGreen Theoretically speaking I'm sure it would be possible, but practically speaking I would expect this to be a very time-consuming project. I don't think it's worth the effort, but if somebody has a good reason and some time to work on it, then it might make sense to at least give it a try. – Skep