Integration of CVC4 into JavaSMT

[PhilippWendler]

No description provided.

[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.

[cheshire]

Ah ok, maybe they did not know that finalizer actually runs in a separate
thread and needs locking?

On Wed, Jan 13, 2016 at 1:20 PM, Thomas Stieglmaier <
notifications@github.com> wrote:

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
https://github.com/sosy-lab/java-smt/files/88810/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.

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

[PhilippWendler]

The CVC4 classes should be made package-private, like all the other solvers.

[cheshire]

Hi,

any updates?

We're definitely not going to write our own JNI bindings for CVC4. However, we should also be somewhat sure that the problem is indeed a finalizer-associated race condition.
It seems very unlikely that such a race condition would be 100% stable on our machines and 100% crash on Travis ones.

Can we somehow increase our certainty is that we are definitely not missing any dependencies on Travis? It still looks like a more likely culprit to me.

If their Java API is unstable, we should move the package to a separate branch.

[stieglma]

Hey George,
I think you can move CVC4 to a separate branch, as up to now I could not figure out how to solve the problem. The finalizing issue is also not the only one. The bigger problem is, that there is most likely still a linking problem somewhere (Unit tests can be run when directly clicking on them in the IDE separately, but when trying to run the whole project as unit test we get the same error as on travis which says no tests were found).

[PhilippWendler]

The README of JavaSMT still claims that support for CVC4 is coming soon. I guess this won't happen, so we should remove this claim.

[cheshire]

@PaulMeng any comments? Is your branch working? https://github.com/PaulMeng/java-smt/tree/cvc4_integration_iowa I can see a few commits were done in December.

[PaulMeng]

Hi @cheshire, My branch is based on the old CVC4 java api, which has some memory-racing issues, and it does not fully support all the JavaSMT features. But we are still actively working on this. And it was in charged by another person since Jan. Now I think he's been working on fixing those CVC4 issues that we talked about in the past.

[kfriedberger]

Work in progress. Implementation and bindings will be updated by a student.

[kfriedberger]

CVC4 binary is available via Ivy now. Some parts are working. There seem to be SegFaults when GC removes CVC4-Objects. The problem is the usage of finalize in Swig.

[PhilippWendler]

Let's close this and add specific issues for the open problems?

[kfriedberger]

Closing this issue as integration as such is finished.
The rest, such as a remaining problem is mentioned in #169.