@@ -2497,6 +2497,18 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
24972497 )
24982498 }
24992499
2500+ /** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */
2501+ private predicate pathSucc ( PathNodeImpl n1 , PathNodeImpl n2 ) {
2502+ n1 .getANonHiddenSuccessor ( _) = n2 and directReach ( n2 )
2503+ }
2504+
2505+ private predicate tcSrc ( PathNodeImpl n ) { n .isSource ( ) }
2506+
2507+ private predicate tcSink ( PathNodeImpl n ) { n .isSink ( ) }
2508+
2509+ private predicate pathSuccPlus ( PathNodeImpl n1 , PathNodeImpl n2 ) =
2510+ doublyBoundedFastTC( pathSucc / 2 , tcSrc / 1 , tcSink / 1 ) ( n1 , n2 )
2511+
25002512 private module DistancePruning {
25012513 private predicate isAnySource ( PathNodeImpl n ) { n .isArbitrarySource ( ) }
25022514
@@ -2520,15 +2532,25 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
25202532
25212533 private int sinkDist ( PathNodeImpl n ) { result = sinkDist1 ( n ) - 1 }
25222534
2535+ private int srcSinkDiff ( ) {
2536+ exists ( PathNodeImpl src , PathNodeImpl sink |
2537+ pathSuccPlus ( src , sink ) and
2538+ result = sinkDist ( src ) - srcDist ( sink )
2539+ )
2540+ }
2541+
25232542 private int pathLength ( ) {
2524- exists ( int fwdLen , int revLen |
2525- result = fwdLen .maximum ( revLen ) and
2543+ exists ( int fwdLen , int revLen , int srcSpread , int sinkSpread |
2544+ // result = fwdLen.maximum(revLen) and
2545+ result = ( fwdLen + revLen + srcSpread + sinkSpread ) / 2 and
25262546 fwdLen = max ( PathNodeImpl n | n .isSink ( ) | srcDist ( n ) ) and
2527- revLen = max ( PathNodeImpl n | n .isSource ( ) | sinkDist ( n ) )
2547+ revLen = max ( PathNodeImpl n | n .isSource ( ) | sinkDist ( n ) ) and
2548+ srcSpread = max ( srcSinkDiff ( ) ) and
2549+ sinkSpread = max ( - srcSinkDiff ( ) )
25282550 )
25292551 }
25302552
2531- private int slack ( ) { result = 15 }
2553+ private int slack ( ) { result = 0 }
25322554
25332555 predicate nearShortestDirectReach ( PathNodeImpl n ) {
25342556 directReach ( n ) and
@@ -2609,16 +2631,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
26092631 }
26102632
26112633 /** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */
2612- private predicate pathSucc ( PathNodeImpl n1 , PathNodeImpl n2 ) {
2634+ private predicate pathSucc_2 ( PathNodeImpl n1 , PathNodeImpl n2 ) {
26132635 n1 .getANonHiddenSuccessor ( _) = n2 and directReach_2 ( n2 )
26142636 }
26152637
2616- private predicate tcSrc ( PathNodeImpl n ) { n .isSource ( ) }
2617-
2618- private predicate tcSink ( PathNodeImpl n ) { n .isSink ( ) }
2619-
2620- private predicate pathSuccPlus ( PathNodeImpl n1 , PathNodeImpl n2 ) =
2621- doublyBoundedFastTC( pathSucc / 2 , tcSrc / 1 , tcSink / 1 ) ( n1 , n2 )
2638+ private predicate pathSuccPlus_2 ( PathNodeImpl n1 , PathNodeImpl n2 ) =
2639+ doublyBoundedFastTC( pathSucc_2 / 2 , tcSrc / 1 , tcSink / 1 ) ( n1 , n2 )
26222640
26232641 /**
26242642 * Holds if data can flow from `source` to `sink`.
@@ -2642,7 +2660,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
26422660 source = flowsource and sink = flowsink
26432661 |
26442662 flowsource .isSource ( ) and
2645- ( flowsource = flowsink or pathSuccPlus ( flowsource , flowsink ) ) and
2663+ ( flowsource = flowsink or pathSuccPlus_2 ( flowsource , flowsink ) ) and
26462664 flowsink .isSink ( )
26472665 )
26482666 }
0 commit comments