diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu')
2 files changed, 534 insertions, 0 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Constraint2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Constraint2Logic.xtend new file mode 100644 index 00000000..414af4c8 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Constraint2Logic.xtend | |||
@@ -0,0 +1,217 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
10 | import java.util.LinkedList | ||
11 | import java.util.Map | ||
12 | import org.eclipse.emf.common.util.Enumerator | ||
13 | import org.eclipse.emf.ecore.EAttribute | ||
14 | import org.eclipse.emf.ecore.EClass | ||
15 | import org.eclipse.emf.ecore.EReference | ||
16 | import org.eclipse.emf.ecore.EStructuralFeature | ||
17 | import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey | ||
18 | import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey | ||
19 | import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey | ||
20 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
21 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable | ||
22 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality | ||
23 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter | ||
24 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality | ||
25 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall | ||
26 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure | ||
27 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue | ||
28 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall | ||
29 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint | ||
30 | |||
31 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
32 | |||
33 | class Constraint2Logic { | ||
34 | val extension LogicProblemBuilder builder = new LogicProblemBuilder | ||
35 | val Ecore2Logic ecore2Logic | ||
36 | |||
37 | new(Ecore2Logic ecore2Logic) { | ||
38 | this.ecore2Logic = ecore2Logic | ||
39 | } | ||
40 | |||
41 | def dispatch Term transformConstraint(Equality constraint, | ||
42 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
43 | Viatra2LogicTrace viatra2LogicTrace, | ||
44 | Map<PVariable, Variable> variable2Variable, | ||
45 | Viatra2LogicConfiguration config) | ||
46 | { | ||
47 | constraint.who.lookup(variable2Variable) | ||
48 | == | ||
49 | constraint.withWhom.lookup(variable2Variable) | ||
50 | } | ||
51 | |||
52 | def dispatch Term transformConstraint(ExportedParameter constraint, | ||
53 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
54 | Viatra2LogicTrace viatra2LogicTrace, | ||
55 | Map<PVariable, Variable> variable2Variable, | ||
56 | Viatra2LogicConfiguration config) | ||
57 | { | ||
58 | return null | ||
59 | } | ||
60 | |||
61 | def dispatch Term transformConstraint(Inequality constraint, | ||
62 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
63 | Viatra2LogicTrace viatra2LogicTrace, | ||
64 | Map<PVariable, Variable> variable2Variable, | ||
65 | Viatra2LogicConfiguration config) | ||
66 | { | ||
67 | constraint.who.lookup(variable2Variable) | ||
68 | != | ||
69 | constraint.withWhom.lookup(variable2Variable) | ||
70 | } | ||
71 | |||
72 | def dispatch Term transformConstraint(NegativePatternCall constraint, | ||
73 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
74 | Viatra2LogicTrace viatra2LogicTrace, | ||
75 | Map<PVariable, Variable> variable2Variable, | ||
76 | Viatra2LogicConfiguration config) | ||
77 | { | ||
78 | val parameterSubstitution = new LinkedList | ||
79 | for(index : 0..<constraint.actualParametersTuple.size) { | ||
80 | val variable = constraint.actualParametersTuple.get(index) as PVariable | ||
81 | parameterSubstitution += variable.lookup(variable2Variable).toTerm | ||
82 | } | ||
83 | |||
84 | val res = constraint.referredQuery.lookup(viatra2LogicTrace.query2Relation).call(parameterSubstitution) | ||
85 | return res.Not | ||
86 | } | ||
87 | |||
88 | def dispatch Term transformConstraint(BinaryTransitiveClosure constraint, | ||
89 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
90 | Viatra2LogicTrace viatra2LogicTrace, | ||
91 | Map<PVariable, Variable> variable2Variable, | ||
92 | Viatra2LogicConfiguration config) | ||
93 | { | ||
94 | throw new UnsupportedOperationException | ||
95 | } | ||
96 | |||
97 | def dispatch Term transformConstraint(ConstantValue constant, | ||
98 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
99 | Viatra2LogicTrace viatra2LogicTrace, | ||
100 | Map<PVariable, Variable> variable2Variable, | ||
101 | Viatra2LogicConfiguration config) | ||
102 | { | ||
103 | val tuple = constant.variablesTuple | ||
104 | if(tuple.size == 1) { | ||
105 | val variable = tuple.get(0) as PVariable | ||
106 | //println(variable.name + " == " + constant.supplierKey + "["+constant.supplierKey.class.name+"]") | ||
107 | val translatedConstant = transformConstantValue(constant.supplierKey,ecore2LogicTrace,viatra2LogicTrace,config); | ||
108 | return variable.lookup(variable2Variable) == translatedConstant | ||
109 | } else throw new AssertionError | ||
110 | } | ||
111 | |||
112 | private def dispatch transformConstantValue( | ||
113 | Enumerator enumerator, | ||
114 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
115 | Viatra2LogicTrace viatra2LogicTrace, | ||
116 | Viatra2LogicConfiguration config) | ||
117 | { | ||
118 | ecore2Logic.Literal(ecore2LogicTrace.trace,enumerator) | ||
119 | } | ||
120 | private def dispatch transformConstantValue( | ||
121 | Integer value, | ||
122 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
123 | Viatra2LogicTrace viatra2LogicTrace, | ||
124 | Viatra2LogicConfiguration config) | ||
125 | { | ||
126 | return value.asTerm | ||
127 | } | ||
128 | private def dispatch transformConstantValue(Object other, | ||
129 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
130 | Viatra2LogicTrace viatra2LogicTrace, | ||
131 | Viatra2LogicConfiguration config) | ||
132 | { | ||
133 | throw new UnsupportedOperationException('''Unknown constant «other»:«other.class.name»''') | ||
134 | } | ||
135 | |||
136 | def dispatch Term transformConstraint(PositivePatternCall constraint, | ||
137 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
138 | Viatra2LogicTrace viatra2LogicTrace, | ||
139 | Map<PVariable, Variable> variable2Variable, | ||
140 | Viatra2LogicConfiguration config) | ||
141 | { | ||
142 | |||
143 | val parameterSubstitution = new LinkedList | ||
144 | for(index : 0..<constraint.variablesTuple.size) { | ||
145 | val variable = constraint.variablesTuple.get(index) as PVariable | ||
146 | parameterSubstitution += variable.lookup(variable2Variable).toTerm | ||
147 | } | ||
148 | val res = constraint.referredQuery.lookup(viatra2LogicTrace.query2Relation).call(parameterSubstitution) | ||
149 | return res | ||
150 | } | ||
151 | |||
152 | def dispatch Term transformConstraint(TypeConstraint constraint, | ||
153 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
154 | Viatra2LogicTrace viatra2LogicTrace, | ||
155 | Map<PVariable, Variable> variable2Variable, | ||
156 | Viatra2LogicConfiguration config) | ||
157 | { | ||
158 | val tuple = constraint.variablesTuple | ||
159 | if(tuple.size == 1) { | ||
160 | val typeConstraint = constraint.equivalentJudgement.inputKey | ||
161 | if(typeConstraint instanceof EClassTransitiveInstancesKey) { | ||
162 | val type = typeConstraint.emfKey | ||
163 | val variable = tuple.get(0) as PVariable | ||
164 | return transformTypeConstraint(type,variable,ecore2LogicTrace,variable2Variable,viatra2LogicTrace) | ||
165 | } else if(typeConstraint instanceof EDataTypeInSlotsKey) { | ||
166 | // If the type is a primitive type or EEnum, then instanceof is an unnecessary constraint | ||
167 | return null | ||
168 | } | ||
169 | } else if(tuple.size == 2) { | ||
170 | val type = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey | ||
171 | val src = tuple.get(0) as PVariable | ||
172 | val trg = tuple.get(1) as PVariable | ||
173 | return transformPathConstraint(type,src,trg,ecore2LogicTrace,variable2Variable,viatra2LogicTrace) | ||
174 | } else throw new IllegalArgumentException('''unknown tuple: «tuple»''') | ||
175 | } | ||
176 | def Term transformTypeConstraint( | ||
177 | EClass type, | ||
178 | PVariable variable, | ||
179 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
180 | Map<PVariable, Variable> variable2Variable, | ||
181 | Viatra2LogicTrace viatra2LogicTrace) | ||
182 | { | ||
183 | InstanceOf( | ||
184 | variable.lookup(variable2Variable), | ||
185 | ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,type)) | ||
186 | } | ||
187 | def Term transformPathConstraint( | ||
188 | EStructuralFeature feature, | ||
189 | PVariable src, PVariable trg, | ||
190 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
191 | Map<PVariable, Variable> variable2Variable, | ||
192 | Viatra2LogicTrace viatra2LogicTrace) | ||
193 | { | ||
194 | if(feature instanceof EReference) { | ||
195 | return ecore2Logic.IsInReference(ecore2LogicTrace.trace, | ||
196 | src.lookup(variable2Variable), | ||
197 | trg.lookup(variable2Variable), | ||
198 | feature) | ||
199 | } else if(feature instanceof EAttribute) { | ||
200 | return ecore2Logic.IsAttributeValue(ecore2LogicTrace.trace, | ||
201 | src.lookup(variable2Variable), | ||
202 | trg.lookup(variable2Variable), | ||
203 | feature) | ||
204 | } else { | ||
205 | throw new IllegalArgumentException('''Unsupported path expression: «feature.class.name»''') | ||
206 | } | ||
207 | } | ||
208 | |||
209 | def dispatch Term transformConstraint(PConstraint constraint, | ||
210 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
211 | Viatra2LogicTrace viatra2LogicTrace, | ||
212 | Map<PVariable, Variable> variable2Variable, | ||
213 | Viatra2LogicConfiguration config) | ||
214 | { | ||
215 | throw new UnsupportedOperationException('''Unkown constraint type: «constraint.class.name»''') | ||
216 | } | ||
217 | } \ No newline at end of file | ||
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend new file mode 100644 index 00000000..d78fe45f --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend | |||
@@ -0,0 +1,317 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDescriptor | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
11 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | ||
12 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsFactory | ||
13 | import java.util.ArrayList | ||
14 | import java.util.HashMap | ||
15 | import java.util.LinkedList | ||
16 | import java.util.List | ||
17 | import java.util.Map | ||
18 | import java.util.Set | ||
19 | import org.eclipse.emf.ecore.EAttribute | ||
20 | import org.eclipse.emf.ecore.EClass | ||
21 | import org.eclipse.emf.ecore.EClassifier | ||
22 | import org.eclipse.emf.ecore.EEnum | ||
23 | import org.eclipse.emf.ecore.EReference | ||
24 | import org.eclipse.emf.ecore.EStructuralFeature | ||
25 | import org.eclipse.emf.ecore.EcorePackage | ||
26 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
27 | import org.eclipse.viatra.query.runtime.emf.EMFQueryMetaContext | ||
28 | import org.eclipse.viatra.query.runtime.emf.types.BaseEMFTypeKey | ||
29 | import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey | ||
30 | import org.eclipse.viatra.query.runtime.emf.types.EClassUnscopedTransitiveInstancesKey | ||
31 | import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey | ||
32 | import org.eclipse.viatra.query.runtime.matchers.psystem.PBody | ||
33 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable | ||
34 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall | ||
35 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter | ||
36 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
37 | import org.eclipse.viatra.query.runtime.matchers.psystem.rewriters.PBodyNormalizer | ||
38 | import org.eclipse.xtend.lib.annotations.Data | ||
39 | |||
40 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
41 | |||
42 | @Data class ViatraQuerySetDescriptor { | ||
43 | val List<? extends IQuerySpecification<?>> patterns | ||
44 | val Set<? extends IQuerySpecification<?>> validationPatterns | ||
45 | val Map<PQuery,EStructuralFeature> derivedFeatures | ||
46 | } | ||
47 | class Viatra2LogicTrace { | ||
48 | public val Map<PQuery, RelationDefinition> query2Relation = new HashMap | ||
49 | public val Map<PQuery, TransfomedViatraQuery> query2Annotation = new HashMap | ||
50 | public val Map<Pair<PQuery,PParameter>, Variable> parameter2Variable = new HashMap | ||
51 | //public val Map<PVariable, Variable> variable2Variable = new HashMap | ||
52 | } | ||
53 | class Viatra2LogicConfiguration { | ||
54 | public var normalize = true | ||
55 | public var transitiveClosureDepth = 3 | ||
56 | } | ||
57 | |||
58 | class Viatra2Logic { | ||
59 | val extension LogicProblemBuilder builder = new LogicProblemBuilder | ||
60 | val extension Viatra2LogicAnnotationsFactory factory = Viatra2LogicAnnotationsFactory.eINSTANCE | ||
61 | val Ecore2Logic ecore2Logic | ||
62 | Constraint2Logic constraint2Logic | ||
63 | |||
64 | new(Ecore2Logic ecore2Logic) { | ||
65 | this.ecore2Logic = ecore2Logic | ||
66 | constraint2Logic = new Constraint2Logic(ecore2Logic) | ||
67 | } | ||
68 | |||
69 | def TracedOutput<LogicProblem,Viatra2LogicTrace> transformQueries( | ||
70 | ViatraQuerySetDescriptor queries, | ||
71 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
72 | Viatra2LogicConfiguration config) | ||
73 | { | ||
74 | val viatra2LogicTrace = new Viatra2LogicTrace | ||
75 | for(query: queries.patterns) { | ||
76 | this.transformQueryHeader(query,ecore2LogicTrace,viatra2LogicTrace,config) | ||
77 | } | ||
78 | for(query: queries.patterns) { | ||
79 | this.transformQuerySpecification(query,ecore2LogicTrace,viatra2LogicTrace,config) | ||
80 | } | ||
81 | /*for(d : viatra2LogicTrace.query2Relation.values) { | ||
82 | checkDefinition(d) | ||
83 | }*/ | ||
84 | |||
85 | transformQueryConstraints( | ||
86 | queries.validationPatterns, | ||
87 | queries.derivedFeatures, | ||
88 | ecore2LogicTrace,viatra2LogicTrace) | ||
89 | return new TracedOutput(ecore2LogicTrace.output,viatra2LogicTrace) | ||
90 | } | ||
91 | |||
92 | def protected transformQueryHeader(IQuerySpecification<?> squery, | ||
93 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
94 | Viatra2LogicTrace viatra2LogicTrace, | ||
95 | Viatra2LogicConfiguration config) | ||
96 | { | ||
97 | val pquery = squery.internalQueryRepresentation | ||
98 | val relationName = '''pattern «pquery.fullyQualifiedName.replace('.',' ')»''' | ||
99 | val parameters = new ArrayList<Variable>(pquery.parameters.size) | ||
100 | for(vParam: pquery.parameters) { | ||
101 | val parameterType = transformTypeReference( | ||
102 | vParam.declaredUnaryType as BaseEMFTypeKey<? extends EClassifier>, | ||
103 | ecore2LogicTrace | ||
104 | ) | ||
105 | if(parameterType == null) { | ||
106 | println(parameterType) | ||
107 | } | ||
108 | val parameterName = '''parameter «vParam.name»''' | ||
109 | val lParam = createVar(parameterName,parameterType) | ||
110 | viatra2LogicTrace.parameter2Variable.put(pquery->vParam,lParam) | ||
111 | parameters+=lParam | ||
112 | } | ||
113 | val lRelation = RelationDefinition(relationName,parameters,null) | ||
114 | |||
115 | viatra2LogicTrace.query2Relation.put(pquery,lRelation); | ||
116 | ecore2LogicTrace.output.relations += lRelation | ||
117 | |||
118 | val annotation = createTransfomedViatraQuery => [ | ||
119 | it.target = lRelation | ||
120 | it.patternFullyQualifiedName = pquery.fullyQualifiedName | ||
121 | ] | ||
122 | viatra2LogicTrace.query2Annotation.put(pquery,annotation) | ||
123 | ecore2LogicTrace.output.annotations += annotation | ||
124 | |||
125 | return lRelation | ||
126 | } | ||
127 | |||
128 | def protected transformQuerySpecification( | ||
129 | IQuerySpecification<?> squery, | ||
130 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
131 | Viatra2LogicTrace viatra2LogicTrace, | ||
132 | Viatra2LogicConfiguration config) | ||
133 | { | ||
134 | val pquery = squery.internalQueryRepresentation | ||
135 | val disjunction = if(config.normalize) { | ||
136 | val normalizer = new PBodyNormalizer(EMFQueryMetaContext.INSTANCE,true) | ||
137 | normalizer.rewrite(pquery) | ||
138 | } else { | ||
139 | pquery.disjunctBodies | ||
140 | } | ||
141 | val translatedBodies = new ArrayList(disjunction.bodies.size) | ||
142 | for(body : disjunction.bodies) { | ||
143 | translatedBodies+=body.transformBody(ecore2LogicTrace,viatra2LogicTrace,config) | ||
144 | } | ||
145 | val relation = pquery.lookup(viatra2LogicTrace.query2Relation) | ||
146 | relation.value = Or(translatedBodies) | ||
147 | } | ||
148 | |||
149 | def transformQueryConstraints( | ||
150 | Set<? extends IQuerySpecification<?>> validationPatterns, | ||
151 | Map<PQuery,EStructuralFeature> derivedFeatures, | ||
152 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
153 | Viatra2LogicTrace viatra2LogicTrace) | ||
154 | { | ||
155 | for(validationPattern : validationPatterns) { | ||
156 | val pquery = validationPattern.internalQueryRepresentation | ||
157 | val constraint = Assertion('''errorpattern «pquery.fullyQualifiedName.replace('.',' ')»''', | ||
158 | Forall[ | ||
159 | for(param: pquery.parameters) { | ||
160 | addVar(param.name,transformTypeReference( | ||
161 | param.declaredUnaryType as BaseEMFTypeKey<? extends EClassifier>, | ||
162 | ecore2LogicTrace)) | ||
163 | } | ||
164 | Not(pquery.lookup(viatra2LogicTrace.query2Relation).call(it.variables)) | ||
165 | ] | ||
166 | ) | ||
167 | val annotation = createTransformedViatraWellformednessConstraint => [ | ||
168 | it.query = pquery.lookup(viatra2LogicTrace.query2Annotation) | ||
169 | it.target = constraint | ||
170 | ] | ||
171 | ecore2LogicTrace.output.add(constraint) | ||
172 | ecore2LogicTrace.output.annotations.add(annotation) | ||
173 | } | ||
174 | for(derivedFeature : derivedFeatures.entrySet) { | ||
175 | val relationDefinition = derivedFeature.key.lookup(viatra2LogicTrace.query2Relation) | ||
176 | val feature = derivedFeature.value | ||
177 | if(feature instanceof EAttribute) { | ||
178 | val declaration = ecore2Logic.relationOfAttribute(ecore2LogicTrace.trace,feature) | ||
179 | relationDefinition.defines = declaration | ||
180 | } else if(feature instanceof EReference) { | ||
181 | val declaration = ecore2Logic.relationOfReference(ecore2LogicTrace.trace,feature) | ||
182 | relationDefinition.defines = declaration | ||
183 | } else throw new IllegalArgumentException('''Unknown feature: «feature»''') | ||
184 | val annotation = createDefinedByDerivedFeature => [ | ||
185 | it.target = relationDefinition.defines | ||
186 | it.query = derivedFeature.key.lookup(viatra2LogicTrace.query2Annotation) | ||
187 | ] | ||
188 | ecore2LogicTrace.output.annotations+=annotation | ||
189 | } | ||
190 | } | ||
191 | |||
192 | def transformBody(PBody body, | ||
193 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
194 | Viatra2LogicTrace viatra2LogicTrace, | ||
195 | Viatra2LogicConfiguration config) | ||
196 | { | ||
197 | val variable2Variable = new HashMap | ||
198 | // Parameter variables | ||
199 | for(parameter : body.symbolicParameters) { | ||
200 | val param = parameter.patternParameter | ||
201 | val variable = parameter.parameterVariable | ||
202 | variable2Variable.put(variable,(body.pattern->param).lookup(viatra2LogicTrace.parameter2Variable)) | ||
203 | } | ||
204 | // Inner Variables | ||
205 | val innerPositiveVariables = new LinkedList | ||
206 | val innerNegativeVariables = new LinkedList | ||
207 | for(innerVariable : body.uniqueVariables) { | ||
208 | if(!variable2Variable.containsKey(innerVariable)) { | ||
209 | val name = '''variable «innerVariable.name.normalizeName»''' | ||
210 | //println(body.pattern.fullyQualifiedName + "-") | ||
211 | val logicType = getType(innerVariable,body,ecore2LogicTrace) | ||
212 | val logicVariable = createVar(name,logicType) | ||
213 | if(innerVariable.isPositiveVariable) { | ||
214 | innerPositiveVariables += logicVariable | ||
215 | } else { | ||
216 | innerNegativeVariables += logicVariable | ||
217 | } | ||
218 | variable2Variable.put(innerVariable,logicVariable) | ||
219 | } | ||
220 | } | ||
221 | |||
222 | val translatedConstraints = body.constraints.map[ | ||
223 | constraint2Logic.transformConstraint(it, | ||
224 | ecore2LogicTrace,viatra2LogicTrace,variable2Variable,config) | ||
225 | ].filterNull | ||
226 | val allConstraintIsSatisfied = And(translatedConstraints) | ||
227 | val allNetativeVariablesAreSatisfied = if(innerNegativeVariables.empty) { | ||
228 | allConstraintIsSatisfied | ||
229 | } else { | ||
230 | Forall(innerNegativeVariables,allConstraintIsSatisfied); | ||
231 | } | ||
232 | val allVariablesAreExisting = if(innerPositiveVariables.empty) { | ||
233 | allNetativeVariablesAreSatisfied | ||
234 | } else { | ||
235 | Exists(innerPositiveVariables,allNetativeVariablesAreSatisfied); | ||
236 | } | ||
237 | |||
238 | return allVariablesAreExisting | ||
239 | } | ||
240 | |||
241 | def private normalizeName(String variableName) { | ||
242 | return variableName.replaceAll("[\\W]|_", "") | ||
243 | } | ||
244 | |||
245 | def TypeDescriptor getType(PVariable v, PBody body, TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
246 | if(v.isPositiveVariable) { | ||
247 | val types = v.lookup( | ||
248 | body.getAllUnaryTypeRestrictions(EMFQueryMetaContext.INSTANCE)) | ||
249 | if(types.size == 0) { | ||
250 | throw new AssertionError('''No type for «v.name»''') | ||
251 | } else if(types.size == 1){ | ||
252 | return (types.head.inputKey as BaseEMFTypeKey<? extends EClassifier>).transformTypeReference(ecore2LogicTrace) | ||
253 | } else { | ||
254 | return this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace, | ||
255 | calculateCommonSubtype(types.map[ | ||
256 | (it.inputKey as BaseEMFTypeKey<EClass>).emfKey as EClass | ||
257 | ],ecore2LogicTrace)) | ||
258 | } | ||
259 | } else { | ||
260 | val onlyConstraint = v.referringConstraints.head as NegativePatternCall | ||
261 | val indexOfVariable = v.lookup(onlyConstraint.actualParametersTuple.invertIndex) | ||
262 | val parameter = onlyConstraint.referredQuery.parameters.get(indexOfVariable) | ||
263 | val declaredUnaryType = parameter.declaredUnaryType as BaseEMFTypeKey<? extends EClassifier> | ||
264 | if(declaredUnaryType == null) { | ||
265 | throw new UnsupportedOperationException( | ||
266 | '''parameter «parameter.name» in pattern « | ||
267 | onlyConstraint.referredQuery.fullyQualifiedName» does not have type!''') | ||
268 | } else return declaredUnaryType.transformTypeReference(ecore2LogicTrace) | ||
269 | } | ||
270 | } | ||
271 | |||
272 | def calculateCommonSubtype(Iterable<EClass> allsuperClasses,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
273 | val superClasses = allsuperClasses.filter[it!=EcorePackage.eINSTANCE.EObject] | ||
274 | val head = superClasses.head | ||
275 | if(superClasses.forall[it.isSuperTypeOf(head)]) return head | ||
276 | else { | ||
277 | val allClasses = this.ecore2Logic.allClassesInScope(ecore2LogicTrace.trace) | ||
278 | //println(allClasses.toList) | ||
279 | val commonSubclasses = allClasses.filter[sub | superClasses.forall[sup | sup.isSuperTypeOf(sub)]] | ||
280 | //println(commonSubclasses.toList) | ||
281 | val mostGenericSubclasses = commonSubclasses.filter[generic | ! commonSubclasses.exists[moreGeneric | moreGeneric!=generic && moreGeneric.isSuperTypeOf(generic)]] | ||
282 | //println(mostGenericSubclasses.toList) | ||
283 | if(mostGenericSubclasses.isEmpty) throw new AssertionError('''No common supertype: | ||
284 | «FOR s : superClasses SEPARATOR ", "»«s.name»«ENDFOR»''') | ||
285 | else return mostGenericSubclasses.head | ||
286 | |||
287 | } | ||
288 | } | ||
289 | |||
290 | def dispatch transformTypeReference(EDataTypeInSlotsKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
291 | val w = k.wrappedKey | ||
292 | if(w == EcorePackage.Literals.EINT) { | ||
293 | return builder.LogicInt | ||
294 | } else if(w == EcorePackage.Literals.EDOUBLE || w == EcorePackage.Literals.EFLOAT) { | ||
295 | return builder.LogicReal | ||
296 | } else if(w == EcorePackage.Literals.EBOOLEAN) { | ||
297 | return builder.LogicBool | ||
298 | } else if(w instanceof EEnum) { | ||
299 | this.ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,w); | ||
300 | } else throw new UnsupportedOperationException('''Unknown reference type «w.class.name»''') | ||
301 | } | ||
302 | |||
303 | def dispatch transformTypeReference(EClassTransitiveInstancesKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
304 | this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,k.wrappedKey) | ||
305 | } | ||
306 | |||
307 | def boolean isPositiveVariable(PVariable v) { | ||
308 | val constraints = v.referringConstraints | ||
309 | if(constraints.size == 1) { | ||
310 | val onlyConstraint = constraints.head | ||
311 | if(onlyConstraint instanceof NegativePatternCall) { | ||
312 | return false | ||
313 | } | ||
314 | } | ||
315 | return true | ||
316 | } | ||
317 | } \ No newline at end of file | ||