Source Code Cross Referenced for SymbolicObjectDiagram.java in  » Testing » KeY » de » uka » ilkd » key » visualdebugger » statevisualisation » Java Source Code / Java DocumentationJava Source Code and Java Documentation

Java Source Code / Java Documentation
1. 6.0 JDK Core
2. 6.0 JDK Modules
3. 6.0 JDK Modules com.sun
4. 6.0 JDK Modules com.sun.java
5. 6.0 JDK Modules sun
6. 6.0 JDK Platform
7. Ajax
8. Apache Harmony Java SE
9. Aspect oriented
10. Authentication Authorization
11. Blogger System
12. Build
13. Byte Code
14. Cache
15. Chart
16. Chat
17. Code Analyzer
18. Collaboration
19. Content Management System
20. Database Client
21. Database DBMS
22. Database JDBC Connection Pool
23. Database ORM
24. Development
25. EJB Server geronimo
26. EJB Server GlassFish
27. EJB Server JBoss 4.2.1
28. EJB Server resin 3.1.5
29. ERP CRM Financial
30. ESB
31. Forum
32. GIS
33. Graphic Library
34. Groupware
35. HTML Parser
36. IDE
37. IDE Eclipse
38. IDE Netbeans
39. Installer
40. Internationalization Localization
41. Inversion of Control
42. Issue Tracking
43. J2EE
44. JBoss
45. JMS
46. JMX
47. Library
48. Mail Clients
49. Net
50. Parser
51. PDF
52. Portal
53. Profiler
54. Project Management
55. Report
56. RSS RDF
57. Rule Engine
58. Science
59. Scripting
60. Search Engine
61. Security
62. Sevlet Container
63. Source Control
64. Swing Library
65. Template Engine
66. Test Coverage
67. Testing
68. UML
69. Web Crawler
70. Web Framework
71. Web Mail
72. Web Server
73. Web Services
74. Web Services apache cxf 2.0.1
75. Web Services AXIS2
76. Wiki Engine
77. Workflow Engines
78. XML
79. XML UI
Java
Java Tutorial
Java Open Source
Jar File Download
Java Articles
Java Products
Java by API
Photoshop Tutorials
Maya Tutorials
Flash Tutorials
3ds-Max Tutorials
Illustrator Tutorials
GIMP Tutorials
C# / C Sharp
C# / CSharp Tutorial
C# / CSharp Open Source
ASP.Net
ASP.NET Tutorial
JavaScript DHTML
JavaScript Tutorial
JavaScript Reference
HTML / CSS
HTML CSS Reference
C / ANSI-C
C Tutorial
C++
C++ Tutorial
Ruby
PHP
Python
Python Tutorial
Python Open Source
SQL Server / T-SQL
SQL Server / T-SQL Tutorial
Oracle PL / SQL
Oracle PL/SQL Tutorial
PostgreSQL
SQL / MySQL
MySQL Tutorial
VB.Net
VB.Net Tutorial
Flash / Flex / ActionScript
VBA / Excel / Access / Word
XML
XML Tutorial
Microsoft Office PowerPoint 2007 Tutorial
Microsoft Office Excel 2007 Tutorial
Microsoft Office Word 2007 Tutorial
Java Source Code / Java Documentation » Testing » KeY » de.uka.ilkd.key.visualdebugger.statevisualisation 
Source Cross Referenced  Class Diagram Java Document (Java Doc) 


