diff options
author | 2018-03-07 12:48:01 -0500 | |
---|---|---|
committer | 2018-03-07 12:48:01 -0500 | |
commit | 5ac36bba74bcf71224d4895cccdae253b07ccbc9 (patch) | |
tree | 85a15ac3d720c24021c9126dc6e00e653135a9b5 /Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend | |
parent | removed unnecessary println (diff) | |
download | VIATRA-Generator-5ac36bba74bcf71224d4895cccdae253b07ccbc9.tar.gz VIATRA-Generator-5ac36bba74bcf71224d4895cccdae253b07ccbc9.tar.zst VIATRA-Generator-5ac36bba74bcf71224d4895cccdae253b07ccbc9.zip |
Rebooting Z3 solver Containment vs Inheritance still has a bug
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend')
-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 | 129 |
1 files changed, 98 insertions, 31 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 c9bafa6c..2796e077 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 | |||
@@ -27,8 +27,10 @@ import java.util.HashMap | |||
27 | import java.util.LinkedList | 27 | import java.util.LinkedList |
28 | import java.util.List | 28 | import java.util.List |
29 | import java.util.Map | 29 | import java.util.Map |
30 | import org.eclipse.emf.ecore.EObject | ||
30 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | 31 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine |
31 | import org.eclipse.viatra.query.runtime.emf.EMFScope | 32 | import org.eclipse.viatra.query.runtime.emf.EMFScope |
33 | import org.eclipse.xtext.EcoreUtil2 | ||
32 | import org.eclipse.xtext.xbase.lib.Functions.Function0 | 34 | import org.eclipse.xtext.xbase.lib.Functions.Function0 |
33 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | 35 | import org.eclipse.xtext.xbase.lib.Functions.Function1 |
34 | 36 | ||
@@ -63,32 +65,77 @@ class Logic2Smt_TypeMapperTrace_FilteredTypes implements Logic2Smt_TypeMapperTra | |||
63 | val a = this | 65 | val a = this |
64 | val b = new Logic2Smt_TypeMapperTrace_FilteredTypes | 66 | val b = new Logic2Smt_TypeMapperTrace_FilteredTypes |
65 | 67 | ||
66 | b.independentClasses = a.independentClasses.copyMap(newModel.typeDeclarations,[name]) | 68 | b.independentClasses = copyMap(a.independentClasses,newModel.typeDeclarations,[name]) |
67 | 69 | b.independentClasses.values.validate(newModel) | |
68 | b.newObjects = newModel.typeDeclarations.filter[it.name == a.newObjects.name].head | 70 | b.newObjects = newModel.typeDeclarations.copyValue(a.newObjects,[name]) |
69 | b.oldObjects = newModel.typeDeclarations.filter[it.name == a.oldObjects.name].head as SMTEnumeratedTypeDeclaration | 71 | b.newObjects.validate(newModel) |
70 | b.elementMap = a.elementMap.copyMap(b.oldObjects.elements,[name]) | 72 | b.oldObjects = newModel.typeDeclarations.copyValue(a.oldObjects,[name]) as SMTEnumeratedTypeDeclaration |
73 | b.oldObjects.validate(newModel) | ||
74 | b.elementMap = a.elementMap.copyMap( | ||
75 | newModel.typeDeclarations | ||
76 | .filter(SMTEnumeratedTypeDeclaration) | ||
77 | .map[it.elements] | ||
78 | .flatten, | ||
79 | [name] | ||
80 | ) | ||
81 | b.elementMap.values.validate(newModel) | ||
71 | 82 | ||
72 | b.oldObjectTypes = newModel.typeDeclarations.filter[it.name == a.newObjects.name].head as SMTEnumeratedTypeDeclaration | 83 | b.oldObjectTypes = newModel.typeDeclarations.copyValue(a.newObjects,[name]) as SMTEnumeratedTypeDeclaration |
84 | b.oldObjectTypes.validate(newModel) | ||
73 | b.oldObjectTypeMap = a.oldObjectTypeMap.copyMap(b.oldObjectTypes.elements,[name]) | 85 | b.oldObjectTypeMap = a.oldObjectTypeMap.copyMap(b.oldObjectTypes.elements,[name]) |
74 | b.oldObjectTypeFunction = newModel.functionDefinition.filter[it.name == a.oldObjectTypeFunction.name].head | 86 | b.oldObjectTypeMap.values.validate(newModel) |
87 | b.oldObjectTypeFunction = newModel.functionDefinition.copyValue(a.oldObjectTypeFunction,[name]) | ||
88 | b.oldObjectTypeFunction.validate(newModel) | ||
75 | b.oldObjectTypePredicates = a.oldObjectTypePredicates.copyMap(newModel.functionDefinition,[name]) | 89 | b.oldObjectTypePredicates = a.oldObjectTypePredicates.copyMap(newModel.functionDefinition,[name]) |
90 | b.oldObjectTypePredicates.values.validate(newModel) | ||
76 | 91 | ||
77 | b.newObjectTypes = newModel.typeDeclarations.filter[it.name == a.newObjectTypes.name].head as SMTEnumeratedTypeDeclaration | 92 | b.newObjectTypes = newModel.typeDeclarations.copyValue(a.newObjectTypes,[name]) as SMTEnumeratedTypeDeclaration |
93 | b.newObjectTypes.validate(newModel) | ||
78 | b.newObjectTypeMap = a.newObjectTypeMap.copyMap(b.newObjectTypes.elements,[name]) | 94 | b.newObjectTypeMap = a.newObjectTypeMap.copyMap(b.newObjectTypes.elements,[name]) |
79 | b.newObjectTypeFunction = newModel.functionDeclarations.filter[it.name == a.newObjectTypeFunction.name].head | 95 | b.newObjectTypeMap.values.validate(newModel) |
96 | b.newObjectTypeFunction = newModel.functionDeclarations.copyValue(a.newObjectTypeFunction,[name]) | ||
97 | b.newObjectTypeFunction.validate(newModel) | ||
80 | b.newObjectTypePredicates = a.newObjectTypePredicates.copyMap(newModel.functionDefinition,[name]) | 98 | b.newObjectTypePredicates = a.newObjectTypePredicates.copyMap(newModel.functionDefinition,[name]) |
81 | 99 | b.newObjectTypePredicates.values.validate(newModel) | |
82 | return b | 100 | return b |
83 | } | 101 | } |
102 | |||
103 | def public static <Type, ValueType> copyValue(Iterable<? extends Type> collection, Type target, Function1<Type,ValueType> extractor) { | ||
104 | if(target===null) { | ||
105 | return null | ||
106 | } else { | ||
107 | val targetValue = extractor.apply(target) | ||
108 | val res = collection.filter[extractor.apply(it)==targetValue].head | ||
109 | return res | ||
110 | } | ||
111 | } | ||
112 | |||
113 | def validate(EObject element, EObject other) { | ||
114 | if(element != null) { | ||
115 | val headOfElement = EcoreUtil2.getContainerOfType(element,SMTDocument) | ||
116 | val expectedHeadOfElement = EcoreUtil2.getContainerOfType(other,SMTDocument) | ||
117 | if(headOfElement !== expectedHeadOfElement) { | ||
118 | throw new AssertionError(''' | ||
119 | Element in different resource: «element» | ||
120 | Expected root: «expectedHeadOfElement» | ||
121 | Found root: «headOfElement»''') | ||
122 | } | ||
123 | } | ||
124 | } | ||
125 | def validate(Iterable<? extends EObject> iterable, EObject root) { | ||
126 | if(iterable !== null) | ||
127 | for(element : iterable) { | ||
128 | element.validate(root) | ||
129 | } | ||
130 | } | ||
84 | } | 131 | } |
85 | 132 | ||
86 | class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { | 133 | class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { |
87 | val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE | 134 | val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE |
88 | val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE | 135 | val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE |
89 | 136 | ||
90 | private def toID(List<String> names) {names.join("!") } | 137 | private def String toID(List<String> names) { names.map[split("\\s+").join("!")].join("!") } |
91 | private def toID(String name) {name.split("\\s+").toID} | 138 | private def String toID(String name) { name.split("\\s+").join("!")} |
92 | 139 | ||
93 | override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) { | 140 | override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) { |
94 | val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes | 141 | val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes |
@@ -105,7 +152,7 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { | |||
105 | val hasNewElements = !connectedTypesWithoutDefintypesWithoutDefinedSupertype.empty | 152 | val hasNewElements = !connectedTypesWithoutDefintypesWithoutDefinedSupertype.empty |
106 | 153 | ||
107 | // 0. map the simple types | 154 | // 0. map the simple types |
108 | this.transformIndependentTypes(independentTypes,trace) | 155 | this.transformIndependentTypes(independentTypes,trace,document) |
109 | 156 | ||
110 | // 1. Has old elements => create supertype for it | 157 | // 1. Has old elements => create supertype for it |
111 | if(hasOldElements) { | 158 | if(hasOldElements) { |
@@ -135,7 +182,7 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { | |||
135 | return types.size == 1 && types.head.isIndependentType | 182 | return types.size == 1 && types.head.isIndependentType |
136 | } | 183 | } |
137 | 184 | ||
138 | protected def transformIndependentTypes(Iterable<TypeDefinition> types,Logic2SmtMapperTrace trace) { | 185 | protected def transformIndependentTypes(Iterable<TypeDefinition> types,Logic2SmtMapperTrace trace, SMTInput document) { |
139 | for(type: types) { | 186 | for(type: types) { |
140 | val independentSMTType = createSMTEnumeratedTypeDeclaration => [ | 187 | val independentSMTType = createSMTEnumeratedTypeDeclaration => [ |
141 | name = toID(#["oldType",type.name]) | 188 | name = toID(#["oldType",type.name]) |
@@ -146,6 +193,7 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { | |||
146 | independentSMTType.elements += enumLiteral | 193 | independentSMTType.elements += enumLiteral |
147 | trace.typeTrace.elementMap.put(element,enumLiteral) | 194 | trace.typeTrace.elementMap.put(element,enumLiteral) |
148 | } | 195 | } |
196 | document.typeDeclarations += independentSMTType | ||
149 | } | 197 | } |
150 | } | 198 | } |
151 | 199 | ||
@@ -474,26 +522,45 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { | |||
474 | val engine = ViatraQueryEngine.on(new EMFScope(problem)) | 522 | val engine = ViatraQueryEngine.on(new EMFScope(problem)) |
475 | val supertypeStarMatcher = SupertypeStarMatcher.on(engine) | 523 | val supertypeStarMatcher = SupertypeStarMatcher.on(engine) |
476 | 524 | ||
477 | val type2Elements = (trace.typeTrace.oldObjectTypeMap.keySet + | 525 | val Map<Type,List<DefinedElement>> type2Elements = new HashMap |
478 | trace.typeTrace.newObjectTypeMap.keySet) | 526 | for(key : problem.types) { |
479 | .toInvertedMap[new LinkedList<DefinedElement>] | 527 | type2Elements.put(key,new LinkedList<DefinedElement>) |
528 | } | ||
480 | 529 | ||
481 | val inverseOldTypeMap = trace.typeTrace.oldObjectTypeMap.bijectiveInverse | 530 | if(trace.typeTrace.independentClasses != null) { |
482 | for(oldElement: trace.typeTrace.elementMap.values) { | 531 | for(type : trace.typeTrace.independentClasses.keySet) { |
483 | val type = interpretation.queryEngine.resolveFunctionDefinition( | 532 | if(type instanceof TypeDefinition) { |
484 | trace.typeTrace.oldObjectTypeFunction,#[oldElement]) as SMTEnumLiteral | 533 | type.lookup(type2Elements).addAll(type.elements) |
485 | val dynamicType = type.lookup(inverseOldTypeMap) | 534 | } else { |
486 | val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType) | 535 | throw new AssertionError('''Independent classes are type definitions, but got: "«type»"''') |
487 | supertypes.forEach[type2Elements.get(it) += oldElement.lookup(smt2logic)] | 536 | } |
537 | } | ||
488 | } | 538 | } |
489 | 539 | ||
490 | val inverseNewTypeMap = trace.typeTrace.newObjectTypeMap.bijectiveInverse | 540 | if(trace.typeTrace.oldObjectTypeFunction != null) { |
491 | for(newElement: newElements.map[value as SMTSymbolicDeclaration]) { | 541 | val inverseOldTypeMap = trace.typeTrace.oldObjectTypeMap.bijectiveInverse |
492 | val type = interpretation.queryEngine.resolveFunctionDeclaration( | 542 | for(oldElement: trace.typeTrace.elementMap.values) { |
493 | trace.typeTrace.newObjectTypeFunction,#[newElement]) as SMTEnumLiteral | 543 | val type = interpretation.queryEngine.resolveFunctionDefinition( |
494 | val dynamicType = type.lookup(inverseNewTypeMap) | 544 | trace.typeTrace.oldObjectTypeFunction,#[oldElement]) as SMTEnumLiteral |
495 | val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType) | 545 | val dynamicType = type.lookup(inverseOldTypeMap) |
496 | supertypes.forEach[type2Elements.get(it) += newElement.lookup(smt2logic)] | 546 | val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType) |
547 | for(superType : supertypes) { | ||
548 | superType.lookup(type2Elements) += oldElement.lookup(smt2logic) | ||
549 | } | ||
550 | } | ||
551 | } | ||
552 | |||
553 | if(trace.typeTrace.newObjectTypeFunction !== null) { | ||
554 | val inverseNewTypeMap = trace.typeTrace.newObjectTypeMap.bijectiveInverse | ||
555 | for(newElement: newElements.map[value as SMTSymbolicDeclaration]) { | ||
556 | val type = interpretation.queryEngine.resolveFunctionDeclaration( | ||
557 | trace.typeTrace.newObjectTypeFunction,#[newElement]) as SMTEnumLiteral | ||
558 | val dynamicType = type.lookup(inverseNewTypeMap) | ||
559 | val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType) | ||
560 | for(superType : supertypes) { | ||
561 | superType.lookup(type2Elements) += newElement.lookup(smt2logic) | ||
562 | } | ||
563 | } | ||
497 | } | 564 | } |
498 | 565 | ||
499 | return new Logic2SMT_TypeMapperInterpretation(type2Elements,logic2smt,smt2logic) | 566 | return new Logic2SMT_TypeMapperInterpretation(type2Elements,logic2smt,smt2logic) |