aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns
diff options
context:
space:
mode:
authorLibravatar Kristóf Marussy <kris7topher@gmail.com>2019-07-30 18:57:01 +0200
committerLibravatar Kristóf Marussy <kris7topher@gmail.com>2019-07-30 18:57:01 +0200
commit4cb0aa5a0b9adac2bb8d4a995be015651bdd5628 (patch)
tree5c917ffa6f334e6b4c268b94fb0bd8910cf892b2 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns
parentAllow infiite upper scope bound in PolyhedronScopePropagator (diff)
downloadVIATRA-Generator-4cb0aa5a0b9adac2bb8d4a995be015651bdd5628.tar.gz
VIATRA-Generator-4cb0aa5a0b9adac2bb8d4a995be015651bdd5628.tar.zst
VIATRA-Generator-4cb0aa5a0b9adac2bb8d4a995be015651bdd5628.zip
Polyhedron scope propagator for non-containment references
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend321
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend184
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend122
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend144
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend15
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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns 1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
2 2
3import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type 3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
5import org.eclipse.emf.ecore.EClass 4import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality 5import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult 6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult
9 7
10class GenericTypeIndexer extends TypeIndexer { 8class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns 1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
2 2
3import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
5import org.eclipse.emf.ecore.EClass
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference 3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference 5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference 6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference 7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
9import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
10import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult
12import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
14import java.math.BigDecimal 13import java.math.BigDecimal
14import org.eclipse.emf.ecore.EClass
15import org.eclipse.xtend.lib.annotations.Accessors
16import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
15 17
18@FinalFieldsConstructor
16abstract class TypeIndexer { 19abstract 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
4import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem 4import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
5import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality 5import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult 6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeRefinementPrecondition
8import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
9import org.eclipse.emf.ecore.EClass
10 7
11class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{ 8class 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) {
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-18 04:42:03 +0000