0001:        // This file is part of KeY - Integrated Deductive Software Design
0002:        // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
0003:        //                         Universitaet Koblenz-Landau, Germany
0004:        //                         Chalmers University of Technology, Sweden
0005:        //
0006:        // The KeY system is protected by the GNU General Public License. 
0007:        // See LICENSE.TXT for details.
0008:        package de.uka.ilkd.key.visualdebugger.statevisualisation;
0009:
0010:        import java.util.*;
0011:
0012:        import de.uka.ilkd.key.java.JavaInfo;
0013:        import de.uka.ilkd.key.java.Services;
0014:        import de.uka.ilkd.key.java.abstraction.ClassType;
0015:        import de.uka.ilkd.key.java.abstraction.KeYJavaType;
0016:        import de.uka.ilkd.key.java.declaration.ArrayOfParameterDeclaration;
0017:        import de.uka.ilkd.key.java.reference.ReferencePrefix;
0018:        import de.uka.ilkd.key.java.reference.TypeRef;
0019:        import de.uka.ilkd.key.java.statement.MethodBodyStatement;
0020:        import de.uka.ilkd.key.logic.*;
0021:        import de.uka.ilkd.key.logic.ldt.BooleanLDT;
0022:        import de.uka.ilkd.key.logic.ldt.IntegerLDT;
0023:        import de.uka.ilkd.key.logic.op.*;
0024:        import de.uka.ilkd.key.logic.sort.ArraySort;
0025:        import de.uka.ilkd.key.logic.sort.Sort;
0026:        import de.uka.ilkd.key.proof.Node;
0027:        import de.uka.ilkd.key.proof.ProgVarReplacer;
0028:        import de.uka.ilkd.key.unittest.ModelGenerator;
0029:        import de.uka.ilkd.key.visualdebugger.HashMapFromPosInOccurrenceToLabel;
0030:        import de.uka.ilkd.key.visualdebugger.IteratorOfPosInOccurrence;
0031:        import de.uka.ilkd.key.visualdebugger.VisualDebugger;
0032:        import de.uka.ilkd.key.visualdebugger.executiontree.ITNode;
0033:
0034:        public class SymbolicObjectDiagram {
0035:            private static Term nullTerm = TermFactory.DEFAULT
0036:                    .createFunctionTerm(Op.NULL);
0037:
0038:            public static boolean checkIndices(Term t, Services serv) {
0039:                if (t.op() instanceof  AttributeOp) {
0040:                    return checkIndices(t.sub(0), serv);
0041:                }
0042:                if (t.op() instanceof  ArrayOp) {
0043:                    if (serv.getTypeConverter().getIntegerLDT()
0044:                            .getNumberSymbol() == t.sub(1).op()) {
0045:                        if (AbstractMetaOperator.convertToDecimalString(
0046:                                t.sub(1), serv).startsWith("-")) {
0047:                            return false;
0048:                        }
0049:                    }
0050:                    return checkIndices(t.sub(0), serv);
0051:                }
0052:                return true;
0053:            }
0054:
0055:            public static boolean isLocation(Term t, Services serv) {
0056:                OpCollector oc = new OpCollector();
0057:                t.execPostOrder(oc);
0058:                if (oc.contains(Op.NULL)) {
0059:                    return false;
0060:                }
0061:
0062:                final IntegerLDT iLDT = serv.getTypeConverter().getIntegerLDT();
0063:                final BooleanLDT bLDT = serv.getTypeConverter().getBooleanLDT();
0064:
0065:                final Function numberTerminator = iLDT.getNumberTerminator();
0066:                final Function boolTRUE = bLDT.getTrueConst();
0067:                final Function boolFALSE = bLDT.getFalseConst();
0068:
0069:                final Operator op = t.op();
0070:                return op instanceof  AttributeOp
0071:                        && checkIndices(t, serv)
0072:                        && !((ProgramVariable) ((AttributeOp) op).attribute())
0073:                                .isImplicit()
0074:                        || op instanceof  ProgramVariable
0075:                        && !((ProgramVariable) op).isImplicit()
0076:                        || op instanceof  ArrayOp
0077:                        && checkIndices(t, serv)
0078:                        // TODO Why is a RigidFunction a location? 
0079:                        // Was a ProgramConstant intended? if so replace the rest
0080:                        // by instanceof ProgramConstant
0081:                        || op instanceof  RigidFunction && t.arity() == 0
0082:                        && numberTerminator != op && boolTRUE != op
0083:                        && boolFALSE != op
0084:                        // TODO remove string comparison in next line
0085:                        && op.name().toString().indexOf("undef(") == -1;
0086:            }
0087:
0088:            private ListOfTerm ante = SLListOfTerm.EMPTY_LIST,
0089:                    succ = SLListOfTerm.EMPTY_LIST;
0090:
0091:            private SetOfTerm arrayLocations;
0092:
0093:            private SetOfTerm indexTerms;
0094:
0095:            private SetOfTerm instanceConfiguration;
0096:
0097:            private ITNode itNode;
0098:
0099:            private SetOfTerm locations = SetAsListOfTerm.EMPTY_SET;
0100:
0101:            private Term methodReferences[];
0102:
0103:            private Node node;
0104:
0105:            ListOfTerm pc = SLListOfTerm.EMPTY_LIST;
0106:
0107:            private SetOfTerm[] possibleIndexTerms;
0108:
0109:            private ListOfTerm postTerms;
0110:
0111:            private HashMap ref2ser;
0112:
0113:            private SetOfTerm refInPC = SetAsListOfTerm.EMPTY_SET;
0114:
0115:            private Services serv;
0116:
0117:            private LinkedList symbolicObjects;
0118:
0119:            private HashMap term2class;
0120:
0121:            LinkedList terms = new LinkedList();
0122:
0123:            private VisualDebugger vd;
0124:
0125:            public SymbolicObjectDiagram(ITNode itNode, Services serv,
0126:                    ListOfTerm pc, SetOfTerm refInPC, ListOfTerm preTerms,
0127:                    ListOfTerm postTerms, boolean pre,
0128:                    SetOfTerm arrayLocations, SetOfTerm[] possibleIndexTerms,
0129:                    SetOfTerm indexTerms, SetOfTerm instanceConfiguration) {
0130:                this .instanceConfiguration = instanceConfiguration;
0131:                prepare(itNode, serv, pc, refInPC);
0132:                this .postTerms = postTerms;
0133:
0134:                this .arrayLocations = arrayLocations;
0135:
0136:                this .possibleIndexTerms = possibleIndexTerms;
0137:
0138:                this .indexTerms = indexTerms;
0139:
0140:                createSymbolicObjects();
0141:                if (!pre) {
0142:                    createSymbolicObjectsForNewInstances(preTerms);
0143:                    createPostState(preTerms, postTerms);
0144:                    setMethodStack(pre);
0145:                }
0146:
0147:                setInstanceNames(symbolicObjects);
0148:            }
0149:
0150:            private void addArrayEntry(LinkedList objects, Term ref,
0151:                    Term index, Term con) {
0152:                final Iterator it = objects.iterator();
0153:                while (it.hasNext()) {
0154:                    SymbolicObject so = (SymbolicObject) it.next();
0155:                    if (so.getTerms().contains(ref)) {
0156:                        ((SymbolicArrayObject) so).addIndexConstraint(index,
0157:                                con);
0158:                    }
0159:                }
0160:
0161:            }
0162:
0163:            private void addAttribute(LinkedList objects, AttributeOp op,
0164:                    Term sub, Term cTerm) {
0165:                Iterator it = objects.iterator();
0166:                while (it.hasNext()) {
0167:                    SymbolicObject so = (SymbolicObject) it.next();
0168:                    if (so.getTerms().contains(sub)) {
0169:                        if (!((ProgramVariable) op.attribute()).isImplicit()
0170:                                || VisualDebugger.showImpliciteAttr)
0171:                            so.addAttributeConstraint((ProgramVariable) op
0172:                                    .attribute(), cTerm);
0173:                    }
0174:                }
0175:
0176:            }
0177:
0178:            private void addIndexReference(Term sub, Term index,
0179:                    SymbolicObject soReferenced, LinkedList objects) {
0180:                Iterator it = objects.iterator();
0181:                while (it.hasNext()) {
0182:                    SymbolicObject so = (SymbolicObject) it.next();
0183:                    if (so.getTerms().contains(sub)) {
0184:                        ((SymbolicArrayObject) so).addAssociationFromIndex(
0185:                                index, soReferenced);
0186:                    }
0187:                }
0188:            }
0189:
0190:            private void addReference(AttributeOp op, Term sub,
0191:                    SymbolicObject soReferenced, LinkedList objects) {
0192:                Iterator it = objects.iterator();
0193:                while (it.hasNext()) {
0194:                    SymbolicObject so = (SymbolicObject) it.next();
0195:                    if (so.getTerms().contains(sub)) {
0196:                        if (op.attribute() instanceof  ProgramVariable)
0197:                            so.addAssociation(op.attribute(), soReferenced);
0198:                        else
0199:                            System.err
0200:                                    .println("op.attribute not instance of ProgramVariable");
0201:                    }
0202:                }
0203:            }
0204:
0205:            private void addStaticAttribute(LinkedList objects,
0206:                    ProgramVariable pv, ClassType ct, Term cTerm) {
0207:                Iterator it = objects.iterator();
0208:                while (it.hasNext()) {
0209:                    SymbolicObject so = (SymbolicObject) it.next();
0210:                    if (so.isStatic() && so.getType().equals(ct)) {
0211:                        if (!pv.isImplicit()
0212:                                || VisualDebugger.showImpliciteAttr)
0213:                            so.addAttributeConstraint(pv, cTerm);
0214:                    }
0215:                }
0216:
0217:            }
0218:
0219:            private void addStaticReference(ProgramVariable op,
0220:                    SymbolicObject soReferenced, LinkedList objects) {
0221:                Iterator it = objects.iterator();
0222:                while (it.hasNext()) {
0223:                    SymbolicObject so = (SymbolicObject) it.next();
0224:                    if (so.isStatic()
0225:                            && so.getType().equals(
0226:                                    op.getContainerType().getJavaType()))
0227:                        so.addAssociation(op, soReferenced);
0228:
0229:                }
0230:
0231:            }
0232:
0233:            private void collectLocations(Term t) {
0234:                if (isLocation(t, serv)) {
0235:                    getEqvClass(t);
0236:                    locations = locations.add(t);
0237:                }
0238:                if (!(t.op() instanceof  Modality
0239:                        || t.op() instanceof  IUpdateOperator || t.op() instanceof  Quantifier)) {
0240:                    for (int i = 0; i < t.arity(); i++) {
0241:                        collectLocations(t.sub(i));
0242:                    }
0243:                }
0244:            }
0245:
0246:            private SetOfTerm collectLocations2(Term t) {
0247:                SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
0248:                if (isLocation(t, serv)) {
0249:                    result = result.add(t);
0250:
0251:                }
0252:                if (!(t.op() instanceof  Modality
0253:                        || t.op() instanceof  IUpdateOperator || t.op() instanceof  Quantifier)) {
0254:                    for (int i = 0; i < t.arity(); i++) {
0255:                        result = result.union(collectLocations2(t.sub(i)));
0256:                    }
0257:                }
0258:                return result;
0259:            }
0260:
0261:            private boolean containsJavaBlock(Term t) {
0262:                if (t.op() == vd.getPostPredicate()) {
0263:                    return true; // TODO
0264:                }
0265:                if (t.javaBlock() != JavaBlock.EMPTY_JAVABLOCK) {
0266:                    return true;
0267:                }
0268:                for (int i = 0; i < t.arity(); i++) {
0269:                    if (containsJavaBlock(t.sub(i))) {
0270:                        return true;
0271:                    }
0272:                }
0273:                return false;
0274:            }
0275:
0276:            private void createEquivalenceClassesAndConstraints() {
0277:                term2class = new HashMap();
0278:                IteratorOfTerm it = ante.iterator();
0279:                while (it.hasNext()) {
0280:                    EquClass ec = null;
0281:                    Term t = it.next();
0282:                    collectLocations(t);
0283:                    if (t.op() instanceof  Equality /* && !containsImplicitAttr(t) */) {
0284:                        if (term2class.containsKey(t.sub(0))) {
0285:                            ec = (EquClass) term2class.get(t.sub(0));
0286:                            if (term2class.containsKey(t.sub(1))) {
0287:                                ec.add((EquClass) term2class.get(t.sub(1)));
0288:                            } else {
0289:                                ec.add(t.sub(1));
0290:                            }
0291:                        } else if (term2class.containsKey(t.sub(1))) {
0292:                            ec = (EquClass) term2class.get(t.sub(1));
0293:                            ec.add(t.sub(0));
0294:                        } else {
0295:                            ec = new EquClass(t.sub(0), t.sub(1));
0296:                        }
0297:                        IteratorOfTerm ecIt = ec.getMembers().iterator();
0298:                        while (ecIt.hasNext()) {
0299:                            term2class.put(ecIt.next(), ec);
0300:                        }
0301:                    }
0302:
0303:                }
0304:                it = succ.iterator();
0305:                while (it.hasNext()) {
0306:                    Term t = it.next();
0307:                    collectLocations(t);
0308:                }
0309:            }
0310:
0311:            private void createPostState(ListOfTerm pre, ListOfTerm post) {
0312:                VisualDebugger.print("createPostState -----");
0313:                IteratorOfTerm pIt = post.iterator();
0314:                for (IteratorOfTerm it = pre.iterator(); it.hasNext();) {
0315:                    Term preTerm = it.next();
0316:                    Term postTerm = pIt.next();
0317:                    // System.out.println(preTerm+":="+postTerm);
0318:                    if (preTerm.op() instanceof  AttributeOp) {
0319:                        final Term sub = preTerm.sub(0);
0320:                        final SymbolicObject so = getObject(sub,
0321:                                symbolicObjects);
0322:                        if (referenceSort(preTerm.sort()))
0323:                            so.addAssociation(((AttributeOp) preTerm.op())
0324:                                    .attribute(), getObject(postTerm,
0325:                                    symbolicObjects));
0326:                        else if (!((ProgramVariable) ((AttributeOp) preTerm
0327:                                .op()).attribute()).isImplicit()
0328:                                || VisualDebugger.showImpliciteAttr)
0329:                            so.addValueTerm(
0330:                                    (ProgramVariable) ((AttributeOp) preTerm
0331:                                            .op()).attribute(), postTerm);
0332:                    } else if (preTerm.op() instanceof  ArrayOp) {
0333:                        final Term sub = preTerm.sub(0);
0334:                        final SymbolicArrayObject sao = (SymbolicArrayObject) getObject(
0335:                                sub, symbolicObjects);
0336:                        if (referenceSort(preTerm.sort()))
0337:                            sao.addAssociationFromIndex(preTerm.sub(1),
0338:                                    getObject(postTerm, symbolicObjects));
0339:                        else
0340:                            sao.setValueTermForIndex(preTerm.sub(1), postTerm);
0341:                    } else if (preTerm.op() instanceof  ProgramVariable) {
0342:                        final ProgramVariable pv = (ProgramVariable) preTerm
0343:                                .op();
0344:                        SymbolicObject staticO = getStaticObject((ClassType) pv
0345:                                .getContainerType().getJavaType(),
0346:                                symbolicObjects);
0347:                        if (staticO == null) {
0348:                            if (!pv.isImplicit()
0349:                                    || VisualDebugger.showImpliciteAttr) {
0350:                                staticO = new SymbolicObject((ClassType) pv
0351:                                        .getContainerType().getJavaType(), serv);
0352:                                symbolicObjects.add(staticO);
0353:                            }
0354:                        }
0355:
0356:                        if (referenceSort(preTerm.sort()))
0357:                            staticO.addAssociation(pv, getObject(postTerm,
0358:                                    symbolicObjects));
0359:                        else if (!pv.isImplicit()
0360:                                || VisualDebugger.showImpliciteAttr)
0361:                            staticO.addValueTerm(pv, postTerm);
0362:                    }
0363:
0364:                }
0365:
0366:            }
0367:
0368:            private void createSymbolicObjects() {
0369:                LinkedList result = new LinkedList();
0370:                EquClass[] npClasses = getNonPrimitiveLocationEqvClasses();
0371:                for (int i = 0; i < npClasses.length; i++) {
0372:                    KeYJavaType t = npClasses[i].getKeYJavaType();
0373:                    if (!disjunct(npClasses[i].getMembers(), refInPC)) {
0374:                        if (npClasses[i].isArray()) {
0375:                            SymbolicArrayObject sao = new SymbolicArrayObject(
0376:                                    npClasses[i].getMembers(), (ClassType) t
0377:                                            .getJavaType(), serv);
0378:                            sao
0379:                                    .setPossibleIndexTermConfigurations(getPossibleIndexTerms(npClasses[i]
0380:                                            .getMembers()));
0381:                            sao
0382:                                    .setIndexConfiguration(getPossibleIndexTermsForArray(
0383:                                            sao.getTerms(), indexTerms));
0384:                            result.add(sao);
0385:                        } else
0386:                            result.add(new SymbolicObject(npClasses[i]
0387:                                    .getMembers(), (ClassType) t.getJavaType(),
0388:                                    serv));
0389:
0390:                    }
0391:                }
0392:
0393:                // create static objects
0394:                // System.out.println("Static Type "+);
0395:                for (Iterator it = this .getStaticClasses().iterator(); it
0396:                        .hasNext();) {
0397:                    result
0398:                            .add(new SymbolicObject((ClassType) (it.next()),
0399:                                    serv));
0400:                }
0401:
0402:                // create self object/ self static class, if not happened
0403:                if (vd.isStaticMethod()) {
0404:                    final ClassType ct = vd.getType();
0405:                    if (this .getStaticObject(ct, result) == null)
0406:                        result.add(new SymbolicObject(ct, serv));
0407:                } else {
0408:                    final Term self = (Term) vd.getInputPV2term().get(
0409:                            (vd.getSelfTerm()));
0410:                    if (this .getObject(self, result) == null)
0411:                        result.add(new SymbolicObject(self, (ClassType) serv
0412:                                .getJavaInfo().getKeYJavaType(self.sort())
0413:                                .getJavaType(), serv));
0414:                }
0415:
0416:                // create unknown objects
0417:                for (IteratorOfTerm it = postTerms.iterator(); it.hasNext();) {
0418:                    Term next = it.next();
0419:                    if (this .referenceSort(next.sort())
0420:                            && !VisualDebugger.containsImplicitAttr(next)) {
0421:                        if (getObject(next, result) == null) {
0422:                            result.add(new SymbolicObject(next,
0423:                                    (ClassType) serv.getJavaInfo()
0424:                                            .getKeYJavaType(next.sort())
0425:                                            .getJavaType(), serv, true));
0426:                        }
0427:
0428:                    }
0429:
0430:                }
0431:
0432:                // Compute Associations...
0433:                Iterator it = result.iterator();
0434:                while (it.hasNext()) {
0435:                    SymbolicObject so = (SymbolicObject) it.next();
0436:                    IteratorOfTerm it2 = so.getTerms().iterator();
0437:                    // SetOfTerm result;
0438:                    // System.out.println("adding assos");
0439:                    while (it2.hasNext()) {
0440:
0441:                        Term t = it2.next();
0442:                        // System.out.println("ref" +t);
0443:
0444:                        if (t.op() instanceof  AttributeOp) {
0445:                            Term sub = t.sub(0);
0446:                            AttributeOp op = (AttributeOp) t.op();
0447:                            if (refInPC.contains(t) || postTerms.contains(t)) // TODO
0448:                                // ???//only
0449:                                // assoc
0450:                                // that
0451:                                // are
0452:                                // in
0453:                                // the
0454:                                // pc
0455:                                addReference(op, sub, so, result);
0456:                        } else if (t.op() instanceof  ArrayOp) {
0457:                            if (refInPC.contains(t) || postTerms.contains(t)) // TODO??
0458:                                addIndexReference(t.sub(0), t.sub(1), so,
0459:                                        result);
0460:
0461:                        } else if (t.op() instanceof  ProgramVariable) {
0462:                            if (refInPC.contains(t) || postTerms.contains(t)) // TODO
0463:                                // ???//only
0464:                                // assoc
0465:                                // that
0466:                                // are
0467:                                // in
0468:                                // the
0469:                                // pc
0470:                                addStaticReference((ProgramVariable) t.op(),
0471:                                        so, result);
0472:
0473:                        }
0474:
0475:                    }
0476:                }
0477:
0478:                for (IteratorOfTerm it2 = pc.iterator(); it2.hasNext();) {
0479:                    Term currentTerm = it2.next();
0480:                    SetOfTerm locs = collectLocations2(currentTerm);
0481:
0482:                    for (IteratorOfTerm it3 = locs.iterator(); it3.hasNext();) {
0483:
0484:                        Term t2 = it3.next();
0485:                        if (!referenceSort(t2.sort())) {
0486:                            if (t2.op() instanceof  AttributeOp) {
0487:                                addAttribute(result, (AttributeOp) t2.op(), t2
0488:                                        .sub(0), currentTerm);
0489:                            } else if (t2.op() instanceof  ArrayOp) {
0490:                                this .addArrayEntry(result, t2.sub(0),
0491:                                        t2.sub(1), currentTerm);
0492:                            } else if (t2.op() instanceof  ProgramVariable) {
0493:                                ProgramVariable pv = (ProgramVariable) t2.op();
0494:                                KeYJavaType kjt = pv.getContainerType();
0495:                                if (kjt != null) {
0496:                                    ClassType ct = (ClassType) kjt
0497:                                            .getJavaType();
0498:                                    this .addStaticAttribute(result, pv, ct,
0499:                                            currentTerm);
0500:
0501:                                }
0502:
0503:                            }
0504:
0505:                        }
0506:
0507:                    }
0508:                }
0509:                setInstanceNames(result);
0510:                symbolicObjects = result;
0511:            }
0512:
0513:            private void createSymbolicObjectsForNewInstances(ListOfTerm pre) {
0514:                for (IteratorOfTerm it = pre.iterator(); it.hasNext();) {
0515:                    Term next = it.next();
0516:
0517:                    if (next.op() instanceof  AttributeOp) {
0518:                        Term sub = next.sub(0);
0519:
0520:                        if (getObject(sub, this .symbolicObjects) == null) {
0521:                            symbolicObjects.add(new SymbolicObject(sub,
0522:                                    (ClassType) serv.getJavaInfo()
0523:                                            .getKeYJavaType(sub.sort())
0524:                                            .getJavaType(), this .serv));
0525:                        }
0526:
0527:                    }
0528:                }
0529:
0530:            }
0531:
0532:            private boolean disjunct(SetOfTerm s1, SetOfTerm s2) {
0533:                for (IteratorOfTerm it = s1.iterator(); it.hasNext();) {
0534:                    if (s2.contains(it.next()))
0535:                        return false;
0536:                }
0537:                return true;
0538:            }
0539:
0540:            private LinkedList filterStaticObjects(LinkedList objects) {
0541:                LinkedList result = new LinkedList();
0542:                Iterator it = objects.iterator();
0543:                while (it.hasNext()) {
0544:                    final SymbolicObject so = (SymbolicObject) it.next();
0545:                    if (!so.isStatic())
0546:                        result.add(so);
0547:                }
0548:                return result;
0549:            }
0550:
0551:            private void findDisjointClasses() {
0552:                IteratorOfTerm it = succ.iterator();
0553:                while (it.hasNext()) {
0554:                    Term t = it.next();
0555:                    EquClass e0, e1;
0556:                    if (t.op() instanceof  Equality /* &&!containsImplicitAttr(t) */) {
0557:                        e0 = getEqvClass(t.sub(0));
0558:                        e1 = getEqvClass(t.sub(1));
0559:                        e0.addDisjoint(t.sub(1));
0560:                        e1.addDisjoint(t.sub(0));
0561:                    }
0562:                }
0563:            }
0564:
0565:            public ListOfTerm getConstraints(Term toFind) {
0566:                // Term pvTerm = TermFactory.DEFAULT.createVariableTerm(pv);
0567:                ListOfTerm result = SLListOfTerm.EMPTY_LIST;
0568:                for (IteratorOfTerm it = pc.iterator(); it.hasNext();) {
0569:                    final Term t = it.next();
0570:                    OpCollector vis = new OpCollector();
0571:                    t.execPostOrder(vis);
0572:
0573:                    if (vis.contains(toFind.op()))
0574:                        result = result.append(t);
0575:
0576:                    // System.out.println(vis.);
0577:
0578:                }
0579:
0580:                return result;
0581:
0582:            }
0583:
0584:            private EquClass getEqvClass(Term t) {
0585:                if (!term2class.containsKey(t)) {
0586:                    term2class.put(t, new EquClass(t));
0587:                }
0588:                return (EquClass) term2class.get(t);
0589:            }
0590:
0591:            public SetOfTerm getIndexTerms() {
0592:                return indexTerms;
0593:            }
0594:
0595:            public EquClass[] getNonPrimitiveLocationEqvClasses() {
0596:                Object[] oa = (new HashSet(term2class.values())).toArray();
0597:                EquClass[] temp = new EquClass[oa.length];
0598:                int l = 0;
0599:                for (int i = 0; i < oa.length; i++) {
0600:                    if (((EquClass) oa[i]).getLocations().size() > 0
0601:                            && (!((EquClass) oa[i]).isInt() && !((EquClass) oa[i])
0602:                                    .isBoolean())) {
0603:                        temp[l++] = (EquClass) oa[i];
0604:                    }
0605:                }
0606:                EquClass[] result = new EquClass[l];
0607:                for (int i = 0; i < l; i++) {
0608:                    result[i] = temp[i];
0609:                }
0610:                return result;
0611:            }
0612:
0613:            private SymbolicObject getObject(Term sub, LinkedList objects) {
0614:                Iterator it = objects.iterator();
0615:                while (it.hasNext()) {
0616:                    final SymbolicObject so = (SymbolicObject) it.next();
0617:                    if (so.getTerms().contains(sub)) {
0618:                        return so;
0619:                    }
0620:                }
0621:                return null;
0622:            }
0623:
0624:            private ListOfTerm getPc(HashMapFromPosInOccurrenceToLabel labels) {
0625:                IteratorOfPosInOccurrence pioIt = labels.keyIterator();
0626:                ListOfTerm pc2 = SLListOfTerm.EMPTY_LIST;
0627:
0628:                while (pioIt.hasNext()) {
0629:                    PosInOccurrence pio = pioIt.next();
0630:                    // PCLabel pcLabel = ((PCLabel)labels.get(pio));
0631:                    if (!containsJavaBlock(pio.constrainedFormula().formula())) {
0632:                        Term t = pio.constrainedFormula().formula();
0633:                        if (pio.isInAntec())
0634:                            pc2 = pc2.append(t);
0635:                        else {
0636:                            if (t.op() == Op.NOT) {
0637:                                pc2 = pc2.append(t.sub(0));
0638:                            } else
0639:                                pc2 = pc2
0640:                                        .append(TermFactory.DEFAULT
0641:                                                .createJunctorTermAndSimplify(
0642:                                                        Op.NOT, t));
0643:                        }
0644:
0645:                        // pc = pc.append(pio.constrainedFormula().formula());
0646:                    }
0647:
0648:                }
0649:                return pc2;
0650:            }
0651:
0652:            private LinkedList getPossibleIndexTerms(SetOfTerm members) {
0653:                LinkedList result = new LinkedList();
0654:                if (possibleIndexTerms != null)
0655:                    for (int i = 0; i < possibleIndexTerms.length; i++) {
0656:                        SetOfTerm currentIndexTerms = possibleIndexTerms[i];
0657:                        SetOfTerm locInd = SetAsListOfTerm.EMPTY_SET;
0658:                        SetOfTerm res = SetAsListOfTerm.EMPTY_SET;
0659:
0660:                        for (IteratorOfTerm locIt = this .arrayLocations
0661:                                .iterator(); locIt.hasNext();) {
0662:                            Term t = locIt.next();
0663:                            if (members.contains(t.sub(0))) {
0664:                                locInd = locInd.add(t.sub(1));
0665:                            }
0666:                        }
0667:
0668:                        for (IteratorOfTerm posIndexTermsIt = currentIndexTerms
0669:                                .iterator(); posIndexTermsIt.hasNext();) {
0670:                            final Term t = posIndexTermsIt.next();
0671:                            final Term t2;
0672:                            if (t.op() == Op.NOT)
0673:                                t2 = t.sub(0);
0674:                            else
0675:                                t2 = t;
0676:                            if (locInd.contains(t2.sub(0))
0677:                                    && locInd.contains(t2.sub(1)))
0678:                                res = res.add(t);
0679:                        }
0680:                        result.add(res);
0681:                    }
0682:                // VisualDebugger.print("POS INDEX TERMS "+result);
0683:                return result;
0684:
0685:            }
0686:
0687:            private SetOfTerm getPossibleIndexTermsForArray(SetOfTerm members,
0688:                    SetOfTerm ic) {
0689:                SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
0690:
0691:                SetOfTerm currentIndexTerms = ic;
0692:                SetOfTerm locInd = SetAsListOfTerm.EMPTY_SET;
0693:                for (IteratorOfTerm locIt = this .arrayLocations.iterator(); locIt
0694:                        .hasNext();) {
0695:                    Term t = locIt.next();
0696:                    if (members.contains(t.sub(0))) {
0697:                        locInd = locInd.add(t.sub(1));
0698:                    }
0699:                }
0700:
0701:                for (IteratorOfTerm posIndexTermsIt = currentIndexTerms
0702:                        .iterator(); posIndexTermsIt.hasNext();) {
0703:                    final Term t = posIndexTermsIt.next();
0704:                    final Term t2;
0705:                    if (t.op() == Op.NOT)
0706:                        t2 = t.sub(0);
0707:                    else
0708:                        t2 = t;
0709:                    if (locInd.contains(t2.sub(0))
0710:                            && locInd.contains(t2.sub(1)))
0711:                        result = result.add(t);
0712:                }
0713:                // result=(res);
0714:
0715:                // VisualDebugger.print("Index terms for member"+ members+" :"+result);
0716:                return result;
0717:
0718:            }
0719:
0720:            // TODO duplicate in statevisualization
0721:            private SetOfTerm getReferences(ListOfTerm terms) {
0722:                // ListOfTerm pc = itNode.getPc();
0723:                SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
0724:                for (IteratorOfTerm it = terms.iterator(); it.hasNext();) {
0725:                    result = result.union(getReferences2(it.next()));
0726:                }
0727:                return result;
0728:            }
0729:
0730:            private SetOfTerm getReferences2(Term t) {
0731:                // System.out.println(t);
0732:                // if (t.sort()!= Sort.FORMULA && !this.isBool(t)&&!this.isInt(t))
0733:
0734:                SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
0735:                if (referenceSort(t.sort()))
0736:                    result = result.add(t);
0737:                for (int i = 0; i < t.arity(); i++) {
0738:                    result = result.union(getReferences2(t.sub(i)));
0739:                }
0740:                return result;
0741:            }
0742:
0743:            private int getSerialNumber(SetOfTerm refs) {
0744:                int current = -1;
0745:
0746:                for (IteratorOfTerm it = refs.iterator(); it.hasNext();) {
0747:                    final Term t = it.next();
0748:                    if (ref2ser.containsKey(t)
0749:                            && ((current == -1) || ((Integer) ref2ser.get(t))
0750:                                    .intValue() < current)) {
0751:                        current = ((Integer) ref2ser.get(t)).intValue();
0752:                    }
0753:                }
0754:
0755:                return current;
0756:            }
0757:
0758:            private Set getStaticClasses() {
0759:                HashSet res = new HashSet();
0760:                for (IteratorOfTerm it = this .pc.iterator(); it.hasNext();) {
0761:                    Term t = it.next();
0762:                    res.addAll(this .getStaticClasses(t));
0763:
0764:                }
0765:
0766:                return res;
0767:            }
0768:
0769:            private Set getStaticClasses(Term t) {
0770:                Set result = new HashSet();
0771:                if (t.op() instanceof  ProgramVariable) {
0772:                    if (((ProgramVariable) t.op()).getContainerType() != null)
0773:                        if (!((ProgramVariable) t.op()).isImplicit()
0774:                                || VisualDebugger.showImpliciteAttr)
0775:                            result.add(((ProgramVariable) t.op())
0776:                                    .getContainerType().getJavaType());
0777:
0778:                }
0779:
0780:                for (int i = 0; i < t.arity(); i++) {
0781:                    result.addAll(getStaticClasses(t.sub(i)));
0782:                }
0783:                return result;
0784:
0785:            }
0786:
0787:            private SymbolicObject getStaticObject(ClassType ct,
0788:                    LinkedList objects) {
0789:                final Iterator it = objects.iterator();
0790:                while (it.hasNext()) {
0791:                    final SymbolicObject so = (SymbolicObject) it.next();
0792:                    if (so.isStatic() && so.getType().equals(ct))
0793:                        return so;
0794:                }
0795:                return null;
0796:            }
0797:
0798:            public LinkedList getSymbolicObjects() {
0799:                return symbolicObjects;
0800:            }
0801:
0802:            // TODO duplicate in prooflistener
0803:
0804:            private void prepare(ITNode itNode, Services serv, ListOfTerm pc,
0805:                    SetOfTerm refInPc) {
0806:
0807:                this .vd = VisualDebugger.getVisualDebugger();
0808:                this .pc = pc;
0809:                // this.node = n;
0810:                this .node = itNode.getNode();
0811:                this .itNode = itNode;
0812:                // this.mediator=mediator;
0813:                // mediator = Main.getInstance().mediator();
0814:                this .serv = serv;
0815:                // goals = mediator.getProof().getSubtreeGoals(node);
0816:
0817:                VisualDebugger.print("--------------------------");
0818:                VisualDebugger.print("Calculating Equ classes for "
0819:                        + node.serialNr());
0820:
0821:                IteratorOfConstrainedFormula itc = node.sequent().antecedent()
0822:                        .iterator();
0823:                while (itc.hasNext()) {
0824:                    ante = ante.append(itc.next().formula());
0825:                }
0826:                itc = node.sequent().succedent().iterator();
0827:                succ = SLListOfTerm.EMPTY_LIST;
0828:                while (itc.hasNext()) {
0829:                    succ = succ.append(itc.next().formula());
0830:                }
0831:
0832:                for (IteratorOfTerm it = this .instanceConfiguration.iterator(); it
0833:                        .hasNext();) {
0834:                    final Term t = it.next();
0835:                    if (t.op() == Op.NOT)
0836:                        succ = succ.append(t.sub(0));
0837:                    else
0838:                        ante = ante.append(t);
0839:                }
0840:
0841:                this .refInPC = refInPc;
0842:
0843:                createEquivalenceClassesAndConstraints();
0844:                getEqvClass(nullTerm);
0845:                findDisjointClasses();
0846:
0847:                Collection cl = term2class.values();
0848:                HashSet s = new HashSet(cl);
0849:                Iterator it5 = s.iterator();
0850:                VisualDebugger.print("All Equi Classses: ");
0851:                while (it5.hasNext())
0852:                    VisualDebugger.print(it5.next());
0853:            }
0854:
0855:            private boolean referenceSort(Sort s) {
0856:                JavaInfo info = serv.getJavaInfo();
0857:                KeYJavaType kjt = info.getKeYJavaType(s);
0858:                // System.out.println("KJT "+kjt);
0859:                if (kjt == null)
0860:                    return false;
0861:                if (kjt.getJavaType() instanceof  ClassType)
0862:                    return true;
0863:
0864:                return false;
0865:            }
0866:
0867:            private void setInstanceNames(LinkedList objects) {
0868:                objects = filterStaticObjects(objects);
0869:                ref2ser = new HashMap();
0870:                ITNode n = this .itNode;
0871:                while (n.getParent() != null) {
0872:                    HashMapFromPosInOccurrenceToLabel labels = n.getNode()
0873:                            .getNodeInfo().getVisualDebuggerState().getLabels();
0874:                    ListOfTerm pc2 = getPc(labels);
0875:                    SetOfTerm refs = getReferences(pc2);
0876:                    for (IteratorOfTerm it = refs.iterator(); it.hasNext();) {
0877:                        Term t = it.next();
0878:                        ref2ser.put(t, new Integer(n.getId()));
0879:
0880:                    }
0881:                    n = n.getParent();
0882:                }
0883:
0884:                // references in post term
0885:                int j = 0;
0886:                if (postTerms != null)
0887:                    for (IteratorOfTerm it = postTerms.iterator(); it.hasNext();) {
0888:
0889:                        Term t = it.next();
0890:                        // System.out.println("pt "+t);
0891:                        if (referenceSort(t.sort())) {
0892:                            if (!ref2ser.containsKey(t)) {
0893:                                j++;
0894:                                ref2ser.put(t, new Integer(itNode.getId() + j));
0895:
0896:                            }
0897:                        }
0898:
0899:                    }
0900:
0901:                VisualDebugger.print("HashMap for Instance Names");
0902:
0903:                if (!vd.isStaticMethod())
0904:                    ref2ser.put(vd.getInputPV2term().get(
0905:                            TermFactory.DEFAULT.createVariableTerm(vd
0906:                                    .getSelfPV())), new Integer(1));
0907:
0908:                VisualDebugger.print(ref2ser);
0909:
0910:                // System.out.println("INPUT VALUES"+inputVal);
0911:
0912:                Iterator it2 = objects.iterator();
0913:                while (it2.hasNext()) {
0914:                    SymbolicObject so = (SymbolicObject) it2.next();
0915:                    so.setId(getSerialNumber(so.getTerms()));
0916:                }
0917:
0918:                SymbolicObject[] sos = (SymbolicObject[]) objects
0919:                        .toArray(new SymbolicObject[objects.size()]);
0920:
0921:                // sort symbolic objects according to their ids
0922:                sort(sos);
0923:
0924:                HashMap counters = new HashMap();
0925:
0926:                for (int i = 0; i < sos.length; i++) {
0927:                    SymbolicObject so = sos[i];
0928:
0929:                    if (so.getId() == -1)
0930:                        continue;
0931:
0932:                    Integer newValue;
0933:                    if (counters.containsKey(so.getType())) {
0934:                        Integer value = (Integer) counters.get(so.getType());
0935:                        newValue = new Integer(value.intValue() + 1);
0936:                        counters.remove(so.getType());
0937:                        counters.put(so.getType(), newValue);
0938:                    } else {
0939:                        newValue = new Integer(0);
0940:                        counters.put(so.getType(), newValue);
0941:
0942:                    }
0943:
0944:                    // instanceName+=newValue.intValue();
0945:
0946:                    // so.setName(instanceName);
0947:
0948:                    so.setId(newValue.intValue());
0949:
0950:                }
0951:
0952:            }
0953:
0954:            private void setMethodStack(boolean pre) {
0955:                try {
0956:                    ITNode it = itNode.getMethodNode();
0957:                    if (it == null) {
0958:                        return;
0959:                    }
0960:
0961:                    MethodBodyStatement mbs = // vd.getLastMethodBodyStatement(itNode.getNode());
0962:                    (MethodBodyStatement) it.getActStatement();
0963:                    // MethodBodyStatement mbs =
0964:                    // vd.getLastMethodBodyStatement(itNode.getNode());
0965:                    if (mbs == null)
0966:                        return;
0967:                    ReferencePrefix refPre = mbs.getMethodReference()
0968:                            .getReferencePrefix();
0969:                    SymbolicObject so;
0970:
0971:                    if (refPre instanceof  TypeRef) {
0972:                        final KeYJavaType kjt = ((TypeRef) refPre)
0973:                                .getKeYJavaType();
0974:                        final ClassType type = (ClassType) kjt.getJavaType();
0975:                        so = getStaticObject(type, symbolicObjects);
0976:                        if (so == null) {
0977:                            so = new SymbolicObject(type, serv);
0978:                            symbolicObjects.add(so);
0979:                        }
0980:
0981:                        so.setMethod(mbs.getProgramMethod(serv));
0982:
0983:                    } else {
0984:
0985:                        final Term t = serv.getTypeConverter()
0986:                                .convertToLogicElement(refPre);
0987:                        methodReferences = new Term[1];
0988:                        methodReferences[0] = t;
0989:                        // System.out.println("AAAAAAAAAAAAAAAAAAAAAA "+t);
0990:                        HashMap map = new HashMap();
0991:                        Term self = vd.getSelfTerm();
0992:                        // vd.getSelfTerm() //TODO
0993:                        // ProgramVariable val =
0994:                        // (ProgramVariable)((Term)vd.getInputPV2term().get(self)).op();
0995:                        Term val = ((Term) vd.getInputPV2term().get(self));
0996:                        map.put(self.op(), val);
0997:                        ProgVarReplacer pvr = new ProgVarReplacer(map);
0998:                        Term res = pvr.replace(t);
0999:
1000:                        so = getObject(res, symbolicObjects);
1001:                        so.setMethod(mbs.getProgramMethod(serv));
1002:
1003:                    }
1004:
1005:                    // ArrayOfExpression aof = mbs.getArguments();;
1006:                    HashSet set = vd.getParam(mbs);
1007:                    ListOfProgramVariable inputPara = vd
1008:                            .arrayOfExpression2ListOfProgVar(
1009:                                    mbs.getArguments(), 0);
1010:                    ProgramVariable[] inputParaArray = inputPara.toArray();
1011:
1012:                    ArrayOfParameterDeclaration paraDecl = mbs
1013:                            .getProgramMethod(serv).getParameters();
1014:
1015:                    final HashMap values = vd.getValuesForLocation(set, vd
1016:                            .getProgramPIO(itNode.getNode().sequent()));
1017:
1018:                    ListOfProgramVariable paramDeclAsPVList = SLListOfProgramVariable.EMPTY_LIST;
1019:
1020:                    for (int i = 0; i < paraDecl.size(); i++) {
1021:                        ProgramVariable next = (ProgramVariable) paraDecl
1022:                                .getParameterDeclaration(i)
1023:                                .getVariableSpecification()
1024:                                .getProgramVariable();
1025:                        Term val = (Term) values.get(TermFactory.DEFAULT
1026:                                .createVariableTerm(inputParaArray[i]));// TODO
1027:                        so.addPara2Value(next, val);
1028:                        paramDeclAsPVList = paramDeclAsPVList.append(next);
1029:                    }
1030:                    so.setParameter(paramDeclAsPVList);
1031:
1032:                } catch (Exception e) {
1033:                    return;
1034:
1035:                }
1036:
1037:            }
1038:
1039:            private void sort(SymbolicObject a[]) {
1040:
1041:                int n = a.length;
1042:                SymbolicObject temp;
1043:
1044:                for (int i = 0; i < n - 1; i = i + 1)
1045:                    for (int j = n - 1; j > i; j = j - 1)
1046:                        if (a[j - 1].getId() > a[j].getId()) {
1047:                            temp = a[j - 1];
1048:                            a[j - 1] = a[j];
1049:                            a[j] = temp;
1050:                        }
1051:            }
1052:
1053:            private class EquClass {
1054:                private SetOfTerm disjointRep = SetAsListOfTerm.EMPTY_SET;
1055:
1056:                private SetOfTerm members;
1057:
1058:                public EquClass(SetOfTerm members) {
1059:                    this .members = members;
1060:                }
1061:
1062:                public EquClass(Term t) {
1063:                    this (SetAsListOfTerm.EMPTY_SET.add(t));
1064:                }
1065:
1066:                public EquClass(Term t1, Term t2) {
1067:                    this (SetAsListOfTerm.EMPTY_SET.add(t1).add(t2));
1068:                }
1069:
1070:                public void add(EquClass ec) {
1071:                    members = members.union(ec.getMembers());
1072:                }
1073:
1074:                public void add(Term t) {
1075:                    members = members.add(t);
1076:                }
1077:
1078:                public void addDisjoint(Term t) {
1079:                    disjointRep = disjointRep.add(t);
1080:                }
1081:
1082:                public boolean equals(Object o) {
1083:                    if (!(o instanceof  EquClass)) {
1084:                        return false;
1085:                    }
1086:                    EquClass eqc = (EquClass) o;
1087:                    if (eqc.members.size() != members.size()) {
1088:                        return false;
1089:                    }
1090:                    IteratorOfTerm it = members.iterator();
1091:                    l: while (it.hasNext()) {
1092:                        IteratorOfTerm it2 = eqc.members.iterator();
1093:                        Term t = it.next();
1094:                        while (it2.hasNext()) {
1095:                            if (t.toString().equals(it2.next().toString())) {
1096:                                continue l;
1097:                            }
1098:                        }
1099:                        return false;
1100:                    }
1101:                    return true;
1102:                }
1103:
1104:                public SetOfTerm getDisjoints() {
1105:                    return disjointRep;
1106:                }
1107:
1108:                public KeYJavaType getKeYJavaType() {
1109:                    IteratorOfTerm it = members.iterator();
1110:                    Sort s = it.next().sort();
1111:                    while (it.hasNext()) {
1112:                        Sort s1 = it.next().sort();
1113:                        if (s1.extendsTrans(s)) {
1114:                            s = s1;
1115:                        }
1116:                    }
1117:                    KeYJavaType result = serv.getJavaInfo().getKeYJavaType(s);
1118:                    if (result == null && isInt(s)) {
1119:                        result = serv.getJavaInfo().getKeYJavaType(
1120:                                serv.getTypeConverter().getIntLDT()
1121:                                        .targetSort());
1122:                    }
1123:                    return result;
1124:                }
1125:
1126:                /**
1127:                 * Returns the locations that are members of this equivalence class.
1128:                 */
1129:                public SetOfTerm getLocations() {
1130:                    SetOfTerm locations = SetAsListOfTerm.EMPTY_SET;
1131:                    IteratorOfTerm it = members.iterator();
1132:                    while (it.hasNext()) {
1133:                        Term t = it.next();
1134:                        if (ModelGenerator.isLocation(t, serv)) {
1135:                            locations = locations.add(t);
1136:                        }
1137:                    }
1138:                    return locations;
1139:                }
1140:
1141:                public SetOfTerm getMembers() {
1142:                    return members;
1143:                }
1144:
1145:                public boolean isArray() {
1146:                    for (IteratorOfTerm it = members.iterator(); it.hasNext();) {
1147:                        Term t = it.next();
1148:                        return isArraySort(t.sort());
1149:                    }
1150:                    return false;
1151:                }
1152:
1153:                private boolean isArraySort(Sort s) {
1154:
1155:                    return (s instanceof  ArraySort);
1156:                }
1157:
1158:                public boolean isBoolean() {
1159:                    for (IteratorOfTerm it = members.iterator(); it.hasNext();) {
1160:                        if (serv.getTypeConverter().getBooleanLDT()
1161:                                .targetSort() == it.next().sort()) {
1162:                            return true;
1163:                        }
1164:                    }
1165:                    return false;
1166:                }
1167:
1168:                public boolean isInt() {
1169:                    for (IteratorOfTerm it = members.iterator(); it.hasNext();) {
1170:                        Term t = it.next();
1171:                        return isInt(t.sort());
1172:                    }
1173:                    return false;
1174:                }
1175:
1176:                private boolean isInt(Sort s) {
1177:                    return s.extendsTrans(serv.getTypeConverter()
1178:                            .getIntegerLDT().targetSort());
1179:                }
1180:
1181:                public String toString() {
1182:                    return "EquClass: (" + members + ")  Disjoint + "
1183:                            + this .disjointRep + " /";
1184:                }
1185:
1186:            }
1187:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.