Dependent parameters, z3, java.library path

[xhajnal]

Selecting dependent parameters on run parameter synthesis in \biodivine-GUI results in error:
"
PID: 10288
Exception in thread "main" java.lang.UnsatisfiedLinkError: no libz3java in java.library.path
at java.lang.ClassLoader.loadLibrary(Unknown Source)
at java.lang.Runtime.loadLibrary0(Unknown Source)
at java.lang.System.loadLibrary(Unknown Source)
at com.microsoft.z3.Native.(Native.java:14)
at com.microsoft.z3.Context.(Context.java:37)
at com.github.sybila.ode.generator.smt.Z3Kt.(z3.kt:10)
at com.github.sybila.ode.generator.smt.SMTOdeFragment.(SMTOdeFragment.kt:18)
at com.github.sybila.biodivine.exe.MainKt.main(Main.kt:96)
"
Please change java.library path in code

[daemontus]

This comment is a set of proposed solutions, becasue this turns out to be a bigger problem than expected.

What we need: Each process has it's own copy of the shared z3 library (necessary for parallel execution) because of file locking.

The "No fix" solution

We say that each user has to figure out on their own how to properly link their z3 with biodivine.
Upside: No work for us.
Downside: Crappy user experience. Possible version and parallel execution problems.

The "Bundled Z3" solution

We bundle a Z3 executable (.dylib, .dll, .so) with the distribution and add the APP_HOME modifier to the startup script.
Upside: Easy to cover most users (ubuntu, windows) + one vanilla "no fix" binary. We control the z3 version (z3 has bugs!).
Downside: Platform dependant distributions. OS X is a special snowflake (see [1])

The "Build your own" solution

We don't bundle anything, but we require the user to copy the shared binaries into a specific directory.
Upside: Less work than bundling, but similar effect.
Downside: We don't control z3 version. User has to build. OS X still won't work.