Document or improve concurrency support for JavaSMT

[kfriedberger]

Currently it is only weakly documented which solvers can use which components in a multi-threaded environment. We should check whether some solvers can use several stacks (for the same context) in parallel and document an exact list of SMT solvers supporting which level of concurrent usage.

This includes:

• a JUnit test for solvers that support multi-threaded usage, i.e., solve two larger formulae in parallel.
• a concrete table for the documentation with more info about solvers.

[baierd]

@kfriedberger Yices2 is not thread safe by default and we need a re-entrant version if we want to use it multithreaded. Yices 2 supports multithreading on seperate contextes only (so not multithreaded stacks).

I've updated the readme to be a bit more clear what solver supports what kind of multithreading at the moment. After we get Yices2 (and maybe OptiMathSAT if you want) re-entrant we can update once more and close this issue as the tests are implemented.

[baierd]

Since i had difficulties running Yices2 in re-entrant mode (unpredictable behavior; SAT/UNSAT on the same problem when running multiple times etc.) i tried several compiliation changes and contacted the devs. The devs tested basicly our tests with their code and even a not yet finished Java wrapper of their own and could not reproduce our results. Additionally i included our wrapper into their makefile to reduce the possibility of the compiliation process being the problem. The bug was persistent however. Either its a system specific problem (so someone else should try compiling it in re-entrant) or we have a bug in our wrapper somewhere.

Guide on how to compile in re-entrant: -Put Yices2 and the gperf, gmp folders into the JavaSMT main folder and compile gmp/gperf (do this with the options given by doc/Developers.md ) -Compile Yices2 in thread-safe mode (described on their github. Simply add --enable-thread-safety to ./configure additionally to the options given by doc/Developers.md ) -Edit the compile.sh located at lib/native/source/yices2j and add -pthread to the gcc calls you need (or all of them to be sure) -Execute compile.sh

Now you should get a re-entrant Yices2 binary in lib/native/source/yices2j.

[baierd]

Current state:

• There is (at least) 1 test that fails on slower systems (CI) sometimes.
• Yices2 is still problematic. (But since development of Yices2 seems stale at the moment i won't pursue further investigation into it at the moment)

[baierd]

Since the problem with the tests described above seems to be only a timeout when initializing threads, it was easily fixable by increasing the timeout time. @kfriedberger would you add more to this issue or can we close it for now?