Integration of CVC4 into JavaSMT

[PhilippWendler]

[stieglma]

I just did some research on that, CVC4 is written in C++. Java bindings can be generated via swig. They seem to be quite useful, however they use finalizers. So the question is if we want to use the bindings or, equal to Z3 and Mathsat create the JNI wrapper ourselves. (Type hierarchy, no need to handle pointer on our side and also no need to create the JNI wrapper versus the usage of finalizers)

[cheshire]

Can we at least convince CVC4 to switch away from finalizers? :P (since they edit the auto-generated code already). We would need supporting data though.

[stieglma]

CVC4 is now (at least partly) integrated in java-smt. Several methods are missing and currently only implemented by throwing an Exception, and also some Unit-Tests do up to now not work properly. Therefore I did not add CVC4 to the Solvers enum right now. I will do that later on when the implementation passes the unit-tests.

After the integration of CVC4 in our ivy-repository I recognized one thing:
While ant resolves all dependencies for the solvers correctly (including binaries). The binaries are saved in the lib/java/runtime/ folder. Shouldn't they be in lib/native/x86_64-linux/? I then found out that in the latter there are symlinks to the .so files in the runtime folder. I think there should be some documentation about that.

[cheshire]

Wow, impressively fast!

On binaries: yeah, they go to java/runtime/ because Ivy puts them there.
I don't know whether it's possible to tell Ivy to put them in a specific directory.

[cheshire]

So what is the status of this? When I've tried to run it, it was dying with some link error.

[stieglma]

I'm working on it at the moment, the linking errors are resolved, but there are a couple of other issues I am fixing right now.

[stieglma]

I just pushed all changes and added versions of CVC4 that look at the right places for the dynamically linked libraries. Locally all unit tests are passing (besides dumping and parsing which I have disabled for CVC4 for now). But on travis the unit-tests don't work. I can only guess why, perhaps of further linking errors (e.g. libgmp is missing or so)

[cheshire]

Thanks a lot!

We need to have Travis working though. https://docs.travis-ci.com/user/installing-dependencies/ can you have a look? They expose an interface for managing dependencies.

Alternatively, can we bundle libgmp as well? We do that for CPAchecker anyway (inside Apron). LGPL should allow us to do that.

[cheshire]

Container infrastructure does not support sudo commands, but we can still use ubuntu packages: https://docs.travis-ci.com/user/apt/

[stieglma]

I tested on a few other computers, too. And found out that following error occurs (different for each Unit-Test file):
No tests found in org.sosy_lab.solver.test.SolverAllSatTest

However when these tests are executed from an IDE they work. I hope I can fix this tomorrow, but if you have any suggestions on that which might help I would be very glad.

You can also see it here (I uploaded the JUnit.html to my webserver):
http://stieglmaier.me/JUnit.html#UfDeclarationImplTest

[cheshire]

But before CVC4 integration the tests worked just fine...

I think it has to be some sort of UnsatisfiedLinkError, which perhaps
causes a cascade of other errors.

On Tue, Jan 12, 2016 at 2:57 PM, Thomas Stieglmaier <
notifications@github.com> wrote:

I tested on a few other computers, too. And found out that following error
occurs (different for each Unit-Test file):
No tests found in org.sosy_lab.solver.test.SolverAllSatTest

However when these tests are executed from an IDE they work. I hope I can
fix this tomorrow, but if you have any suggestions on that which might help
I would be very glad.

You can also see it here (I uploaded the JUnit.html to my webserver):
http://stieglmaier.me/JUnit.html#UfDeclarationImplTest

—
Reply to this email directly or view it on GitHub
#2 (comment).

[cheshire]

We also should package the sources of CVC4 Java bindings as well.

[cheshire]

Had to temporarily disabled it to get a reliable integration on.

[stieglma]

I did some more research and the problems seem to be related to issues with the Finalizer thread,. this can be seen in this logfile: hs_err_pid3981.txt

I am still curious why this is not happening on sosy-lab machines, but only on travis and other computers, but I also have no idea how we could fix this without writing our own Java bindings (and this is not an option for me) which do not use finalizers.