@@ -38,6 +38,13 @@ predicate hasNameWithNumberSuffix(Predicate p, string name, int n) {
38
38
p .getName ( ) = name + n .toString ( )
39
39
}
40
40
41
+ pragma [ noinline]
42
+ predicate isHelperPredicate ( string orgName , string helperName ) {
43
+ orgName = any ( Predicate p ) .getName ( ) and
44
+ helperName =
45
+ orgName .regexpCapture ( "(.+)" + [ "0" , "helper" , "aux" , "cand" , "Helper" , "Aux" , "Cand" ] , 1 )
46
+ }
47
+
41
48
/**
42
49
* A candidate predicate for another predicate.
43
50
*
@@ -47,15 +54,14 @@ predicate hasNameWithNumberSuffix(Predicate p, string name, int n) {
47
54
class CandidatePredicate extends Predicate {
48
55
Predicate pred ;
49
56
57
+ pragma [ nomagic]
50
58
CandidatePredicate ( ) {
51
59
// This predicate "guards" the predicate `pred` (i.e., it's always evaluated before `pred`).
52
60
guards ( this , pred .getBody ( ) ) and
53
61
(
54
62
// The name of `pred` is "foo", and the name of this predicate is `foo0`, or `fooHelper`, or any
55
63
// other the other cases.
56
- pragma [ only_bind_into ] ( pred ) .getName ( ) =
57
- this .getName ( )
58
- .regexpCapture ( "(.+)" + [ "0" , "helper" , "aux" , "cand" , "Helper" , "Aux" , "Cand" ] , 1 )
64
+ isHelperPredicate ( this .getName ( ) , pred .getName ( ) )
59
65
or
60
66
// Or this predicate is named "foo02" and `pred` is named "foo01".
61
67
exists ( int n , string name |
@@ -66,6 +72,7 @@ class CandidatePredicate extends Predicate {
66
72
}
67
73
68
74
/** Holds if this predicate is a candidate predicate for `p`. */
75
+ pragma [ nomagic]
69
76
predicate isCandidateFor ( Predicate p ) { p = pred }
70
77
}
71
78
0 commit comments