Dependencies in the .jar release

[daniel-raffler]

Hello everyone,
we'd like to use SMTInterpol together with lasso-ranker from the Ultimate repository. Both tools depend on the SMTLIB library (here for SMTInterpol, and here for lasso-ranker) and include different versions of it in their release. When SMTInterpol and lasso-ranker are used together, it seems to be random which version of the library is loaded, and this is causing us crashes as the Ultimate version of the library is missing some newer symbols that are needed by SMTInterpol.

Would it be possible to factor out this library and have it released separately so that SMTInterpol and lasso-ranker can depend on the same version?

We've run into this issue some time ago (see here and here) and were unable to find any easy fix on our side. Currently it is blocking us from upgrading to a newer version of SMTInterpol (see this issue) as we would have to give up using lasso-ranker for it.

[jhoenicke]

What would be the best solution here? @Heizmann

I think the differences between Ultimate's SMTLIB and SMTInterpol should now be gone, right?

I would like to keep LibrarySMTLIB inside smtinterpol repository, as we often have to change it for tweaking the logic, fixing bugs etc. We can make it a separate maven package if that helps. But then lasso-ranker and ultimate automizer would need to include this maven package.

I'm not that familiar with maven myself to know if there is a simple solution for this. But the current way of manually updating smtinterpol in the ultimate repository is probably also not ideal.

There's also the issue with javacup IIRC, so the javacup runtime needs to be another separate maven package?

[daniel-raffler]

Hello Jochen,
thanks for looking into this issue! There is now a PR here that would make SMTInterpol a regular dependency for the Ultimate repository. I've tested it recently, and it does take care of most of the collisions. However, there is still some overlap in de.uni_freiburg.informatik.ultimate.util:

• Here is the SMTInterpol package
• ... and this is the same package in the Ultimate repository

The package only has 5 files in SMTInterpol, while it is much larger for Ultimate. Would it maybe be possible to move the package from de.uni_freiburg.informatik.ultimate.util to de.uni_freiburg.informatik.ultimate.logic.util (or something similar) in SMTInterpol? As far as I can see the classes in the package are only used internally, so changing their location should be save. This would then allow Ultimate to continue using the original de.uni_freiburg.informatik.ultimate.util package name without causing any collisions

There's also the issue with javacup IIRC, so the javacup runtime needs to be another separate maven package?

Ideally, yes. However, from what I can see SMTInterpol and Ultimate both use the same version of javacup, so the duplicates are probably fine for now