1 files changed, 317 insertions, 0 deletions
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 @@
+package hu.bme.mit.inf.dslreasoner.viatra2logic
+import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
+import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDescriptor
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
+import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsFactory
+import java.util.ArrayList
+import java.util.HashMap
+import java.util.LinkedList
+import java.util.List
+import java.util.Map
+import java.util.Set
+import org.eclipse.emf.ecore.EAttribute
+import org.eclipse.emf.ecore.EClass
+import org.eclipse.emf.ecore.EClassifier
+import org.eclipse.emf.ecore.EEnum
+import org.eclipse.emf.ecore.EReference
+import org.eclipse.emf.ecore.EStructuralFeature
+import org.eclipse.emf.ecore.EcorePackage
+import org.eclipse.viatra.query.runtime.api.IQuerySpecification
+import org.eclipse.viatra.query.runtime.emf.EMFQueryMetaContext
+import org.eclipse.viatra.query.runtime.emf.types.BaseEMFTypeKey
+import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
+import org.eclipse.viatra.query.runtime.emf.types.EClassUnscopedTransitiveInstancesKey
+import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
+import org.eclipse.viatra.query.runtime.matchers.psystem.PBody
+import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
+import org.eclipse.viatra.query.runtime.matchers.psystem.rewriters.PBodyNormalizer
+import org.eclipse.xtend.lib.annotations.Data
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+@Data class ViatraQuerySetDescriptor {
+        val List<? extends IQuerySpecification<?>> patterns
+        val Set<? extends IQuerySpecification<?>> validationPatterns
+        val Map<PQuery,EStructuralFeature> derivedFeatures
+}
+class Viatra2LogicTrace {
+        public val Map<PQuery, RelationDefinition> query2Relation = new HashMap
+        public val Map<PQuery, TransfomedViatraQuery> query2Annotation = new HashMap
+        public val Map<Pair<PQuery,PParameter>, Variable> parameter2Variable = new HashMap
+        //public val Map<PVariable, Variable> variable2Variable = new HashMap
+}
+class Viatra2LogicConfiguration {
+        public var normalize = true
+        public var transitiveClosureDepth = 3
+}
+class  Viatra2Logic {
+        val extension LogicProblemBuilder builder = new LogicProblemBuilder
+        val extension Viatra2LogicAnnotationsFactory factory = Viatra2LogicAnnotationsFactory.eINSTANCE
+        val Ecore2Logic ecore2Logic
+        Constraint2Logic constraint2Logic
+        
+        new(Ecore2Logic ecore2Logic) {
+                this.ecore2Logic = ecore2Logic
+                constraint2Logic = new Constraint2Logic(ecore2Logic)
+        }
+        
+        def TracedOutput<LogicProblem,Viatra2LogicTrace> transformQueries(
+                ViatraQuerySetDescriptor queries,
+                TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
+                Viatra2LogicConfiguration config)
+        {
+                val viatra2LogicTrace = new Viatra2LogicTrace
+                for(query: queries.patterns) {
+                        this.transformQueryHeader(query,ecore2LogicTrace,viatra2LogicTrace,config)
+                }
+                for(query: queries.patterns) {
+                        this.transformQuerySpecification(query,ecore2LogicTrace,viatra2LogicTrace,config)
+                }
+                /*for(d : viatra2LogicTrace.query2Relation.values) {
+                        checkDefinition(d)
+                }*/
+                
+                transformQueryConstraints(
+                        queries.validationPatterns,
+                        queries.derivedFeatures,
+                        ecore2LogicTrace,viatra2LogicTrace)
+                return new TracedOutput(ecore2LogicTrace.output,viatra2LogicTrace)
+        }
+        
+        def protected transformQueryHeader(IQuerySpecification<?> squery,
+                TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
+                Viatra2LogicTrace viatra2LogicTrace,
+                Viatra2LogicConfiguration config)
+        {
+                val pquery = squery.internalQueryRepresentation
+                val relationName = '''pattern «pquery.fullyQualifiedName.replace('.',' ')»'''
+                val parameters = new ArrayList<Variable>(pquery.parameters.size)
+                for(vParam: pquery.parameters) {
+                        val parameterType = transformTypeReference(
+                                vParam.declaredUnaryType as BaseEMFTypeKey<? extends EClassifier>,
+                                ecore2LogicTrace
+                        )
+                        if(parameterType == null) {
+                                println(parameterType)
+                        }
+                        val parameterName = '''parameter «vParam.name»'''
+                        val lParam = createVar(parameterName,parameterType)
+                        viatra2LogicTrace.parameter2Variable.put(pquery->vParam,lParam)
+                        parameters+=lParam
+                }
+                val lRelation = RelationDefinition(relationName,parameters,null)
+                
+                viatra2LogicTrace.query2Relation.put(pquery,lRelation);
+                ecore2LogicTrace.output.relations += lRelation
+                
+                val annotation = createTransfomedViatraQuery => [
+                        it.target = lRelation
+                        it.patternFullyQualifiedName = pquery.fullyQualifiedName
+                ]
+                viatra2LogicTrace.query2Annotation.put(pquery,annotation)
+                ecore2LogicTrace.output.annotations += annotation
+                
+                return lRelation
+        }
+        
+        def protected transformQuerySpecification(
+                IQuerySpecification<?> squery,
+                TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
+                Viatra2LogicTrace viatra2LogicTrace,
+                Viatra2LogicConfiguration config)
+        {
+                val pquery = squery.internalQueryRepresentation
+                val disjunction = if(config.normalize) {
+                        val normalizer = new PBodyNormalizer(EMFQueryMetaContext.INSTANCE,true)
+                        normalizer.rewrite(pquery)
+                } else {
+                        pquery.disjunctBodies
+                }
+                val translatedBodies = new ArrayList(disjunction.bodies.size)
+                for(body : disjunction.bodies) {
+                        translatedBodies+=body.transformBody(ecore2LogicTrace,viatra2LogicTrace,config)
+                }
+                val relation = pquery.lookup(viatra2LogicTrace.query2Relation)
+                relation.value = Or(translatedBodies)
+        }
+        
+        def transformQueryConstraints(
+                Set<? extends IQuerySpecification<?>> validationPatterns,
+                Map<PQuery,EStructuralFeature> derivedFeatures,
+                TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
+                Viatra2LogicTrace viatra2LogicTrace)
+        {
+                for(validationPattern : validationPatterns) {
+                        val pquery = validationPattern.internalQueryRepresentation
+                        val constraint = Assertion('''errorpattern «pquery.fullyQualifiedName.replace('.',' ')»''',
+                                Forall[
+                                        for(param: pquery.parameters) {
+                                                addVar(param.name,transformTypeReference(
+                                                        param.declaredUnaryType as BaseEMFTypeKey<? extends EClassifier>,
+                                                        ecore2LogicTrace))
+                                        }
+                                        Not(pquery.lookup(viatra2LogicTrace.query2Relation).call(it.variables))
+                                ]
+                        )
+                        val annotation = createTransformedViatraWellformednessConstraint => [
+                                it.query = pquery.lookup(viatra2LogicTrace.query2Annotation)
+                                it.target = constraint
+                        ]
+                        ecore2LogicTrace.output.add(constraint)
+                        ecore2LogicTrace.output.annotations.add(annotation)
+                }
+                for(derivedFeature : derivedFeatures.entrySet) {
+                        val relationDefinition = derivedFeature.key.lookup(viatra2LogicTrace.query2Relation)
+                        val feature = derivedFeature.value
+                        if(feature instanceof EAttribute) {
+                                val declaration = ecore2Logic.relationOfAttribute(ecore2LogicTrace.trace,feature)
+                                relationDefinition.defines = declaration
+                        } else if(feature instanceof EReference) {
+                                val declaration = ecore2Logic.relationOfReference(ecore2LogicTrace.trace,feature)
+                                relationDefinition.defines = declaration
+                        } else throw new IllegalArgumentException('''Unknown feature: «feature»''')
+                        val annotation = createDefinedByDerivedFeature => [
+                                it.target = relationDefinition.defines
+                                it.query = derivedFeature.key.lookup(viatra2LogicTrace.query2Annotation)
+                        ]
+                        ecore2LogicTrace.output.annotations+=annotation
+                }
+        }
+        
+        def transformBody(PBody body,
+                TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
+                Viatra2LogicTrace viatra2LogicTrace,
+                Viatra2LogicConfiguration config)
+        {
+                val variable2Variable = new HashMap
+                // Parameter variables
+                for(parameter : body.symbolicParameters) {
+                        val param = parameter.patternParameter
+                        val variable = parameter.parameterVariable
+                        variable2Variable.put(variable,(body.pattern->param).lookup(viatra2LogicTrace.parameter2Variable))
+                }
+                // Inner Variables
+                val innerPositiveVariables = new LinkedList
+                val innerNegativeVariables = new LinkedList
+                for(innerVariable : body.uniqueVariables) {
+                        if(!variable2Variable.containsKey(innerVariable)) {
+                                val name = '''variable «innerVariable.name.normalizeName»'''
+                                //println(body.pattern.fullyQualifiedName + "-")
+                                val logicType = getType(innerVariable,body,ecore2LogicTrace)
+                                val logicVariable = createVar(name,logicType)
+                                if(innerVariable.isPositiveVariable) {
+                                        innerPositiveVariables += logicVariable
+                                } else {
+                                        innerNegativeVariables += logicVariable
+                                }
+                                variable2Variable.put(innerVariable,logicVariable)
+                        }
+                }
+                
+                val translatedConstraints = body.constraints.map[
+                        constraint2Logic.transformConstraint(it,
+                                ecore2LogicTrace,viatra2LogicTrace,variable2Variable,config)
+                ].filterNull
+                val allConstraintIsSatisfied = And(translatedConstraints)
+                val allNetativeVariablesAreSatisfied = if(innerNegativeVariables.empty) {
+                        allConstraintIsSatisfied
+                } else {
+                        Forall(innerNegativeVariables,allConstraintIsSatisfied);
+                }
+                val allVariablesAreExisting = if(innerPositiveVariables.empty) {
+                        allNetativeVariablesAreSatisfied
+                } else {
+                        Exists(innerPositiveVariables,allNetativeVariablesAreSatisfied);
+                }
+                
+                return allVariablesAreExisting
+        }
+        
+        def private normalizeName(String variableName) {
+                return variableName.replaceAll("[\\W]|_", "")
+        }
+        
+        def TypeDescriptor getType(PVariable v, PBody body, TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
+                if(v.isPositiveVariable) {
+                        val types = v.lookup(
+                                body.getAllUnaryTypeRestrictions(EMFQueryMetaContext.INSTANCE))
+                        if(types.size == 0) {
+                                throw new AssertionError('''No type for «v.name»''')
+                        } else if(types.size == 1){
+                                return (types.head.inputKey as BaseEMFTypeKey<? extends EClassifier>).transformTypeReference(ecore2LogicTrace)
+                        } else {
+                                return this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,
+                                        calculateCommonSubtype(types.map[
+                                                (it.inputKey as BaseEMFTypeKey<EClass>).emfKey as EClass
+                                        ],ecore2LogicTrace))
+                        }
+                } else {
+                        val onlyConstraint = v.referringConstraints.head as NegativePatternCall
+                        val indexOfVariable = v.lookup(onlyConstraint.actualParametersTuple.invertIndex)
+                        val parameter = onlyConstraint.referredQuery.parameters.get(indexOfVariable)
+                        val declaredUnaryType = parameter.declaredUnaryType as BaseEMFTypeKey<? extends EClassifier>
+                        if(declaredUnaryType == null) {
+                                throw new UnsupportedOperationException(
+                                '''parameter «parameter.name» in pattern «
+                                onlyConstraint.referredQuery.fullyQualifiedName» does not have type!''')
+                        } else return declaredUnaryType.transformTypeReference(ecore2LogicTrace)
+                }
+        }
+        
+        def calculateCommonSubtype(Iterable<EClass> allsuperClasses,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
+                val superClasses = allsuperClasses.filter[it!=EcorePackage.eINSTANCE.EObject]
+                val head = superClasses.head
+                if(superClasses.forall[it.isSuperTypeOf(head)]) return head
+                else {
+                        val allClasses = this.ecore2Logic.allClassesInScope(ecore2LogicTrace.trace)
+                        //println(allClasses.toList)
+                        val commonSubclasses = allClasses.filter[sub | superClasses.forall[sup | sup.isSuperTypeOf(sub)]]
+                        //println(commonSubclasses.toList)
+                        val mostGenericSubclasses = commonSubclasses.filter[generic | ! commonSubclasses.exists[moreGeneric | moreGeneric!=generic && moreGeneric.isSuperTypeOf(generic)]]
+                        //println(mostGenericSubclasses.toList)
+                        if(mostGenericSubclasses.isEmpty) throw new AssertionError('''No common supertype:
+                        «FOR s : superClasses SEPARATOR ", "»«s.name»«ENDFOR»''')
+                        else return mostGenericSubclasses.head
+                        
+                }
+        }
+        
+        def dispatch transformTypeReference(EDataTypeInSlotsKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
+                val w = k.wrappedKey 
+                if(w == EcorePackage.Literals.EINT) {
+                        return builder.LogicInt
+                } else if(w == EcorePackage.Literals.EDOUBLE || w == EcorePackage.Literals.EFLOAT) {
+                        return builder.LogicReal
+                } else if(w == EcorePackage.Literals.EBOOLEAN) {
+                        return builder.LogicBool
+                } else if(w instanceof EEnum) {
+                        this.ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,w);
+                } else throw new UnsupportedOperationException('''Unknown reference type «w.class.name»''')
+        }
+        
+        def dispatch transformTypeReference(EClassTransitiveInstancesKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
+                this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,k.wrappedKey)
+        }
+        
+        def boolean isPositiveVariable(PVariable v) {
+                val constraints = v.referringConstraints
+                if(constraints.size == 1) {
+                        val onlyConstraint = constraints.head
+                        if(onlyConstraint instanceof NegativePatternCall) {
+                                return false
+                        }
+                }
+                return true
+        }
+}
+\ 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