Generalize abstractor, refiner, cegarchecker, visualizer

[RipplB]

These classes/interfaces depended on ARG and Trace before, which heavily limits reusability. They are now generalized over Witness and Cex. To ease the switch, the old entry points are replicated in "Arg..." classes, so a lot of these changes are just renames.

[RipplB]

Witness should be renamed to Proof

[RipplB]

@AdamZsofi @leventeBajczi @mondokm @szdan97 What should be the generic template letter associated with Proof? (as P usually means Precision)

[RipplB]

Refiner does not need S and A

[leventeBajczi]

@AdamZsofi @leventeBajczi @mondokm @szdan97 What should be the generic template letter associated with Proof? (as P usually means Precision)

If you're still undecided about this, I'd go simply with PROOF, SafetyProof, or something similar. I don't think it's necessary to use single-letter abbreviations. If we do stick with single-letter ones, I'd advocate for something unrelated, such as Q (the next letter to P).

[AdamZsofi]

@AdamZsofi @leventeBajczi @mondokm @szdan97 What should be the generic template letter associated with Proof? (as P usually means Precision)

I like Proof - SafetyProof is a bit long in my opinion. PROOF works as well. (I don't see any reason to stick to single letters.)

[leventeBajczi]

@AdamZsofi @leventeBajczi @mondokm @szdan97 What should be the generic template letter associated with Proof? (as P usually means Precision)

I like Proof - SafetyProof is a bit long in my opinion. PROOF works as well. (I don't see any reason to stick to single letters.)

I don't think it can be Proof, as that would cause a circular name resolution with a class/iface named Proof.

[RipplB]

We settled with Pr for now @leventeBajczi @AdamZsofi

[leventeBajczi]

We settled with Pr for now @leventeBajczi @AdamZsofi

That will clear up prec and proof

[leventeBajczi]

Just a heads up: we merged #305, and because the IntelliJ formatter had a version mismatch in the CI (2023.x) and offline (2024.x), we ran the reformat. However, it seems like the code style xml is not IDEA version agnostic. This is honestly a big surprise for me, as I would have expected it to remain stable. I will try and port our code style XML to a checkstyle-based solution, as that is way better in a lot of ways (you could run it as a gradle task, also possibly in a pre-commit hook, and also, hopefully it will stay stable).

I just wanted to let you know that you probably should not merge these changes you see between master and your fork until this work is done, so that you don't have to do it multiple times.

Sorry!

[leventeBajczi]

See #306 for (hopefully) getting rid of these merge issues.

[sonarcloud[bot]]

Quality Gate failed

Failed conditions
54.0% Coverage on New Code (required ≥ 60%)

See analysis details on SonarCloud