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?

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.

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.