aboutsummaryrefslogtreecommitdiffstats
path: root/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme
diff options
context:
space:
mode:
authorLibravatar OszkarSemerath <oszka@152.66.252.189>2017-06-10 19:05:05 +0200
committerLibravatar OszkarSemerath <oszka@152.66.252.189>2017-06-10 19:05:05 +0200
commit60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme
parentInitial commit, migrating from SVN (diff)
downloadVIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip
Migrating Additional projects
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme')
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Constraint2Logic.xtend217
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend317
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 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic
2
3import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
5import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
6import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
9import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
10import java.util.LinkedList
11import java.util.Map
12import org.eclipse.emf.common.util.Enumerator
13import org.eclipse.emf.ecore.EAttribute
14import org.eclipse.emf.ecore.EClass
15import org.eclipse.emf.ecore.EReference
16import org.eclipse.emf.ecore.EStructuralFeature
17import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
18import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
19import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey
20import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
21import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
22import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality
23import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter
24import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality
25import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
26import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure
27import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue
28import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall
29import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint
30
31import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
32
33class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic
2
3import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
5import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
6import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDescriptor
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
10import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
11import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
12import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsFactory
13import java.util.ArrayList
14import java.util.HashMap
15import java.util.LinkedList
16import java.util.List
17import java.util.Map
18import java.util.Set
19import org.eclipse.emf.ecore.EAttribute
20import org.eclipse.emf.ecore.EClass
21import org.eclipse.emf.ecore.EClassifier
22import org.eclipse.emf.ecore.EEnum
23import org.eclipse.emf.ecore.EReference
24import org.eclipse.emf.ecore.EStructuralFeature
25import org.eclipse.emf.ecore.EcorePackage
26import org.eclipse.viatra.query.runtime.api.IQuerySpecification
27import org.eclipse.viatra.query.runtime.emf.EMFQueryMetaContext
28import org.eclipse.viatra.query.runtime.emf.types.BaseEMFTypeKey
29import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
30import org.eclipse.viatra.query.runtime.emf.types.EClassUnscopedTransitiveInstancesKey
31import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
32import org.eclipse.viatra.query.runtime.matchers.psystem.PBody
33import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
34import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
35import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter
36import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
37import org.eclipse.viatra.query.runtime.matchers.psystem.rewriters.PBodyNormalizer
38import org.eclipse.xtend.lib.annotations.Data
39
40import 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}
47class 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}
53class Viatra2LogicConfiguration {
54 public var normalize = true
55 public var transitiveClosureDepth = 3
56}
57
58class 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
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-29 08:52:31 +0000