Use SMTInterpol as a Maven dependency

[schuessf]

I recently found that there is a package of SMTInterpol on Maven (with even a more recent version than in Ultimate), therefore I tried to use it in Ultimate, where we currently have a copy of the source code instead.

(This PR is not really urgent though)

Pros:

• The update of SMTInterpol is much simpler: We can just update the version number in Ultimate_E4.32_Java21.target (requires a new version on Maven of course) instead of running a shell script that does some complicated git commands 😉
• We are actually forced to treat SMTInterpol like an external dependecy and don't accidentally modifiy its code, which can lead to diverged versions of SMTInterpol in Ultimate and the "original" (see also some cases below).

Cons:

• The dependencies are not seperated anymore between the actual solver (SMTInterpol) and necessary datastructures / utilities etc. (Library-SMTLIB). For example, even if a plugin just needs classes like Script or Term, the same package (wrapped.de.uni-freiburg.informatik.ultimate.smtinterpol) has to be included, as if the actual solver is used.
• Possible issues of SMTInterpol are not shown anymore in Ultimate's Jenkins and Sonar. If we really want that, we could have Jenkins and Sonar for SMTInterpol, or just copy the tests to run them also in Ultimate.

Regarding the second pro: There are actually a few changes that I found in Ultimate's version of SMTInterpol that are not present in the original code:

• INonSolverScript and DebugMessage were only created in Ultimate's version of SMTInterpol, therefore I moved them to Library-SmtLibUtils instead (75f5f80).
• ddd1310 and 6d19ff8 modified ConstantTermNormalizer (which is only used in Ultimate) to fix a bug. There is even a PR for SMTInterpol (Move ConstantTermNormalizer smtinterpol#150). As a workaround (to run the tests successfully), I copied the files to Ultimate (640085e), but instead the PR should be merged (@Heizmann)
• 16acc54 (is actually integrated) and c9b6d9b made minor changes. Is this crucial @Heizmann?

[danieldietsch]

In the past, we did not do this because

1. we are afraid of changes in SMTInterpol that break things in Ultimate
2. we wanted to be able to make our own modifications to SMTInterpol if necessary
3. there was no Maven version
4. the process of integrating Maven dependencies was complicated
5. we don't want to wait for Maven releases
6. we want to be able to use unreleased SMTInterpol features, like specific branches, where students implemented new algorithms
7. we want to be able to read the SMTInterpol source while debugging

Point 1 might be ok given the retention of Maven versions.
Point 2 is still an issue: see he very old PR that doesn't get merged, and see the "minor" changes: the first is allowing us to use more logics than the official SMTInterpol, and they don't include them because of philosophy, the second deals with quoting of our identifiers, which would also not make any sense in an SMTInterpol release.
Points 3 and 4 are not issues anymore.
Point 5 and 6 are still issues.
Point 7 is also doable with Maven dependencies if they contain the source (I did not check if this PR retains that ability)

I am in favor of not merging this PR and keeping our SMTInterpol dependencies manual.
The updating is also not really much simpler. As it is, we have a script that performs an update to any SMTInterpol branch and it works sufficiently well that there are not really any manual interactions necessary (perhaps a manual git add for test cases).

I get that we like to rely on standardized tools and hence, want to get rid of some crummy scripts that are necessary for some tasks. But the right^TM way of doing that would mean forking SMTInterpol and maintaining that fork, complete with our own releases for it. This would still complicate point 6, although there are ways to deal with that (which probably also involve a script if you don't want to pollute some public release repository or set up and maintain a private one).

[schuessf]

2. we wanted to be able to make our own modifications to SMTInterpol if necessary

Point 2 is still an issue: see he very old PR that doesn't get merged, and see the "minor" changes: the first is allowing us to use more logics than the official SMTInterpol, and they don't include them because of philosophy, the second deals with quoting of our identifiers, which would also not make any sense in an SMTInterpol release.

6. we want to be able to use unreleased SMTInterpol features, like specific branches, where students implemented new algorithms

I see, if we want to deviate from the official SMTInterpol, we cannot just use the Maven build.
I am not sure though, if there are students that will implement something new in SMTInterpol.
Nevertheless, I don't think we should be able to modify code of SMTInterpol in Ultimate (this got even worse because of the coding conventions). If we still want to be able to use "unofficial" SMTInterpol versions, we should have another solution (maybe using a fork).

7. we want to be able to read the SMTInterpol source while debugging

Point 7 is also doable with Maven dependencies if they contain the source (I did not check if this PR retains that ability)

Yes, they Maven dependencies also contain the source files. This behviour seems also good to me, as you can view the sources and even set breakpoints there, but you cannot modify the sources.

[danieldietsch]

We had two cases that I can remember where students implemented things for us in SMTInterpol and we did experiments with that, but those cases were of course together with the SMTInterpol people. Nevertheless, it would have been complicated to run experiments if we would have needed to go through Maven to integrate.

If you like, we can have a meeting and talk about what would be needed for a fork and what we could do to support this scenario.

And, of course, perhaps @maul-esel or @Heizmann also have additional pointers.

[schuessf]

Point 2 is still an issue: see he very old PR that doesn't get merged, and see the "minor" changes: the first is allowing us to use more logics than the official SMTInterpol, and they don't include them because of philosophy, the second deals with quoting of our identifiers, which would also not make any sense in an SMTInterpol release.

So, I did already run Jenkins and even without those two commits (only with the fix for the unmerged PR), all tests seem to pass.

We had two cases that I can remember where students implemented things for us in SMTInterpol and we did experiments with that, but those cases were of course together with the SMTInterpol people. Nevertheless, it would have been complicated to run experiments if we would have needed to go through Maven to integrate.

If you like, we can have a meeting and talk about what would be needed for a fork and what we could do to support this scenario.

I think, I have an idea:

• We could have a fork of SMTInterpol, where we can apply out desired changes (and additional ones for student projects or experiments)
• Then, we can just build it (using ant) and move the keep the JAR in our own P2.
• In Ultimate we can then just use the version from our P2 instead of Maven. So, everything should be the same as in this PR, with just a small change in the target file.

This way, we can be more flexible to change SMTInterpol to our needs, without the need to duplicate the code in the Ultimate repo.

But again: This is not really urgent, I just wanted to try if using SMTInterpol as a dependency does work 😉

[danieldietsch]

That is probably the best way, yes.