diff options
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner')
-rw-r--r-- | Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend index 2796e077..56668b79 100644 --- a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend | |||
@@ -7,8 +7,8 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | |||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
10 | import hu.bme.mit.inf.dslreasoner.logic.model.patterns.PossibleDynamicTypeMatcher | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.patterns.PossibleDynamicType |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStar |
12 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference | 12 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference |
13 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument | 13 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument |
14 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral | 14 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral |
@@ -111,7 +111,7 @@ class Logic2Smt_TypeMapperTrace_FilteredTypes implements Logic2Smt_TypeMapperTra | |||
111 | } | 111 | } |
112 | 112 | ||
113 | def validate(EObject element, EObject other) { | 113 | def validate(EObject element, EObject other) { |
114 | if(element != null) { | 114 | if(element !== null) { |
115 | val headOfElement = EcoreUtil2.getContainerOfType(element,SMTDocument) | 115 | val headOfElement = EcoreUtil2.getContainerOfType(element,SMTDocument) |
116 | val expectedHeadOfElement = EcoreUtil2.getContainerOfType(other,SMTDocument) | 116 | val expectedHeadOfElement = EcoreUtil2.getContainerOfType(other,SMTDocument) |
117 | if(headOfElement !== expectedHeadOfElement) { | 117 | if(headOfElement !== expectedHeadOfElement) { |
@@ -234,8 +234,8 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { | |||
234 | } | 234 | } |
235 | 235 | ||
236 | protected def transformOldTypes(Iterable<Type> oldTypes,Iterable<DefinedElement> oldElements, Logic2SmtMapperTrace trace, SMTInput document, ViatraQueryEngine engine) { | 236 | protected def transformOldTypes(Iterable<Type> oldTypes,Iterable<DefinedElement> oldElements, Logic2SmtMapperTrace trace, SMTInput document, ViatraQueryEngine engine) { |
237 | val possibleTypeMatcher = PossibleDynamicTypeMatcher.on(engine) | 237 | val possibleTypeMatcher = PossibleDynamicType.Matcher.on(engine) |
238 | val supertypeStarMatcher = SupertypeStarMatcher.on(engine) | 238 | val supertypeStarMatcher = SupertypeStar.Matcher.on(engine) |
239 | // val possibleTypes = new LinkedList | 239 | // val possibleTypes = new LinkedList |
240 | // if(hasDefinedElement) possibleTypes += typesWithDefinedSupertype | 240 | // if(hasDefinedElement) possibleTypes += typesWithDefinedSupertype |
241 | // if(hasUndefinedElement) possibleTypes += typesWithoutDefinedSupertype | 241 | // if(hasUndefinedElement) possibleTypes += typesWithoutDefinedSupertype |
@@ -351,7 +351,7 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { | |||
351 | Iterable<TypeDeclaration> typesWithoutDefinedSupertype, | 351 | Iterable<TypeDeclaration> typesWithoutDefinedSupertype, |
352 | Logic2SmtMapperTrace trace, SMTInput document, ViatraQueryEngine engine) | 352 | Logic2SmtMapperTrace trace, SMTInput document, ViatraQueryEngine engine) |
353 | { | 353 | { |
354 | val supertypeStarMatcher = SupertypeStarMatcher.on(engine) | 354 | val supertypeStarMatcher = SupertypeStar.Matcher.on(engine) |
355 | val possibleTypes = typesWithoutDefinedSupertype | 355 | val possibleTypes = typesWithoutDefinedSupertype |
356 | val possibleConcreteTypes = possibleTypes.filter[!it.isIsAbstract].toList | 356 | val possibleConcreteTypes = possibleTypes.filter[!it.isIsAbstract].toList |
357 | 357 | ||
@@ -483,7 +483,7 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { | |||
483 | } | 483 | } |
484 | 484 | ||
485 | if(list.empty) throw new AssertionError('''Typereference to type is «type.name» empty''') | 485 | if(list.empty) throw new AssertionError('''Typereference to type is «type.name» empty''') |
486 | if(list.exists[it.type == null]){ | 486 | if(list.exists[it.type === null]){ |
487 | throw new AssertionError('''Typereference to null!''') | 487 | throw new AssertionError('''Typereference to null!''') |
488 | } | 488 | } |
489 | return list | 489 | return list |
@@ -520,14 +520,14 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { | |||
520 | } | 520 | } |
521 | 521 | ||
522 | val engine = ViatraQueryEngine.on(new EMFScope(problem)) | 522 | val engine = ViatraQueryEngine.on(new EMFScope(problem)) |
523 | val supertypeStarMatcher = SupertypeStarMatcher.on(engine) | 523 | val supertypeStarMatcher = SupertypeStar.Matcher.on(engine) |
524 | 524 | ||
525 | val Map<Type,List<DefinedElement>> type2Elements = new HashMap | 525 | val Map<Type,List<DefinedElement>> type2Elements = new HashMap |
526 | for(key : problem.types) { | 526 | for(key : problem.types) { |
527 | type2Elements.put(key,new LinkedList<DefinedElement>) | 527 | type2Elements.put(key,new LinkedList<DefinedElement>) |
528 | } | 528 | } |
529 | 529 | ||
530 | if(trace.typeTrace.independentClasses != null) { | 530 | if(trace.typeTrace.independentClasses !== null) { |
531 | for(type : trace.typeTrace.independentClasses.keySet) { | 531 | for(type : trace.typeTrace.independentClasses.keySet) { |
532 | if(type instanceof TypeDefinition) { | 532 | if(type instanceof TypeDefinition) { |
533 | type.lookup(type2Elements).addAll(type.elements) | 533 | type.lookup(type2Elements).addAll(type.elements) |
@@ -537,7 +537,7 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { | |||
537 | } | 537 | } |
538 | } | 538 | } |
539 | 539 | ||
540 | if(trace.typeTrace.oldObjectTypeFunction != null) { | 540 | if(trace.typeTrace.oldObjectTypeFunction !== null) { |
541 | val inverseOldTypeMap = trace.typeTrace.oldObjectTypeMap.bijectiveInverse | 541 | val inverseOldTypeMap = trace.typeTrace.oldObjectTypeMap.bijectiveInverse |
542 | for(oldElement: trace.typeTrace.elementMap.values) { | 542 | for(oldElement: trace.typeTrace.elementMap.values) { |
543 | val type = interpretation.queryEngine.resolveFunctionDefinition( | 543 | val type = interpretation.queryEngine.resolveFunctionDefinition( |