search

ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
200 stars 41 forks source link

Wip/lf/pea complement only #670

Closed henkele closed 3 months ago

henkele commented 3 months ago

Implements PEA complement and redundancy analysis

danieldietsch commented 3 months ago

Due to the size, reviewing this will take some time.

bahnwaerter commented 3 months ago

[...] @bahnwaerter , perhaps we could look into a pre-commit hook and a CI check? [...]

That's a good idea. Using a linter, we could also check compliance with the styles in the CI pipeline before a merge takes place. However, we still need to think about a strategy, because there are still a lot of (old) source code fragments that do not follow the current style. But all of that is not the content of this topic and should become a new discussion on quality improvement of the code in general.

danieldietsch commented 3 months ago

@henkele @Langenfeld I fixed the various CC issues in 1a1883ad4c5d106f36f8dc9d181b594c3f141fff. From my side, only the issues with CDD.getDecisionsConjunction() remain.

danieldietsch commented 3 months ago

Oh, and I just realized: not all new files have copyright headers. Could you check for 

A       trunk/source/Library-PEA/src/de/uni_freiburg/informatik/ultimate/lib/pea/InitialTransition.java
A       trunk/source/Library-PEA/src/de/uni_freiburg/informatik/ultimate/lib/pea/PEAComplement.java
A       trunk/source/Library-PEATest/src/de/uni_freiburg/informatik/ultimate/lib/pea/test/CddUnitTest.java
A       trunk/source/Library-PEATest/src/de/uni_freiburg/informatik/ultimate/lib/pea/test/ComplementPEATest.java
A       trunk/source/Library-PEATest/src/de/uni_freiburg/informatik/ultimate/lib/pea/test/RangeDecisionTest.java
A       trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/RedundancyTransformer.java
A       trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/RedundancyTransformerReq2Pea.java
A       trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRedundancyRegressionTestSuite.java