001 package escjava.vcGeneration.pvs;
002
003 import java.io.*;
004
005 import escjava.vcGeneration.*;
006
007 class TProofSimplifier extends TVisitor {
008
009 TProofSimplifier() {
010 // The term itself is modified, so no need for an output stream here
011 super(null);
012 }
013
014 /*
015 * Generic functions used by different visit* functions
016 */
017 public void visitTFunction(/*@ non_null @*/TFunction n) throws IOException {
018
019 int i = 0;
020 int sizeTemp = n.sons.size();
021
022 /* recursive call on the sons */
023 for (; i <= n.sons.size() - 1;) {
024
025 sizeTemp = n.sons.size();
026 n.getChildAt(i).accept(this);
027
028 /*
029 * If a son has been deleted, do not increase index
030 */
031 if (!(sizeTemp > n.sons.size()))
032 ++i;
033
034 }
035
036 }
037
038 /*
039 * Methods used to simplify the proof
040 */
041
042 // @ requires indexOfSons >= 0 & indexOfSons <= n.sons.size() - 1;
043 /*@
044 @ requires n.sons.contains(m);
045 @*/
046 public void simplify(/*@ non_null @*/TBoolRes n, TNode m) {
047
048 int i = 0;
049
050 //++
051 if ((i = n.sons.indexOf(m)) == -1)
052 TDisplay.err(this, "simplify(TBoolAnd n, TNode m)",
053 "!n.sons.contains(m)");
054 //++
055 else
056 n.sons.remove(i);
057
058 /*
059 * Behavior of simplification process done here.
060 */
061 i = n.sons.size();
062
063 if (i >= 2)
064 ; // this node still makes sense, do nothing
065 else {
066
067 if (i == 1) {
068 // check that the remaining node returns a boolean
069
070 //++
071 if (!(n.getChildAt(0) instanceof TBoolRes))
072 TDisplay
073 .err(this, "simplify(TBoolRes n, TNode m)",
074 "Remaining child does not return a boolean, continuing anyway...");
075 //++
076
077 /*
078 this piece of code delete the BoolAnd node and add the sons
079 to its parent.
080 ie changing x -> n -> m to x -> m
081 */
082 simplify(n.parent, n, m);
083 }
084
085 }
086
087 }
088
089 /*
090 * Node m is replaced by o in the list of sons of n.
091 * Note that after the operation, \old(n.indexOf(m)) == n.indexOf(o);
092 */
093 // @ requires m.sons.contains(o);
094 // @ ensures \old(n.indexOf(m)) == n.indexOf(o);
095 /*@
096 @ requires n.sons.contains(m);
097 @ ensures n.sons.contains(o);
098 @ ensures !n.sons.contains(m);
099 @*/
100 public void simplify(TFunction n, TNode m, TNode o) {
101
102 int i = n.sons.indexOf(m);
103
104 //++
105 if (i == -1)
106 TDisplay.err(this, "simplify(TFunction n, TNode m, TNode o)",
107 "!n.contiains(m)");
108 //++
109
110 n.sons.setElementAt(o, i);
111 }
112
113 /*
114 * non automatic generated class
115 */
116 public void visitTName(/*@ non_null @*/TName n) throws IOException {
117 }
118
119 public void visitTRoot(/*@ non_null @*/TRoot n) throws IOException {
120 for (int i = 0; i <= n.sons.size() - 1; i++)
121 n.getChildAt(i).accept(this);
122 }
123
124 /*
125 * class created using the perl script
126 */
127 public void visitTBoolImplies(/*@ non_null @*/TBoolImplies n) throws IOException {
128 visitTFunction(n);
129 }
130
131 public void visitTBoolAnd(/*@ non_null @*/TBoolAnd n) throws IOException {
132 visitTFunction(n);
133 }
134
135 public void visitTBoolOr(/*@ non_null @*/TBoolOr n) throws IOException {
136 visitTFunction(n);
137 }
138
139 public void visitTBoolNot(/*@ non_null @*/TBoolNot n) throws IOException {
140 visitTFunction(n);
141 }
142
143 public void visitTBoolEQ(/*@ non_null @*/TBoolEQ n) throws IOException {
144 visitTFunction(n);
145 }
146
147 public void visitTBoolNE(/*@ non_null @*/TBoolNE n) throws IOException {
148 visitTFunction(n);
149 }
150
151 public void visitTAllocLT(/*@ non_null @*/TAllocLT n) throws IOException {
152 visitTFunction(n);
153 }
154
155 public void visitTAllocLE(/*@ non_null @*/TAllocLE n) throws IOException {
156 visitTFunction(n);
157 }
158
159 public void visitTAnyEQ(/*@ non_null @*/TAnyEQ n) throws IOException {
160 visitTFunction(n);
161 }
162
163 public void visitTAnyNE(/*@ non_null @*/TAnyNE n) throws IOException {
164 visitTFunction(n);
165 }
166
167 public void visitTIntegralEQ(/*@ non_null @*/TIntegralEQ n) throws IOException {
168 visitTFunction(n);
169 }
170
171 public void visitTIntegralGE(/*@ non_null @*/TIntegralGE n) throws IOException {
172 visitTFunction(n);
173 }
174
175 public void visitTIntegralGT(/*@ non_null @*/TIntegralGT n) throws IOException {
176 visitTFunction(n);
177 }
178
179 public void visitTIntegralLE(/*@ non_null @*/TIntegralLE n) throws IOException {
180 visitTFunction(n);
181 }
182
183 public void visitTIntegralLT(/*@ non_null @*/TIntegralLT n) throws IOException {
184 visitTFunction(n);
185 }
186
187 public void visitTIntegralNE(/*@ non_null @*/TIntegralNE n) throws IOException {
188 visitTFunction(n);
189 }
190
191 public void visitTIntegralAdd(/*@ non_null @*/TIntegralAdd n) throws IOException {
192 visitTFunction(n);
193 }
194
195 public void visitTIntegralDiv(/*@ non_null @*/TIntegralDiv n) throws IOException {
196 visitTFunction(n);
197 }
198
199 public void visitTIntegralMod(/*@ non_null @*/TIntegralMod n) throws IOException {
200 visitTFunction(n);
201 }
202
203 public void visitTIntegralMul(/*@ non_null @*/TIntegralMul n) throws IOException {
204 visitTFunction(n);
205 }
206
207 public void visitTFloatEQ(/*@ non_null @*/TFloatEQ n) throws IOException {
208 visitTFunction(n);
209 }
210
211 public void visitTFloatGE(/*@ non_null @*/TFloatGE n) throws IOException {
212 visitTFunction(n);
213 }
214
215 public void visitTFloatGT(/*@ non_null @*/TFloatGT n) throws IOException {
216 visitTFunction(n);
217 }
218
219 public void visitTFloatLE(/*@ non_null @*/TFloatLE n) throws IOException {
220 visitTFunction(n);
221 }
222
223 public void visitTFloatLT(/*@ non_null @*/TFloatLT n) throws IOException {
224 visitTFunction(n);
225 }
226
227 public void visitTFloatNE(/*@ non_null @*/TFloatNE n) throws IOException {
228 visitTFunction(n);
229 }
230
231 public void visitTFloatAdd(/*@ non_null @*/TFloatAdd n) throws IOException {
232 visitTFunction(n);
233 }
234
235 public void visitTFloatDiv(/*@ non_null @*/TFloatDiv n) throws IOException {
236 visitTFunction(n);
237 }
238
239 public void visitTFloatMod(/*@ non_null @*/TFloatMod n) throws IOException {
240 visitTFunction(n);
241 }
242
243 public void visitTFloatMul(/*@ non_null @*/TFloatMul n) throws IOException {
244 visitTFunction(n);
245 }
246
247 public void visitTLockLE(/*@ non_null @*/TLockLE n) throws IOException {
248 visitTFunction(n);
249 }
250
251 public void visitTLockLT(/*@ non_null @*/TLockLT n) throws IOException {
252 visitTFunction(n);
253 }
254
255 public void visitTRefEQ(/*@ non_null @*/TRefEQ n) throws IOException {
256 visitTFunction(n);
257 }
258
259 public void visitTRefNE(/*@ non_null @*/TRefNE n) throws IOException {
260 visitTFunction(n);
261 }
262
263 public void visitTTypeEQ(/*@ non_null @*/TTypeEQ n) throws IOException {
264 visitTFunction(n);
265 }
266
267 public void visitTTypeNE(/*@ non_null @*/TTypeNE n) throws IOException {
268 visitTFunction(n);
269 }
270
271 public void visitTTypeLE(/*@ non_null @*/TTypeLE n) throws IOException {
272 visitTFunction(n);
273 }
274
275 public void visitTCast(/*@ non_null @*/TCast n) throws IOException {
276 visitTFunction(n);
277 }
278
279 public void visitTIs(/*@ non_null @*/TIs n) throws IOException {
280
281 if (n.parent instanceof TBoolRes) {
282 TBoolRes nTemp = (TBoolRes) n.parent;
283 simplify(nTemp, n);
284 } else
285 TDisplay.err(this, "visitTIs",
286 "TIs node has a parent which type is != from TBoolRes");
287
288 }
289
290 public void visitTSelect(/*@ non_null @*/TSelect n) throws IOException {
291 visitTFunction(n);
292 }
293
294 public void visitTStore(/*@ non_null @*/TStore n) throws IOException {
295 visitTFunction(n);
296 }
297
298 public void visitTTypeOf(/*@ non_null @*/TTypeOf n) throws IOException {
299 visitTFunction(n);
300 }
301
302 public void visitTForAll(/*@ non_null @*/TForAll n) throws IOException {
303
304 if (n.parent instanceof TBoolRes) {
305 TBoolRes nTemp = (TBoolRes) n.parent;
306 simplify(nTemp, n);
307 } else
308 TDisplay.err(this, "visitTForAll",
309 "TIs node has a parent which type is != from TBoolRes");
310
311 }
312
313 public void visitTExist(/*@ non_null @*/TExist n) throws IOException {
314
315 if (n.parent instanceof TBoolRes) {
316 TBoolRes nTemp = (TBoolRes) n.parent;
317 simplify(nTemp, n);
318 } else
319 TDisplay.err(this, "visitTExist",
320 "TIs node has a parent which type is != from TBoolRes");
321
322 }
323
324 public void visitTIsAllocated(/*@ non_null @*/TIsAllocated n) throws IOException {
325 visitTFunction(n);
326 }
327
328 public void visitTEClosedTime(/*@ non_null @*/TEClosedTime n) throws IOException {
329 visitTFunction(n);
330 }
331
332 public void visitTFClosedTime(/*@ non_null @*/TFClosedTime n) throws IOException {
333 visitTFunction(n);
334 }
335
336 public void visitTAsElems(/*@ non_null @*/TAsElems n) throws IOException {
337 visitTFunction(n);
338 }
339
340 public void visitTAsField(/*@ non_null @*/TAsField n) throws IOException {
341 visitTFunction(n);
342 }
343
344 public void visitTAsLockSet(/*@ non_null @*/TAsLockSet n) throws IOException {
345 visitTFunction(n);
346 }
347
348 public void visitTArrayLength(/*@ non_null @*/TArrayLength n) throws IOException {
349 visitTFunction(n);
350 }
351
352 public void visitTArrayFresh(/*@ non_null @*/TArrayFresh n) throws IOException {
353 visitTFunction(n);
354 }
355
356 public void visitTArrayShapeOne(/*@ non_null @*/TArrayShapeOne n) throws IOException {
357 visitTFunction(n);
358 }
359
360 public void visitTArrayShapeMore(/*@ non_null @*/TArrayShapeMore n) throws IOException {
361 visitTFunction(n);
362 }
363
364 public void visitTIsNewArray(/*@ non_null @*/TIsNewArray n) throws IOException {
365 visitTFunction(n);
366 }
367
368 public void visitTString(/*@ non_null @*/TString n) throws IOException {
369 }
370
371 public void visitTBoolean(/*@ non_null @*/TBoolean n) throws IOException {
372
373 if (n.parent instanceof TBoolRes) {
374 TBoolRes nTemp = (TBoolRes) n.parent;
375 simplify(nTemp, n);
376 } else
377 TDisplay.err(this, "visitTBoolean",
378 "TIs node has a parent which type is != from TBoolRes");
379
380 }
381
382 public void visitTChar(/*@ non_null @*/TChar n) throws IOException {
383 }
384
385 public void visitTInt(/*@ non_null @*/TInt n) throws IOException {
386 }
387
388 public void visitTFloat(/*@ non_null @*/TFloat n) throws IOException {
389 }
390
391 public void visitTDouble(/*@ non_null @*/TDouble n) throws IOException {
392 }
393
394 public void visitTNull(/*@ non_null @*/TNull n) throws IOException {
395 }
396
397 public void visitTUnset(/*@ non_null @*/TUnset n) throws IOException {
398 // TODO Auto-generated method stub
399
400 }
401
402 public void visitTMethodCall(/*@ non_null @*/TMethodCall call) throws IOException {
403 // TODO Auto-generated method stub
404
405 }
406
407 public void visitTIntegralSub(/*@ non_null @*/TIntegralSub sub) throws IOException {
408 // TODO Auto-generated method stub
409
410 }
411
412 public void visitTSum(TSum s) {
413 // TODO Auto-generated method stub
414
415 }
416
417 }