From 60f01f46ba232ed6416054f0a6115cb2a9b70b4e Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sat, 10 Jun 2017 19:05:05 +0200 Subject: Migrating Additional projects --- .../viatra2logic/Constraint2Logic.xtend | 217 ++++++++++++++ .../dslreasoner/viatra2logic/Viatra2Logic.xtend | 317 +++++++++++++++++++++ 2 files changed, 534 insertions(+) create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Constraint2Logic.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit') 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 @@ +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.Term +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import java.util.LinkedList +import java.util.Map +import org.eclipse.emf.common.util.Enumerator +import org.eclipse.emf.ecore.EAttribute +import org.eclipse.emf.ecore.EClass +import org.eclipse.emf.ecore.EReference +import org.eclipse.emf.ecore.EStructuralFeature +import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey +import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey +import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey +import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint +import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall +import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure +import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue +import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall +import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class Constraint2Logic { + val extension LogicProblemBuilder builder = new LogicProblemBuilder + val Ecore2Logic ecore2Logic + + new(Ecore2Logic ecore2Logic) { + this.ecore2Logic = ecore2Logic + } + + def dispatch Term transformConstraint(Equality constraint, + TracedOutput ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Map variable2Variable, + Viatra2LogicConfiguration config) + { + constraint.who.lookup(variable2Variable) + == + constraint.withWhom.lookup(variable2Variable) + } + + def dispatch Term transformConstraint(ExportedParameter constraint, + TracedOutput ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Map variable2Variable, + Viatra2LogicConfiguration config) + { + return null + } + + def dispatch Term transformConstraint(Inequality constraint, + TracedOutput ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Map variable2Variable, + Viatra2LogicConfiguration config) + { + constraint.who.lookup(variable2Variable) + != + constraint.withWhom.lookup(variable2Variable) + } + + def dispatch Term transformConstraint(NegativePatternCall constraint, + TracedOutput ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Map variable2Variable, + Viatra2LogicConfiguration config) + { + val parameterSubstitution = new LinkedList + for(index : 0.. ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Map variable2Variable, + Viatra2LogicConfiguration config) + { + throw new UnsupportedOperationException + } + + def dispatch Term transformConstraint(ConstantValue constant, + TracedOutput ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Map variable2Variable, + Viatra2LogicConfiguration config) + { + val tuple = constant.variablesTuple + if(tuple.size == 1) { + val variable = tuple.get(0) as PVariable + //println(variable.name + " == " + constant.supplierKey + "["+constant.supplierKey.class.name+"]") + val translatedConstant = transformConstantValue(constant.supplierKey,ecore2LogicTrace,viatra2LogicTrace,config); + return variable.lookup(variable2Variable) == translatedConstant + } else throw new AssertionError + } + + private def dispatch transformConstantValue( + Enumerator enumerator, + TracedOutput ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Viatra2LogicConfiguration config) + { + ecore2Logic.Literal(ecore2LogicTrace.trace,enumerator) + } + private def dispatch transformConstantValue( + Integer value, + TracedOutput ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Viatra2LogicConfiguration config) + { + return value.asTerm + } + private def dispatch transformConstantValue(Object other, + TracedOutput ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Viatra2LogicConfiguration config) + { + throw new UnsupportedOperationException('''Unknown constant «other»:«other.class.name»''') + } + + def dispatch Term transformConstraint(PositivePatternCall constraint, + TracedOutput ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Map variable2Variable, + Viatra2LogicConfiguration config) + { + + val parameterSubstitution = new LinkedList + for(index : 0.. ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Map variable2Variable, + Viatra2LogicConfiguration config) + { + val tuple = constraint.variablesTuple + if(tuple.size == 1) { + val typeConstraint = constraint.equivalentJudgement.inputKey + if(typeConstraint instanceof EClassTransitiveInstancesKey) { + val type = typeConstraint.emfKey + val variable = tuple.get(0) as PVariable + return transformTypeConstraint(type,variable,ecore2LogicTrace,variable2Variable,viatra2LogicTrace) + } else if(typeConstraint instanceof EDataTypeInSlotsKey) { + // If the type is a primitive type or EEnum, then instanceof is an unnecessary constraint + return null + } + } else if(tuple.size == 2) { + val type = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey + val src = tuple.get(0) as PVariable + val trg = tuple.get(1) as PVariable + return transformPathConstraint(type,src,trg,ecore2LogicTrace,variable2Variable,viatra2LogicTrace) + } else throw new IllegalArgumentException('''unknown tuple: «tuple»''') + } + def Term transformTypeConstraint( + EClass type, + PVariable variable, + TracedOutput ecore2LogicTrace, + Map variable2Variable, + Viatra2LogicTrace viatra2LogicTrace) + { + InstanceOf( + variable.lookup(variable2Variable), + ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,type)) + } + def Term transformPathConstraint( + EStructuralFeature feature, + PVariable src, PVariable trg, + TracedOutput ecore2LogicTrace, + Map variable2Variable, + Viatra2LogicTrace viatra2LogicTrace) + { + if(feature instanceof EReference) { + return ecore2Logic.IsInReference(ecore2LogicTrace.trace, + src.lookup(variable2Variable), + trg.lookup(variable2Variable), + feature) + } else if(feature instanceof EAttribute) { + return ecore2Logic.IsAttributeValue(ecore2LogicTrace.trace, + src.lookup(variable2Variable), + trg.lookup(variable2Variable), + feature) + } else { + throw new IllegalArgumentException('''Unsupported path expression: «feature.class.name»''') + } + } + + def dispatch Term transformConstraint(PConstraint constraint, + TracedOutput ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Map variable2Variable, + Viatra2LogicConfiguration config) + { + throw new UnsupportedOperationException('''Unkown constraint type: «constraint.class.name»''') + } +} \ 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 @@ +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> patterns + val Set> validationPatterns + val Map derivedFeatures +} +class Viatra2LogicTrace { + public val Map query2Relation = new HashMap + public val Map query2Annotation = new HashMap + public val Map, Variable> parameter2Variable = new HashMap + //public val Map 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 transformQueries( + ViatraQuerySetDescriptor queries, + TracedOutput 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 ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Viatra2LogicConfiguration config) + { + val pquery = squery.internalQueryRepresentation + val relationName = '''pattern «pquery.fullyQualifiedName.replace('.',' ')»''' + val parameters = new ArrayList(pquery.parameters.size) + for(vParam: pquery.parameters) { + val parameterType = transformTypeReference( + vParam.declaredUnaryType as BaseEMFTypeKey, + 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 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> validationPatterns, + Map derivedFeatures, + TracedOutput 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, + 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 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 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).transformTypeReference(ecore2LogicTrace) + } else { + return this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace, + calculateCommonSubtype(types.map[ + (it.inputKey as BaseEMFTypeKey).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 + 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 allsuperClasses,TracedOutput 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 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 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 -- cgit v1.2.3-54-g00ecf