Fixing js binding

[jurajsic]

This PR fixes building of JS binding with more detailed readme.
It seems to be working, however some tests fail, because either they want to use model/proof generation which is by default disabled in noodler, or there is a timeout, and I do not know why it timeouts (the tests are very simple).

[vhavlena]

I tried it and I am a bit stuck. After npm run build:wasm I got the following error:

wasm-ld: error: ../../../build/libz3.a(ca_str_constr.cpp.o): undefined symbol: mata::nfa::Nfa::get_words(unsigned int) const
emcc: error: '/opt/homebrew/Cellar/emscripten/3.1.74/libexec/llvm/bin/wasm-ld @/var/folders/k8/vb71jppj43x35pc3qvksjy4w0000gn/T/emscripten_u_l4r1au.rsp.utf-8' failed (returned 1)
Process exited with status 1

Built against the current mata.

[jurajsic]

I tried it and I am a bit stuck. After npm run build:wasm I got the following error:

wasm-ld: error: ../../../build/libz3.a(ca_str_constr.cpp.o): undefined symbol: mata::nfa::Nfa::get_words(unsigned int) const
emcc: error: '/opt/homebrew/Cellar/emscripten/3.1.74/libexec/llvm/bin/wasm-ld @/var/folders/k8/vb71jppj43x35pc3qvksjy4w0000gn/T/emscripten_u_l4r1au.rsp.utf-8' failed (returned 1)
Process exited with status 1

Built against the current mata.

Did you follow the steps exactly the same? Mainly if you are usingemscripten from emsdk, because it looks like you are using the installed emscripten trough brew (you might need to uninstall emscripten trough brew, otherwise it can clash).

[vhavlena]

It is working now (even with the brew-installed usingemscripten ). The problem was that I have installed a different version of mata using emsdk than the one installed by the regular means (make). It seems that you have to use the very same version of mata for both installs.

[vhavlena]

Great! It remains to fix the failing tests and we are there.

[jurajsic]

It seems the failing tests are either because we turn off model generation by default (while in Z3 it is always turned on), or because there are quantifiers (and string solver is initialized, which leads to error) => the binding should work correctly