Refactor assert orders #699
Conversation
schuessf
requested review from
maul-esel,
Heizmann,
bahnwaerter and
danieldietsch
...g/informatik/ultimate/lib/tracecheckerutils/assertorders/AssertOrderSmtFeatureHeuristic.java
Outdated
Show resolved
Hide resolved
|
|
||
| /** | ||
| * Partition the statement positions between lowerIndex and upperIndex according to their depth. (See documentation | ||
| * for the meaning of 'depth'). The result is stored in the map 'depth2Statements'. The partitioning is done |
There was a problem hiding this comment.
Where is this documentation regarding the meaning of "depth"?
There was a problem hiding this comment.
Should be fixed, this part was removed and some documentation added to partitionStatementsAccordingDepth.
| mAnnotSSA.setFormulaAtNonCallPos(i, mAnnotateAndAssertCodeBlocks.annotateAndAssertNonCall(i)); | ||
| } | ||
| } | ||
|
|
||
| assert callPositions.containsAll(mTrace.getCallPositions()); | ||
| assert mTrace.getCallPositions().containsAll(callPositions); |
There was a problem hiding this comment.
Did you intend to remove these checks?
There was a problem hiding this comment.
Oh, that's interesting: These checks were not present in AnnotateAndAsserterWithStmtOrderPrioritization (which is the basis for the new AnnotateAndAsserter). Therefore I also removed the variable callPositions, because it was unused. But I think it does not hurt to add these checks again.
There was a problem hiding this comment.
Wait, these assertions state that all calls of the trace are already asserted. This is only reasonable, if the whole SSA is asserted here. We could keep the second assertion, but it would be trivially satisfied, since for all i, if trace.isCallPosition(i) is true, then i is element of trace.getCallPositions(). So I think it is reasonable to remove these assertions.
This is already checked in Counterexample::requireControlConfigurations
This PR aims to refactor the assert orders. Currently the situation is as follows:
AssertCodeBlockOrderType).NOT_INCREMENTALLYis handled in the classAnnotateAndAsserter, while all the others are handled in the subclassAnnotateAndAsserterWithStmtOrderPrioritization(that hardly makes use of the methods of the superclass).AnnotateAndAsserterWithStmtOrderPrioritizationare just methods (e.g.annotateAndAssertOutsideLoopFirst1) that doe not only the partitioning of the trace, but also asserts the SSA directly and thus returns aLBool.This situation is not nice for several reasons:
NOT_INCREMENTALLYdoes not need any special handling, it can be also seen as an assert order that partitions the trace into a single partition.AnnotateAndAsserterWithStmtOrderPrioritizationcontains many methods that just belong to a single assertion order.Therefore the following changes were made:
IAssertOrderwith a single methods that performs the partitioning, but not the assertion itself.AnnotateAndAsserterWithStmtOrderPrioritizationto the new classAssertOrderUtilsNOT_INCREMENTALLYthere exists also an implementation ofIAssertOrder,AssertOrderNotIncrementally. ThereforeAnnotateAndAsserteris no more required and thus was deleted andAnnotateAndAsserterWithStmtOrderPrioritizationwas renamed toAnnotateAndAsserterAnnotateAndAsserterwe first create an instance of the desiredIAssertOrderingetAssertOrder, perform the partioning and then assert the partioned SSA inannotateAndAssert(which was previosuly performed by every assert order itself).Note: I ran already the nightly build, but there was a small bug (connected to #692). I just fixed it and re-ran the nightly build.