diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns')
5 files changed, 371 insertions, 415 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend index d6a15c1a..0e0f1f02 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend | |||
@@ -1,209 +1,150 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
5 | import org.eclipse.emf.ecore.EClass | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | 5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult |
9 | 7 | ||
10 | class GenericTypeIndexer extends TypeIndexer { | 8 | class GenericTypeIndexer extends TypeIndexer { |
11 | val PatternGenerator base; | ||
12 | |||
13 | new(PatternGenerator base) { | 9 | new(PatternGenerator base) { |
14 | this.base = base | 10 | super(base) |
15 | } | 11 | } |
12 | |||
16 | override requiresTypeAnalysis() { false } | 13 | override requiresTypeAnalysis() { false } |
17 | 14 | ||
18 | public override getRequiredQueries() ''' | 15 | override getRequiredQueries() ''' |
19 | private pattern newELement(interpretation: PartialInterpretation, element: DefinedElement) { | 16 | «super.requiredQueries» |
20 | PartialInterpretation.newElements(interpretation,element); | 17 | |
21 | } | 18 | /** |
22 | 19 | * Direct supertypes of a type. | |
23 | private pattern typeInterpretation(problem:LogicProblem, interpetation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialComplexTypeInterpretation) { | 20 | */ |
24 | find interpretation(problem,interpetation); | 21 | private pattern supertypeDirect(subtype : Type, supertype : Type) { |
25 | LogicProblem.types(problem,type); | 22 | Type.supertypes(subtype, supertype); |
26 | PartialInterpretation.partialtypeinterpratation(interpetation,typeInterpretation); | 23 | } |
27 | PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); | 24 | |
28 | } | 25 | /** |
29 | 26 | * All supertypes of a type. | |
30 | private pattern directInstanceOf(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement, type:Type) { | 27 | */ |
31 | find interpretation(problem,interpetation); | 28 | private pattern supertypeStar(subtype: Type, supertype: Type) { |
32 | find mustExist(problem,interpetation,element); | 29 | subtype == supertype; |
33 | LogicProblem.types(problem,type); | 30 | } or { |
34 | TypeDefinition.elements(type,element); | 31 | find supertypeDirect+(subtype,supertype); |
35 | } or { | 32 | } |
36 | find mustExist(problem,interpetation,element); | 33 | |
37 | find typeInterpretation(problem,interpetation,type,typeInterpretation); | 34 | /// Complex type reasoning patterns /// |
38 | PartialComplexTypeInterpretation.elements(typeInterpretation,element); | 35 | // |
39 | } | 36 | // In a valid type system, for each element e there is exactly one type T where |
40 | 37 | // 1: T(e) - but we dont know this for type declaration | |
41 | /** | 38 | // 2: For the dynamic type D and another type T, where D(e) && D-->T, T(e) is true. |
42 | * Direct supertypes of a type. | 39 | // 2e: A type hierarchy is invalid, if there is a supertype T for a dynamic type D which does no contains e: |
43 | */ | 40 | // D(e) && D-->T && !T(e) |
44 | private pattern supertypeDirect(subtype : Type, supertype : Type) { | 41 | // 3: There is no T' that T'->T and T'(e) |
45 | Type.supertypes(subtype, supertype); | 42 | // 3e: A type hierarcy is invalid, if there is a type T for a dynamic type D, which contains e, but not subtype of T: |
46 | } | 43 | // D(e) && ![T--->D] && T(e) |
47 | |||
48 | /** | ||
49 | * All supertypes of a type. | ||
50 | */ | ||
51 | private pattern supertypeStar(subtype: Type, supertype: Type) { | ||
52 | subtype == supertype; | ||
53 | } or { | ||
54 | find supertypeDirect+(subtype,supertype); | ||
55 | } | ||
56 | |||
57 | /// Complex type reasoning patterns /// | ||
58 | // | ||
59 | // In a valid type system, for each element e there is exactly one type T where | ||
60 | // 1: T(e) - but we dont know this for type declaration | ||
61 | // 2: For the dynamic type D and another type T, where D(e) && D-->T, T(e) is true. | ||
62 | // 2e: A type hierarchy is invalid, if there is a supertype T for a dynamic type D which does no contains e: | ||
63 | // D(e) && D-->T && !T(e) | ||
64 | // 3: There is no T' that T'->T and T'(e) | ||
65 | // 3e: A type hierarcy is invalid, if there is a type T for a dynamic type D, which contains e, but not subtype of T: | ||
66 | // D(e) && ![T--->D] && T(e) | ||
67 | // 4: T is not abstract | ||
68 | // Such type T is called Dynamic type of e, while other types are called static types. | ||
69 | // | ||
70 | // The following patterns checks the possible dynamic types for an element | ||
71 | |||
72 | private pattern wellformedType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) { | ||
73 | // 1: T(e) | ||
74 | find directInstanceOf(problem,interpretation,element,dynamic); | ||
75 | // 2e is not true: D(e) && D-->T && !T(e) | ||
76 | neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); | ||
77 | // 3e is not true: D(e) && ![T--->D] && T(e) | ||
78 | neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); | ||
79 | // 4: T is not abstract | ||
80 | Type.isAbstract(dynamic,false); | ||
81 | } | ||
82 | |||
83 | |||
84 | private pattern isPrimitive(element: PrimitiveElement) { | ||
85 | PrimitiveElement(element); | ||
86 | } | ||
87 | |||
88 | private pattern possibleDynamicType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) | ||
89 | // case 1: element is defined at least once | ||
90 | { | ||
91 | LogicProblem.types(problem,dynamic); | ||
92 | // select a random definition 'randomType' | ||
93 | find directInstanceOf(problem,interpretation,element,randomType); | ||
94 | // dynamic is a subtype of 'randomType' | ||
95 | find supertypeStar(dynamic,randomType); | ||
96 | // 2e is not true: D(e) && D-->T && !T(e) | ||
97 | neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); | ||
98 | // 3e is not true: D(e) && ![T--->D] && T(e) | ||
99 | neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); | ||
100 | // 4: T is not abstract | ||
101 | Type.isAbstract(dynamic,false); | ||
102 | // 5. element is not primitive datatype | ||
103 | neg find isPrimitive(element); | ||
104 | } or | ||
105 | // case 2: element is not defined anywhere | ||
106 | { | ||
107 | find mayExist(problem,interpretation,element); | ||
108 | // there is no definition | ||
109 | neg find directInstanceOf(problem,interpretation,element,_); | ||
110 | // 2e is not true: D(e) && D-->T && !T(e) | ||
111 | // because non of the definition contains element, the type cannot have defined supertype | ||
112 | LogicProblem.types(problem,dynamic); | ||
113 | PartialInterpretation.problem(interpretation,problem); | ||
114 | neg find typeWithDefinedSupertype(dynamic); | ||
115 | // 3e is not true: D(e) && ![T--->D] && T(e) | ||
116 | // because there is no definition, dynamic covers all definition | ||
117 | // 4: T is not abstract | 44 | // 4: T is not abstract |
118 | Type.isAbstract(dynamic,false); | 45 | // Such type T is called Dynamic type of e, while other types are called static types. |
119 | // 5. element is not primitive datatype | 46 | // |
120 | neg find isPrimitive(element); | 47 | // The following patterns checks the possible dynamic types for an element |
121 | } | 48 | |
122 | 49 | private pattern wellformedType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) { | |
123 | /** | 50 | // 1: T(e) |
124 | * supertype -------> element <------- otherSupertype | 51 | find directInstanceOf(problem,interpretation,element,dynamic); |
125 | * A A | 52 | // 2e is not true: D(e) && D-->T && !T(e) |
126 | * | | | 53 | neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); |
127 | * wrongDynamic -----------------------------X | 54 | // 3e is not true: D(e) && ![T--->D] && T(e) |
128 | */ | 55 | neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); |
129 | private pattern dynamicTypeNotSubtypeOfADefinition(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic : Type) { | 56 | // 4: T is not abstract |
130 | find directInstanceOf(problem,interpretation,element,supertype); | 57 | Type.isAbstract(dynamic,false); |
131 | find directInstanceOf(problem,interpretation,element,otherSupertype); | 58 | } |
132 | find supertypeStar(wrongDynamic,supertype); | 59 | |
133 | neg find supertypeStar(wrongDynamic,otherSupertype); | 60 | private pattern possibleDynamicType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) |
134 | } | 61 | // case 1: element is defined at least once |
135 | 62 | { | |
136 | /** | 63 | LogicProblem.types(problem,dynamic); |
137 | * supertype -------> element <---X--- otherSupertype | 64 | // select a random definition 'randomType' |
138 | * A A | 65 | find directInstanceOf(problem,interpretation,element,randomType); |
139 | * | | | 66 | // dynamic is a subtype of 'randomType' |
140 | * wrongDynamic -----------------------------+ | 67 | find supertypeStar(dynamic,randomType); |
141 | */ | 68 | // 2e is not true: D(e) && D-->T && !T(e) |
142 | private pattern dynamicTypeIsSubtypeOfANonDefinition(problem: LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic:Type) { | 69 | neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); |
143 | find directInstanceOf(problem,interpretation,element,supertype); | 70 | // 3e is not true: D(e) && ![T--->D] && T(e) |
144 | neg find elementInTypeDefinition(element,otherSupertype); | 71 | neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); |
145 | TypeDefinition(otherSupertype); | 72 | // 4: T is not abstract |
146 | find supertypeStar(wrongDynamic, supertype); | 73 | Type.isAbstract(dynamic,false); |
147 | find supertypeStar(wrongDynamic, otherSupertype); | 74 | // 5. element is not primitive datatype |
148 | } | 75 | neg find isPrimitive(element); |
149 | 76 | } or | |
150 | private pattern elementInTypeDefinition(element:DefinedElement, definition:TypeDefinition) { | 77 | // case 2: element is not defined anywhere |
151 | TypeDefinition.elements(definition,element); | 78 | { |
152 | } | 79 | find mayExist(problem,interpretation,element); |
153 | 80 | // there is no definition | |
154 | private pattern typeWithDefinedSupertype(type:Type) { | 81 | neg find directInstanceOf(problem,interpretation,element,_); |
155 | find supertypeStar(type,definedSupertype); | 82 | // 2e is not true: D(e) && D-->T && !T(e) |
156 | TypeDefinition(definedSupertype); | 83 | // because non of the definition contains element, the type cannot have defined supertype |
157 | } | 84 | LogicProblem.types(problem,dynamic); |
158 | 85 | PartialInterpretation.problem(interpretation,problem); | |
159 | private pattern scopeDisallowsNewElementsFromType(typeInterpretation:PartialComplexTypeInterpretation) { | 86 | neg find typeWithDefinedSupertype(dynamic); |
160 | Scope.targetTypeInterpretation(scope,typeInterpretation); | 87 | // 3e is not true: D(e) && ![T--->D] && T(e) |
161 | Scope.maxNewElements(scope,0); | 88 | // because there is no definition, dynamic covers all definition |
162 | } | 89 | // 4: T is not abstract |
163 | ''' | 90 | Type.isAbstract(dynamic,false); |
164 | 91 | // 5. element is not primitive datatype | |
165 | public override generateInstanceOfQueries(LogicProblem problem, PartialInterpretation emptySolution,TypeAnalysisResult typeAnalysisResult) { | 92 | neg find isPrimitive(element); |
166 | ''' | 93 | } |
167 | «FOR type:problem.types» | 94 | |
168 | «problem.generateMustInstenceOf(type)» | ||
169 | «problem.generateMayInstanceOf(type)» | ||
170 | «ENDFOR» | ||
171 | ''' | ||
172 | } | ||
173 | |||
174 | private def patternName(Type type, Modality modality) | ||
175 | '''«modality.toString.toLowerCase»InstanceOf«base.canonizeName(type.name)»''' | ||
176 | |||
177 | private def generateMustInstenceOf(LogicProblem problem, Type type) { | ||
178 | ''' | ||
179 | /** | 95 | /** |
180 | * An element must be an instance of type "«type.name»". | 96 | * supertype -------> element <------- otherSupertype |
97 | * A A | ||
98 | * | | | ||
99 | * wrongDynamic -----------------------------X | ||
181 | */ | 100 | */ |
182 | private pattern «patternName(type,Modality.MUST)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | 101 | private pattern dynamicTypeNotSubtypeOfADefinition(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic : Type) { |
183 | Type.name(type,"«type.name»"); | 102 | find directInstanceOf(problem,interpretation,element,supertype); |
184 | find directInstanceOf(problem,interpretation,element,type); | 103 | find directInstanceOf(problem,interpretation,element,otherSupertype); |
104 | find supertypeStar(wrongDynamic,supertype); | ||
105 | neg find supertypeStar(wrongDynamic,otherSupertype); | ||
185 | } | 106 | } |
186 | ''' | 107 | |
187 | } | ||
188 | |||
189 | private def generateMayInstanceOf(LogicProblem problem, Type type) { | ||
190 | ''' | ||
191 | /** | 108 | /** |
192 | * An element may be an instance of type "«type.name»". | 109 | * supertype -------> element <---X--- otherSupertype |
110 | * A A | ||
111 | * | | | ||
112 | * wrongDynamic -----------------------------+ | ||
193 | */ | 113 | */ |
194 | private pattern «patternName(type,Modality.MAY)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | 114 | private pattern dynamicTypeIsSubtypeOfANonDefinition(problem: LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic:Type) { |
195 | Type.name(type,"«type.name»"); | 115 | find directInstanceOf(problem,interpretation,element,supertype); |
196 | find possibleDynamicType(problem,interpretation,dynamic,element); | 116 | neg find elementInTypeDefinition(element,otherSupertype); |
197 | find supertypeStar(dynamic,type); | 117 | TypeDefinition(otherSupertype); |
198 | neg find scopeDisallowsNewElementsFromType(dynamic); | 118 | find supertypeStar(wrongDynamic, supertype); |
119 | find supertypeStar(wrongDynamic, otherSupertype); | ||
120 | } | ||
121 | |||
122 | private pattern elementInTypeDefinition(element:DefinedElement, definition:TypeDefinition) { | ||
123 | TypeDefinition.elements(definition,element); | ||
124 | } | ||
125 | |||
126 | private pattern typeWithDefinedSupertype(type:Type) { | ||
127 | find supertypeStar(type,definedSupertype); | ||
128 | TypeDefinition(definedSupertype); | ||
129 | } | ||
130 | |||
131 | private pattern scopeDisallowsNewElementsFromType(typeInterpretation:PartialComplexTypeInterpretation) { | ||
132 | Scope.targetTypeInterpretation(scope,typeInterpretation); | ||
133 | Scope.maxNewElements(scope,0); | ||
199 | } | 134 | } |
135 | ''' | ||
136 | |||
137 | protected override generateMayInstanceOf(LogicProblem problem, Type type, TypeAnalysisResult typeAnalysisResult) { | ||
138 | ''' | ||
139 | /** | ||
140 | * An element may be an instance of type "«type.name»". | ||
141 | */ | ||
142 | private pattern «patternName(type,Modality.MAY)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | ||
143 | Type.name(type,"«type.name»"); | ||
144 | find possibleDynamicType(problem,interpretation,dynamic,element); | ||
145 | find supertypeStar(dynamic,type); | ||
146 | neg find scopeDisallowsNewElementsFromType(dynamic); | ||
147 | } | ||
200 | ''' | 148 | ''' |
201 | } | 149 | } |
202 | 150 | } | |
203 | public override referInstanceOf(Type type, Modality modality, String variableName) { | ||
204 | '''find «patternName(type,modality)»(problem,interpretation,«variableName»);''' | ||
205 | } | ||
206 | public override referInstanceOf(EClass type, Modality modality, String variableName) { | ||
207 | '''find «modality.toString.toLowerCase»InstanceOf«base.canonizeName('''«type.name» class''')»(problem,interpretation,«variableName»);''' | ||
208 | } | ||
209 | } \ No newline at end of file | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend index c9f6abce..52f0cbea 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend | |||
@@ -14,107 +14,111 @@ class GenericTypeRefinementGenerator extends TypeRefinementGenerator { | |||
14 | new(PatternGenerator base) { | 14 | new(PatternGenerator base) { |
15 | super(base) | 15 | super(base) |
16 | } | 16 | } |
17 | |||
17 | override requiresTypeAnalysis() { false } | 18 | override requiresTypeAnalysis() { false } |
18 | 19 | ||
19 | override generateRefineObjectQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { | 20 | override generateRefineObjectQueries(LogicProblem p, PartialInterpretation emptySolution, |
21 | TypeAnalysisResult typeAnalysisResult) { | ||
20 | val containment = p.containmentHierarchies.head | 22 | val containment = p.containmentHierarchies.head |
21 | val newObjectTypes = p.types.filter(TypeDeclaration).filter[!isAbstract] | 23 | val newObjectTypes = p.types.filter(TypeDeclaration).filter[!isAbstract] |
22 | val inverseRelations = new HashMap | 24 | val inverseRelations = new HashMap |
23 | p.annotations.filter(InverseRelationAssertion).forEach[ | 25 | p.annotations.filter(InverseRelationAssertion).forEach [ |
24 | inverseRelations.put(it.inverseA,it.inverseB) | 26 | inverseRelations.put(it.inverseA, it.inverseB) |
25 | inverseRelations.put(it.inverseB,it.inverseA) | 27 | inverseRelations.put(it.inverseB, it.inverseA) |
26 | ] | 28 | ] |
27 | return ''' | 29 | return ''' |
28 | pattern «hasElementInContainmentName»(problem:LogicProblem, interpretation:PartialInterpretation) | 30 | pattern «hasElementInContainmentName»(problem:LogicProblem, interpretation:PartialInterpretation) |
29 | «FOR type :containment.typesOrderedInHierarchy SEPARATOR "or"»{ | 31 | «FOR type : containment.typesOrderedInHierarchy SEPARATOR "or"»{ |
30 | find interpretation(problem,interpretation); | ||
31 | «base.typeIndexer.referInstanceOf(type,Modality.MUST,"root")» | ||
32 | find mustExist(problem, interpretation, root); | ||
33 | }«ENDFOR» | ||
34 | «FOR type:newObjectTypes» | ||
35 | «IF(containment.typesOrderedInHierarchy.contains(type))» | ||
36 | «FOR containmentRelation : containment.containmentRelations.filter[canBeContainedByRelation(it,type)]» | ||
37 | «IF inverseRelations.containsKey(containmentRelation)» | ||
38 | pattern «this.patternName(containmentRelation,inverseRelations.get(containmentRelation),type)»( | ||
39 | problem:LogicProblem, interpretation:PartialInterpretation, | ||
40 | relationInterpretation:PartialRelationInterpretation, inverseInterpretation:PartialRelationInterpretation ,typeInterpretation:PartialComplexTypeInterpretation, | ||
41 | container:DefinedElement) | ||
42 | { | ||
43 | find interpretation(problem,interpretation); | ||
44 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); | ||
45 | PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); | ||
46 | PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation); | ||
47 | PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"«containmentRelation.name»"); | ||
48 | PartialInterpretation.partialrelationinterpretation(interpretation,inverseInterpretation); | ||
49 | PartialRelationInterpretation.interpretationOf.name(inverseInterpretation,"«inverseRelations.get(containmentRelation).name»"); | ||
50 | «base.typeIndexer.referInstanceOf((containmentRelation.parameters.get(0) as ComplexTypeReference).referred,Modality.MUST,"container")» | ||
51 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» | ||
52 | «base.relationDeclarationIndexer.referRelation(containmentRelation as RelationDeclaration,"container","newObject",Modality.MAY)» | ||
53 | find mustExist(problem, interpretation, container); | ||
54 | neg find mustExist(problem, interpretation, newObject); | ||
55 | } | ||
56 | «ELSE» | ||
57 | pattern «this.patternName(containmentRelation,null,type)»( | ||
58 | problem:LogicProblem, interpretation:PartialInterpretation, | ||
59 | relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation, | ||
60 | container:DefinedElement) | ||
61 | { | ||
62 | find interpretation(problem,interpretation); | ||
63 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); | ||
64 | PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); | ||
65 | PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation); | ||
66 | PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"«containmentRelation.name»"); | ||
67 | «base.typeIndexer.referInstanceOf((containmentRelation.parameters.get(0) as ComplexTypeReference).referred,Modality.MUST,"container")» | ||
68 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» | ||
69 | «base.relationDeclarationIndexer.referRelation(containmentRelation as RelationDeclaration,"container","newObject",Modality.MAY)» | ||
70 | find mustExist(problem, interpretation, container); | ||
71 | neg find mustExist(problem, interpretation, newObject); | ||
72 | } | ||
73 | «ENDIF» | ||
74 | «ENDFOR» | ||
75 | pattern «patternName(null,null,type)»( | ||
76 | problem:LogicProblem, interpretation:PartialInterpretation, | ||
77 | typeInterpretation:PartialComplexTypeInterpretation) | ||
78 | { | ||
79 | find interpretation(problem,interpretation); | 32 | find interpretation(problem,interpretation); |
80 | neg find «hasElementInContainmentName»(problem,interpretation); | 33 | «base.typeIndexer.referInstanceOf(type,Modality.MUST,"root")» |
81 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); | 34 | find mustExist(problem, interpretation, root); |
82 | PartialComplexTypeInterpretation.interpretationOf.name(type,"«type.name»"); | 35 | }«ENDFOR» |
83 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» | 36 | «FOR type : newObjectTypes» |
84 | find mayExist(problem, interpretation, newObject); | 37 | «IF(containment.typesOrderedInHierarchy.contains(type))» |
85 | neg find mustExist(problem, interpretation, newObject); | 38 | «FOR containmentRelation : containment.containmentRelations.filter[canBeContainedByRelation(it,type)]» |
86 | } | 39 | «IF inverseRelations.containsKey(containmentRelation)» |
87 | «ELSE» | 40 | pattern «this.patternName(containmentRelation,inverseRelations.get(containmentRelation),type)»( |
88 | pattern createObject_«this.patternName(null,null,type)»( | 41 | problem:LogicProblem, interpretation:PartialInterpretation, |
89 | problem:LogicProblem, interpretation:PartialInterpretation, | 42 | relationInterpretation:PartialRelationInterpretation, inverseInterpretation:PartialRelationInterpretation ,typeInterpretation:PartialComplexTypeInterpretation, |
90 | typeInterpretation:PartialComplexTypeInterpretation) | 43 | container:DefinedElement) |
91 | { | 44 | { |
92 | find interpretation(problem,interpretation); | 45 | find interpretation(problem,interpretation); |
93 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); | 46 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); |
94 | PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); | 47 | PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); |
95 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» | 48 | PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation); |
96 | find mayExist(problem, interpretation, newObject); | 49 | PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"«containmentRelation.name»"); |
97 | neg find mustExist(problem, interpretation, newObject); | 50 | PartialInterpretation.partialrelationinterpretation(interpretation,inverseInterpretation); |
98 | } | 51 | PartialRelationInterpretation.interpretationOf.name(inverseInterpretation,"«inverseRelations.get(containmentRelation).name»"); |
99 | «ENDIF» | 52 | «base.typeIndexer.referInstanceOf((containmentRelation.parameters.get(0) as ComplexTypeReference).referred,Modality.MUST,"container")» |
100 | «ENDFOR» | 53 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» |
54 | «base.relationDeclarationIndexer.referRelation(containmentRelation as RelationDeclaration,"container","newObject",Modality.MAY)» | ||
55 | find mustExist(problem, interpretation, container); | ||
56 | neg find mustExist(problem, interpretation, newObject); | ||
57 | } | ||
58 | «ELSE» | ||
59 | pattern «this.patternName(containmentRelation,null,type)»( | ||
60 | problem:LogicProblem, interpretation:PartialInterpretation, | ||
61 | relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation, | ||
62 | container:DefinedElement) | ||
63 | { | ||
64 | find interpretation(problem,interpretation); | ||
65 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); | ||
66 | PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); | ||
67 | PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation); | ||
68 | PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"«containmentRelation.name»"); | ||
69 | «base.typeIndexer.referInstanceOf((containmentRelation.parameters.get(0) as ComplexTypeReference).referred,Modality.MUST,"container")» | ||
70 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» | ||
71 | «base.relationDeclarationIndexer.referRelation(containmentRelation as RelationDeclaration,"container","newObject",Modality.MAY)» | ||
72 | find mustExist(problem, interpretation, container); | ||
73 | neg find mustExist(problem, interpretation, newObject); | ||
74 | } | ||
75 | «ENDIF» | ||
76 | «ENDFOR» | ||
77 | pattern «patternName(null,null,type)»( | ||
78 | problem:LogicProblem, interpretation:PartialInterpretation, | ||
79 | typeInterpretation:PartialComplexTypeInterpretation) | ||
80 | { | ||
81 | find interpretation(problem,interpretation); | ||
82 | neg find «hasElementInContainmentName»(problem,interpretation); | ||
83 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); | ||
84 | PartialComplexTypeInterpretation.interpretationOf.name(type,"«type.name»"); | ||
85 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» | ||
86 | find mayExist(problem, interpretation, newObject); | ||
87 | neg find mustExist(problem, interpretation, newObject); | ||
88 | } | ||
89 | «ELSE» | ||
90 | pattern createObject_«this.patternName(null,null,type)»( | ||
91 | problem:LogicProblem, interpretation:PartialInterpretation, | ||
92 | typeInterpretation:PartialComplexTypeInterpretation) | ||
93 | { | ||
94 | find interpretation(problem,interpretation); | ||
95 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); | ||
96 | PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); | ||
97 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» | ||
98 | find mayExist(problem, interpretation, newObject); | ||
99 | neg find mustExist(problem, interpretation, newObject); | ||
100 | } | ||
101 | «ENDIF» | ||
102 | «ENDFOR» | ||
101 | ''' | 103 | ''' |
102 | } | 104 | } |
103 | 105 | ||
104 | override generateRefineTypeQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { | 106 | override generateRefineTypeQueries(LogicProblem p, PartialInterpretation emptySolution, |
107 | TypeAnalysisResult typeAnalysisResult) { | ||
105 | return ''' | 108 | return ''' |
106 | «FOR type : p.types.filter(TypeDeclaration).filter[!it.isAbstract]» | 109 | «FOR type : p.types.filter(TypeDeclaration).filter[!it.isAbstract]» |
107 | pattern refineTypeTo_«base.canonizeName(type.name)»(problem:LogicProblem, interpretation:PartialInterpretation, object: DefinedElement) { | 110 | pattern refineTypeTo_«base.canonizeName(type.name)»(problem:LogicProblem, interpretation:PartialInterpretation, object: DefinedElement) { |
108 | find interpretation(problem,interpretation); | 111 | find interpretation(problem,interpretation); |
109 | find mustExist(problem, interpretation, object); | 112 | find mustExist(problem, interpretation, object); |
110 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"object")» | 113 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"object")» |
111 | neg «base.typeIndexer.referInstanceOf(type,Modality.MUST,"object")» | 114 | neg «base.typeIndexer.referInstanceOf(type,Modality.MUST,"object")» |
112 | } | 115 | } |
113 | «ENDFOR» | 116 | «ENDFOR» |
114 | ''' | 117 | ''' |
115 | } | 118 | } |
116 | 119 | ||
117 | override getRefineTypeQueryNames(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { | 120 | override getRefineTypeQueryNames(LogicProblem p, PartialInterpretation emptySolution, |
121 | TypeAnalysisResult typeAnalysisResult) { | ||
118 | p.types.filter(TypeDeclaration).toInvertedMap['''refineTypeTo_«base.canonizeName(it.name)»'''] | 122 | p.types.filter(TypeDeclaration).toInvertedMap['''refineTypeTo_«base.canonizeName(it.name)»'''] |
119 | } | 123 | } |
120 | } \ No newline at end of file | 124 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend index d1d57189..7d687e99 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend | |||
@@ -1,52 +1,122 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
5 | import org.eclipse.emf.ecore.EClass | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
14 | import java.math.BigDecimal | 13 | import java.math.BigDecimal |
14 | import org.eclipse.emf.ecore.EClass | ||
15 | import org.eclipse.xtend.lib.annotations.Accessors | ||
16 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
15 | 17 | ||
18 | @FinalFieldsConstructor | ||
16 | abstract class TypeIndexer { | 19 | abstract class TypeIndexer { |
17 | public def CharSequence getRequiredQueries() | 20 | @Accessors(PROTECTED_GETTER) val PatternGenerator base |
18 | public def boolean requiresTypeAnalysis() | 21 | |
19 | public def CharSequence generateInstanceOfQueries(LogicProblem problem,PartialInterpretation emptySolution,TypeAnalysisResult typeAnalysisResult) | 22 | def CharSequence getRequiredQueries() ''' |
20 | public def CharSequence referInstanceOf(Type type, Modality modality, String variableName) | 23 | private pattern typeInterpretation(problem:LogicProblem, interpretation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialComplexTypeInterpretation) { |
21 | public def CharSequence referInstanceOf(EClass type, Modality modality, String variableName) | 24 | find interpretation(problem,interpretation); |
22 | 25 | LogicProblem.types(problem,type); | |
23 | public def dispatch CharSequence referInstanceOfByReference(ComplexTypeReference reference, Modality modality, String variableName) { | 26 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); |
24 | reference.referred.referInstanceOf(modality,variableName) | 27 | PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); |
25 | } | 28 | } |
26 | public def dispatch CharSequence referInstanceOfByReference(BoolTypeReference reference, Modality modality, String variableName) { | 29 | |
30 | private pattern directInstanceOf(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, type:Type) { | ||
31 | find interpretation(problem,interpretation); | ||
32 | LogicProblem.types(problem,type); | ||
33 | TypeDefinition.elements(type,element); | ||
34 | } or { | ||
35 | find interpretation(problem,interpretation); | ||
36 | find typeInterpretation(problem,interpretation,type,typeInterpretation); | ||
37 | PartialComplexTypeInterpretation.elements(typeInterpretation,element); | ||
38 | } | ||
39 | |||
40 | private pattern isPrimitive(element: PrimitiveElement) { | ||
41 | PrimitiveElement(element); | ||
42 | } | ||
43 | ''' | ||
44 | |||
45 | def boolean requiresTypeAnalysis() | ||
46 | |||
47 | def CharSequence generateInstanceOfQueries(LogicProblem problem, PartialInterpretation emptySolution, | ||
48 | TypeAnalysisResult typeAnalysisResult) ''' | ||
49 | «FOR type : problem.types» | ||
50 | «problem.generateMustInstenceOf(type, typeAnalysisResult)» | ||
51 | «problem.generateMayInstanceOf(type, typeAnalysisResult)» | ||
52 | «ENDFOR» | ||
53 | ''' | ||
54 | |||
55 | protected def CharSequence generateMustInstenceOf(LogicProblem problem, Type type, | ||
56 | TypeAnalysisResult typeAnalysisResult) ''' | ||
57 | /** | ||
58 | * An element must be an instance of type "«type.name»". | ||
59 | */ | ||
60 | private pattern «patternName(type,Modality.MUST)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | ||
61 | Type.name(type,"«type.name»"); | ||
62 | find directInstanceOf(problem,interpretation,element,type); | ||
63 | } | ||
64 | ''' | ||
65 | |||
66 | protected def CharSequence generateMayInstanceOf(LogicProblem problem, Type type, | ||
67 | TypeAnalysisResult typeAnalysisResult) | ||
68 | |||
69 | protected def patternName(Type type, | ||
70 | Modality modality) '''«modality.toBase»InstanceOf«base.canonizeName(type.name)»''' | ||
71 | |||
72 | def referInstanceOf(Type type, Modality modality, String variableName) { | ||
73 | '''find «patternName(type,modality)»(problem,interpretation,«variableName»);''' | ||
74 | } | ||
75 | |||
76 | def referInstanceOf(EClass type, Modality modality, String variableName) { | ||
77 | '''find «modality.toBase»InstanceOf«base.canonizeName('''«type.name» class''')»(problem,interpretation,«variableName»);''' | ||
78 | } | ||
79 | |||
80 | def dispatch CharSequence referInstanceOfByReference(ComplexTypeReference reference, Modality modality, | ||
81 | String variableName) { | ||
82 | reference.referred.referInstanceOf(modality, variableName) | ||
83 | } | ||
84 | |||
85 | def dispatch CharSequence referInstanceOfByReference(BoolTypeReference reference, Modality modality, | ||
86 | String variableName) { | ||
27 | '''BooleanElement(«variableName»);''' | 87 | '''BooleanElement(«variableName»);''' |
28 | } | 88 | } |
29 | public def dispatch CharSequence referInstanceOfByReference(IntTypeReference reference, Modality modality, String variableName) { | 89 | |
90 | def dispatch CharSequence referInstanceOfByReference(IntTypeReference reference, Modality modality, | ||
91 | String variableName) { | ||
30 | '''IntegerElement(«variableName»);''' | 92 | '''IntegerElement(«variableName»);''' |
31 | } | 93 | } |
32 | public def dispatch CharSequence referInstanceOfByReference(RealTypeReference reference, Modality modality, String variableName) { | 94 | |
95 | def dispatch CharSequence referInstanceOfByReference(RealTypeReference reference, Modality modality, | ||
96 | String variableName) { | ||
33 | '''RealElement(«variableName»);''' | 97 | '''RealElement(«variableName»);''' |
34 | } | 98 | } |
35 | public def dispatch CharSequence referInstanceOfByReference(StringTypeReference reference, Modality modality, String variableName) { | 99 | |
100 | def dispatch CharSequence referInstanceOfByReference(StringTypeReference reference, Modality modality, | ||
101 | String variableName) { | ||
36 | '''StringElement(«variableName»);''' | 102 | '''StringElement(«variableName»);''' |
37 | } | 103 | } |
38 | public def dispatch CharSequence referPrimitiveValue(String variableName, Boolean value) { | 104 | |
105 | def dispatch CharSequence referPrimitiveValue(String variableName, Boolean value) { | ||
39 | '''BooleanElement.value(«variableName»,«value»);''' | 106 | '''BooleanElement.value(«variableName»,«value»);''' |
40 | } | 107 | } |
41 | public def dispatch CharSequence referPrimitiveValue(String variableName, Integer value) { | 108 | |
109 | def dispatch CharSequence referPrimitiveValue(String variableName, Integer value) { | ||
42 | '''IntegerElement.value(«variableName»,«value»);''' | 110 | '''IntegerElement.value(«variableName»,«value»);''' |
43 | } | 111 | } |
44 | public def dispatch CharSequence referPrimitiveValue(String variableName, BigDecimal value) { | 112 | |
113 | def dispatch CharSequence referPrimitiveValue(String variableName, BigDecimal value) { | ||
45 | '''RealElement.value(«variableName»,«value»);''' | 114 | '''RealElement.value(«variableName»,«value»);''' |
46 | } | 115 | } |
47 | ///TODO: de-escaping string literals | 116 | |
48 | public def dispatch CharSequence referPrimitiveValue(String variableName, String value) { | 117 | def dispatch CharSequence referPrimitiveValue(String variableName, String value) { |
118 | // /TODO: de-escaping string literals | ||
49 | '''StringElement.value(«variableName»,"«value»");''' | 119 | '''StringElement.value(«variableName»,"«value»");''' |
50 | } | 120 | } |
51 | 121 | ||
52 | } \ No newline at end of file | 122 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend index d3af0426..0393b803 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend | |||
@@ -4,113 +4,51 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | |||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | 5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality |
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeRefinementPrecondition | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
9 | import org.eclipse.emf.ecore.EClass | ||
10 | 7 | ||
11 | class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{ | 8 | class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer { |
12 | val PatternGenerator base; | ||
13 | |||
14 | new(PatternGenerator base) { | 9 | new(PatternGenerator base) { |
15 | this.base = base | 10 | super(base) |
16 | } | 11 | } |
12 | |||
17 | override requiresTypeAnalysis() { true } | 13 | override requiresTypeAnalysis() { true } |
18 | 14 | ||
19 | override getRequiredQueries() ''' | 15 | protected override generateMayInstanceOf(LogicProblem problem, Type type, TypeAnalysisResult typeAnalysisResult) { |
20 | private pattern typeInterpretation(problem:LogicProblem, interpretation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialComplexTypeInterpretation) { | 16 | val precondition = typeAnalysisResult?.mayNewTypePreconditions?.get(type) |
21 | find interpretation(problem,interpretation); | 17 | val inhibitorTypes = precondition?.inhibitorTypes |
22 | LogicProblem.types(problem,type); | ||
23 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); | ||
24 | PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); | ||
25 | } | ||
26 | |||
27 | private pattern directInstanceOf(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, type:Type) { | ||
28 | find interpretation(problem,interpretation); | ||
29 | LogicProblem.types(problem,type); | ||
30 | TypeDefinition.elements(type,element); | ||
31 | } or { | ||
32 | find interpretation(problem,interpretation); | ||
33 | find typeInterpretation(problem,interpretation,type,typeInterpretation); | ||
34 | PartialComplexTypeInterpretation.elements(typeInterpretation,element); | ||
35 | } | ||
36 | |||
37 | private pattern isPrimitive(element: PrimitiveElement) { | ||
38 | PrimitiveElement(element); | ||
39 | } | ||
40 | ''' | ||
41 | |||
42 | override generateInstanceOfQueries(LogicProblem problem, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { | ||
43 | val mayNewTypePreconditions = typeAnalysisResult.mayNewTypePreconditions | ||
44 | |||
45 | return ''' | ||
46 | «FOR type:problem.types» | ||
47 | «problem.generateMustInstenceOf(type)» | ||
48 | «problem.generateMayInstanceOf(type,mayNewTypePreconditions.get(type))» | ||
49 | «ENDFOR» | ||
50 | ''' | ||
51 | } | ||
52 | |||
53 | private def patternName(Type type, Modality modality) | ||
54 | '''«modality.toString.toLowerCase»InstanceOf«base.canonizeName(type.name)»''' | ||
55 | |||
56 | private def generateMustInstenceOf(LogicProblem problem, Type type) { | ||
57 | ''' | ||
58 | /** | ||
59 | * An element must be an instance of type "«type.name»". | ||
60 | */ | ||
61 | private pattern «patternName(type,Modality.MUST)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | ||
62 | Type.name(type,"«type.name»"); | ||
63 | find directInstanceOf(problem,interpretation,element,type); | ||
64 | } | ||
65 | ''' | ||
66 | } | ||
67 | |||
68 | private def generateMayInstanceOf(LogicProblem problem, Type type, TypeRefinementPrecondition precondition) { | ||
69 | val inhibitorTypes = if(precondition!=null) { | ||
70 | precondition.inhibitorTypes | ||
71 | } else { | ||
72 | null | ||
73 | } | ||
74 | ''' | 18 | ''' |
75 | private pattern scopeDisallowsNew«base.canonizeName(type.name)»(problem:LogicProblem, interpretation:PartialInterpretation) { | 19 | private pattern scopeDisallowsNew«base.canonizeName(type.name)»(problem:LogicProblem, interpretation:PartialInterpretation) { |
76 | find interpretation(problem,interpretation); | 20 | find interpretation(problem,interpretation); |
77 | PartialInterpretation.scopes(interpretation,scope); | 21 | PartialInterpretation.scopes(interpretation,scope); |
78 | Scope.targetTypeInterpretation(scope,typeInterpretation); | 22 | Scope.targetTypeInterpretation(scope,typeInterpretation); |
79 | Scope.maxNewElements(scope,0); | 23 | Scope.maxNewElements(scope,0); |
80 | PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); | 24 | PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); |
81 | Type.name(type,"«type.name»"); | 25 | Type.name(type,"«type.name»"); |
82 | } | 26 | } |
83 | 27 | ||
84 | /** | 28 | /** |
85 | * An element may be an instance of type "«type.name»". | 29 | * An element may be an instance of type "«type.name»". |
86 | */ | 30 | */ |
87 | private pattern «patternName(type,Modality.MAY)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) | 31 | private pattern «patternName(type,Modality.MAY)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) |
88 | «IF inhibitorTypes !== null»{ | 32 | «IF inhibitorTypes !== null» |
89 | find interpretation(problem,interpretation); | 33 | { |
90 | PartialInterpretation.newElements(interpretation,element); | 34 | find interpretation(problem,interpretation); |
91 | «FOR inhibitorType : inhibitorTypes» | 35 | PartialInterpretation.newElements(interpretation,element); |
92 | neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» | 36 | «FOR inhibitorType : inhibitorTypes» |
93 | «ENDFOR» | 37 | neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» |
94 | neg find scopeDisallowsNew«base.canonizeName(type.name)»(problem, interpretation); | 38 | «ENDFOR» |
95 | neg find isPrimitive(element); | 39 | neg find scopeDisallowsNew«base.canonizeName(type.name)»(problem, interpretation); |
96 | } or { | 40 | neg find isPrimitive(element); |
97 | find interpretation(problem,interpretation); | 41 | } or { |
98 | PartialInterpretation.openWorldElements(interpretation,element); | 42 | find interpretation(problem,interpretation); |
99 | «FOR inhibitorType : inhibitorTypes» | 43 | PartialInterpretation.openWorldElements(interpretation,element); |
100 | neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» | 44 | «FOR inhibitorType : inhibitorTypes» |
101 | «ENDFOR» | 45 | neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» |
102 | neg find scopeDisallowsNew«base.canonizeName(type.name)»(problem, interpretation); | 46 | «ENDFOR» |
103 | neg find isPrimitive(element); | 47 | neg find scopeDisallowsNew«base.canonizeName(type.name)»(problem, interpretation); |
104 | } or | 48 | neg find isPrimitive(element); |
105 | «ENDIF» | 49 | } or |
106 | { «referInstanceOf(type,Modality.MUST,"element")» } | 50 | «ENDIF» |
51 | { «referInstanceOf(type,Modality.MUST,"element")» } | ||
107 | ''' | 52 | ''' |
108 | } | 53 | } |
109 | 54 | } | |
110 | public override referInstanceOf(Type type, Modality modality, String variableName) { | ||
111 | '''find «patternName(type,modality)»(problem,interpretation,«variableName»);''' | ||
112 | } | ||
113 | public override referInstanceOf(EClass type, Modality modality, String variableName) { | ||
114 | '''find «modality.toString.toLowerCase»InstanceOf«base.canonizeName('''«type.name» class''')»(problem,interpretation,«variableName»);''' | ||
115 | } | ||
116 | } \ No newline at end of file | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend index 286756a8..15b5a047 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend | |||
@@ -74,7 +74,7 @@ class UnfinishedIndexer { | |||
74 | «ENDIF» | 74 | «ENDIF» |
75 | 75 | ||
76 | «IF indexUpperMultiplicities» | 76 | «IF indexUpperMultiplicities» |
77 | «IF constraint.constrainsUnrepairable» | 77 | «IF constraint.constrainsUnrepairable || constraint.constrainsRemainingInverse» |
78 | private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) { | 78 | private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) { |
79 | find interpretation(problem,interpretation); | 79 | find interpretation(problem,interpretation); |
80 | find mustExist(problem,interpretation,source); | 80 | find mustExist(problem,interpretation,source); |
@@ -84,15 +84,17 @@ class UnfinishedIndexer { | |||
84 | neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)» | 84 | neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)» |
85 | «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)» | 85 | «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)» |
86 | } | 86 | } |
87 | 87 | «ENDIF» | |
88 | |||
89 | «IF constraint.constrainsUnrepairable» | ||
88 | private pattern «unrepairableMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, unrepairableMultiplicity:java Integer) { | 90 | private pattern «unrepairableMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, unrepairableMultiplicity:java Integer) { |
89 | find interpretation(problem,interpretation); | 91 | find interpretation(problem,interpretation); |
90 | find mustExist(problem,interpretation,object); | 92 | find mustExist(problem,interpretation,object); |
91 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» | 93 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» |
92 | find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, object, missingMultiplicity); | 94 | find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, object, missingMultiplicity); |
93 | numerOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _); | 95 | numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _); |
94 | check(numerOfRepairMatches < missingMultiplicity); | 96 | check(numberOfRepairMatches < missingMultiplicity); |
95 | unrepairableMultiplicity == eval(missingMultiplicity-numerOfRepairMatches); | 97 | unrepairableMultiplicity == eval(missingMultiplicity-numberOfRepairMatches); |
96 | } | 98 | } |
97 | 99 | ||
98 | private pattern «unrepairableMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, unrepairableMultiplicity:java Integer) { | 100 | private pattern «unrepairableMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, unrepairableMultiplicity:java Integer) { |
@@ -112,7 +114,8 @@ class UnfinishedIndexer { | |||
112 | «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"object")» | 114 | «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"object")» |
113 | numberOfExistingReferences == count «base.referRelation(constraint.relation,"_","object",Modality.MUST,fqn2PQuery)» | 115 | numberOfExistingReferences == count «base.referRelation(constraint.relation,"_","object",Modality.MUST,fqn2PQuery)» |
114 | check(numberOfExistingReferences < «constraint.inverseUpperBound»); | 116 | check(numberOfExistingReferences < «constraint.inverseUpperBound»); |
115 | remainingMultiplicity == eval(«constraint.inverseUpperBound»-numberOfExistingReferences); | 117 | numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, _, object); |
118 | remainingMultiplicity == eval(Math.min(«constraint.inverseUpperBound»-numberOfExistingReferences, numberOfRepairMatches)); | ||
116 | } | 119 | } |
117 | 120 | ||
118 | pattern «remainingMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { | 121 | pattern «remainingMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { |