The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
At the moment, the splits arising from disjuncts are processed "eagerly". Imagine this is our situation, and we are processing additions in the current state:
Here, we are about to process the disjunct. However, we have already processed some other term which produced a new state with the given delta (+(x==y+1)). Processing the disjunct will cause a split leading to the following (temporary) position:
The key is that the next state to be processed will be the first split state (marked next above). At this point, the delta between current and next will be computed as: +(x==y+1), +(x), -(x || y). This is suboptimal because it means the term x == y+1will be processed separately on both branches.
At the moment, the splits arising from disjuncts are processed "eagerly". Imagine this is our situation, and we are processing additions in the current state:
Here, we are about to process the disjunct. However, we have already processed some other term which produced a new state with the given delta (
+(x==y+1)
). Processing the disjunct will cause a split leading to the following (temporary) position:The key is that the next state to be processed will be the first split state (marked
next
above). At this point, the delta betweencurrent
andnext
will be computed as:+(x==y+1)
,+(x)
,-(x || y)
. This is suboptimal because it means the termx == y+1
will be processed separately on both branches.