@@ -35,13 +35,43 @@ module MakeDualGraph<LocationSig Location, DualGraphInputSig<Location> Input> {
3535 TForward ( Node n ) or
3636 TBackward ( Node n )
3737
38+ cached
39+ private module Cached {
40+ /** Gets the node representing the backward node wrapping `n`. */
41+ cached
42+ DualNode getBackwardNode ( Node n ) { result = TBackward ( n ) }
43+
44+ /** Gets the node representing the forward node wrapping `n`. */
45+ cached
46+ DualNode getForwardNode ( Node n ) { result = TForward ( n ) }
47+
48+ /**
49+ * Holds if the dual graph contains the edge `node1 -> node2`. See `MakeDualGraph`.
50+ */
51+ private predicate dualEdge ( DualNode node1 , DualNode node2 ) {
52+ edge ( node1 .asForward ( ) , node2 .asForward ( ) )
53+ or
54+ edge ( node2 .asBackward ( ) , node1 .asBackward ( ) )
55+ or
56+ node1 .asBackward ( ) = node2 .asForward ( )
57+ }
58+
59+ /**
60+ * Holds if there is a non-empty path from `node1 -> node2` in the dual graph.
61+ */
62+ cached
63+ predicate dualPath ( DualNode node1 , DualNode node2 ) = fastTC( dualEdge / 2 ) ( node1 , node2 )
64+ }
65+
66+ import Cached
67+
3868 /** A forward or backward copy of a node from the original graph. */
3969 class DualNode extends TDualNode {
4070 /** Gets the underlying node if this is a forward node. */
41- Node asForward ( ) { this = TForward ( result ) }
71+ Node asForward ( ) { this = getForwardNode ( result ) }
4272
4373 /** Gets the underlying node if this is a backward node. */
44- Node asBackward ( ) { this = TBackward ( result ) }
74+ Node asBackward ( ) { this = getBackwardNode ( result ) }
4575
4676 /** Gets a string representation of this node. */
4777 string toString ( ) {
@@ -58,29 +88,6 @@ module MakeDualGraph<LocationSig Location, DualGraphInputSig<Location> Input> {
5888 }
5989 }
6090
61- /** Gets the node representing the backward node wrapping `n`. */
62- DualNode getBackwardNode ( Node n ) { result .asBackward ( ) = n }
63-
64- /** Gets the node representing the forward node wrapping `n`. */
65- DualNode getForwardNode ( Node n ) { result .asForward ( ) = n }
66-
67- /**
68- * Holds if the dual graph contains the edge `node1 -> node2`. See `MakeDualGraph`.
69- */
70- predicate dualEdge ( DualNode node1 , DualNode node2 ) {
71- edge ( node1 .asForward ( ) , node2 .asForward ( ) )
72- or
73- edge ( node2 .asBackward ( ) , node1 .asBackward ( ) )
74- or
75- node1 .asBackward ( ) = node2 .asForward ( )
76- }
77-
78- /**
79- * Holds if there is a non-empty path from `node1 -> node2` in the dual graph.
80- */
81- cached
82- predicate dualPath ( DualNode node1 , DualNode node2 ) = fastTC( dualEdge / 2 ) ( node1 , node2 )
83-
8491 /**
8592 * Holds if `node1` and `node2` have a common ancestor in the original graph, that is,
8693 * there exists a node from which both nodes are reachable.
0 commit comments