@@ -91,194 +91,3 @@ int asciiPrintable(string char) {
9191 .charAt ( _)
9292 )
9393}
94-
95- /**
96- * Escapes all characters in `s` that have special meaning in regular expressions.
97- */
98- bindingset [ s]
99- string regexpEscape ( string s ) {
100- result = s .regexpReplaceAll ( "([\\\\.*+?\\[^\\]$(){}=!<>|:\\-])" , "\\\\$1" )
101- }
102-
103- /** Provides the input to `InverseAppend`. */
104- signature module InverseAppendInputSig {
105- /** A prefix matching result. */
106- bindingset [ this ]
107- class Result ;
108-
109- /**
110- * Holds if `prefix` is a prefix candidate with resulting value `res`.
111- */
112- predicate prefixCandidate ( string prefix , Result res ) ;
113- }
114-
115- /** Provides the `inverseAppend` predicate. */
116- module InverseAppend< InverseAppendInputSig Input> {
117- /**
118- * Holds if `s = prefix + suffix` with resulting value `res`.
119- *
120- * The predicate avoids unnecessary result fan-out by first constraining the
121- * prefix using a regular expression match.
122- */
123- bindingset [ s]
124- predicate inverseAppend ( string s , string prefix , string suffix , Input:: Result res ) {
125- exists ( string regexp |
126- regexp =
127- "(" +
128- strictconcat ( string prefixCand |
129- Input:: prefixCandidate ( prefixCand , _)
130- |
131- regexpEscape ( prefixCand ) , "|"
132- ) + ").*" and
133- prefix = s .regexpCapture ( regexp , 1 ) and
134- s = prefix + suffix and
135- Input:: prefixCandidate ( prefix , res )
136- )
137- }
138- }
139-
140- /** Provides the input to `InverseAppend1`. */
141- signature module InverseAppend1InputSig {
142- /** A prefix matching context. */
143- bindingset [ this ]
144- class C ;
145-
146- /** A prefix matching result. */
147- bindingset [ this ]
148- class Result ;
149-
150- /**
151- * Holds if `prefix` is a prefix candidate in the context `c`
152- * with resulting value `res`.
153- */
154- predicate prefixCandidate ( string prefix , C c , Result res ) ;
155- }
156-
157- /** Provides the `inverseAppend` predicate. */
158- module InverseAppend1< InverseAppend1InputSig Input> {
159- /**
160- * Holds if `s = prefix + suffix` in the context `c` with resulting
161- * value `res`.
162- *
163- * The predicate avoids unnecessary result fan-out by first constraining the
164- * prefix using a regular expression match.
165- */
166- bindingset [ s]
167- predicate inverseAppend ( string s , string prefix , string suffix , Input:: C c , Input:: Result res ) {
168- exists ( string regexp |
169- regexp =
170- "(" +
171- strictconcat ( string prefixCand |
172- Input:: prefixCandidate ( prefixCand , c , _)
173- |
174- regexpEscape ( prefixCand ) , "|"
175- ) + ").*" and
176- prefix = s .regexpCapture ( regexp , 1 ) and
177- s = prefix + suffix and
178- Input:: prefixCandidate ( prefix , c , res )
179- )
180- }
181- }
182-
183- /** Provides the input to `InverseAppend2`. */
184- signature module InverseAppend2InputSig {
185- /** A prefix matching context. */
186- bindingset [ this ]
187- class C1 ;
188-
189- /** A prefix matching context. */
190- bindingset [ this ]
191- class C2 ;
192-
193- /** A prefix matching result. */
194- bindingset [ this ]
195- class Result ;
196-
197- /**
198- * Holds if `prefix` is a prefix candidate in the context `(c1, c2)`
199- * with resulting value `res`.
200- */
201- predicate prefixCandidate ( string prefix , C1 c1 , C2 c2 , Result res ) ;
202- }
203-
204- /** Provides the `inverseAppend` predicate. */
205- module InverseAppend2< InverseAppend2InputSig Input> {
206- /**
207- * Holds if `s = prefix + suffix` in the context `(c1, c2)` with resulting
208- * value `res`.
209- *
210- * The predicate avoids unnecessary result fan-out by first constraining the
211- * prefix using a regular expression match.
212- */
213- bindingset [ s]
214- predicate inverseAppend (
215- string s , string prefix , string suffix , Input:: C1 c1 , Input:: C2 c2 , Input:: Result res
216- ) {
217- exists ( string regexp |
218- regexp =
219- "(" +
220- strictconcat ( string prefixCand |
221- Input:: prefixCandidate ( prefixCand , c1 , c2 , _)
222- |
223- regexpEscape ( prefixCand ) , "|"
224- ) + ").*" and
225- prefix = s .regexpCapture ( regexp , 1 ) and
226- s = prefix + suffix and
227- Input:: prefixCandidate ( prefix , c1 , c2 , res )
228- )
229- }
230- }
231-
232- /** Provides the input to `InverseAppend3`. */
233- signature module InverseAppend3InputSig {
234- /** A prefix matching context. */
235- bindingset [ this ]
236- class C1 ;
237-
238- /** A prefix matching context. */
239- bindingset [ this ]
240- class C2 ;
241-
242- /** A prefix matching context. */
243- bindingset [ this ]
244- class C3 ;
245-
246- /** A prefix matching result. */
247- bindingset [ this ]
248- class Result ;
249-
250- /**
251- * Holds if `prefix` is a prefix candidate in the context `(c1, c2, c3)`
252- * with resulting value `res`.
253- */
254- predicate prefixCandidate ( string prefix , C1 c1 , C2 c2 , C3 c3 , Result res ) ;
255- }
256-
257- /** Provides the `inverseAppend` predicate. */
258- module InverseAppend3< InverseAppend3InputSig Input> {
259- /**
260- * Holds if `s = prefix + suffix` in the context `(c1, c2, c3)` with resulting
261- * value `res`.
262- *
263- * The predicate avoids unnecessary result fan-out by first constraining the
264- * prefix using a regular expression match.
265- */
266- bindingset [ s]
267- predicate inverseAppend (
268- string s , string prefix , string suffix , Input:: C1 c1 , Input:: C2 c2 , Input:: C3 c3 ,
269- Input:: Result res
270- ) {
271- exists ( string regexp |
272- regexp =
273- "(" +
274- strictconcat ( string prefixCand |
275- Input:: prefixCandidate ( prefixCand , c1 , c2 , c3 , _)
276- |
277- regexpEscape ( prefixCand ) , "|"
278- ) + ").*" and
279- prefix = s .regexpCapture ( regexp , 1 ) and
280- s = prefix + suffix and
281- Input:: prefixCandidate ( prefix , c1 , c2 , c3 , res )
282- )
283- }
284- }
0 commit comments