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:
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.xtend186
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend158
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend146
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend6
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend102
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend126
-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/TypeRefinementGenerator.xtend83
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend6
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend231
11 files changed, 806 insertions, 703 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 2e03d6ed..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
@@ -11,110 +11,114 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par
11import java.util.HashMap 11import java.util.HashMap
12 12
13class GenericTypeRefinementGenerator extends TypeRefinementGenerator { 13class GenericTypeRefinementGenerator extends TypeRefinementGenerator {
14 public 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 private pattern hasElementInContainment(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 hasElementInContainment(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/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
index 677170b8..f3125b80 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
@@ -1,7 +1,6 @@
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.ecore2logic.ecore2logicannotations.InverseRelationAssertion 3import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion
4import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference 4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference 5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference 6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
@@ -17,7 +16,11 @@ import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Transform
17import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality 16import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
18import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult 17import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult
19import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod 18import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
19import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
20import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraints
21import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy
20import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation 22import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
23import java.util.Collection
21import java.util.HashMap 24import java.util.HashMap
22import java.util.Map 25import java.util.Map
23import org.eclipse.emf.ecore.EAttribute 26import org.eclipse.emf.ecore.EAttribute
@@ -36,21 +39,23 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
36} 39}
37 40
38class PatternGenerator { 41class PatternGenerator {
39 @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer //= new TypeIndexer(this) 42 @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this)
40 @Accessors(PUBLIC_GETTER) val RelationDeclarationIndexer relationDeclarationIndexer = new RelationDeclarationIndexer(this) 43 @Accessors(PUBLIC_GETTER) val RelationDeclarationIndexer relationDeclarationIndexer = new RelationDeclarationIndexer(
41 @Accessors(PUBLIC_GETTER) val RelationDefinitionIndexer relationDefinitionIndexer = new RelationDefinitionIndexer(this) 44 this)
45 @Accessors(PUBLIC_GETTER) val RelationDefinitionIndexer relationDefinitionIndexer = new RelationDefinitionIndexer(
46 this)
42 @Accessors(PUBLIC_GETTER) val ContainmentIndexer containmentIndexer = new ContainmentIndexer(this) 47 @Accessors(PUBLIC_GETTER) val ContainmentIndexer containmentIndexer = new ContainmentIndexer(this)
43 @Accessors(PUBLIC_GETTER) val InvalidIndexer invalidIndexer = new InvalidIndexer(this) 48 @Accessors(PUBLIC_GETTER) val InvalidIndexer invalidIndexer = new InvalidIndexer(this)
44 @Accessors(PUBLIC_GETTER) val UnfinishedIndexer unfinishedIndexer = new UnfinishedIndexer(this) 49 @Accessors(PUBLIC_GETTER) val UnfinishedIndexer unfinishedIndexer
45 @Accessors(PUBLIC_GETTER) val TypeRefinementGenerator typeRefinementGenerator //= new RefinementGenerator(this) 50 @Accessors(PUBLIC_GETTER) val TypeRefinementGenerator typeRefinementGenerator //= new RefinementGenerator(this)
46 @Accessors(PUBLIC_GETTER) val RelationRefinementGenerator relationRefinementGenerator = new RelationRefinementGenerator(this) 51 @Accessors(PUBLIC_GETTER) val RelationRefinementGenerator relationRefinementGenerator = new RelationRefinementGenerator(this)
47 @Accessors(PUBLIC_GETTER) val UnitPropagationPreconditionGenerator unitPropagationPreconditionGenerator = new UnitPropagationPreconditionGenerator(this) 52 @Accessors(PUBLIC_GETTER) val UnitPropagationPreconditionGenerator unitPropagationPreconditionGenerator = new UnitPropagationPreconditionGenerator(this)
48 53
49 public new(TypeInferenceMethod typeInferenceMethod) { 54 public new(TypeInferenceMethod typeInferenceMethod, ScopePropagatorStrategy scopePropagatorStrategy) {
50 if(typeInferenceMethod == TypeInferenceMethod.Generic) { 55 if(typeInferenceMethod == TypeInferenceMethod.Generic) {
51 this.typeIndexer = new GenericTypeIndexer(this) 56 this.typeIndexer = new GenericTypeIndexer(this)
52 this.typeRefinementGenerator = new GenericTypeRefinementGenerator(this) 57 this.typeRefinementGenerator = new GenericTypeRefinementGenerator(this)
53 } else if(typeInferenceMethod == TypeInferenceMethod.PreliminaryAnalysis) { 58 } else if (typeInferenceMethod == TypeInferenceMethod.PreliminaryAnalysis) {
54 this.typeIndexer = new TypeIndexerWithPreliminaryTypeAnalysis(this) 59 this.typeIndexer = new TypeIndexerWithPreliminaryTypeAnalysis(this)
55 this.typeRefinementGenerator = new TypeRefinementWithPreliminaryTypeAnalysis(this) 60 this.typeRefinementGenerator = new TypeRefinementWithPreliminaryTypeAnalysis(this)
56 } else { 61 } else {
@@ -58,110 +63,101 @@ class PatternGenerator {
58 this.typeRefinementGenerator = null 63 this.typeRefinementGenerator = null
59 throw new IllegalArgumentException('''Unknown type indexing technique : «typeInferenceMethod.name»''') 64 throw new IllegalArgumentException('''Unknown type indexing technique : «typeInferenceMethod.name»''')
60 } 65 }
66 this.unfinishedIndexer = new UnfinishedIndexer(this, scopePropagatorStrategy.requiresUpperBoundIndexing)
61 } 67 }
62 68
63 public def requiresTypeAnalysis() { 69 def requiresTypeAnalysis() {
64 typeIndexer.requiresTypeAnalysis || typeRefinementGenerator.requiresTypeAnalysis 70 typeIndexer.requiresTypeAnalysis || typeRefinementGenerator.requiresTypeAnalysis
65 } 71 }
66 72
67 public dispatch def referRelation( 73 dispatch def CharSequence referRelation(RelationDeclaration referred, String sourceVariable, String targetVariable,
68 RelationDeclaration referred, 74 Modality modality, Map<String, PQuery> fqn2PQuery) {
69 String sourceVariable, 75 return this.relationDeclarationIndexer.referRelation(referred, sourceVariable, targetVariable, modality)
70 String targetVariable,
71 Modality modality,
72 Map<String,PQuery> fqn2PQuery)
73 {
74 return this.relationDeclarationIndexer.referRelation(referred,sourceVariable,targetVariable,modality)
75 } 76 }
76 public dispatch def referRelation( 77
77 RelationDefinition referred, 78 dispatch def CharSequence referRelation(RelationDefinition referred, String sourceVariable, String targetVariable,
78 String sourceVariable, 79 Modality modality, Map<String, PQuery> fqn2PQuery) {
79 String targetVariable, 80 val pattern = referred.annotations.filter(TransfomedViatraQuery).head.patternFullyQualifiedName.lookup(
80 Modality modality, 81 fqn2PQuery)
81 Map<String,PQuery> fqn2PQuery) 82 return this.relationDefinitionIndexer.referPattern(pattern, #[sourceVariable, targetVariable], modality, true,
82 { 83 false)
83 val pattern = referred.annotations.filter(TransfomedViatraQuery).head.patternFullyQualifiedName.lookup(fqn2PQuery)
84 return this.relationDefinitionIndexer.referPattern(pattern,#[sourceVariable,targetVariable],modality,true,false)
85 } 84 }
86 85
87 def public referRelationByName(EReference reference, 86 def referRelationByName(EReference reference, String sourceVariable, String targetVariable, Modality modality) {
88 String sourceVariable, 87 '''find «modality.name.toLowerCase»InRelation«canonizeName('''«reference.name» reference «reference.EContainingClass.name»''')»(problem,interpretation,«sourceVariable»,«targetVariable»);'''
89 String targetVariable,
90 Modality modality)
91 {
92 '''find «modality.name.toLowerCase»InRelation«canonizeName('''«reference.name» reference «reference.EContainingClass.name»''')
93 »(problem,interpretation,«sourceVariable»,«targetVariable»);'''
94 } 88 }
95 89
96 def public CharSequence referAttributeByName(EAttribute attribute, 90 def CharSequence referAttributeByName(EAttribute attribute, String sourceVariable, String targetVariable,
97 String sourceVariable, 91 Modality modality) {
98 String targetVariable, 92 '''find «modality.name.toLowerCase»InRelation«canonizeName('''«attribute.name» attribute «attribute.EContainingClass.name»''')»(problem,interpretation,«sourceVariable»,«targetVariable»);'''
99 Modality modality)
100 {
101 '''find «modality.name.toLowerCase»InRelation«canonizeName('''«attribute.name» attribute «attribute.EContainingClass.name»''')
102 »(problem,interpretation,«sourceVariable»,«targetVariable»);'''
103 } 93 }
104 94
105 public def canonizeName(String name) { 95 def canonizeName(String name) {
106 name.split(' ').join('_') 96 name.split(' ').join('_')
107 } 97 }
108 98
109 public def lowerMultiplicities(LogicProblem problem) { 99 def wfQueries(LogicProblem problem) {
110 problem.assertions.map[annotations].flatten.filter(LowerMultiplicityAssertion).filter[!it.relation.isDerived] 100 problem.assertions.map[it.annotations].flatten.filter(TransformedViatraWellformednessConstraint).map[it.query]
111 }
112 public def wfQueries(LogicProblem problem) {
113 problem.assertions.map[it.annotations]
114 .flatten
115 .filter(TransformedViatraWellformednessConstraint)
116 .map[it.query]
117 } 101 }
118 public def getContainments(LogicProblem p) { 102
103 def getContainments(LogicProblem p) {
119 return p.containmentHierarchies.head.containmentRelations 104 return p.containmentHierarchies.head.containmentRelations
120 } 105 }
121 public def getInverseRelations(LogicProblem p) { 106
107 def getInverseRelations(LogicProblem p) {
122 val inverseRelations = new HashMap 108 val inverseRelations = new HashMap
123 p.annotations.filter(InverseRelationAssertion).forEach[ 109 p.annotations.filter(InverseRelationAssertion).forEach [
124 inverseRelations.put(it.inverseA,it.inverseB) 110 inverseRelations.put(it.inverseA, it.inverseB)
125 inverseRelations.put(it.inverseB,it.inverseA) 111 inverseRelations.put(it.inverseB, it.inverseA)
126 ] 112 ]
127 return inverseRelations 113 return inverseRelations
128 } 114 }
129 public def isRepresentative(Relation relation, Relation inverse) { 115
130 if(inverse == null) { 116 def isRepresentative(Relation relation, Relation inverse) {
117 if (relation === null) {
118 return false
119 } else if (inverse === null) {
131 return true 120 return true
132 } else { 121 } else {
133 relation.name.compareTo(inverse.name)<1 122 relation.name.compareTo(inverse.name) < 1
134 } 123 }
135 } 124 }
136 125
137 public def isDerived(Relation relation) { 126 def isDerived(Relation relation) {
138 relation.annotations.exists[it instanceof DefinedByDerivedFeature] 127 relation.annotations.exists[it instanceof DefinedByDerivedFeature]
139 } 128 }
140 public def getDerivedDefinition(RelationDeclaration relation) { 129
130 def getDerivedDefinition(RelationDeclaration relation) {
141 relation.annotations.filter(DefinedByDerivedFeature).head.query 131 relation.annotations.filter(DefinedByDerivedFeature).head.query
142 } 132 }
143 133
144 private def allTypeReferences(LogicProblem problem) { 134 private def allTypeReferences(LogicProblem problem) {
145 problem.eAllContents.filter(TypeReference).toIterable 135 problem.eAllContents.filter(TypeReference).toIterable
146 } 136 }
137
147 protected def hasBoolean(LogicProblem problem) { 138 protected def hasBoolean(LogicProblem problem) {
148 problem.allTypeReferences.exists[it instanceof BoolTypeReference] 139 problem.allTypeReferences.exists[it instanceof BoolTypeReference]
149 } 140 }
141
150 protected def hasInteger(LogicProblem problem) { 142 protected def hasInteger(LogicProblem problem) {
151 problem.allTypeReferences.exists[it instanceof IntTypeReference] 143 problem.allTypeReferences.exists[it instanceof IntTypeReference]
152 } 144 }
145
153 protected def hasReal(LogicProblem problem) { 146 protected def hasReal(LogicProblem problem) {
154 problem.allTypeReferences.exists[it instanceof RealTypeReference] 147 problem.allTypeReferences.exists[it instanceof RealTypeReference]
155 } 148 }
149
156 protected def hasString(LogicProblem problem) { 150 protected def hasString(LogicProblem problem) {
157 problem.allTypeReferences.exists[it instanceof StringTypeReference] 151 problem.allTypeReferences.exists[it instanceof StringTypeReference]
158 } 152 }
159 153
160 public def PatternGeneratorResult transformBaseProperties( 154 def transformBaseProperties(
161 LogicProblem problem, 155 LogicProblem problem,
162 PartialInterpretation emptySolution, 156 PartialInterpretation emptySolution,
163 Map<String,PQuery> fqn2PQuery, 157 Map<String, PQuery> fqn2PQuery,
164 TypeAnalysisResult typeAnalysisResult 158 TypeAnalysisResult typeAnalysisResult,
159 RelationConstraints constraints,
160 Collection<LinearTypeConstraintHint> hints
165 ) { 161 ) {
166 val first = 162 val first =
167 ''' 163 '''
@@ -199,7 +195,7 @@ class PatternGenerator {
199 195
200 private pattern elementCloseWorld(element:DefinedElement) { 196 private pattern elementCloseWorld(element:DefinedElement) {
201 PartialInterpretation.openWorldElements(i,element); 197 PartialInterpretation.openWorldElements(i,element);
202 PartialInterpretation.maxNewElements(i,0); 198 PartialInterpretation.maxNewElements(i,0);
203 } or { 199 } or {
204 Scope.targetTypeInterpretation(scope,interpretation); 200 Scope.targetTypeInterpretation(scope,interpretation);
205 PartialTypeInterpratation.elements(interpretation,element); 201 PartialTypeInterpratation.elements(interpretation,element);
@@ -288,7 +284,9 @@ class PatternGenerator {
288 ////////// 284 //////////
289 // 1.1.1 Required Patterns by TypeIndexer 285 // 1.1.1 Required Patterns by TypeIndexer
290 ////////// 286 //////////
287
291 «typeIndexer.requiredQueries» 288 «typeIndexer.requiredQueries»
289
292 ////////// 290 //////////
293 // 1.1.2 primitive Type Indexers 291 // 1.1.2 primitive Type Indexers
294 ////////// 292 //////////
@@ -306,6 +304,7 @@ class PatternGenerator {
306 // > StringElement.value(variableName,value) 304 // > StringElement.value(variableName,value)
307 // Whether a value is set is defined by: 305 // Whether a value is set is defined by:
308 // > PrimitiveElement.valueSet(variableName,isFilled); 306 // > PrimitiveElement.valueSet(variableName,isFilled);
307
309 ////////// 308 //////////
310 // 1.1.3 domain-specific Type Indexers 309 // 1.1.3 domain-specific Type Indexers
311 ////////// 310 //////////
@@ -338,7 +337,7 @@ class PatternGenerator {
338 ////////// 337 //////////
339 // 3.1 Unfinishedness Measured by Multiplicity 338 // 3.1 Unfinishedness Measured by Multiplicity
340 ////////// 339 //////////
341 «unfinishedIndexer.generateUnfinishedMultiplicityQueries(problem,fqn2PQuery)» 340 «unfinishedIndexer.generateUnfinishedMultiplicityQueries(constraints.multiplicityConstraints,fqn2PQuery)»
342 341
343 ////////// 342 //////////
344 // 3.2 Unfinishedness Measured by WF Queries 343 // 3.2 Unfinishedness Measured by WF Queries
@@ -363,11 +362,18 @@ class PatternGenerator {
363 «relationRefinementGenerator.generateRefineReference(problem)» 362 «relationRefinementGenerator.generateRefineReference(problem)»
364 363
365 ////////// 364 //////////
366 // 5 Unit Propagations 365 // 5 Hints
366 //////////
367 «FOR hint : hints»
368 «hint.getAdditionalPatterns(this)»
369 «ENDFOR»
370
371 //////////
372 // 6 Unit Propagations
367 ////////// 373 //////////
368 ''' 374 '''
369 val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery) 375 val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery)
370 val second = up.definitions 376 val second = up.definitions
371 return new PatternGeneratorResult(first+second,up.constraint2MustPreconditionName,up.constraint2CurrentPreconditionName) 377 return new PatternGeneratorResult(first+second,up.constraint2MustPreconditionName,up.constraint2CurrentPreconditionName)
372 } 378 }
373} 379}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
index f3de4ccc..ac4a0855 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
@@ -2,78 +2,95 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
2 2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation 3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration 4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type 6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
6import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem 7import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics 9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysis 10import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysis
9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult 11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult
10import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod 12import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
13import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
14import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraints
15import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationMultiplicityConstraint
16import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy
11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util.ParseUtil 17import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util.ParseUtil
12import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation 18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
13import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace 19import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
20import java.util.Collection
21import java.util.HashMap
14import java.util.Map 22import java.util.Map
23import java.util.Set
15import org.eclipse.viatra.query.runtime.api.IPatternMatch 24import org.eclipse.viatra.query.runtime.api.IPatternMatch
16import org.eclipse.viatra.query.runtime.api.IQuerySpecification 25import org.eclipse.viatra.query.runtime.api.IQuerySpecification
17import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher 26import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
27import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
18import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery 28import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
19import org.eclipse.xtend.lib.annotations.Data 29import org.eclipse.xtend.lib.annotations.Data
20 30
21import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 31import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
22import java.util.Collection
23import java.util.Set
24import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
25import java.util.HashMap
26 32
27@Data class GeneratedPatterns { 33@Data class GeneratedPatterns {
28 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries 34 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries
29 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries 35 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries
30 public Map<Relation, Pair<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>,Integer>> unfinishedContainmentMulticiplicityQueries 36 public Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> multiplicityConstraintQueries
31 public Map<Relation, Pair<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>,Integer>> unfinishedNonContainmentMulticiplicityQueries 37 public IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery
32 public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries 38 public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries
33 public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries 39 public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries
34 public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries 40 public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries
35 public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns 41 public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns
36 public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns 42 public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns
43 public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries
37 public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries 44 public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries
38} 45}
39 46
47@Data
48class ModalPatternQueries {
49 val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mayQuery
50 val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mustQuery
51 val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> currentQuery
52}
53
54@Data
55class UnifinishedMultiplicityQueries {
56 val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> unfinishedMultiplicityQuery
57 val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> unrepairableMultiplicityQuery
58 val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> remainingInverseMultiplicityQuery
59 val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> remainingContentsQuery
60}
61
40class PatternProvider { 62class PatternProvider {
41 63
42 val TypeAnalysis typeAnalysis = new TypeAnalysis 64 val TypeAnalysis typeAnalysis = new TypeAnalysis
43 65
44 public def generateQueries( 66 def generateQueries(LogicProblem problem, PartialInterpretation emptySolution, ModelGenerationStatistics statistics,
45 LogicProblem problem, 67 Set<PQuery> existingQueries, ReasonerWorkspace workspace, TypeInferenceMethod typeInferenceMethod,
46 PartialInterpretation emptySolution, 68 ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints,
47 ModelGenerationStatistics statistics, 69 Collection<LinearTypeConstraintHint> hints, boolean writeToFile) {
48 Set<PQuery> existingQueries,
49 ReasonerWorkspace workspace,
50 TypeInferenceMethod typeInferenceMethod,
51 boolean writeToFile)
52 {
53 val fqn2Query = existingQueries.toMap[it.fullyQualifiedName] 70 val fqn2Query = existingQueries.toMap[it.fullyQualifiedName]
54 val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod) 71 val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod, scopePropagatorStrategy)
55 val typeAnalysisResult = if(patternGenerator.requiresTypeAnalysis) { 72 val typeAnalysisResult = if (patternGenerator.requiresTypeAnalysis) {
56 val startTime = System.nanoTime 73 val startTime = System.nanoTime
57 val result = typeAnalysis.performTypeAnalysis(problem,emptySolution) 74 val result = typeAnalysis.performTypeAnalysis(problem, emptySolution)
58 val typeAnalysisTime = System.nanoTime - startTime 75 val typeAnalysisTime = System.nanoTime - startTime
59 statistics.PreliminaryTypeAnalisisTime = typeAnalysisTime 76 statistics.preliminaryTypeAnalisisTime = typeAnalysisTime
60 result 77 result
61 } else { 78 } else {
62 null 79 null
63 } 80 }
64 val patternGeneratorResult = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) 81 val patternGeneratorResult = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query,
65 val baseIndexerFile = patternGeneratorResult.patternText 82 typeAnalysisResult, relationConstraints, hints)
66 val mustUnitPropagationTrace = patternGeneratorResult.constraint2MustPreconditionName 83 if (writeToFile) {
67 val currentUnitPropagationTrace = patternGeneratorResult.constraint2CurrentPreconditionName 84 workspace.writeText('''generated3valued.vql_deactivated''', patternGeneratorResult.patternText)
68 if(writeToFile) {
69 workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile)
70 } 85 }
71 val ParseUtil parseUtil = new ParseUtil 86 val ParseUtil parseUtil = new ParseUtil
72 val generatedQueries = parseUtil.parse(baseIndexerFile) 87 val generatedQueries = parseUtil.parse(patternGeneratorResult.patternText)
73 val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,mustUnitPropagationTrace,currentUnitPropagationTrace,generatedQueries); 88 val runtimeQueries = calclulateRuntimeQueries(patternGenerator, problem, emptySolution, typeAnalysisResult,
89 patternGeneratorResult.constraint2MustPreconditionName, patternGeneratorResult.constraint2CurrentPreconditionName,
90 relationConstraints, generatedQueries)
74 return runtimeQueries 91 return runtimeQueries
75 } 92 }
76 93
77 private def GeneratedPatterns calclulateRuntimeQueries( 94 private def GeneratedPatterns calclulateRuntimeQueries(
78 PatternGenerator patternGenerator, 95 PatternGenerator patternGenerator,
79 LogicProblem problem, 96 LogicProblem problem,
@@ -81,31 +98,23 @@ class PatternProvider {
81 TypeAnalysisResult typeAnalysisResult, 98 TypeAnalysisResult typeAnalysisResult,
82 HashMap<PConstraint, String> mustUnitPropagationTrace, 99 HashMap<PConstraint, String> mustUnitPropagationTrace,
83 HashMap<PConstraint, String> currentUnitPropagationTrace, 100 HashMap<PConstraint, String> currentUnitPropagationTrace,
101 RelationConstraints relationConstraints,
84 Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries 102 Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries
85 ) { 103 ) {
86 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 104 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
87 invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] 105 invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)]
88 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 106 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
89 unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)] 107 unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)]
90 108
91 val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(problem) 109 val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(relationConstraints.multiplicityConstraints)
92 val unfinishedContainmentMultiplicities = new HashMap 110 val multiplicityConstraintQueries = unfinishedMultiplicities.mapValues [
93 val unfinishedNonContainmentMultiplicities = new HashMap 111 new UnifinishedMultiplicityQueries(unfinishedMultiplicityQueryName?.lookup(queries),
94 for(entry : unfinishedMultiplicities.entrySet) { 112 unrepairableMultiplicityQueryName?.lookup(queries),
95 val relation = entry.key 113 remainingInverseMultiplicityQueryName?.lookup(queries), remainingContentsQueryName?.lookup(queries))
96 val name = entry.value.key 114 ]
97 val amount = entry.value.value 115 val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup(
98 val query = name.lookup(queries) 116 queries)
99 if(problem.containmentHierarchies.head.containmentRelations.contains(relation)) { 117
100 unfinishedContainmentMultiplicities.put(relation,query->amount)
101 } else {
102 unfinishedNonContainmentMultiplicities.put(relation,query->amount)
103 }
104 }
105// val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
106// unfinishedMultiplicityQueries = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(problem).mapValues[it.lookup(queries)]
107//
108
109 val Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 118 val Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
110 refineObjectsQueries = patternGenerator.typeRefinementGenerator.getRefineObjectQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] 119 refineObjectsQueries = patternGenerator.typeRefinementGenerator.getRefineObjectQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)]
111 val Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 120 val Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
@@ -116,16 +125,27 @@ class PatternProvider {
116 mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.mapValues[it.lookup(queries)] 125 mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.mapValues[it.lookup(queries)]
117 val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 126 val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
118 currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.mapValues[it.lookup(queries)] 127 currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.mapValues[it.lookup(queries)]
128
129 val modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition |
130 val indexer = patternGenerator.relationDefinitionIndexer
131 new ModalPatternQueries(
132 indexer.relationDefinitionName(relationDefinition, Modality.MAY).lookup(queries),
133 indexer.relationDefinitionName(relationDefinition, Modality.MUST).lookup(queries),
134 indexer.relationDefinitionName(relationDefinition, Modality.CURRENT).lookup(queries)
135 )
136 ])
137
119 return new GeneratedPatterns( 138 return new GeneratedPatterns(
120 invalidWFQueries, 139 invalidWFQueries,
121 unfinishedWFQueries, 140 unfinishedWFQueries,
122 unfinishedContainmentMultiplicities, 141 multiplicityConstraintQueries,
123 unfinishedNonContainmentMultiplicities, 142 hasElementInContainmentQuery,
124 refineObjectsQueries, 143 refineObjectsQueries,
125 refineTypeQueries, 144 refineTypeQueries,
126 refineRelationQueries, 145 refineRelationQueries,
127 mustUnitPropagationPreconditionPatterns, 146 mustUnitPropagationPreconditionPatterns,
128 currentUnitPropagationPreconditionPatterns, 147 currentUnitPropagationPreconditionPatterns,
148 modalRelationQueries,
129 queries.values 149 queries.values
130 ) 150 )
131 } 151 }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend
index 37950834..338a9af2 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend
@@ -7,10 +7,10 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
7import java.util.Map 7import java.util.Map
8import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable 8import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
9import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure 9import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure
10import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction
10import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery 11import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
11 12
12import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 13import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
13import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction
14 14
15class RelationDefinitionIndexer { 15class RelationDefinitionIndexer {
16 public val PatternGenerator base; 16 public val PatternGenerator base;
@@ -60,7 +60,7 @@ class RelationDefinitionIndexer {
60 ] 60 ]
61 } 61 }
62 62
63 private def relationDefinitionName(RelationDefinition relation, Modality modality) 63 def String relationDefinitionName(RelationDefinition relation, Modality modality)
64 '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»''' 64 '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»'''
65 65
66 def canonizeName(PVariable v) { 66 def canonizeName(PVariable v) {
@@ -102,6 +102,4 @@ class RelationDefinitionIndexer {
102 def referPattern(PQuery p, String[] variables, Modality modality, boolean positive, boolean transitive) ''' 102 def referPattern(PQuery p, String[] variables, Modality modality, boolean positive, boolean transitive) '''
103 «IF !positive»neg «ENDIF»find «IF transitive»twoParam_«ENDIF»«modality.name.toLowerCase»InRelation_pattern_«p.fullyQualifiedName.replace('.','_')»«IF transitive»+«ENDIF»(«IF !transitive»problem,interpretation,«ENDIF»«variables.join(',')»); 103 «IF !positive»neg «ENDIF»find «IF transitive»twoParam_«ENDIF»«modality.name.toLowerCase»InRelation_pattern_«p.fullyQualifiedName.replace('.','_')»«IF transitive»+«ENDIF»(«IF !transitive»problem,interpretation,«ENDIF»«variables.join(',')»);
104 ''' 104 '''
105
106
107} \ No newline at end of file 105} \ 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/RelationRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend
index f9e9baea..d915d47e 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend
@@ -9,77 +9,71 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
9 9
10class RelationRefinementGenerator { 10class RelationRefinementGenerator {
11 PatternGenerator base; 11 PatternGenerator base;
12
12 public new(PatternGenerator base) { 13 public new(PatternGenerator base) {
13 this.base = base 14 this.base = base
14 } 15 }
15 16
16 def CharSequence generateRefineReference(LogicProblem p) { 17 def CharSequence generateRefineReference(LogicProblem p) '''
17 return ''' 18 «FOR relationRefinement : this.getRelationRefinements(p)»
18 «FOR relationRefinement: this.getRelationRefinements(p)» 19 pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»(
19 pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»( 20 problem:LogicProblem, interpretation:PartialInterpretation,
20 problem:LogicProblem, interpretation:PartialInterpretation, 21 relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF»,
21 relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value != null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», 22 from: DefinedElement, to: DefinedElement)
22 from: DefinedElement, to: DefinedElement) 23 {
23 { 24 find interpretation(problem,interpretation);
24 find interpretation(problem,interpretation); 25 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
25 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); 26 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»");
26 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»"); 27 «IF relationRefinement.value !== null»
27 «IF relationRefinement.value != null» 28 PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation);
28 PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation); 29 PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»");
29 PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»"); 30 «ENDIF»
30 «ENDIF» 31 find mustExist(problem, interpretation, from);
31 find mustExist(problem, interpretation, from); 32 find mustExist(problem, interpretation, to);
32 find mustExist(problem, interpretation, to); 33 «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")»
33 «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")» 34 «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")»
34 «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")» 35 «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)»
35 «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)» 36 neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)»
36 neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)» 37 }
37 }
38 «ENDFOR» 38 «ENDFOR»
39 ''' 39 '''
40 } 40
41
42 def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) { 41 def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) {
43 '''«IF inverseRelation != null 42 '''«IF inverseRelation !== null»refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelation.name)»«ELSE»refineRelation_«base.canonizeName(relation.name)»«ENDIF»'''
44 »refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelation.name)»«
45 ELSE
46 »refineRelation_«base.canonizeName(relation.name)»«ENDIF»'''
47 } 43 }
48 44
49 def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName, 45 def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName,
50 String inverseInterpretationName, String sourceName, String targetName) 46 String inverseInterpretationName, String sourceName,
51 '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation != null»inverseInterpretationName, «ENDIF»«sourceName», «targetName»);''' 47 String targetName) '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation !== null»«inverseInterpretationName», «ENDIF»«sourceName», «targetName»);'''
52 48
53 def getRefineRelationQueries(LogicProblem p) { 49 def getRefineRelationQueries(LogicProblem p) {
54// val containmentRelations = p.containmentHierarchies.map[containmentRelations].flatten.toSet 50// val containmentRelations = p.containmentHierarchies.map[containmentRelations].flatten.toSet
55// p.relations.filter(RelationDeclaration).filter[!containmentRelations.contains(it)].toInvertedMap['''refineRelation_«base.canonizeName(it.name)»'''] 51// p.relations.filter(RelationDeclaration).filter[!containmentRelations.contains(it)].toInvertedMap['''refineRelation_«base.canonizeName(it.name)»''']
56 /* 52 /*
57 val res = new LinkedHashMap 53 * val res = new LinkedHashMap
58 for(relation: getRelationRefinements(p)) { 54 * for(relation: getRelationRefinements(p)) {
59 if(inverseRelations.containsKey(relation)) { 55 * if(inverseRelations.containsKey(relation)) {
60 val name = '''refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelations.get(relation).name)»''' 56 * val name = '''refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelations.get(relation).name)»'''
61 res.put(relation -> inverseRelations.get(relation),name) 57 * res.put(relation -> inverseRelations.get(relation),name)
62 } else { 58 * } else {
63 val name = '''refineRelation_«base.canonizeName(relation.name)»''' 59 * val name = '''refineRelation_«base.canonizeName(relation.name)»'''
64 res.put(relation -> null,name) 60 * res.put(relation -> null,name)
65 } 61 * }
66 } 62 * }
67 return res*/ 63 return res*/
68 64 getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key, it.value)]
69 getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key,it.value)]
70 } 65 }
71
72 66
73 def getRelationRefinements(LogicProblem p) { 67 def getRelationRefinements(LogicProblem p) {
74 val inverses = base.getInverseRelations(p) 68 val inverses = base.getInverseRelations(p)
75 val containments = base.getContainments(p) 69 val containments = base.getContainments(p)
76 val list = new LinkedList 70 val list = new LinkedList
77 for(relation : p.relations.filter(RelationDeclaration)) { 71 for (relation : p.relations.filter(RelationDeclaration)) {
78 if(!containments.contains(relation)) { 72 if (!containments.contains(relation)) {
79 if(inverses.containsKey(relation)) { 73 if (inverses.containsKey(relation)) {
80 val inverse = inverses.get(relation) 74 val inverse = inverses.get(relation)
81 if(!containments.contains(inverse)) { 75 if (!containments.contains(inverse)) {
82 if(base.isRepresentative(relation,inverse)) { 76 if (base.isRepresentative(relation, inverse)) {
83 list += (relation -> inverse) 77 list += (relation -> inverse)
84 } 78 }
85 } 79 }
@@ -90,4 +84,4 @@ class RelationRefinementGenerator {
90 } 84 }
91 return list 85 return list
92 } 86 }
93} \ No newline at end of file 87}
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 41eb75a8..e4e2aa30 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,54 +1,126 @@
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 public def CharSequence referPrimitiveFilled(String variableName, boolean isFilled) { 121
122 def CharSequence referPrimitiveFilled(String variableName, boolean isFilled) {
52 '''PrimitiveElement.valueSet(«variableName»,«isFilled»);''' 123 '''PrimitiveElement.valueSet(«variableName»,«isFilled»);'''
53 } 124 }
54} \ No newline at end of file 125}
126
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/TypeRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend
index 7e3fad91..4ef336ae 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend
@@ -25,69 +25,76 @@ class ObjectCreationPrecondition {
25 25
26abstract class TypeRefinementGenerator { 26abstract class TypeRefinementGenerator {
27 val protected PatternGenerator base; 27 val protected PatternGenerator base;
28 public new(PatternGenerator base) { 28
29 new(PatternGenerator base) {
29 this.base = base 30 this.base = base
30 } 31 }
31 32
32 public def boolean requiresTypeAnalysis() 33 def boolean requiresTypeAnalysis()
33 public def CharSequence generateRefineObjectQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) 34
34 public def CharSequence generateRefineTypeQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) 35 def CharSequence generateRefineObjectQueries(LogicProblem p, PartialInterpretation emptySolution,
35 public def Map<? extends Type, String> getRefineTypeQueryNames(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) 36 TypeAnalysisResult typeAnalysisResult)
36 37
37 public def getRefineObjectQueryNames(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { 38 def CharSequence generateRefineTypeQueries(LogicProblem p, PartialInterpretation emptySolution,
38 val Map<ObjectCreationPrecondition,String> objectCreationQueries = new LinkedHashMap 39 TypeAnalysisResult typeAnalysisResult)
40
41 def Map<? extends Type, String> getRefineTypeQueryNames(LogicProblem p, PartialInterpretation emptySolution,
42 TypeAnalysisResult typeAnalysisResult)
43
44 def getRefineObjectQueryNames(LogicProblem p, PartialInterpretation emptySolution,
45 TypeAnalysisResult typeAnalysisResult) {
46 val Map<ObjectCreationPrecondition, String> objectCreationQueries = new LinkedHashMap
39 val containment = p.containmentHierarchies.head 47 val containment = p.containmentHierarchies.head
40 val inverseRelations = new HashMap 48 val inverseRelations = new HashMap
41 p.annotations.filter(InverseRelationAssertion).forEach[ 49 p.annotations.filter(InverseRelationAssertion).forEach [
42 inverseRelations.put(it.inverseA,it.inverseB) 50 inverseRelations.put(it.inverseA, it.inverseB)
43 inverseRelations.put(it.inverseB,it.inverseA) 51 inverseRelations.put(it.inverseB, it.inverseA)
44 ] 52 ]
45 for(type: p.types.filter(TypeDeclaration).filter[!it.isAbstract]) { 53 for (type : p.types.filter(TypeDeclaration).filter[!it.isAbstract]) {
46 if(containment.typeInContainment(type)) { 54 if (containment.typeInContainment(type)) {
47 for(containmentRelation : containment.containmentRelations.filter[canBeContainedByRelation(it,type)]) { 55 for (containmentRelation : containment.containmentRelations.
48 if(inverseRelations.containsKey(containmentRelation)) { 56 filter[canBeContainedByRelation(it, type)]) {
57 if (inverseRelations.containsKey(containmentRelation)) {
49 objectCreationQueries.put( 58 objectCreationQueries.put(
50 new ObjectCreationPrecondition(containmentRelation,inverseRelations.get(containmentRelation),type), 59 new ObjectCreationPrecondition(containmentRelation,
51 this.patternName(containmentRelation,inverseRelations.get(containmentRelation),type)) 60 inverseRelations.get(containmentRelation), type),
61 this.patternName(containmentRelation, inverseRelations.get(containmentRelation), type))
52 } else { 62 } else {
53 objectCreationQueries.put( 63 objectCreationQueries.put(new ObjectCreationPrecondition(containmentRelation, null, type),
54 new ObjectCreationPrecondition(containmentRelation,null,type), 64 patternName(containmentRelation, null, type))
55 patternName(containmentRelation,null,type))
56 } 65 }
57 } 66 }
58 objectCreationQueries.put( 67 objectCreationQueries.put(new ObjectCreationPrecondition(null, null, type),
59 new ObjectCreationPrecondition(null,null,type), 68 patternName(null, null, type))
60 patternName(null,null,type))
61 } else { 69 } else {
62 objectCreationQueries.put( 70 objectCreationQueries.put(new ObjectCreationPrecondition(null, null, type),
63 new ObjectCreationPrecondition(null,null,type), 71 this.patternName(null, null, type))
64 this.patternName(null,null,type))
65 } 72 }
66 } 73 }
67 return objectCreationQueries 74 return objectCreationQueries
68 } 75 }
69 76
70 protected def canBeContainedByRelation(Relation r, Type t) { 77 protected def canBeContainedByRelation(Relation r, Type t) {
71 if(r.parameters.size==2) { 78 if (r.parameters.size == 2) {
72 val param = r.parameters.get(1) 79 val param = r.parameters.get(1)
73 if(param instanceof ComplexTypeReference) { 80 if (param instanceof ComplexTypeReference) {
74 val allSuperTypes = t.transitiveClosureStar[it.supertypes] 81 val allSuperTypes = t.transitiveClosureStar[it.supertypes]
75 for(superType : allSuperTypes) { 82 for (superType : allSuperTypes) {
76 if(param.referred == superType) return true 83 if(param.referred == superType) return true
77 } 84 }
78 } 85 }
79 } 86 }
80 return false 87 return false
81 } 88 }
82 89
83 private def typeInContainment(ContainmentHierarchy hierarchy, Type type) { 90 private def typeInContainment(ContainmentHierarchy hierarchy, Type type) {
84 val allSuperTypes = type.transitiveClosureStar[it.supertypes] 91 val allSuperTypes = type.transitiveClosureStar[it.supertypes]
85 return allSuperTypes.exists[hierarchy.typesOrderedInHierarchy.contains(it)] 92 return allSuperTypes.exists[hierarchy.typesOrderedInHierarchy.contains(it)]
86 } 93 }
87 94
88 protected def String patternName(Relation containmentRelation, Relation inverseContainment, Type newType) { 95 protected def String patternName(Relation containmentRelation, Relation inverseContainment, Type newType) {
89 if(containmentRelation != null) { 96 if (containmentRelation !== null) {
90 if(inverseContainment != null) { 97 if (inverseContainment !== null) {
91 '''createObject_«base.canonizeName(newType.name)»_by_«base.canonizeName(containmentRelation.name)»_with_«base.canonizeName(inverseContainment.name)»''' 98 '''createObject_«base.canonizeName(newType.name)»_by_«base.canonizeName(containmentRelation.name)»_with_«base.canonizeName(inverseContainment.name)»'''
92 } else { 99 } else {
93 '''createObject_«base.canonizeName(newType.name)»_by_«base.canonizeName(containmentRelation.name)»''' 100 '''createObject_«base.canonizeName(newType.name)»_by_«base.canonizeName(containmentRelation.name)»'''
@@ -96,4 +103,8 @@ abstract class TypeRefinementGenerator {
96 '''createObject_«base.canonizeName(newType.name)»''' 103 '''createObject_«base.canonizeName(newType.name)»'''
97 } 104 }
98 } 105 }
99} \ No newline at end of file 106
107 def hasElementInContainmentName() {
108 "hasElementInContainment"
109 }
110}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend
index cbbbcb08..1a81695e 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend
@@ -10,7 +10,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par
10import java.util.HashMap 10import java.util.HashMap
11 11
12class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{ 12class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{
13 public new(PatternGenerator base) { 13 new(PatternGenerator base) {
14 super(base) 14 super(base)
15 } 15 }
16 override requiresTypeAnalysis() { true } 16 override requiresTypeAnalysis() { true }
@@ -24,7 +24,7 @@ class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{
24 inverseRelations.put(it.inverseB,it.inverseA) 24 inverseRelations.put(it.inverseB,it.inverseA)
25 ] 25 ]
26 return ''' 26 return '''
27 private pattern hasElementInContainment(problem:LogicProblem, interpretation:PartialInterpretation) 27 pattern «hasElementInContainmentName»(problem:LogicProblem, interpretation:PartialInterpretation)
28 «FOR type :containment.typesOrderedInHierarchy SEPARATOR "or"»{ 28 «FOR type :containment.typesOrderedInHierarchy SEPARATOR "or"»{
29 find interpretation(problem,interpretation); 29 find interpretation(problem,interpretation);
30 «base.typeIndexer.referInstanceOf(type,Modality.MUST,"root")» 30 «base.typeIndexer.referInstanceOf(type,Modality.MUST,"root")»
@@ -76,7 +76,7 @@ class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{
76 typeInterpretation:PartialComplexTypeInterpretation) 76 typeInterpretation:PartialComplexTypeInterpretation)
77 { 77 {
78 find interpretation(problem,interpretation); 78 find interpretation(problem,interpretation);
79 neg find hasElementInContainment(problem,interpretation); 79 neg find «hasElementInContainmentName»(problem,interpretation);
80 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); 80 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
81 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); 81 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»");
82 «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» 82 «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")»
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 1df402fa..a8a07756 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
@@ -1,85 +1,204 @@
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.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion 3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
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.viatra2logic.viatra2logicannotations.TransformedViatraWellformednessConstraint 5import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationMultiplicityConstraint
7import java.util.LinkedHashMap
8import java.util.List
6import java.util.Map 9import java.util.Map
7import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery 10import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
11import org.eclipse.xtend.lib.annotations.Data
8 12
9import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 13import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
10import java.util.LinkedHashMap 14
11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality 15@Data
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference 16class UnifinishedMultiplicityQueryNames {
17 val String unfinishedMultiplicityQueryName
18 val String unrepairableMultiplicityQueryName
19 val String remainingInverseMultiplicityQueryName
20 val String remainingContentsQueryName
21}
13 22
14class UnfinishedIndexer { 23class UnfinishedIndexer {
15 val PatternGenerator base 24 val PatternGenerator base
16 25 val boolean indexUpperMultiplicities
17 new(PatternGenerator patternGenerator) { 26
27 new(PatternGenerator patternGenerator, boolean indexUpperMultiplicities) {
18 this.base = patternGenerator 28 this.base = patternGenerator
29 this.indexUpperMultiplicities = indexUpperMultiplicities
19 } 30 }
20 31
21 def generateUnfinishedWfQueries(LogicProblem problem, Map<String,PQuery> fqn2PQuery) { 32 def generateUnfinishedWfQueries(LogicProblem problem, Map<String, PQuery> fqn2PQuery) {
22 val wfQueries = base.wfQueries(problem) 33 val wfQueries = base.wfQueries(problem)
23 ''' 34 '''
24 «FOR wfQuery: wfQueries» 35 «FOR wfQuery : wfQueries»
25 pattern unfinishedBy_«base.canonizeName(wfQuery.target.name)»(problem:LogicProblem, interpretation:PartialInterpretation, 36 pattern unfinishedBy_«base.canonizeName(wfQuery.target.name)»(problem:LogicProblem, interpretation:PartialInterpretation,
26 «FOR param : wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters SEPARATOR ', '»var_«param.name»«ENDFOR») 37 «FOR param : wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters SEPARATOR ', '»var_«param.name»«ENDFOR»)
27 { 38 {
28 «base.relationDefinitionIndexer.referPattern( 39 «base.relationDefinitionIndexer.referPattern(
29 wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery), 40 wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery),
30 wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters.map['''var_«it.name»'''], 41 wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters.map['''var_«it.name»'''],
31 Modality.CURRENT, 42 Modality.CURRENT,
32 true,false)» 43 true,false)»
33 } 44 }
34 «ENDFOR» 45 «ENDFOR»
35 ''' 46 '''
36 } 47 }
48
37 def getUnfinishedWFQueryNames(LogicProblem problem) { 49 def getUnfinishedWFQueryNames(LogicProblem problem) {
38 val wfQueries = base.wfQueries(problem) 50 val wfQueries = base.wfQueries(problem)
39 val map = new LinkedHashMap 51 val map = new LinkedHashMap
40 for(wfQuery : wfQueries) { 52 for (wfQuery : wfQueries) {
41 map.put(wfQuery.target,'''unfinishedBy_«base.canonizeName(wfQuery.target.name)»''') 53 map.put(wfQuery.target, '''unfinishedBy_«base.canonizeName(wfQuery.target.name)»''')
42 } 54 }
43 return map 55 return map
44 } 56 }
45 def generateUnfinishedMultiplicityQueries(LogicProblem problem, Map<String,PQuery> fqn2PQuery) { 57
46 val lowerMultiplicities = base.lowerMultiplicities(problem) 58 def generateUnfinishedMultiplicityQueries(List<RelationMultiplicityConstraint> constraints,
47 return ''' 59 Map<String, PQuery> fqn2PQuery) '''
48 «FOR lowerMultiplicity : lowerMultiplicities» 60 «FOR constraint : constraints»
49 pattern «unfinishedMultiplicityName(lowerMultiplicity)»(problem:LogicProblem, interpretation:PartialInterpretation, relationIterpretation:PartialRelationInterpretation, object:DefinedElement,numberOfExistingReferences) { 61 «IF constraint.constrainsUnfinished»
50 find interpretation(problem,interpretation); 62 private pattern «unfinishedMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, missingMultiplicity:java Integer) {
51 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); 63 find interpretation(problem,interpretation);
52 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«lowerMultiplicity.relation.name»"); 64 find mustExist(problem,interpretation,object);
53 «base.typeIndexer.referInstanceOf(lowerMultiplicity.firstParamTypeOfRelation,Modality::MUST,"object")» 65 «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")»
54 numberOfExistingReferences == count «base.referRelation(lowerMultiplicity.relation,"object","_",Modality.MUST,fqn2PQuery)» 66 numberOfExistingReferences == count «base.referRelation(constraint.relation,"object","_",Modality.MUST,fqn2PQuery)»
55««« numberOfExistingReferences < «lowerMultiplicity.lower»; 67 check(numberOfExistingReferences < «constraint.lowerBound»);
56««« missingMultiplicity == eval(«lowerMultiplicity.lower»-numberOfExistingReferences); 68 missingMultiplicity == eval(«constraint.lowerBound»-numberOfExistingReferences);
57 } 69 }
70
71 pattern «unfinishedMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, missingMultiplicity:java Integer) {
72 find interpretation(problem,interpretation);
73 missingMultiplicity == sum find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, _, #_);
74 }
75 «ENDIF»
76
77 «IF indexUpperMultiplicities»
78 «IF constraint.constrainsUnrepairable || constraint.constrainsRemainingInverse»
79 private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) {
80 «IF base.isRepresentative(constraint.relation, constraint.inverseRelation) && constraint.relation instanceof RelationDeclaration»
81 «base.relationRefinementGenerator.referRefinementQuery(constraint.relation as RelationDeclaration, constraint.inverseRelation, "_", "_", "source", "target")»
82 «ELSE»
83 «IF base.isRepresentative(constraint.inverseRelation, constraint.relation) && constraint.inverseRelation instanceof RelationDeclaration»
84 «base.relationRefinementGenerator.referRefinementQuery(constraint.inverseRelation as RelationDeclaration, constraint.relation, "_", "_", "target", "source")»
85 «ELSE»
86 find interpretation(problem,interpretation);
87 find mustExist(problem,interpretation,source);
88 «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"source")»
89 find mustExist(problem,interpretation,target);
90 «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"target")»
91 neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)»
92 «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)»
93 «ENDIF»
94 «ENDIF»
95 }
96 «ENDIF»
97
98 «IF constraint.constrainsUnrepairable»
99 private pattern «unrepairableMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, unrepairableMultiplicity:java Integer) {
100 find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, object, missingMultiplicity);
101 numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _);
102 check(numberOfRepairMatches < missingMultiplicity);
103 unrepairableMultiplicity == eval(missingMultiplicity-numberOfRepairMatches);
104 }
105
106 private pattern «unrepairableMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, unrepairableMultiplicity:java Integer) {
107 find interpretation(problem,interpretation);
108 unrepairableMultiplicity == max find «unrepairableMultiplicityName(constraint)»_helper(problem, interpretation, _, #_);
109 } or {
110 find interpretation(problem,interpretation);
111 neg find «unrepairableMultiplicityName(constraint)»_helper(problem, interpretation, _, _);
112 unrepairableMultiplicity == 0;
113 }
114 «ENDIF»
115
116 «IF constraint.constrainsRemainingInverse»
117 private pattern «remainingMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, remainingMultiplicity:java Integer) {
118 find interpretation(problem,interpretation);
119 find mustExist(problem,interpretation,object);
120 «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"object")»
121 numberOfExistingReferences == count «base.referRelation(constraint.relation,"_","object",Modality.MUST,fqn2PQuery)»
122 check(numberOfExistingReferences < «constraint.inverseUpperBound»);
123 numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, _, object);
124 remainingMultiplicity == eval(Math.min(«constraint.inverseUpperBound»-numberOfExistingReferences, numberOfRepairMatches));
125 }
126
127 pattern «remainingMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) {
128 find interpretation(problem,interpretation);
129 remainingMultiplicity == sum find «remainingMultiplicityName(constraint)»_helper(problem, interpretation, _, #_);
130 }
131 «ENDIF»
132
133 «IF constraint.constrainsRemainingContents»
134 «IF constraint.upperBoundFinite»
135 private pattern «remainingContentsName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, remainingMultiplicity:java Integer) {
136 find interpretation(problem,interpretation);
137 find mustExist(problem,interpretation,object);
138 «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")»
139 numberOfExistingReferences == count «base.referRelation(constraint.relation,"object","_",Modality.MUST,fqn2PQuery)»
140 check(numberOfExistingReferences < «constraint.upperBound»);
141 remainingMultiplicity == eval(«constraint.upperBound»-numberOfExistingReferences);
142 }
143
144 pattern «remainingContentsName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) {
145 find interpretation(problem,interpretation);
146 remainingMultiplicity == sum find «remainingContentsName(constraint)»_helper(problem, interpretation, _, #_);
147 }
148 «ELSE»
149 pattern «remainingContentsName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation) {
150 find interpretation(problem,interpretation);
151 find mustExist(problem,interpretation,object);
152 «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")»
153 }
154
155 pattern «remainingContentsName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) {
156 find interpretation(problem,interpretation);
157 find «remainingContentsName(constraint)»_helper(problem, interpretation);
158 remainingMultiplicity == -1;
159 } or {
160 find interpretation(problem,interpretation);
161 neg find «remainingContentsName(constraint)»_helper(problem, interpretation);
162 remainingMultiplicity == 0;
163 }
164 «ENDIF»
165 «ENDIF»
166 «ENDIF»
58 «ENDFOR» 167 «ENDFOR»
59 ''' 168 '''
60 } 169
61 def String unfinishedMultiplicityName(LowerMultiplicityAssertion lowerMultiplicityAssertion) 170 def String unfinishedMultiplicityName(
62 '''unfinishedLowerMultiplicity_«base.canonizeName(lowerMultiplicityAssertion.relation.name)»''' 171 RelationMultiplicityConstraint constraint) '''unfinishedLowerMultiplicity_«base.canonizeName(constraint.relation.name)»'''
63 172
64 //def public referUnfinishedMultiplicityQuery(LowerMultiplicityAssertion lowerMultiplicityAssertion) 173 def String unrepairableMultiplicityName(
65 // '''find «unfinishedMultiplicityName(lowerMultiplicityAssertion)»(problem, interpretation ,object, missingMultiplicity);''' 174 RelationMultiplicityConstraint constraint) '''unrepairableLowerMultiplicity_«base.canonizeName(constraint.relation.name)»'''
66 175
67 def getFirstParamTypeOfRelation(LowerMultiplicityAssertion lowerMultiplicityAssertion) { 176 private def String repairMatchName(
68 val parameters = lowerMultiplicityAssertion.relation.parameters 177 RelationMultiplicityConstraint constraint) '''repair_«base.canonizeName(constraint.relation.name)»'''
69 if(parameters.size == 2) { 178
70 val firstParam = parameters.get(0) 179 def String remainingMultiplicityName(
71 if(firstParam instanceof ComplexTypeReference) { 180 RelationMultiplicityConstraint constraint) '''remainingInverseUpperMultiplicity_«base.canonizeName(constraint.relation.name)»'''
72 return firstParam.referred 181
73 } 182 def String remainingContentsName(
74 } 183 RelationMultiplicityConstraint constraint) '''remainingContents_«base.canonizeName(constraint.relation.name)»'''
75 } 184
76 185 def getUnfinishedMultiplicityQueries(List<RelationMultiplicityConstraint> constraints) {
77 def getUnfinishedMultiplicityQueries(LogicProblem problem) { 186 constraints.toInvertedMap [ constraint |
78 val lowerMultiplicities = base.lowerMultiplicities(problem) 187 new UnifinishedMultiplicityQueryNames(
79 val map = new LinkedHashMap 188 if(constraint.constrainsUnfinished) unfinishedMultiplicityName(constraint) else null,
80 for(lowerMultiplicity : lowerMultiplicities) { 189 if (indexUpperMultiplicities && constraint.constrainsUnrepairable)
81 map.put(lowerMultiplicity.relation,unfinishedMultiplicityName(lowerMultiplicity)->lowerMultiplicity.lower) 190 unrepairableMultiplicityName(constraint)
82 } 191 else
83 return map 192 null,
193 if (indexUpperMultiplicities && constraint.constrainsRemainingInverse)
194 remainingMultiplicityName(constraint)
195 else
196 null,
197 if (indexUpperMultiplicities && constraint.constrainsRemainingContents)
198 remainingContentsName(constraint)
199 else
200 null
201 )
202 ]
84 } 203 }
85} 204}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-17 02:52:47 +0000