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/PConstraintTransformer.xtend275
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend116
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend303
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend172
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend158
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend184
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend174
-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.xtend172
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend302
15 files changed, 1758 insertions, 964 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/PConstraintTransformer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend
new file mode 100644
index 00000000..dd5cade1
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend
@@ -0,0 +1,275 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
2
3import hu.bme.mit.inf.dslreasoner.viatra2logic.XExpressionExtractor
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
5import org.eclipse.emf.ecore.EAttribute
6import org.eclipse.emf.ecore.EEnumLiteral
7import org.eclipse.emf.ecore.EReference
8import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
9import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
10import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey
11import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
12import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
13import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality
14import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter
15import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
16import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality
17import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
18import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint
19import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure
20import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue
21import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall
22import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint
23import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.VariableMapping
24import java.util.List
25import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
26import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
27import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference
28import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
29import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
30import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
31import java.util.Map
32
33class PConstraintTransformer {
34 val extension RelationDefinitionIndexer relationDefinitionIndexer;
35 val expressionExtractor = new XExpressionExtractor
36 val expressionGenerator = new PExpressionGenerator
37
38 new(RelationDefinitionIndexer relationDefinitionIndexer) {
39 this.relationDefinitionIndexer = relationDefinitionIndexer
40 }
41
42 dispatch def transformConstraint(TypeConstraint constraint, Modality modality, List<VariableMapping> variableMapping) {
43 val touple = constraint.variablesTuple
44 if(touple.size == 1) {
45 val inputKey = constraint.equivalentJudgement.inputKey
46 if(inputKey instanceof EClassTransitiveInstancesKey) {
47 return relationDefinitionIndexer.base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,
48 constraint.getVariableInTuple(0).canonizeName)
49 } else if(inputKey instanceof EDataTypeInSlotsKey){
50 return '''// type constraint is enforced by construction'''
51 }
52
53 } else if(touple.size == 2){
54 val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey
55 if(key instanceof EReference) {
56 return base.referRelationByName(
57 key,
58 constraint.getVariableInTuple(0).canonizeName,
59 constraint.getVariableInTuple(1).canonizeName,
60 modality.toMustMay)
61 } else if (key instanceof EAttribute) {
62 return base.referAttributeByName(key,
63 constraint.getVariableInTuple(0).canonizeName,
64 constraint.getVariableInTuple(1).canonizeName,
65 modality.toMustMay)
66 } else throw new UnsupportedOperationException('''unknown key: «key.class»''')
67 } else {
68 throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
69 }
70 }
71 dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality, List<VariableMapping> variableMapping) {
72 val touple = constraint.variablesTuple
73 if(touple.size == 1) {
74 val inputKey = constraint.equivalentJudgement.inputKey
75 if(inputKey instanceof EClassTransitiveInstancesKey) {
76 return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,
77 (constraint.getVariablesTuple.get(0) as PVariable).canonizeName)
78 } else if(inputKey instanceof EDataTypeInSlotsKey){
79 return '''// type constraint is enforced by construction'''
80 }
81
82 } else if(touple.size == 2){
83 val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey
84 if(key instanceof EReference) {
85 return base.referRelationByName(
86 key,
87 (constraint.getVariablesTuple.get(0) as PVariable).canonizeName,
88 (constraint.getVariablesTuple.get(1) as PVariable).canonizeName,
89 modality.toMustMay)
90 } else if (key instanceof EAttribute) {
91 return base.referAttributeByName(key,
92 (constraint.getVariablesTuple.get(0) as PVariable).canonizeName,
93 (constraint.getVariablesTuple.get(1) as PVariable).canonizeName,
94 modality.toMustMay)
95 } else throw new UnsupportedOperationException('''unknown key: «key.class»''')
96 } else {
97 throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
98 }
99 }
100
101 dispatch def transformConstraint(Equality equality, Modality modality, List<VariableMapping> variableMapping) {
102 val a = equality.who
103 val b = equality.withWhom
104 transformEquality(modality.toMustMay, a, b)
105 }
106
107 private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) {
108 if(modality.isMustOrCurrent) '''find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
109 else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
110 }
111
112 dispatch def transformConstraint(Inequality inequality, Modality modality, List<VariableMapping> variableMapping) {
113 val a = inequality.who
114 val b = inequality.withWhom
115 if(modality.isCurrent) {
116 return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
117 } else if(modality.isMust) {
118 return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
119 } else { // modality.isMay
120 return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
121 }
122 }
123
124 dispatch def transformConstraint(NegativePatternCall pcall, Modality modality, List<VariableMapping> variableMapping) {
125 val params = (0..<pcall.actualParametersTuple.size).map[index |
126 val variable = pcall.actualParametersTuple.get(index) as PVariable
127 return variable.canonizeName
128 ]
129 return referPattern(pcall.referredQuery,params,modality.dual,false,false)
130 }
131
132 dispatch def transformConstraint(PositivePatternCall pcall, Modality modality, List<VariableMapping> variableMapping) {
133 val params = (0..<pcall.variablesTuple.size).map[index |
134 val variable = pcall.variablesTuple.get(index) as PVariable
135 return variable.canonizeName
136 ]
137 return referPattern(pcall.referredQuery,params,modality,true,false)
138 }
139 dispatch def transformConstraint(BinaryTransitiveClosure pcall, Modality modality, List<VariableMapping> variableMapping) {
140 val params = (0..1).map[index |
141 val variable = pcall.getVariableInTuple(index) as PVariable
142 return variable.canonizeName
143 ]
144 return referPattern(pcall.referredQuery,params,modality,true,true)
145 }
146 dispatch def transformConstraint(ExportedParameter e, Modality modality, List<VariableMapping> variableMapping) {
147 val v1 = '''var_«e.parameterName»'''
148 val v2 = e.parameterVariable.canonizeName
149 if(v1.compareTo(v2) == 0) {
150 return '''// «v1» exported'''
151 } else {
152 return '''«v1» == «v2»;'''
153 }
154 }
155 dispatch def transformConstraint(ConstantValue c, Modality modality, List<VariableMapping> variableMapping) {
156 val target = c.supplierKey
157
158 var String targetString;
159 var String additionalDefinition;
160 if(target instanceof EEnumLiteral) {
161 targetString = '''const_«target.name»_«target.EEnum.name»'''
162 additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» «target.EEnum.name»"); //LogicProblem.elements(problem,«targetString»);'''
163 } else if(target instanceof Integer) {
164 targetString = '''const_«target»_Integer'''
165 additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); IntegerElement.value(«targetString»,«target»);'''
166 } else if(target instanceof Boolean) {
167 targetString = '''const_«target»_Boolean'''
168 additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); BooleanElement.value(«targetString»,«target»);'''
169 } else if(target instanceof String) {
170 targetString = '''const_«target»_String'''
171 additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); StringElement.value(«targetString»,"«target»");'''
172 } else if(target instanceof Double) {
173 targetString = '''const_«target»_Real'''
174 additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); RealElement.value(«targetString»,«target»);'''
175 } else if(target instanceof Float) {
176 targetString = '''const_«target»_Real'''
177 additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); RealElement.value(«targetString»,«target»);'''
178 } else {
179 throw new UnsupportedOperationException('''Unknown constant type: «target.class»''')
180 }
181
182 val source = c.variablesTuple
183 var String sourceName
184 if(source.size == 1)
185 sourceName = (source.get(0) as PVariable).canonizeName
186 else throw new UnsupportedOperationException("unknown source")
187 return '''«sourceName» == «targetString»;«additionalDefinition»''';
188 }
189
190 protected def valueVariable(PVariable v) {
191 "value_"+v.canonizeName
192 }
193 protected def valueSetted(PVariable v) {
194 "setted_"+v.canonizeName
195 }
196 def hasValue(PVariable v, String target, Modality m, List<VariableMapping> variableMapping) {
197 val typeReference = variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range as PrimitiveTypeReference
198 if(m.isMay) {
199 '''PrimitiveElement.valueSet(«v.canonizeName»,«v.valueSetted»); «hasValueExpressionByRef(typeReference,v,v.valueVariable)»
200««« check(!«v.valueSetted»||«v.valueVariable»==«target»));
201'''
202 } else { // Must or current
203 '''PrimitiveElement.valueSet(«v.canonizeName»,true);«hasValueExpressionByRef(typeReference,v,target)»'''
204 }
205 }
206
207 private def hasValueExpression(List<VariableMapping> variableMapping, PVariable v, String target) {
208 val mapping = variableMapping.filter[
209 val v2 = (it.sourcePVariable as PVariable)
210 v2 === v
211 ].head
212 val range = mapping.targetLogicVariable.range
213 hasValueExpressionByRef(
214 range,
215 v,
216 target
217 )
218 }
219 private def dispatch hasValueExpressionByRef(BoolTypeReference typeReference, PVariable v, String target) '''BooleanElement.value(«v.canonizeName»,«target»);'''
220 private def dispatch hasValueExpressionByRef(IntTypeReference typeReference, PVariable v, String target) '''IntegerElement.value(«v.canonizeName»,«target»);'''
221 private def dispatch hasValueExpressionByRef(RealTypeReference typeReference, PVariable v, String target) '''RealElement.value(«v.canonizeName»,«target»);'''
222 private def dispatch hasValueExpressionByRef(StringTypeReference typeReference, PVariable v, String target) '''StringElement.value(«v.canonizeName»,«target»);'''
223 private def dispatch hasValueExpressionByRef(TypeReference typeReference, PVariable v, String target) {
224 throw new UnsupportedOperationException('''Unsupported primitive type reference: «typeReference.class»''')
225 }
226
227 dispatch def transformConstraint(ExpressionEvaluation e, Modality modality, List<VariableMapping> variableMapping) {
228 if(e.outputVariable!==null) {
229 throw new UnsupportedOperationException('''Only check expressions are supported "«e.class.name»"!''')
230 } else {
231 val expression = expressionExtractor.extractExpression(e.evaluator)
232 val Map<PVariable, PrimitiveTypeReference> variable2Type = e.affectedVariables.toInvertedMap[v|variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range as PrimitiveTypeReference]
233 if(modality.isMay) {
234 return '''
235 «FOR variable: e.affectedVariables»
236 PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
237 «ENDFOR»
238««« check(
239««« «FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR»
240««« «IF variable2Type.values.filter(RealTypeReference).empty»
241««« ||
242««« («expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)»)
243««« «ENDIF»
244««« );
245 '''
246 } else { // Must or Current
247 return '''
248 «FOR variable: e.affectedVariables»
249 PrimitiveElement.valueSet(«variable.canonizeName»,true); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
250 «ENDFOR»
251««« «IF variable2Type.values.filter(RealTypeReference).empty»
252««« check(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)»);
253««« «ENDIF»
254 '''
255 }
256 }
257 }
258
259 dispatch def transformConstraint(PConstraint c, Modality modality, List<VariableMapping> variableMapping) {
260 throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''')
261 }
262
263 dispatch def transformConstraintUnset(ExpressionEvaluation e, List<VariableMapping> variableMapping) {
264 return '''
265 «FOR variable: e.affectedVariables»
266 PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
267 «ENDFOR»
268««« check(«FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR»);
269 '''
270 }
271
272 dispatch def transformConstraintUnset(PConstraint c, List<VariableMapping> variableMapping) {
273 throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''')
274 }
275} \ 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/PExpressionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend
new file mode 100644
index 00000000..62ff92b2
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend
@@ -0,0 +1,116 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
2
3import java.util.Map
4import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
5import org.eclipse.xtext.xbase.XBinaryOperation
6import org.eclipse.xtext.xbase.XExpression
7import org.eclipse.xtext.xbase.XFeatureCall
8import org.eclipse.xtext.xbase.XMemberFeatureCall
9import org.eclipse.xtext.xbase.XNumberLiteral
10import org.eclipse.xtext.xbase.XUnaryOperation
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
13
14class PExpressionGenerator {
15 static val N_Base = "org.eclipse.xtext.xbase.lib."
16
17 static val N_PLUS1 = "operator_plus"
18 static val N_MINUS1 = "operator_minus"
19
20 static val N_MINUS2 = "operator_minus"
21 static val N_PLUS2 = "operator_plus"
22 static val N_POWER = "operator_power"
23 static val N_MULTIPLY = "operator_multiply"
24 static val N_DIVIDE = "operator_divide"
25 static val N_MODULO = "operator_modulo"
26 static val N_LESSTHAN = "operator_lessThan"
27 static val N_LESSEQUALSTHAN = "operator_lessEqualsThan"
28 static val N_GREATERTHAN = "operator_greaterThan"
29 static val N_GREATEREQUALTHAN = "operator_greaterEqualsThan"
30 static val N_EQUALS = "operator_equals"
31 static val N_NOTEQUALS = "operator_notEquals"
32 static val N_EQUALS3 = "operator_tripleEquals"
33 static val N_NOTEQUALS3 = "operator_tripleNotEquals"
34
35 protected def isN(String name, String s) {
36 val res = name.startsWith(N_Base) && name.endsWith(s)
37 //println('''[«res»] «name» ?= «N_Base»*«s»''')
38 return res
39 }
40
41 static val N_POWER2 = "java.lang.Math.pow"
42
43 def dispatch CharSequence translateExpression(XBinaryOperation e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
44 val left = e.leftOperand.translateExpression(valueName,variable2Type)
45 val right = e.rightOperand.translateExpression(valueName,variable2Type)
46 val feature = e.feature.qualifiedName
47 if(feature.isN(N_MINUS2)) { return '''(«left»-«right»)'''}
48 else if(feature.isN(N_PLUS2)) { return '''(«left»+«right»)''' }
49 else if(feature.isN(N_POWER)) { return '''(«left»^«right»)''' }
50 else if(feature.isN(N_MULTIPLY)) { return '''(«left»*«right»)''' }
51 else if(feature.isN(N_DIVIDE)) { return '''(«left»/«right»)''' }
52 else if(feature.isN(N_MODULO)) { return '''(«left»%«right»)''' }
53 else if(feature.isN(N_LESSTHAN)) { return '''(«left»<«right»)''' }
54 else if(feature.isN(N_LESSEQUALSTHAN)) { return '''(«left»<=«right»)''' }
55 else if(feature.isN(N_GREATERTHAN)) { return '''(«left»>«right»)''' }
56 else if(feature.isN(N_GREATEREQUALTHAN)) { return '''(«left»>=«right»)''' }
57 else if(feature.isN(N_EQUALS)) { return '''(«left»==«right»)''' }
58 else if(feature.isN(N_NOTEQUALS)) { return '''(«left»!=«right»)''' }
59 else if(feature.isN(N_EQUALS3)) { return '''(«left»===«right»)''' }
60 else if(feature.isN(N_NOTEQUALS3)) { return '''(«left»!==«right»)''' }
61 else {
62 println("-> " + e.feature+","+e.class)
63 println("-> " + e.leftOperand)
64 println("-> " + e.rightOperand)
65 println("-> " + e.feature.qualifiedName)
66 throw new UnsupportedOperationException('''Unsupported binary operator feature: "«e.feature.class.simpleName»" - «e»''')
67 }
68 }
69
70 def dispatch CharSequence translateExpression(XUnaryOperation e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
71 val operand = e.operand.translateExpression(valueName,variable2Type)
72 val feature = e.feature.qualifiedName
73 if(feature.isN(N_MINUS1)) { return '''(-«operand»)'''}
74 else if(feature.isN(N_PLUS1)) { return '''(+«operand»)'''}
75 else{
76 println("-> " + e.feature+","+e.class)
77 println("-> " + e.operand)
78 println("-> " + e.feature.qualifiedName)
79 throw new UnsupportedOperationException('''Unsupported unary operator feature: "«e.feature.class.simpleName»" - «e»''')
80 }
81 }
82
83 def dispatch CharSequence translateExpression(XMemberFeatureCall e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
84 val transformedArguments = e.actualArguments.map[translateExpression(valueName,variable2Type)]
85 val feature = e.feature.qualifiedName
86 if(feature == N_POWER2) {
87 return '''Math.pow(«transformedArguments.get(0)»,«transformedArguments.get(1)»)'''
88 }else {
89 println(e.feature+","+e.class)
90 println(e.actualArguments.join(", "))
91 println(e.feature.qualifiedName)
92 throw new UnsupportedOperationException('''Unsupported feature call: "«e.feature.qualifiedName»" - «e»''')
93 }
94 }
95
96 def dispatch CharSequence translateExpression(XFeatureCall e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
97 val featureName = e.feature.qualifiedName
98 val type = variable2Type.entrySet.filter[it.key.name===featureName].head.value
99 val entryWithName = valueName.entrySet.filter[it.key.name == featureName].head
100 if(entryWithName !== null) {
101 if(type instanceof RealTypeReference) {
102 return '''(«entryWithName.value».doubleValue)'''
103 } else {
104 return entryWithName.value
105 }
106 } else {
107 throw new IllegalArgumentException('''Feature call reference to unavailable variable "«featureName»"''')
108 }
109 }
110
111 def dispatch CharSequence translateExpression(XNumberLiteral l, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) '''«l.value»'''
112
113 def dispatch CharSequence translateExpression(XExpression expression, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
114 throw new UnsupportedOperationException('''Unsupported expression in check or eval: «expression.class.name», «expression»"''')
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/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 d4c76bb4..edf92343 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,31 +16,55 @@ 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
24import org.eclipse.emf.ecore.EReference 27import org.eclipse.emf.ecore.EReference
28import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
25import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery 29import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
26import org.eclipse.xtend.lib.annotations.Accessors 30import org.eclipse.xtend.lib.annotations.Accessors
31import org.eclipse.xtend.lib.annotations.Data
32import org.eclipse.xtend2.lib.StringConcatenationClient
27 33
28import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 34import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
29 35
36@Data class PatternGeneratorResult {
37 CharSequence patternText
38 HashMap<PConstraint,String> constraint2MustPreconditionName
39 HashMap<PConstraint,String> constraint2CurrentPreconditionName
40}
41
42interface UnitPropagationPatternGenerator {
43 def Map<Relation, String> getMustPatterns()
44
45 def Map<Relation, String> getMustNotPatterns()
46
47 def StringConcatenationClient getAdditionalPatterns(PatternGenerator generator, Map<String, PQuery> fqn2PQuery)
48}
49
30class PatternGenerator { 50class PatternGenerator {
31 @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer //= new TypeIndexer(this) 51 @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this)
32 @Accessors(PUBLIC_GETTER) val RelationDeclarationIndexer relationDeclarationIndexer = new RelationDeclarationIndexer(this) 52 @Accessors(PUBLIC_GETTER) val RelationDeclarationIndexer relationDeclarationIndexer = new RelationDeclarationIndexer(
33 @Accessors(PUBLIC_GETTER) val RelationDefinitionIndexer relationDefinitionIndexer = new RelationDefinitionIndexer(this) 53 this)
54 @Accessors(PUBLIC_GETTER) val RelationDefinitionIndexer relationDefinitionIndexer = new RelationDefinitionIndexer(
55 this)
34 @Accessors(PUBLIC_GETTER) val ContainmentIndexer containmentIndexer = new ContainmentIndexer(this) 56 @Accessors(PUBLIC_GETTER) val ContainmentIndexer containmentIndexer = new ContainmentIndexer(this)
35 @Accessors(PUBLIC_GETTER) val InvalidIndexer invalidIndexer = new InvalidIndexer(this) 57 @Accessors(PUBLIC_GETTER) val InvalidIndexer invalidIndexer = new InvalidIndexer(this)
36 @Accessors(PUBLIC_GETTER) val UnfinishedIndexer unfinishedIndexer = new UnfinishedIndexer(this) 58 @Accessors(PUBLIC_GETTER) val UnfinishedIndexer unfinishedIndexer
37 @Accessors(PUBLIC_GETTER) val TypeRefinementGenerator typeRefinementGenerator //= new RefinementGenerator(this) 59 @Accessors(PUBLIC_GETTER) val TypeRefinementGenerator typeRefinementGenerator //= new RefinementGenerator(this)
38 @Accessors(PUBLIC_GETTER) val RelationRefinementGenerator relationRefinementGenerator = new RelationRefinementGenerator(this) 60 @Accessors(PUBLIC_GETTER) val RelationRefinementGenerator relationRefinementGenerator = new RelationRefinementGenerator(this)
61 @Accessors(PUBLIC_GETTER) val UnitPropagationPreconditionGenerator unitPropagationPreconditionGenerator = new UnitPropagationPreconditionGenerator(this)
39 62
40 public new(TypeInferenceMethod typeInferenceMethod) { 63 new(TypeInferenceMethod typeInferenceMethod, ScopePropagatorStrategy scopePropagatorStrategy) {
41 if(typeInferenceMethod == TypeInferenceMethod.Generic) { 64 if(typeInferenceMethod == TypeInferenceMethod.Generic) {
42 this.typeIndexer = new GenericTypeIndexer(this) 65 this.typeIndexer = new GenericTypeIndexer(this)
43 this.typeRefinementGenerator = new GenericTypeRefinementGenerator(this) 66 this.typeRefinementGenerator = new GenericTypeRefinementGenerator(this)
44 } else if(typeInferenceMethod == TypeInferenceMethod.PreliminaryAnalysis) { 67 } else if (typeInferenceMethod == TypeInferenceMethod.PreliminaryAnalysis) {
45 this.typeIndexer = new TypeIndexerWithPreliminaryTypeAnalysis(this) 68 this.typeIndexer = new TypeIndexerWithPreliminaryTypeAnalysis(this)
46 this.typeRefinementGenerator = new TypeRefinementWithPreliminaryTypeAnalysis(this) 69 this.typeRefinementGenerator = new TypeRefinementWithPreliminaryTypeAnalysis(this)
47 } else { 70 } else {
@@ -49,113 +72,105 @@ class PatternGenerator {
49 this.typeRefinementGenerator = null 72 this.typeRefinementGenerator = null
50 throw new IllegalArgumentException('''Unknown type indexing technique : «typeInferenceMethod.name»''') 73 throw new IllegalArgumentException('''Unknown type indexing technique : «typeInferenceMethod.name»''')
51 } 74 }
75 this.unfinishedIndexer = new UnfinishedIndexer(this, scopePropagatorStrategy.requiresUpperBoundIndexing)
52 } 76 }
53 77
54 public def requiresTypeAnalysis() { 78 def requiresTypeAnalysis() {
55 typeIndexer.requiresTypeAnalysis || typeRefinementGenerator.requiresTypeAnalysis 79 typeIndexer.requiresTypeAnalysis || typeRefinementGenerator.requiresTypeAnalysis
56 } 80 }
57 81
58 public dispatch def referRelation( 82 dispatch def CharSequence referRelation(RelationDeclaration referred, String sourceVariable, String targetVariable,
59 RelationDeclaration referred, 83 Modality modality, Map<String, PQuery> fqn2PQuery) {
60 String sourceVariable, 84 return this.relationDeclarationIndexer.referRelation(referred, sourceVariable, targetVariable, modality)
61 String targetVariable,
62 Modality modality,
63 Map<String,PQuery> fqn2PQuery)
64 {
65 return this.relationDeclarationIndexer.referRelation(referred,sourceVariable,targetVariable,modality)
66 } 85 }
67 public dispatch def referRelation( 86
68 RelationDefinition referred, 87 dispatch def CharSequence referRelation(RelationDefinition referred, String sourceVariable, String targetVariable,
69 String sourceVariable, 88 Modality modality, Map<String, PQuery> fqn2PQuery) {
70 String targetVariable, 89 val pattern = referred.annotations.filter(TransfomedViatraQuery).head.patternFullyQualifiedName.lookup(
71 Modality modality, 90 fqn2PQuery)
72 Map<String,PQuery> fqn2PQuery) 91 return this.relationDefinitionIndexer.referPattern(pattern, #[sourceVariable, targetVariable], modality, true,
73 { 92 false)
74 val pattern = referred.annotations.filter(TransfomedViatraQuery).head.patternFullyQualifiedName.lookup(fqn2PQuery)
75 return this.relationDefinitionIndexer.referPattern(pattern,#[sourceVariable,targetVariable],modality,true,false)
76 } 93 }
77 94
78 def public referRelationByName(EReference reference, 95 def referRelationByName(EReference reference, String sourceVariable, String targetVariable, Modality modality) {
79 String sourceVariable, 96 '''find «modality.name.toLowerCase»InRelation«canonizeName('''«reference.name» reference «reference.EContainingClass.name»''')»(problem,interpretation,«sourceVariable»,«targetVariable»);'''
80 String targetVariable,
81 Modality modality)
82 {
83 '''find «modality.name.toLowerCase»InRelation«canonizeName('''«reference.name» reference «reference.EContainingClass.name»''')
84 »(problem,interpretation,«sourceVariable»,«targetVariable»);'''
85 } 97 }
86 98
87 def public CharSequence referAttributeByName(EAttribute attribute, 99 def CharSequence referAttributeByName(EAttribute attribute, String sourceVariable, String targetVariable,
88 String sourceVariable, 100 Modality modality) {
89 String targetVariable, 101 '''find «modality.name.toLowerCase»InRelation«canonizeName('''«attribute.name» attribute «attribute.EContainingClass.name»''')»(problem,interpretation,«sourceVariable»,«targetVariable»);'''
90 Modality modality)
91 {
92 '''find «modality.name.toLowerCase»InRelation«canonizeName('''«attribute.name» attribute «attribute.EContainingClass.name»''')
93 »(problem,interpretation,«sourceVariable»,«targetVariable»);'''
94 } 102 }
95 103
96 public def canonizeName(String name) { 104 def canonizeName(String name) {
97 name.split(' ').join('_') 105 name.split(' ').join('_')
98 } 106 }
99 107
100 public def lowerMultiplicities(LogicProblem problem) { 108 def wfQueries(LogicProblem problem) {
101 problem.assertions.map[annotations].flatten.filter(LowerMultiplicityAssertion).filter[!it.relation.isDerived] 109 problem.assertions.map[it.annotations].flatten.filter(TransformedViatraWellformednessConstraint).map[it.query]
102 }
103 public def wfQueries(LogicProblem problem) {
104 problem.assertions.map[it.annotations]
105 .flatten
106 .filter(TransformedViatraWellformednessConstraint)
107 .map[it.query]
108 } 110 }
109 public def getContainments(LogicProblem p) { 111
112 def getContainments(LogicProblem p) {
110 return p.containmentHierarchies.head.containmentRelations 113 return p.containmentHierarchies.head.containmentRelations
111 } 114 }
112 public def getInverseRelations(LogicProblem p) { 115
116 def getInverseRelations(LogicProblem p) {
113 val inverseRelations = new HashMap 117 val inverseRelations = new HashMap
114 p.annotations.filter(InverseRelationAssertion).forEach[ 118 p.annotations.filter(InverseRelationAssertion).forEach [
115 inverseRelations.put(it.inverseA,it.inverseB) 119 inverseRelations.put(it.inverseA, it.inverseB)
116 inverseRelations.put(it.inverseB,it.inverseA) 120 inverseRelations.put(it.inverseB, it.inverseA)
117 ] 121 ]
118 return inverseRelations 122 return inverseRelations
119 } 123 }
120 public def isRepresentative(Relation relation, Relation inverse) { 124
121 if(inverse == null) { 125 def isRepresentative(Relation relation, Relation inverse) {
126 if (relation === null) {
127 return false
128 } else if (inverse === null) {
122 return true 129 return true
123 } else { 130 } else {
124 relation.name.compareTo(inverse.name)<1 131 relation.name.compareTo(inverse.name) < 1
125 } 132 }
126 } 133 }
127 134
128 public def isDerived(Relation relation) { 135 def isDerived(Relation relation) {
129 relation.annotations.exists[it instanceof DefinedByDerivedFeature] 136 relation.annotations.exists[it instanceof DefinedByDerivedFeature]
130 } 137 }
131 public def getDerivedDefinition(RelationDeclaration relation) { 138
139 def getDerivedDefinition(RelationDeclaration relation) {
132 relation.annotations.filter(DefinedByDerivedFeature).head.query 140 relation.annotations.filter(DefinedByDerivedFeature).head.query
133 } 141 }
134 142
135 private def allTypeReferences(LogicProblem problem) { 143 private def allTypeReferences(LogicProblem problem) {
136 problem.eAllContents.filter(TypeReference).toIterable 144 problem.eAllContents.filter(TypeReference).toIterable
137 } 145 }
146
138 protected def hasBoolean(LogicProblem problem) { 147 protected def hasBoolean(LogicProblem problem) {
139 problem.allTypeReferences.exists[it instanceof BoolTypeReference] 148 problem.allTypeReferences.exists[it instanceof BoolTypeReference]
140 } 149 }
150
141 protected def hasInteger(LogicProblem problem) { 151 protected def hasInteger(LogicProblem problem) {
142 problem.allTypeReferences.exists[it instanceof IntTypeReference] 152 problem.allTypeReferences.exists[it instanceof IntTypeReference]
143 } 153 }
154
144 protected def hasReal(LogicProblem problem) { 155 protected def hasReal(LogicProblem problem) {
145 problem.allTypeReferences.exists[it instanceof RealTypeReference] 156 problem.allTypeReferences.exists[it instanceof RealTypeReference]
146 } 157 }
158
147 protected def hasString(LogicProblem problem) { 159 protected def hasString(LogicProblem problem) {
148 problem.allTypeReferences.exists[it instanceof StringTypeReference] 160 problem.allTypeReferences.exists[it instanceof StringTypeReference]
149 } 161 }
150 162
151 public def transformBaseProperties( 163 def transformBaseProperties(
152 LogicProblem problem, 164 LogicProblem problem,
153 PartialInterpretation emptySolution, 165 PartialInterpretation emptySolution,
154 Map<String,PQuery> fqn2PQuery, 166 Map<String, PQuery> fqn2PQuery,
155 TypeAnalysisResult typeAnalysisResult 167 TypeAnalysisResult typeAnalysisResult,
168 RelationConstraints constraints,
169 Collection<LinearTypeConstraintHint> hints,
170 Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators
156 ) { 171 ) {
157 172 val first =
158 return ''' 173 '''
159 import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage" 174 import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage"
160 import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" 175 import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem"
161 import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" 176 import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language"
@@ -170,6 +185,7 @@ class PatternGenerator {
170 ///////////////////////// 185 /////////////////////////
171 // 0.1 Existence 186 // 0.1 Existence
172 ///////////////////////// 187 /////////////////////////
188 /** [[exist(element)]]=1 */
173 private pattern mustExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 189 private pattern mustExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
174 find interpretation(problem,interpretation); 190 find interpretation(problem,interpretation);
175 LogicProblem.elements(problem,element); 191 LogicProblem.elements(problem,element);
@@ -178,6 +194,7 @@ class PatternGenerator {
178 PartialInterpretation.newElements(interpretation,element); 194 PartialInterpretation.newElements(interpretation,element);
179 } 195 }
180 196
197 /** [[exist(element)]]>=1/2 */
181 private pattern mayExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 198 private pattern mayExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
182 find mustExist(problem,interpretation,element); 199 find mustExist(problem,interpretation,element);
183 } or { 200 } or {
@@ -188,7 +205,7 @@ class PatternGenerator {
188 205
189 private pattern elementCloseWorld(element:DefinedElement) { 206 private pattern elementCloseWorld(element:DefinedElement) {
190 PartialInterpretation.openWorldElements(i,element); 207 PartialInterpretation.openWorldElements(i,element);
191 PartialInterpretation.maxNewElements(i,0); 208 PartialInterpretation.maxNewElements(i,0);
192 } or { 209 } or {
193 Scope.targetTypeInterpretation(scope,interpretation); 210 Scope.targetTypeInterpretation(scope,interpretation);
194 PartialTypeInterpratation.elements(interpretation,element); 211 PartialTypeInterpratation.elements(interpretation,element);
@@ -198,64 +215,115 @@ class PatternGenerator {
198 //////////////////////// 215 ////////////////////////
199 // 0.2 Equivalence 216 // 0.2 Equivalence
200 //////////////////////// 217 ////////////////////////
201 pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { 218 pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement)
219 // For non-primitive type. Boolean types always must equivalent or cannot equivalent
220 {
202 find mayExist(problem,interpretation,a); 221 find mayExist(problem,interpretation,a);
203 find mayExist(problem,interpretation,b); 222 find mayExist(problem,interpretation,b);
204 a == b; 223 a == b;
224««« } or {
225««« find mayExist(problem,interpretation,a);
226««« find mayExist(problem,interpretation,b);
227««« IntegerElement(a);
228««« IntegerElement(b);
229««« PrimitiveElement.valueSet(a,false);
230««« } or {
231««« find mayExist(problem,interpretation,a);
232««« find mayExist(problem,interpretation,b);
233««« IntegerElement(a);
234««« IntegerElement(b);
235««« PrimitiveElement.valueSet(b,false);
236««« } or {
237««« find mayExist(problem,interpretation,a);
238««« find mayExist(problem,interpretation,b);
239««« RealElement(a);
240««« RealElement(b);
241««« PrimitiveElement.valueSet(a,false);
242««« } or {
243««« find mayExist(problem,interpretation,a);
244««« find mayExist(problem,interpretation,b);
245««« RealElement(a);
246««« RealElement(b);
247««« PrimitiveElement.valueSet(b,false);
248««« } or {
249««« find mayExist(problem,interpretation,a);
250««« find mayExist(problem,interpretation,b);
251««« StringElement(a);
252««« StringElement(b);
253««« PrimitiveElement.valueSet(a,false);
254««« } or {
255««« find mayExist(problem,interpretation,a);
256««« find mayExist(problem,interpretation,b);
257««« StringElement(a);
258««« StringElement(b);
259««« PrimitiveElement.valueSet(b,false);
205 } 260 }
261
206 pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { 262 pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) {
263 // For non-primitive and Boolean primitive type
207 find mustExist(problem,interpretation,a); 264 find mustExist(problem,interpretation,a);
208 find mustExist(problem,interpretation,b); 265 find mustExist(problem,interpretation,b);
209 a == b; 266 a == b;
267««« } or {
268««« find mustExist(problem,interpretation,a);
269««« find mustExist(problem,interpretation,b);
270««« PrimitiveElement.valueSet(a,true);
271««« PrimitiveElement.valueSet(b,true);
272««« IntegerElement.value(a,value);
273««« IntegerElement.value(b,value);
274««« } or {
275««« find mustExist(problem,interpretation,a);
276««« find mustExist(problem,interpretation,b);
277««« PrimitiveElement.valueSet(a,true);
278««« PrimitiveElement.valueSet(b,true);
279««« RealElement.value(a,value);
280««« RealElement.value(b,value);
281««« } or {
282««« find mustExist(problem,interpretation,a);
283««« find mustExist(problem,interpretation,b);
284««« PrimitiveElement.valueSet(a,true);
285««« PrimitiveElement.valueSet(b,true);
286««« StringElement.value(a,value);
287««« StringElement.value(b,value);
210 } 288 }
211 289
212 ////////////////////////
213 // 0.3 Required Patterns by TypeIndexer
214 ////////////////////////
215 «typeIndexer.requiredQueries»
216
217 ////////// 290 //////////
218 // 1. Problem-Specific Base Indexers 291 // 1. Problem-Specific Base Indexers
219 ////////// 292 //////////
220 // 1.1 Type Indexers 293 // 1.1 Type Indexers
221 ////////// 294 //////////
222 // 1.1.1 primitive Type Indexers 295 // 1.1.1 Required Patterns by TypeIndexer
223 ////////// 296 //////////
224««« pattern instanceofBoolean(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 297
225««« find interpretation(problem,interpretation); 298 «typeIndexer.requiredQueries»
226««« PartialInterpretation.booleanelements(interpretation,element);
227««« }
228««« pattern instanceofInteger(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
229««« find interpretation(problem,interpretation);
230««« PartialInterpretation.integerelements(interpretation,element);
231««« } or {
232««« find interpretation(problem,interpretation);
233««« PartialInterpretation.newIntegers(interpetation,element);
234««« }
235««« pattern instanceofReal(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
236««« find interpretation(problem,interpretation);
237««« PartialInterpretation.realelements(interpretation,element);
238««« } or {
239««« find interpretation(problem,interpretation);
240««« PartialInterpretation.newReals(interpetation,element);
241««« }
242««« pattern instanceofString(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
243««« find interpretation(problem,interpretation);
244««« PartialInterpretation.stringelements(interpretation,element);
245««« } or {
246««« find interpretation(problem,interpretation);
247««« PartialInterpretation.newStrings(interpetation,element);
248««« }
249 299
250 ////////// 300 //////////
251 // 1.1.2 domain-specific Type Indexers 301 // 1.1.2 primitive Type Indexers
302 //////////
303 // Currently unused. Refer primitive types as:
304 // > PrimitiveElement(element)
305 // specific types are referred as:
306 // > BooleanElement(variableName)
307 // > IntegerElement(variableName)
308 // > RealElement(variableName)
309 // > StringElement(variableName)
310 // And their value as
311 // > BooleanElement.value(variableName,value)
312 // > IntegerElement.value(variableName,value)
313 // > RealElement.value(variableName,value)
314 // > StringElement.value(variableName,value)
315 // Whether a value is set is defined by:
316 // > PrimitiveElement.valueSet(variableName,isFilled);
317
318 //////////
319 // 1.1.3 domain-specific Type Indexers
252 ////////// 320 //////////
253 «typeIndexer.generateInstanceOfQueries(problem,emptySolution,typeAnalysisResult)» 321 «typeIndexer.generateInstanceOfQueries(problem,emptySolution,typeAnalysisResult)»
254 322
255 ////////// 323 //////////
256 // 1.2 Relation Declaration Indexers 324 // 1.2 Relation Declaration Indexers
257 ////////// 325 //////////
258 «relationDeclarationIndexer.generateRelationIndexers(problem,problem.relations.filter(RelationDeclaration),fqn2PQuery)» 326 «relationDeclarationIndexer.generateRelationIndexers(problem,problem.relations.filter(RelationDeclaration),unitPropagationPatternGenerators,fqn2PQuery)»
259 327
260 ////////// 328 //////////
261 // 1.3 Relation Definition Indexers 329 // 1.3 Relation Definition Indexers
@@ -279,7 +347,7 @@ class PatternGenerator {
279 ////////// 347 //////////
280 // 3.1 Unfinishedness Measured by Multiplicity 348 // 3.1 Unfinishedness Measured by Multiplicity
281 ////////// 349 //////////
282 «unfinishedIndexer.generateUnfinishedMultiplicityQueries(problem,fqn2PQuery)» 350 «unfinishedIndexer.generateUnfinishedMultiplicityQueries(constraints.multiplicityConstraints,fqn2PQuery)»
283 351
284 ////////// 352 //////////
285 // 3.2 Unfinishedness Measured by WF Queries 353 // 3.2 Unfinishedness Measured by WF Queries
@@ -301,7 +369,24 @@ class PatternGenerator {
301 ////////// 369 //////////
302 // 4.3 Relation refinement 370 // 4.3 Relation refinement
303 ////////// 371 //////////
304 «relationRefinementGenerator.generateRefineReference(problem)» 372 «relationRefinementGenerator.generateRefineReference(problem, unitPropagationPatternGenerators)»
373
374 //////////
375 // 5 Hints
376 //////////
377 «FOR hint : hints»
378 «hint.getAdditionalPatterns(this, fqn2PQuery)»
379 «ENDFOR»
380 «FOR generator : unitPropagationPatternGenerators»
381 «generator.getAdditionalPatterns(this, fqn2PQuery)»
382 «ENDFOR»
383
384 //////////
385 // 6 Unit Propagations
386 //////////
305 ''' 387 '''
388 val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery)
389 val second = up.definitions
390 return new PatternGeneratorResult(first+second,up.constraint2MustPreconditionName,up.constraint2CurrentPreconditionName)
306 } 391 }
307} 392}
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 0e13a5e1..2e786286 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
@@ -1,97 +1,171 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns 1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
2 2
3import com.google.common.collect.ImmutableSet
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation 4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration 5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type 7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
6import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem 8import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics 10import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysis 11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysis
9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult 12import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult
10import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod 13import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
14import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
15import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraints
16import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationMultiplicityConstraint
17import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy
11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util.ParseUtil 18import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util.ParseUtil
12import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation 19import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
13import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace 20import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
21import java.util.Collection
22import java.util.HashMap
14import java.util.Map 23import java.util.Map
24import java.util.Set
15import org.eclipse.viatra.query.runtime.api.IPatternMatch 25import org.eclipse.viatra.query.runtime.api.IPatternMatch
16import org.eclipse.viatra.query.runtime.api.IQuerySpecification 26import org.eclipse.viatra.query.runtime.api.IQuerySpecification
17import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher 27import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
28import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
18import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery 29import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
19import org.eclipse.xtend.lib.annotations.Data 30import org.eclipse.xtend.lib.annotations.Data
20 31
21import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 32import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
22import java.util.Collection
23import java.util.Set
24 33
25@Data class GeneratedPatterns { 34@Data class GeneratedPatterns {
26 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries 35 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries
27 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries 36 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries
28 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedMulticiplicityQueries 37 public Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> multiplicityConstraintQueries
29 public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries 38 public IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery
30 public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries 39 public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries
31 public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries 40 public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries
41 public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineRelationQueries
42 public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustRelationPropagationQueries
43 public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns
44 public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns
45 public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries
32 public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries 46 public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries
33} 47}
34 48
49@Data
50class ModalPatternQueries {
51 val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mayQuery
52 val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mustQuery
53 val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> currentQuery
54}
55
56@Data
57class UnifinishedMultiplicityQueries {
58 val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingMultiplicityQuery
59 val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingInverseMultiplicityQuery
60
61 def Set<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> getAllQueries() {
62 val builder = ImmutableSet.builder
63 if (existingMultiplicityQuery !== null) {
64 builder.add(existingMultiplicityQuery)
65 }
66 if (existingInverseMultiplicityQuery !== null) {
67 builder.add(existingInverseMultiplicityQuery)
68 }
69 builder.build
70 }
71}
72
35class PatternProvider { 73class PatternProvider {
36
37 val TypeAnalysis typeAnalysis = new TypeAnalysis 74 val TypeAnalysis typeAnalysis = new TypeAnalysis
38 75
39 public def generateQueries( 76 def generateQueries(LogicProblem problem, PartialInterpretation emptySolution, ModelGenerationStatistics statistics,
40 LogicProblem problem, 77 Set<PQuery> existingQueries, ReasonerWorkspace workspace, TypeInferenceMethod typeInferenceMethod,
41 PartialInterpretation emptySolution, 78 ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints,
42 ModelGenerationStatistics statistics, 79 Collection<LinearTypeConstraintHint> hints,
43 Set<PQuery> existingQueries, 80 Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators, boolean writeToFile) {
44 ReasonerWorkspace workspace,
45 TypeInferenceMethod typeInferenceMethod,
46 boolean writeToFile)
47 {
48 val fqn2Query = existingQueries.toMap[it.fullyQualifiedName] 81 val fqn2Query = existingQueries.toMap[it.fullyQualifiedName]
49 val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod) 82 val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod, scopePropagatorStrategy)
50 val typeAnalysisResult = if(patternGenerator.requiresTypeAnalysis) { 83 val typeAnalysisResult = if (patternGenerator.requiresTypeAnalysis) {
51 val startTime = System.nanoTime 84 val startTime = System.nanoTime
52 val result = typeAnalysis.performTypeAnalysis(problem,emptySolution) 85 val result = typeAnalysis.performTypeAnalysis(problem, emptySolution)
53 val typeAnalysisTime = System.nanoTime - startTime 86 val typeAnalysisTime = System.nanoTime - startTime
54 statistics.PreliminaryTypeAnalisisTime = typeAnalysisTime 87 statistics.preliminaryTypeAnalisisTime = typeAnalysisTime
55 result 88 result
56 } else { 89 } else {
57 null 90 null
58 } 91 }
59 val baseIndexerFile = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) 92 val patternGeneratorResult = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query,
60 if(writeToFile) { 93 typeAnalysisResult, relationConstraints, hints, unitPropagationPatternGenerators)
61 workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile) 94 if (writeToFile) {
95 workspace.writeText('''generated3valued.vql_deactivated''', patternGeneratorResult.patternText)
62 } 96 }
63 val ParseUtil parseUtil = new ParseUtil 97 val ParseUtil parseUtil = new ParseUtil
64 val generatedQueries = parseUtil.parse(baseIndexerFile) 98 val generatedQueries = parseUtil.parse(patternGeneratorResult.patternText)
65 val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,generatedQueries); 99 val runtimeQueries = calclulateRuntimeQueries(patternGenerator, problem, emptySolution, typeAnalysisResult,
100 patternGeneratorResult.constraint2MustPreconditionName,
101 patternGeneratorResult.constraint2CurrentPreconditionName, relationConstraints,
102 unitPropagationPatternGenerators, generatedQueries)
66 return runtimeQueries 103 return runtimeQueries
67 } 104 }
68 105
69 private def GeneratedPatterns calclulateRuntimeQueries( 106 private def GeneratedPatterns calclulateRuntimeQueries(
70 PatternGenerator patternGenerator, 107 PatternGenerator patternGenerator,
71 LogicProblem problem, 108 LogicProblem problem,
72 PartialInterpretation emptySolution, 109 PartialInterpretation emptySolution,
73 TypeAnalysisResult typeAnalysisResult, 110 TypeAnalysisResult typeAnalysisResult,
74 Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries 111 HashMap<PConstraint, String> mustUnitPropagationTrace,
112 HashMap<PConstraint, String> currentUnitPropagationTrace,
113 RelationConstraints relationConstraints,
114 Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators,
115 Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries
75 ) { 116 ) {
76 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 117 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries = patternGenerator.
77 invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] 118 invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)]
78 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 119 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries = patternGenerator.
79 unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)] 120 unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)]
80 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 121
81 unfinishedMultiplicityQueries = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(problem).mapValues[it.lookup(queries)] 122 val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(
82 val Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 123 relationConstraints.multiplicityConstraints)
83 refineObjectsQueries = patternGenerator.typeRefinementGenerator.getRefineObjectQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] 124 val multiplicityConstraintQueries = unfinishedMultiplicities.mapValues [
84 val Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 125 new UnifinishedMultiplicityQueries(existingMultiplicityQueryName?.lookup(queries),
85 refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] 126 existingInverseMultiplicityQueryName?.lookup(queries))
86 val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 127 ]
87 refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] 128 val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup(
129 queries)
130
131 val Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectsQueries = patternGenerator.
132 typeRefinementGenerator.getRefineObjectQueryNames(problem, emptySolution, typeAnalysisResult).mapValues [
133 it.lookup(queries)
134 ]
135 val Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries = patternGenerator.
136 typeRefinementGenerator.getRefineTypeQueryNames(problem, emptySolution, typeAnalysisResult).mapValues [
137 it.lookup(queries)
138 ]
139 val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineRelationQueries = patternGenerator.
140 relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)]
141 val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustRelationPropagationQueries = patternGenerator.
142 relationRefinementGenerator.getMustPropagationQueries(problem, unitPropagationPatternGenerators).mapValues[it.lookup(queries)]
143 val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.
144 mapValues[it.lookup(queries)]
145 val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.
146 mapValues[it.lookup(queries)]
147
148 val modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition |
149 val indexer = patternGenerator.relationDefinitionIndexer
150 new ModalPatternQueries(
151 indexer.relationDefinitionName(relationDefinition, Modality.MAY).lookup(queries),
152 indexer.relationDefinitionName(relationDefinition, Modality.MUST).lookup(queries),
153 indexer.relationDefinitionName(relationDefinition, Modality.CURRENT).lookup(queries)
154 )
155 ])
156
88 return new GeneratedPatterns( 157 return new GeneratedPatterns(
89 invalidWFQueries, 158 invalidWFQueries,
90 unfinishedWFQueries, 159 unfinishedWFQueries,
91 unfinishedMultiplicityQueries, 160 multiplicityConstraintQueries,
161 hasElementInContainmentQuery,
92 refineObjectsQueries, 162 refineObjectsQueries,
93 refineTypeQueries, 163 refineTypeQueries,
94 refineRelationQueries, 164 refineRelationQueries,
165 mustRelationPropagationQueries,
166 mustUnitPropagationPreconditionPatterns,
167 currentUnitPropagationPreconditionPatterns,
168 modalRelationQueries,
95 queries.values 169 queries.values
96 ) 170 )
97 } 171 }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend
index f384cd50..23ba3cad 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend
@@ -1,10 +1,13 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns 1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
2 2
3import com.google.common.collect.ImmutableMap
4import com.google.common.collect.ImmutableSet
3import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion 5import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation 6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration 7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
6import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem 8import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality 9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
10import java.util.Collection
8import java.util.HashMap 11import java.util.HashMap
9import java.util.List 12import java.util.List
10import java.util.Map 13import java.util.Map
@@ -14,41 +17,40 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
14 17
15class RelationDeclarationIndexer { 18class RelationDeclarationIndexer {
16 val PatternGenerator base; 19 val PatternGenerator base;
17 20
18 new(PatternGenerator base) { 21 new(PatternGenerator base) {
19 this.base = base 22 this.base = base
20 } 23 }
21 24
22 public def generateRelationIndexers(LogicProblem problem, Iterable<RelationDeclaration> relations, Map<String,PQuery> fqn2PQuery) { 25 def generateRelationIndexers(LogicProblem problem, Iterable<RelationDeclaration> relations,
26 Iterable<UnitPropagationPatternGenerator> unitPropagationPatternGenerators, Map<String, PQuery> fqn2PQuery) {
23 val upperMultiplicities = new HashMap 27 val upperMultiplicities = new HashMap
24 problem.annotations.filter(UpperMultiplicityAssertion).forEach[ 28 problem.annotations.filter(UpperMultiplicityAssertion).forEach [
25 upperMultiplicities.put(it.relation,it.upper) 29 upperMultiplicities.put(it.relation, it.upper)
26 ] 30 ]
27 31 val mustNotRelations = ImmutableMap.copyOf(unitPropagationPatternGenerators.flatMap[mustNotPatterns.entrySet].
32 groupBy[key].mapValues[ImmutableSet.copyOf(map[value])])
33
28 return ''' 34 return '''
29 «FOR relation : relations» 35 «FOR relation : relations»
30 «IF base.isDerived(relation)» 36 «IF base.isDerived(relation)»
31 «generateDerivedMustRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))» 37 «generateDerivedMustRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))»
32 «generateDerivedMayRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))» 38 «generateDerivedMayRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))»
33 «ELSE» 39 «ELSE»
34 «generateMustRelation(problem,relation)» 40 «generateMustRelation(problem, relation)»
35 «generateMayRelation(problem,relation,upperMultiplicities,base.getContainments(problem),base.getInverseRelations(problem),fqn2PQuery)» 41 «generateMayRelation(problem, relation, upperMultiplicities, base.getContainments(problem), base.getInverseRelations(problem), mustNotRelations.get(relation) ?: emptySet, fqn2PQuery)»
36 «ENDIF» 42 «ENDIF»
37 «ENDFOR» 43 «ENDFOR»
38 ''' 44 '''
39 } 45 }
40 46
41 def private patternName(RelationDeclaration r, Modality modality) { 47 def private patternName(RelationDeclaration r, Modality modality) {
42 '''«modality.name.toLowerCase»InRelation«base.canonizeName(r.name)»''' 48 '''«modality.name.toLowerCase»InRelation«base.canonizeName(r.name)»'''
43 } 49 }
44 50
45 public def referRelation( 51 def referRelation(RelationDeclaration referred, String sourceVariable, String targetVariable,
46 RelationDeclaration referred, 52 Modality modality) '''find «referred.patternName(modality)»(problem,interpretation,«sourceVariable»,«targetVariable»);'''
47 String sourceVariable, 53
48 String targetVariable,
49 Modality modality)
50 '''find «referred.patternName(modality)»(problem,interpretation,«sourceVariable»,«targetVariable»);'''
51
52 def generateMustRelation(LogicProblem problem, RelationDeclaration relation) ''' 54 def generateMustRelation(LogicProblem problem, RelationDeclaration relation) '''
53 /** 55 /**
54 * Matcher for detecting tuples t where []«relation.name»(source,target) 56 * Matcher for detecting tuples t where []«relation.name»(source,target)
@@ -65,59 +67,64 @@ class RelationDeclarationIndexer {
65 BinaryElementRelationLink.param2(link,target); 67 BinaryElementRelationLink.param2(link,target);
66 } 68 }
67 ''' 69 '''
70
68 def generateMayRelation(LogicProblem problem, RelationDeclaration relation, 71 def generateMayRelation(LogicProblem problem, RelationDeclaration relation,
69 Map<Relation, Integer> upperMultiplicities, 72 Map<Relation, Integer> upperMultiplicities, List<Relation> containments,
70 List<Relation> containments, 73 HashMap<Relation, Relation> inverseRelations, Collection<String> mustNotRelations,
71 HashMap<Relation, Relation> inverseRelations, 74 Map<String, PQuery> fqn2PQuery) {
72 Map<String,PQuery> fqn2PQuery)
73 {
74 return ''' 75 return '''
75 /** 76 /**
76 * Matcher for detecting tuples t where <>«relation.name»(source,target) 77 * Matcher for detecting tuples t where <>«relation.name»(source,target)
77 */ 78 */
78 private pattern «relation.patternName(Modality.MAY)»( 79 private pattern «relation.patternName(Modality.MAY)»(
79 problem:LogicProblem, interpretation:PartialInterpretation, 80 problem:LogicProblem, interpretation:PartialInterpretation,
80 source: DefinedElement, target:DefinedElement) 81 source: DefinedElement, target:DefinedElement)
81 { 82 {
82 find interpretation(problem,interpretation); 83 find interpretation(problem,interpretation);
83 // The two endpoint of the link have to exist 84 // The two endpoint of the link have to exist
84 find mayExist(problem, interpretation, source); 85 find mayExist(problem, interpretation, source);
85 find mayExist(problem, interpretation, target); 86 find mayExist(problem, interpretation, target);
86 // Type consistency 87 // Type consistency
87 «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(0),Modality.MAY,"source")» 88 «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(0),Modality.MAY,"source")»
88 «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(1),Modality.MAY,"target")» 89 «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(1),Modality.MAY,"target")»
89 «IF upperMultiplicities.containsKey(relation)» 90 «IF upperMultiplicities.containsKey(relation)»
90 // There are "numberOfExistingReferences" currently existing instances of the reference from the source, 91 // There are "numberOfExistingReferences" currently existing instances of the reference from the source,
91 // the upper bound of the multiplicity should be considered. 92 // the upper bound of the multiplicity should be considered.
92 numberOfExistingReferences == count «referRelation(relation,"source","_",Modality.MUST)» 93 numberOfExistingReferences == count «referRelation(relation,"source","_",Modality.MUST)»
93 check(numberOfExistingReferences < «upperMultiplicities.get(relation)»); 94 numberOfExistingReferences != «upperMultiplicities.get(relation)»;
94 «ENDIF» 95 «ENDIF»
95 «IF inverseRelations.containsKey(relation) && upperMultiplicities.containsKey(inverseRelations.get(relation))» 96 «IF inverseRelations.containsKey(relation) && upperMultiplicities.containsKey(inverseRelations.get(relation))»
96 // There are "numberOfExistingReferences" currently existing instances of the reference to the target, 97 // There are "numberOfExistingReferences" currently existing instances of the reference to the target,
97 // the upper bound of the opposite reference multiplicity should be considered. 98 // the upper bound of the opposite reference multiplicity should be considered.
98 numberOfExistingOppositeReferences == count «base.referRelation(inverseRelations.get(relation),"target","_",Modality.MUST,fqn2PQuery)» 99 numberOfExistingOppositeReferences == count «base.referRelation(inverseRelations.get(relation),"target","_",Modality.MUST,fqn2PQuery)»
99 check(numberOfExistingOppositeReferences < «upperMultiplicities.get(inverseRelations.get(relation))»); 100 numberOfExistingOppositeReferences != «upperMultiplicities.get(inverseRelations.get(relation))»;
100 «ENDIF» 101 «ENDIF»
101 «IF containments.contains(relation)» 102 «IF containments.contains(relation)»
102 // The reference is containment, then a new reference cannot be create if: 103 // The reference is containment, then a new reference cannot be create if:
103 // 1. Multiple parents 104 // 1. Multiple parents
104 neg «base.containmentIndexer.referMustContaint("_","target")» 105 neg «base.containmentIndexer.referMustContaint("_","target")»
105 // 2. Circle in the containment hierarchy 106 // 2. Circle in the containment hierarchy
106 neg «base.containmentIndexer.referTransitiveMustContains("target","source")» 107 neg «base.containmentIndexer.referTransitiveMustContains("target","source")»
107 «ENDIF» 108 «ENDIF»
108 «IF inverseRelations.containsKey(relation) && containments.contains(inverseRelations.get(relation))» 109 «IF inverseRelations.containsKey(relation) && containments.contains(inverseRelations.get(relation))»
109 // The eOpposite of the reference is containment, then a referene cannot be created if 110 // The eOpposite of the reference is containment, then a referene cannot be created if
110 // 1. Multiple parents 111 // 1. Multiple parents
111 neg «base.containmentIndexer.referMustContaint("source","_")» 112 neg «base.containmentIndexer.referMustContaint("source","_")»
112 // 2. Circle in the containment hierarchy 113 // 2. Circle in the containment hierarchy
113 neg «base.containmentIndexer.referTransitiveMustContains("source","target")» 114 neg «base.containmentIndexer.referTransitiveMustContains("source","target")»
114 «ENDIF» 115 «ENDIF»
115 } or { 116 «IF !mustNotRelations.empty»
116 «relation.referRelation("source","target",Modality.MUST)» 117 // ![] unit propagation relations
117 } 118 «FOR mustNotRelation : mustNotRelations»
118 ''' 119 neg find «mustNotRelation»(problem, interpretation, source, target);
120 «ENDFOR»
121 «ENDIF»
122 } or {
123 «relation.referRelation("source","target",Modality.MUST)»
124 }
125 '''
119 } 126 }
120 127
121 def generateDerivedMustRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) ''' 128 def generateDerivedMustRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) '''
122 /** 129 /**
123 * Matcher for detecting tuples t where []«relation.name»(source,target) 130 * Matcher for detecting tuples t where []«relation.name»(source,target)
@@ -129,6 +136,7 @@ class RelationDeclarationIndexer {
129 «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MUST,true,false)» 136 «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MUST,true,false)»
130 } 137 }
131 ''' 138 '''
139
132 def generateDerivedMayRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) ''' 140 def generateDerivedMayRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) '''
133 /** 141 /**
134 * Matcher for detecting tuples t where []«relation.name»(source,target) 142 * Matcher for detecting tuples t where []«relation.name»(source,target)
@@ -140,4 +148,4 @@ class RelationDeclarationIndexer {
140 «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MAY,true,false)» 148 «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MAY,true,false)»
141 } 149 }
142 ''' 150 '''
143} \ No newline at end of file 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 9723373f..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
@@ -5,38 +5,27 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
5import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery 5import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality 6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
7import java.util.Map 7import java.util.Map
8import org.eclipse.emf.ecore.EAttribute
9import org.eclipse.emf.ecore.EEnumLiteral
10import org.eclipse.emf.ecore.EReference
11import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
12import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
13import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey
14import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
15import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable 8import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
16import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality
17import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter
18import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality
19import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
20import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure 9import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure
21import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue 10import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction
22import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall
23import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint
24import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery 11import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
25 12
26import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 13import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
27import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint
28 14
29class RelationDefinitionIndexer { 15class RelationDefinitionIndexer {
30 val PatternGenerator base; 16 public val PatternGenerator base;
17 val PConstraintTransformer constraintTransformer;
31 18
32 new(PatternGenerator base) { 19 new(PatternGenerator base) {
33 this.base = base 20 this.base = base
21 this.constraintTransformer = new PConstraintTransformer(this);
34 } 22 }
35 23
36 public def generateRelationDefinitions( 24 def generateRelationDefinitions(
37 LogicProblem problem, 25 LogicProblem problem,
38 Iterable<RelationDefinition> relations, 26 Iterable<RelationDefinition> relations,
39 Map<String,PQuery> fqn2PQuery) { 27 Map<String,PQuery> fqn2PQuery)
28 {
40 val relation2PQuery = relations.toInvertedMap[ 29 val relation2PQuery = relations.toInvertedMap[
41 annotations.filter(TransfomedViatraQuery).head.patternFullyQualifiedName.lookup(fqn2PQuery) 30 annotations.filter(TransfomedViatraQuery).head.patternFullyQualifiedName.lookup(fqn2PQuery)
42 ] 31 ]
@@ -71,23 +60,24 @@ class RelationDefinitionIndexer {
71 ] 60 ]
72 } 61 }
73 62
74 private def relationDefinitionName(RelationDefinition relation, Modality modality) 63 def String relationDefinitionName(RelationDefinition relation, Modality modality)
75 '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»''' 64 '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»'''
76 65
77 private def canonizeName(PVariable v) { 66 def canonizeName(PVariable v) {
78 return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»''' 67 return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»'''
79 } 68 }
80 69
81 private def transformPattern(RelationDefinition relation, PQuery p, Modality modality) { 70 private def transformPattern(RelationDefinition relation, PQuery p, Modality modality) {
82 try { 71 try {
72 val bodies = (relation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies
83 return ''' 73 return '''
84 private pattern «relationDefinitionName(relation,modality)»( 74 private pattern «relationDefinitionName(relation,modality)»(
85 problem:LogicProblem, interpretation:PartialInterpretation, 75 problem:LogicProblem, interpretation:PartialInterpretation,
86 «FOR param : p.parameters SEPARATOR ', '»var_«param.name»«ENDFOR») 76 «FOR param : p.parameters SEPARATOR ', '»var_«param.name»«ENDFOR»)
87 «FOR body : p.disjunctBodies.bodies SEPARATOR "or"»{ 77 «FOR body : bodies SEPARATOR "or"»{
88 find interpretation(problem,interpretation); 78 find interpretation(problem,interpretation);
89 «FOR constraint : body.constraints» 79 «FOR constraint : body.constraints»
90 «constraint.transformConstraint(modality)» 80 «this.constraintTransformer.transformConstraint(constraint,modality,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
91 «ENDFOR» 81 «ENDFOR»
92 }«ENDFOR» 82 }«ENDFOR»
93 ''' 83 '''
@@ -104,158 +94,12 @@ class RelationDefinitionIndexer {
104 ''' 94 '''
105 } 95 }
106 96
107 private def toMustMay(Modality modality) { 97 def toMustMay(Modality modality) {
108 if(modality == Modality::MAY) return Modality::MAY 98 if(modality == Modality::MAY) return Modality::MAY
109 else return Modality::MUST 99 else return Modality::MUST
110 } 100 }
111 101
112 def public referPattern(PQuery p, String[] variables, Modality modality, boolean positive, boolean transitive) ''' 102 def referPattern(PQuery p, String[] variables, Modality modality, boolean positive, boolean transitive) '''
113 «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(',')»);
114 ''' 104 '''
115
116 private dispatch def transformConstraint(TypeConstraint constraint, Modality modality) {
117 val touple = constraint.variablesTuple
118 if(touple.size == 1) {
119 val inputKey = constraint.equivalentJudgement.inputKey
120 if(inputKey instanceof EClassTransitiveInstancesKey) {
121 return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,
122 constraint.getVariableInTuple(0).canonizeName)
123 } else if(inputKey instanceof EDataTypeInSlotsKey){
124 return '''// type constraint is enforced by construction'''
125 }
126
127 } else if(touple.size == 2){
128 val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey
129 if(key instanceof EReference) {
130 return base.referRelationByName(
131 key,
132 constraint.getVariableInTuple(0).canonizeName,
133 constraint.getVariableInTuple(1).canonizeName,
134 modality.toMustMay)
135 } else if (key instanceof EAttribute) {
136 return base.referAttributeByName(key,
137 constraint.getVariableInTuple(0).canonizeName,
138 constraint.getVariableInTuple(1).canonizeName,
139 modality.toMustMay)
140 } else throw new UnsupportedOperationException('''unknown key: «key.class»''')
141 } else {
142 throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
143 }
144 }
145 private dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality) {
146 val touple = constraint.variablesTuple
147 if(touple.size == 1) {
148 val inputKey = constraint.equivalentJudgement.inputKey
149 if(inputKey instanceof EClassTransitiveInstancesKey) {
150 return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,
151 (constraint.getVariablesTuple.get(0) as PVariable).canonizeName)
152 } else if(inputKey instanceof EDataTypeInSlotsKey){
153 return '''// type constraint is enforced by construction'''
154 }
155
156 } else if(touple.size == 2){
157 val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey
158 if(key instanceof EReference) {
159 return base.referRelationByName(
160 key,
161 (constraint.getVariablesTuple.get(0) as PVariable).canonizeName,
162 (constraint.getVariablesTuple.get(1) as PVariable).canonizeName,
163 modality.toMustMay)
164 } else if (key instanceof EAttribute) {
165 return base.referAttributeByName(key,
166 (constraint.getVariablesTuple.get(0) as PVariable).canonizeName,
167 (constraint.getVariablesTuple.get(1) as PVariable).canonizeName,
168 modality.toMustMay)
169 } else throw new UnsupportedOperationException('''unknown key: «key.class»''')
170 } else {
171 throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
172 }
173 }
174
175 private dispatch def transformConstraint(Equality equality, Modality modality) {
176 val a = equality.who
177 val b = equality.withWhom
178 transformEquality(modality.toMustMay, a, b)
179 }
180
181 private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) {
182 if(modality.isMustOrCurrent) '''find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
183 else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
184 }
185
186 private dispatch def transformConstraint(Inequality inequality, Modality modality) {
187 val a = inequality.who
188 val b = inequality.withWhom
189 if(modality.isCurrent) {
190 return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
191 } else if(modality.isMust) {
192 return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
193 } else { // modality.isMay
194 return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
195 }
196 }
197
198 private dispatch def transformConstraint(NegativePatternCall pcall, Modality modality) {
199 val params = (0..<pcall.actualParametersTuple.size).map[index |
200 val variable = pcall.actualParametersTuple.get(index) as PVariable
201 return variable.canonizeName
202 ]
203 return referPattern(pcall.referredQuery,params,modality.dual,false,false)
204 }
205
206 private dispatch def transformConstraint(PositivePatternCall pcall, Modality modality) {
207 val params = (0..<pcall.variablesTuple.size).map[index |
208 val variable = pcall.variablesTuple.get(index) as PVariable
209 return variable.canonizeName
210 ]
211 return referPattern(pcall.referredQuery,params,modality,true,false)
212 }
213 private dispatch def transformConstraint(BinaryTransitiveClosure pcall, Modality modality) {
214 val params = (0..1).map[index |
215 val variable = pcall.getVariableInTuple(index) as PVariable
216 return variable.canonizeName
217 ]
218 return referPattern(pcall.referredQuery,params,modality,true,true)
219 }
220 private dispatch def transformConstraint(ExportedParameter e, Modality modality) {
221 return '''// «e.parameterName» is exported'''
222 }
223 private dispatch def transformConstraint(ConstantValue c, Modality modality) {
224 val target = c.supplierKey
225
226 var String targetString;
227 var String additionalDefinition;
228 if(target instanceof EEnumLiteral) {
229 targetString = '''const_«target.name»_«target.EEnum.name»'''
230 additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» «target.EEnum.name»"); //LogicProblem.elements(problem,«targetString»);'''
231 } else if(target instanceof Integer) {
232 targetString = '''const_«target»_Integer'''
233 additionalDefinition = '''IntegerElement.value(«targetString»,«target»);'''
234 } else if(target instanceof Boolean) {
235 targetString = '''const_«target»_Boolean'''
236 additionalDefinition = '''BooleanElement.value(«targetString»,«target»);'''
237 } else if(target instanceof String) {
238 targetString = '''const_«target»_String'''
239 additionalDefinition = '''StringElement.value(«targetString»,"«target»");'''
240 } else if(target instanceof Double) {
241 targetString = '''const_«target»_Number'''
242 additionalDefinition = '''RealElement.value(«targetString»,"«target»");'''
243 } else if(target instanceof Float) {
244 targetString = '''const_«target»_Number'''
245 additionalDefinition = '''RealElement.value(«targetString»,"«target»");'''
246 } else {
247 throw new UnsupportedOperationException('''Unknown constant type: «target.class»''')
248 }
249
250 val source = c.variablesTuple
251 var String sourceName
252 if(source.size == 1)
253 sourceName = (source.get(0) as PVariable).canonizeName
254 else throw new UnsupportedOperationException("unknown source")
255 return '''«sourceName» == «targetString»;«additionalDefinition»''';
256 }
257
258 private dispatch def transformConstraint(PConstraint c, Modality modality) {
259 throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''')
260 }
261} \ 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..6f5f2402 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
@@ -1,85 +1,93 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns 1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
2 2
3import com.google.common.collect.ImmutableList
4import com.google.common.collect.ImmutableMap
5import com.google.common.collect.ImmutableSet
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation 6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration 7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
5import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem 8import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality 9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
10import java.util.Collection
7import java.util.LinkedList 11import java.util.LinkedList
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference 12import java.util.Map
13import java.util.Set
14import org.eclipse.xtend2.lib.StringConcatenationClient
9 15
10class RelationRefinementGenerator { 16class RelationRefinementGenerator {
11 PatternGenerator base; 17 PatternGenerator base;
12 public new(PatternGenerator base) { 18
19 new(PatternGenerator base) {
13 this.base = base 20 this.base = base
14 } 21 }
15 22
16 def CharSequence generateRefineReference(LogicProblem p) { 23 def CharSequence generateRefineReference(LogicProblem p,
17 return ''' 24 Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) {
18 «FOR relationRefinement: this.getRelationRefinements(p)» 25 val mustRelations = getMustRelations(unitPropagationPatternGenerators)
19 pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»( 26
20 problem:LogicProblem, interpretation:PartialInterpretation, 27 '''
21 relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value != null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», 28 «FOR relationRefinement : this.getRelationRefinements(p)»
22 from: DefinedElement, to: DefinedElement) 29 pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»(
23 { 30 problem:LogicProblem, interpretation:PartialInterpretation,
24 find interpretation(problem,interpretation); 31 relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF»,
25 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); 32 from: DefinedElement, to: DefinedElement)
26 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»"); 33 {
27 «IF relationRefinement.value != null» 34 find interpretation(problem,interpretation);
28 PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation); 35 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
29 PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»"); 36 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»");
30 «ENDIF» 37 «IF relationRefinement.value !== null»
31 find mustExist(problem, interpretation, from); 38 PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation);
32 find mustExist(problem, interpretation, to); 39 PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»");
33 «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")» 40 «ENDIF»
34 «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")» 41 find mustExist(problem, interpretation, from);
35 «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)» 42 find mustExist(problem, interpretation, to);
36 neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)» 43 «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")»
37 } 44 «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")»
38 «ENDFOR» 45 «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)»
46 neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)»
47 }
48
49 «IF isMustPropagationQueryNeeded(relationRefinement.key, relationRefinement.value, mustRelations)»
50 pattern «mustPropagationQueryName(relationRefinement.key)»(
51 problem:LogicProblem, interpretation:PartialInterpretation,
52 relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF»,
53 from: DefinedElement, to: DefinedElement)
54 «FOR body : getMustPropagationBodies(relationRefinement.key, relationRefinement.value, mustRelations) SEPARATOR " or "»
55 {
56 «referRefinementQuery(relationRefinement.key, relationRefinement.value, "relationIterpretation", "oppositeInterpretation", "from", "to")»
57 «body»
58 }
59 «ENDFOR»
60 «ENDIF»
61 «ENDFOR»
39 ''' 62 '''
40 } 63 }
41 64
42 def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) { 65 def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) {
43 '''«IF inverseRelation != null 66 '''«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 } 67 }
48 68
69 def String mustPropagationQueryName(RelationDeclaration relation) {
70 '''mustPropagation_«base.canonizeName(relation.name)»'''
71 }
72
49 def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName, 73 def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName,
50 String inverseInterpretationName, String sourceName, String targetName) 74 String inverseInterpretationName, String sourceName,
51 '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation != null»inverseInterpretationName, «ENDIF»«sourceName», «targetName»);''' 75 String targetName) '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation !== null»«inverseInterpretationName», «ENDIF»«sourceName», «targetName»);'''
52 76
53 def getRefineRelationQueries(LogicProblem p) { 77 def getRefineRelationQueries(LogicProblem p) {
54// val containmentRelations = p.containmentHierarchies.map[containmentRelations].flatten.toSet 78 getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key, it.value)]
55// p.relations.filter(RelationDeclaration).filter[!containmentRelations.contains(it)].toInvertedMap['''refineRelation_«base.canonizeName(it.name)»''']
56 /*
57 val res = new LinkedHashMap
58 for(relation: getRelationRefinements(p)) {
59 if(inverseRelations.containsKey(relation)) {
60 val name = '''refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelations.get(relation).name)»'''
61 res.put(relation -> inverseRelations.get(relation),name)
62 } else {
63 val name = '''refineRelation_«base.canonizeName(relation.name)»'''
64 res.put(relation -> null,name)
65 }
66 }
67 return res*/
68
69 getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key,it.value)]
70 } 79 }
71
72 80
73 def getRelationRefinements(LogicProblem p) { 81 def getRelationRefinements(LogicProblem p) {
74 val inverses = base.getInverseRelations(p) 82 val inverses = base.getInverseRelations(p)
75 val containments = base.getContainments(p) 83 val containments = base.getContainments(p)
76 val list = new LinkedList 84 val list = new LinkedList
77 for(relation : p.relations.filter(RelationDeclaration)) { 85 for (relation : p.relations.filter(RelationDeclaration)) {
78 if(!containments.contains(relation)) { 86 if (!containments.contains(relation)) {
79 if(inverses.containsKey(relation)) { 87 if (inverses.containsKey(relation)) {
80 val inverse = inverses.get(relation) 88 val inverse = inverses.get(relation)
81 if(!containments.contains(inverse)) { 89 if (!containments.contains(inverse)) {
82 if(base.isRepresentative(relation,inverse)) { 90 if (base.isRepresentative(relation, inverse)) {
83 list += (relation -> inverse) 91 list += (relation -> inverse)
84 } 92 }
85 } 93 }
@@ -90,4 +98,54 @@ class RelationRefinementGenerator {
90 } 98 }
91 return list 99 return list
92 } 100 }
93} \ No newline at end of file 101
102 def getMustPropagationQueries(LogicProblem p,
103 Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) {
104 val refinements = getRelationRefinements(p)
105 val mustRelations = getMustRelations(unitPropagationPatternGenerators)
106 refinements.filter[isMustPropagationQueryNeeded(key, value, mustRelations)].toInvertedMap [
107 mustPropagationQueryName(key)
108 ]
109 }
110
111 private def getMustRelations(Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) {
112 ImmutableMap.copyOf(unitPropagationPatternGenerators.flatMap[mustPatterns.entrySet].groupBy[key].mapValues [
113 ImmutableSet.copyOf(map[value])
114 ])
115 }
116
117 private def isMustPropagationQueryNeeded(Relation relation, Relation inverseRelation,
118 Map<Relation, ? extends Set<String>> mustRelations) {
119 val mustSet = mustRelations.get(relation)
120 if (mustSet !== null && !mustSet.empty) {
121 return true
122 }
123 if (inverseRelation !== null) {
124 val inverseMustSet = mustRelations.get(inverseRelation)
125 if (inverseMustSet !== null && !inverseMustSet.empty) {
126 return true
127 }
128 }
129 false
130 }
131
132 private def getMustPropagationBodies(Relation relation, Relation inverseRelation,
133 Map<Relation, ? extends Set<String>> mustRelations) {
134 val builder = ImmutableList.<StringConcatenationClient>builder()
135 val mustSet = mustRelations.get(relation)
136 if (mustSet !== null) {
137 for (refinementQuery : mustSet) {
138 builder.add('''find «refinementQuery»(problem, interpretation, from, to);''')
139 }
140 }
141 if (inverseRelation !== null && inverseRelation != relation) {
142 val inverseMustSet = mustRelations.get(inverseRelation)
143 if (inverseMustSet !== null) {
144 for (refinementQuery : inverseMustSet) {
145 builder.add('''find «refinementQuery»(problem, interpretation, to, from);''')
146 }
147 }
148 }
149 builder.build
150 }
151}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend
index d1d57189..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,52 +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 121
52} \ No newline at end of file 122 def CharSequence referPrimitiveFilled(String variableName, boolean isFilled) {
123 '''PrimitiveElement.valueSet(«variableName»,«isFilled»);'''
124 }
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 ad1c9033..65ad3d48 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,149 @@
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 existingMultiplicityQueryName
18 val String existingInverseMultiplicityQueryName
19}
13 20
14class UnfinishedIndexer { 21class UnfinishedIndexer {
15 val PatternGenerator base 22 val PatternGenerator base
16 23 val boolean indexUpperMultiplicities
17 new(PatternGenerator patternGenerator) { 24
25 new(PatternGenerator patternGenerator, boolean indexUpperMultiplicities) {
18 this.base = patternGenerator 26 this.base = patternGenerator
27 this.indexUpperMultiplicities = indexUpperMultiplicities
19 } 28 }
20 29
21 def generateUnfinishedWfQueries(LogicProblem problem, Map<String,PQuery> fqn2PQuery) { 30 def generateUnfinishedWfQueries(LogicProblem problem, Map<String, PQuery> fqn2PQuery) {
22 val wfQueries = base.wfQueries(problem) 31 val wfQueries = base.wfQueries(problem)
23 ''' 32 '''
24 «FOR wfQuery: wfQueries» 33 «FOR wfQuery : wfQueries»
25 pattern unfinishedBy_«base.canonizeName(wfQuery.target.name)»(problem:LogicProblem, interpretation:PartialInterpretation, 34 pattern unfinishedBy_«base.canonizeName(wfQuery.target.name)»(problem:LogicProblem, interpretation:PartialInterpretation,
26 «FOR param : wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters SEPARATOR ', '»var_«param.name»«ENDFOR») 35 «FOR param : wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters SEPARATOR ', '»var_«param.name»«ENDFOR»)
27 { 36 {
28 «base.relationDefinitionIndexer.referPattern( 37 «base.relationDefinitionIndexer.referPattern(
29 wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery), 38 wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery),
30 wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters.map['''var_«it.name»'''], 39 wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters.map['''var_«it.name»'''],
31 Modality.CURRENT, 40 Modality.CURRENT,
32 true,false)» 41 true,false)»
33 } 42 }
34 «ENDFOR» 43 «ENDFOR»
35 ''' 44 '''
36 } 45 }
46
37 def getUnfinishedWFQueryNames(LogicProblem problem) { 47 def getUnfinishedWFQueryNames(LogicProblem problem) {
38 val wfQueries = base.wfQueries(problem) 48 val wfQueries = base.wfQueries(problem)
39 val map = new LinkedHashMap 49 val map = new LinkedHashMap
40 for(wfQuery : wfQueries) { 50 for (wfQuery : wfQueries) {
41 map.put(wfQuery.target,'''unfinishedBy_«base.canonizeName(wfQuery.target.name)»''') 51 map.put(wfQuery.target, '''unfinishedBy_«base.canonizeName(wfQuery.target.name)»''')
42 } 52 }
43 return map 53 return map
44 } 54 }
45 def generateUnfinishedMultiplicityQueries(LogicProblem problem, Map<String,PQuery> fqn2PQuery) { 55
46 val lowerMultiplicities = base.lowerMultiplicities(problem) 56 def generateUnfinishedMultiplicityQueries(List<RelationMultiplicityConstraint> constraints,
47 return ''' 57 Map<String, PQuery> fqn2PQuery) '''
48 «FOR lowerMultiplicity : lowerMultiplicities» 58 «FOR constraint : constraints»
49 pattern «unfinishedMultiplicityName(lowerMultiplicity)»(problem:LogicProblem, interpretation:PartialInterpretation, relationIterpretation:PartialRelationInterpretation, object:DefinedElement,missingMultiplicity) { 59 «IF constraint.shouldIndexExistingMultiplicites(indexUpperMultiplicities)»
50 find interpretation(problem,interpretation); 60 private pattern «existingMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, numberOfExistingReferences:java Integer«IF constraint.shouldIndexRepairMultiplcities(indexUpperMultiplicities)», numberOfRepairMatches: java Integer«ENDIF») {
51 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); 61 find interpretation(problem,interpretation);
52 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«lowerMultiplicity.relation.name»"); 62 find mustExist(problem,interpretation,object);
53 «base.typeIndexer.referInstanceOf(lowerMultiplicity.firstParamTypeOfRelation,Modality::MUST,"object")» 63 «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")»
54 numberOfExistingReferences == count «base.referRelation(lowerMultiplicity.relation,"object","_",Modality.MUST,fqn2PQuery)» 64 numberOfExistingReferences == count «base.referRelation(constraint.relation,"object","_",Modality.MUST,fqn2PQuery)»
55 check(numberOfExistingReferences < «lowerMultiplicity.lower»); 65 «IF constraint.shouldIndexRepairMultiplcities(indexUpperMultiplicities)»
56 missingMultiplicity == eval(«lowerMultiplicity.lower»-numberOfExistingReferences); 66 numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _);
57 } 67 «ENDIF»
68 }
69 «ENDIF»
70
71 «IF constraint.shouldIndexRepairMatches(indexUpperMultiplicities)»
72 private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) {
73 «IF constraint.containment || constraint.container»
74 «repairMatchFallback(constraint, fqn2PQuery)»
75 «ELSEIF base.isRepresentative(constraint.relation, constraint.inverseRelation) && constraint.relation instanceof RelationDeclaration»
76 «base.relationRefinementGenerator.referRefinementQuery(constraint.relation as RelationDeclaration, constraint.inverseRelation, "_", "_", "source", "target")»
77 «ELSEIF base.isRepresentative(constraint.inverseRelation, constraint.relation) && constraint.inverseRelation instanceof RelationDeclaration»
78 «base.relationRefinementGenerator.referRefinementQuery(constraint.inverseRelation as RelationDeclaration, constraint.relation, "_", "_", "target", "source")»
79 «ELSE»
80 «repairMatchFallback(constraint, fqn2PQuery)»
81 «ENDIF»
82 }
83 «ENDIF»
84
85 «IF constraint.shouldIndexInverseMultiplicites(indexUpperMultiplicities)»
86 private pattern «existingInverseMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, numberOfExistingReferences:java Integer, numberOfRepairMatches: java Integer) {
87 find interpretation(problem,interpretation);
88 find mustExist(problem,interpretation,object);
89 «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"object")»
90 numberOfExistingReferences == count «base.referRelation(constraint.relation,"_","object",Modality.MUST,fqn2PQuery)»
91 numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, _, object);
92 }
93 «ENDIF»
58 «ENDFOR» 94 «ENDFOR»
59 ''' 95 '''
96
97 private def repairMatchFallback(RelationMultiplicityConstraint constraint, Map<String, PQuery> fqn2PQuery) '''
98 find interpretation(problem,interpretation);
99 find mustExist(problem,interpretation,source);
100 «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"source")»
101 find mustExist(problem,interpretation,target);
102 «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"target")»
103 neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)»
104 «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)»
105 '''
106
107 def String existingMultiplicityName(
108 RelationMultiplicityConstraint constraint) '''existingMultiplicity_«base.canonizeName(constraint.relation.name)»'''
109
110 def String existingInverseMultiplicityName(
111 RelationMultiplicityConstraint constraint) '''existingInverseMultiplicity_«base.canonizeName(constraint.relation.name)»'''
112
113 private def String repairMatchName(
114 RelationMultiplicityConstraint constraint) '''repair_«base.canonizeName(constraint.relation.name)»'''
115
116 def getUnfinishedMultiplicityQueries(List<RelationMultiplicityConstraint> constraints) {
117 constraints.toInvertedMap [ constraint |
118 new UnifinishedMultiplicityQueryNames(
119 if (constraint.shouldIndexExistingMultiplicites(indexUpperMultiplicities)) {
120 existingMultiplicityName(constraint)
121 } else {
122 null
123 },
124 if (constraint.shouldIndexInverseMultiplicites(indexUpperMultiplicities)) {
125 existingInverseMultiplicityName(constraint)
126 } else {
127 null
128 }
129 )
130 ]
60 } 131 }
61 def String unfinishedMultiplicityName(LowerMultiplicityAssertion lowerMultiplicityAssertion) 132
62 '''unfinishedLowerMultiplicity_«base.canonizeName(lowerMultiplicityAssertion.relation.name)»''' 133 static def shouldIndexExistingMultiplicites(RelationMultiplicityConstraint it, boolean indexUpperMultiplicities) {
63 134 constrainsUnfinished || (indexUpperMultiplicities && constrainsRemainingContents)
64 def public referUnfinishedMultiplicityQuery(LowerMultiplicityAssertion lowerMultiplicityAssertion)
65 '''find «unfinishedMultiplicityName(lowerMultiplicityAssertion)»(problem, interpretation ,object, missingMultiplicity);'''
66
67 def getFirstParamTypeOfRelation(LowerMultiplicityAssertion lowerMultiplicityAssertion) {
68 val parameters = lowerMultiplicityAssertion.relation.parameters
69 if(parameters.size == 2) {
70 val firstParam = parameters.get(0)
71 if(firstParam instanceof ComplexTypeReference) {
72 return firstParam.referred
73 }
74 }
75 } 135 }
76 136
77 def getUnfinishedMultiplicityQueries(LogicProblem problem) { 137 static def shouldIndexRepairMultiplcities(RelationMultiplicityConstraint it, boolean indexUpperMultiplicities) {
78 val lowerMultiplicities = base.lowerMultiplicities(problem) 138 shouldIndexExistingMultiplicites(indexUpperMultiplicities) && constrainsUnrepairable
79 val map = new LinkedHashMap 139 }
80 for(lowerMultiplicity : lowerMultiplicities) { 140
81 map.put(lowerMultiplicity.relation,unfinishedMultiplicityName(lowerMultiplicity)) 141 static def shouldIndexInverseMultiplicites(RelationMultiplicityConstraint it, boolean indexUpperMultiplicities) {
82 } 142 indexUpperMultiplicities && constrainsRemainingInverse
83 return map 143 }
144
145 static def shouldIndexRepairMatches(RelationMultiplicityConstraint it, boolean indexUpperMultiplicities) {
146 shouldIndexRepairMultiplcities(indexUpperMultiplicities) ||
147 shouldIndexInverseMultiplicites(indexUpperMultiplicities)
84 } 148 }
85} 149}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend
new file mode 100644
index 00000000..400f47bc
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend
@@ -0,0 +1,302 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
5import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
6import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.PropagationModality
9import java.util.Map
10import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
11import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
12import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
13import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
14
15import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
16import java.util.LinkedList
17import java.util.List
18import org.eclipse.xtend.lib.annotations.Data
19import java.util.HashMap
20import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall
21import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
22import java.util.Comparator
23import java.util.ArrayList
24import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction
25import java.util.LinkedHashSet
26
27@Data class UnitPropagation {
28 val PQuery q
29 val PConstraint c
30 val PropagationModality pm
31 val Modality m3
32}
33@Data
34class UnitPropagationPreconditionGenerationResult {
35 List<CharSequence> definitions= new LinkedList
36 Map<UnitPropagation,String> unitPropagation2PatternName = new HashMap
37 Map<PConstraint,String> constraintOccurence2Name = new HashMap
38
39 def registerQuery(PQuery q, PConstraint c, PropagationModality pm, Modality m3, String patternName, CharSequence definition) {
40 val key = new UnitPropagation(q,c,pm,m3)
41 definitions += definition
42 unitPropagation2PatternName.put(key,patternName)
43 }
44 def registerUnsatQuery(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
45 val key = new UnitPropagation(q,c,pm,m3)
46 unitPropagation2PatternName.put(key,null)
47 }
48 def contains(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
49 val key = new UnitPropagation(q,c,pm,m3)
50 return unitPropagation2PatternName.containsKey(key)
51 }
52 def getName(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
53 val key = new UnitPropagation(q,c,pm,m3)
54 return key.lookup(unitPropagation2PatternName)
55 }
56 def isDefined(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
57 val key = new UnitPropagation(q,c,pm,m3)
58 return unitPropagation2PatternName.get(key) !== null
59 }
60}
61@Data
62class UnitPropagationPreconditionFinalResult {
63 CharSequence definitions
64 HashMap<PConstraint,String> constraint2MustPreconditionName
65 HashMap<PConstraint,String> constraint2CurrentPreconditionName
66}
67
68class UnitPropagationPreconditionGenerator {
69 val PatternGenerator base
70 val PConstraintTransformer constraintTransformer;
71
72 new(PatternGenerator patternGenerator) {
73 this.base = patternGenerator
74 this.constraintTransformer = new PConstraintTransformer(base.relationDefinitionIndexer)
75 }
76
77 def generateUnitPropagationRules(
78 LogicProblem problem,
79 Iterable<RelationDefinition> relations,
80 Map<String,PQuery> fqn2PQuery)
81 {
82 // Create an empty result
83 val res = new UnitPropagationPreconditionGenerationResult
84 val wfs = base.wfQueries(problem)//.map[it.patternPQuery]
85 val Map<PConstraint,List<Pair<String,Integer>>> mainMustPropagationNames = new HashMap
86 val Map<PConstraint,List<Pair<String,Integer>>> mainCurrentPropagationNames = new HashMap
87 for(wf : wfs) {
88 val query = wf.patternPQuery as PQuery
89 val relation = wf.target
90 val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation)
91
92 for(referredCheck : allReferredChecks) {
93 val mustPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST)
94 val currentPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::CURRENT)
95 if(!mainMustPropagationNames.containsKey(referredCheck)) {
96 mainMustPropagationNames.put(referredCheck,new LinkedList)
97 }
98 if(!mainCurrentPropagationNames.containsKey(referredCheck)) {
99 mainCurrentPropagationNames.put(referredCheck,new LinkedList)
100 }
101 if(mustPropagationPrecondition !== null) {
102 mainMustPropagationNames.get(referredCheck).add(mustPropagationPrecondition->query.parameterNames.size)
103 }
104 if(currentPropagationPrecondition !== null) {
105 mainCurrentPropagationNames.get(referredCheck).add(currentPropagationPrecondition->query.parameterNames.size)
106 }
107 }
108 }
109 val preconditions = new LinkedList
110 val constraint2MustPrecondition = new HashMap
111 val constraint2CurrentPrecondition = new HashMap
112 for(entry : mainMustPropagationNames.entrySet) {
113 val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»''';
114 val def = '''
115 pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»)
116 «FOR propagation : entry.value SEPARATOR " or "»
117 { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); }
118 «ENDFOR»'''
119 preconditions+=def
120 constraint2MustPrecondition.put(entry.key,name)
121 }
122 for(entry : mainCurrentPropagationNames.entrySet) {
123 val name = '''UPCurrentPropagate_«res.getOrGenerateConstraintName(entry.key)»''';
124 val def = '''
125 pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»)
126 «FOR propagation : entry.value SEPARATOR " or "»
127 { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); }
128 «ENDFOR»'''
129 preconditions+=def
130 constraint2CurrentPrecondition.put(entry.key,name)
131 }
132
133 val definitions = '''
134 «FOR def : res.definitions»
135 «def»
136 «ENDFOR»
137
138 // Collected propagation preconditions:
139
140 «FOR predondition : preconditions»
141 «predondition»
142 «ENDFOR»
143 '''
144 return new UnitPropagationPreconditionFinalResult(definitions,constraint2MustPrecondition,constraint2CurrentPrecondition)
145 }
146 def allReferredConstraints(Relation relation, PQuery query) {
147 val allReferredQueries = query.allReferredQueries
148 val problem = relation.eContainer as LogicProblem
149 val constraints = new LinkedHashSet
150 for(referredQuery: #[query]+allReferredQueries) {
151 val referredRelation = problem.annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredQuery].head.target
152 val bodies = (referredRelation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies
153 constraints.addAll(bodies.map[getConstraints].flatten)
154 }
155
156 return constraints
157 }
158
159 def getOrGeneratePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
160 if(res.contains(q,c,pm,m3)) {
161 return res.getName(q,c,pm,m3)
162 } else {
163 res.generatePropagationRule(relation,q,c,pm,m3)
164 return res.getName(q,c,pm,m3)
165 }
166 }
167 def getOrGenerateConstraintName(UnitPropagationPreconditionGenerationResult res, PConstraint c){
168 if(res.constraintOccurence2Name.containsKey(c)) {
169 return res.constraintOccurence2Name.get(c)
170 } else {
171 val constraintName = '''Constraint«res.constraintOccurence2Name.size»'''
172 res.constraintOccurence2Name.put(c,constraintName)
173 return constraintName
174 }
175 }
176
177 def void generatePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
178 val name = relationDefinitionName(res,relation,q,c,pm,m3)
179 val constraintArity = c.arity
180 val bodies = (relation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies
181 val generatedBodies = new LinkedList
182 for(body : bodies) {
183 if(body.constraints.contains(c)) {
184 if(pm === PropagationModality::UP) {
185 generatedBodies += '''
186 // Original Constraints
187 «FOR constraint : body.constraints.filter[it !== c]»
188 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
189 «ENDFOR»
190 // Propagation for constraint
191 «this.constraintTransformer.transformConstraintUnset(c as ExpressionEvaluation,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
192 // Matching variables
193 «this.propagateVariables(c,pm)»
194 '''
195 }
196 // Otherwise, for PropagationModality::DOWN, the body cannot be satisfied
197 } else {
198 val positives = body.constraints.filter(PositivePatternCall)
199 for(positive: positives) {
200 val referredPQuery = positive.referredQuery
201 val referredRelation = (relation.eContainer as LogicProblem)
202 .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target
203 if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) {
204 val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3)
205 if(referredName !== null) {
206 generatedBodies += '''
207 // Original Constraints
208 «FOR constraint : body.constraints.filter[it !== positive]»
209 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
210 «ENDFOR»
211 // Propagation for constraint referred indirectly from this pattern through «referredName»
212 find «referredName»(problem, interpretation,
213 «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«positive.getVariableInTuple(index).canonizeName»«ENDFOR»,
214 «FOR index : 1..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»);
215 '''
216 }
217 // Otherwise, if the referred pattern is not satisfiable, this pattern is not satisfiable either
218 }
219 }
220
221 val negatives = body.constraints.filter(NegativePatternCall)
222 for(negative : negatives) {
223 val referredPQuery = negative.referredQuery
224 val referredRelation = (relation.eContainer as LogicProblem)
225 .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target
226 if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) {
227 val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3.dual)
228 if(referredName !== null) {
229 generatedBodies += '''
230 // Original Constraints
231 «FOR constraint : body.constraints.filter[it !== negative]»
232 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
233 «ENDFOR»
234 // Propagation for constraint referred indirectly from this pattern through «referredName»
235 find «referredName»(problem, interpretation,
236 «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«(negative.actualParametersTuple.get(index) as PVariable).canonizeName»«ENDFOR»,
237 «FOR index : 1..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»);
238 '''
239 } else {
240 generatedBodies += '''
241 // Original Constraints
242 «FOR constraint : body.constraints.filter[it !== negative]»
243 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
244 «ENDFOR»
245 // Propagation for constraint referred indirectly from this pattern through «referredName»,
246 // which was unsatisfiable
247 '''
248 }
249 }
250 }
251 }
252 }
253
254 // Register the result
255 if(generatedBodies.empty) {
256 res.registerUnsatQuery(q,c,pm,m3)
257 } else {
258 val definition = '''
259 private pattern «name»(
260 problem:LogicProblem, interpretation:PartialInterpretation,
261 «FOR param : q.parameters SEPARATOR ', '»var_«param.name»«ENDFOR»,
262 «FOR arity : 1..constraintArity SEPARATOR ', '»«canonizeName(arity,pm)»«ENDFOR»)
263 «FOR generatedBody: generatedBodies SEPARATOR " or "»{
264 «generatedBody»
265 }«ENDFOR»
266 '''
267 res.registerQuery(q,c,pm,m3,name,definition)
268 }
269 }
270
271 private def String relationDefinitionName(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3)
272 '''«pm.name»«m3.name»Propagate«res.getOrGenerateConstraintName(c)»_«base.canonizeName(relation.name)»'''
273
274 def canonizeName(PVariable v) {
275 return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»'''
276 }
277
278 def canonizeName(int index, PropagationModality m) {
279 return '''«m.name.toLowerCase»_«index»'''
280 }
281
282 def dispatch propagateVariables(ExpressionEvaluation c, PropagationModality m) {
283 val comparator = new Comparator<PVariable>(){
284 override compare(PVariable o1, PVariable o2) {
285 o1.name.compareTo(o2.name)
286 }
287 }
288 val variablesInOrder = new ArrayList(c.affectedVariables)
289 variablesInOrder.toList.sort(comparator)
290 return '''«FOR variableIndex : 1..variablesInOrder.size»«variablesInOrder.get(variableIndex-1).canonizeName»==«canonizeName(variableIndex,m)»;«ENDFOR»'''
291 }
292 def dispatch propagateVariables(PConstraint c, PropagationModality m) {
293 throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''')
294 }
295
296 def dispatch arity(ExpressionEvaluation c) {
297 c.affectedVariables.size
298 }
299 def dispatch arity(PConstraint c) {
300 throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''')
301 }
302} \ No newline at end of file
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-03 13:41:30 +0000