From 6e56760734f62857d437cbb54746e9ff487f46d3 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Fri, 17 Apr 2020 00:17:45 +0200 Subject: check expressions are mapped to WF constraints --- .../patterns/PConstraintTransformer.xtend | 97 +++++++++++++----- .../patterns/PExpressionGenerator.xtend | 109 +++++++++++++++++++++ 2 files changed, 183 insertions(+), 23 deletions(-) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend index 64fbb2f1..a421d1fd 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend @@ -20,16 +20,25 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.Binary 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 hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.VariableMapping +import java.util.List +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference class PConstraintTransformer { val extension RelationDefinitionIndexer relationDefinitionIndexer; val expressionExtractor = new XExpressionExtractor + val expressionGenerator = new PExpressionGenerator new(RelationDefinitionIndexer relationDefinitionIndexer) { this.relationDefinitionIndexer = relationDefinitionIndexer } - dispatch def transformConstraint(TypeConstraint constraint, Modality modality) { + dispatch def transformConstraint(TypeConstraint constraint, Modality modality, List variableMapping) { val touple = constraint.variablesTuple if(touple.size == 1) { val inputKey = constraint.equivalentJudgement.inputKey @@ -58,7 +67,7 @@ class PConstraintTransformer { throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''') } } - dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality) { + dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality, List variableMapping) { val touple = constraint.variablesTuple if(touple.size == 1) { val inputKey = constraint.equivalentJudgement.inputKey @@ -88,7 +97,7 @@ class PConstraintTransformer { } } - dispatch def transformConstraint(Equality equality, Modality modality) { + dispatch def transformConstraint(Equality equality, Modality modality, List variableMapping) { val a = equality.who val b = equality.withWhom transformEquality(modality.toMustMay, a, b) @@ -99,7 +108,7 @@ class PConstraintTransformer { else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' } - dispatch def transformConstraint(Inequality inequality, Modality modality) { + dispatch def transformConstraint(Inequality inequality, Modality modality, List variableMapping) { val a = inequality.who val b = inequality.withWhom if(modality.isCurrent) { @@ -111,7 +120,7 @@ class PConstraintTransformer { } } - dispatch def transformConstraint(NegativePatternCall pcall, Modality modality) { + dispatch def transformConstraint(NegativePatternCall pcall, Modality modality, List variableMapping) { val params = (0.. variableMapping) { val params = (0.. variableMapping) { val params = (0..1).map[index | val variable = pcall.getVariableInTuple(index) as PVariable return variable.canonizeName ] return referPattern(pcall.referredQuery,params,modality,true,true) } - dispatch def transformConstraint(ExportedParameter e, Modality modality) { + dispatch def transformConstraint(ExportedParameter e, Modality modality, List variableMapping) { return '''// «e.parameterName» is exported''' } - dispatch def transformConstraint(ConstantValue c, Modality modality) { + dispatch def transformConstraint(ConstantValue c, Modality modality, List variableMapping) { val target = c.supplierKey var String targetString; @@ -146,19 +155,19 @@ class PConstraintTransformer { additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» «target.EEnum.name»"); //LogicProblem.elements(problem,«targetString»);''' } else if(target instanceof Integer) { targetString = '''const_«target»_Integer''' - additionalDefinition = '''IntegerElement.value(«targetString»,«target»);''' + additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); IntegerElement.value(«targetString»,«target»);''' } else if(target instanceof Boolean) { targetString = '''const_«target»_Boolean''' - additionalDefinition = '''BooleanElement.value(«targetString»,«target»);''' + additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); BooleanElement.value(«targetString»,«target»);''' } else if(target instanceof String) { targetString = '''const_«target»_String''' - additionalDefinition = '''StringElement.value(«targetString»,"«target»");''' + additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); StringElement.value(«targetString»,"«target»");''' } else if(target instanceof Double) { - targetString = '''const_«target»_Number''' - additionalDefinition = '''RealElement.value(«targetString»,"«target»");''' + targetString = '''const_«target»_Real''' + additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); RealElement.value(«targetString»,«target»);''' } else if(target instanceof Float) { - targetString = '''const_«target»_Number''' - additionalDefinition = '''RealElement.value(«targetString»,"«target»");''' + targetString = '''const_«target»_Real''' + additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); RealElement.value(«targetString»,«target»);''' } else { throw new UnsupportedOperationException('''Unknown constant type: «target.class»''') } @@ -171,22 +180,64 @@ class PConstraintTransformer { return '''«sourceName» == «targetString»;«additionalDefinition»'''; } + protected def valueVariable(PVariable v) { + "value_"+v.canonizeName + } + protected def valueSetted(PVariable v) { + "setted_"+v.canonizeName + } + def hasValue(PVariable v, String target, Modality m, List variableMapping) { + val typeReference = variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range as PrimitiveTypeReference + if(m.isMay) { + '''PrimitiveElement.valueSet(«v.canonizeName»,«v.valueSetted»); «hasValueExpression(typeReference,v,v.valueVariable)» check(!«v.valueSetted»||«v.valueVariable»==«target»));''' + } else { // Must or current + '''PrimitiveElement.valueSet(«v.canonizeName»,true);«hasValueExpression(typeReference,v,target)»''' + } + } + private def hasValueExpression(List variableMapping, PVariable v, String target) { + hasValueExpression( + variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range, + v, + target + ) + } + private def dispatch hasValueExpression(BoolTypeReference typeReference, PVariable v, String target) '''BooleanElement.value(«v.canonizeName»,«target»);''' + private def dispatch hasValueExpression(IntTypeReference typeReference, PVariable v, String target) '''IntegerElement.value(«v.canonizeName»,«target»);''' + private def dispatch hasValueExpression(RealTypeReference typeReference, PVariable v, String target) '''RealElement.value(«v.canonizeName»,«target»);''' + private def dispatch hasValueExpression(StringTypeReference typeReference, PVariable v, String target) '''StringElement.value(«v.canonizeName»,«target»);''' + private def dispatch hasValueExpression(TypeReference typeReference, PVariable v, String target) { + throw new UnsupportedOperationException('''Unsupported primitive type reference: «typeReference.class»''') + } - dispatch def transformConstrait(ExpressionEvaluation e, Modality modality) { + dispatch def transformConstraint(ExpressionEvaluation e, Modality modality, List variableMapping) { if(e.outputVariable!==null) { throw new UnsupportedOperationException('''Only check expressions are supported "«e.class.name»"!''') } else { val expression = expressionExtractor.extractExpression(e.evaluator) - if(modality.isMust) { - return '''''' - } else if(modality.isMay) { - return '''''' + if(modality.isMay) { + return ''' + «FOR variable: e.affectedVariables» + PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)» + «ENDFOR» + check( + «FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR» + || + («expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable])») + ); + ''' + } else { // Must or Current + return ''' + «FOR variable: e.affectedVariables» + PrimitiveElement.valueSet(«variable.canonizeName»,true); «hasValueExpression(variableMapping,variable,variable.valueVariable)» + «ENDFOR» + check(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable])»); + ''' } } } - - dispatch def transformConstraint(PConstraint c, Modality modality) { + + dispatch def transformConstraint(PConstraint c, Modality modality, List variableMapping) { throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''') } } \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend new file mode 100644 index 00000000..303c87b9 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend @@ -0,0 +1,109 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns + +import java.util.Map +import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable +import org.eclipse.xtext.xbase.XBinaryOperation +import org.eclipse.xtext.xbase.XExpression +import org.eclipse.xtext.xbase.XFeatureCall +import org.eclipse.xtext.xbase.XMemberFeatureCall +import org.eclipse.xtext.xbase.XNumberLiteral +import org.eclipse.xtext.xbase.XUnaryOperation + +class PExpressionGenerator { + static val N_Base = "org.eclipse.xtext.xbase.lib." + + static val N_PLUS1 = "operator_plus" + static val N_MINUS1 = "operator_minus" + + static val N_MINUS2 = "operator_minus" + static val N_PLUS2 = "operator_plus" + static val N_POWER = "operator_power" + static val N_MULTIPLY = "operator_multiply" + static val N_DIVIDE = "operator_divide" + static val N_MODULO = "operator_modulo" + static val N_LESSTHAN = "operator_lessThan" + static val N_LESSEQUALSTHAN = "operator_lessEqualsThan" + static val N_GREATERTHAN = "operator_greaterThan" + static val N_GREATEREQUALTHAN = "operator_greaterEqualsThan" + static val N_EQUALS = "operator_equals" + static val N_NOTEQUALS = "operator_notEquals" + static val N_EQUALS3 = "operator_tripleEquals" + static val N_NOTEQUALS3 = "operator_tripleNotEquals" + + protected def isN(String name, String s) { + val res = name.startsWith(N_Base) && name.endsWith(s) + //println('''[«res»] «name» ?= «N_Base»*«s»''') + return res + } + + static val N_POWER2 = "java.lang.Math.pow" + + def dispatch CharSequence translateExpression(XBinaryOperation e, Map valueName) { + val left = e.leftOperand.translateExpression(valueName) + val right = e.rightOperand.translateExpression(valueName) + val feature = e.feature.qualifiedName + if(feature.isN(N_MINUS2)) { return '''(«left»-«right»)'''} + else if(feature.isN(N_PLUS2)) { return '''(«left»+«right»)''' } + else if(feature.isN(N_POWER)) { return '''(«left»^«right»)''' } + else if(feature.isN(N_MULTIPLY)) { return '''(«left»*«right»)''' } + else if(feature.isN(N_DIVIDE)) { return '''(«left»/«right»)''' } + else if(feature.isN(N_MODULO)) { return '''(«left»%«right»)''' } + else if(feature.isN(N_LESSTHAN)) { return '''(«left»<«right»)''' } + else if(feature.isN(N_LESSEQUALSTHAN)) { return '''(«left»<=«right»)''' } + else if(feature.isN(N_GREATERTHAN)) { return '''(«left»>«right»)''' } + else if(feature.isN(N_GREATEREQUALTHAN)) { return '''(«left»>=«right»)''' } + else if(feature.isN(N_EQUALS)) { return '''(«left»==«right»)''' } + else if(feature.isN(N_NOTEQUALS)) { return '''(«left»!=«right»)''' } + else if(feature.isN(N_EQUALS3)) { return '''(«left»===«right»)''' } + else if(feature.isN(N_NOTEQUALS3)) { return '''(«left»!==«right»)''' } + else { + println("-> " + e.feature+","+e.class) + println("-> " + e.leftOperand) + println("-> " + e.rightOperand) + println("-> " + e.feature.qualifiedName) + throw new UnsupportedOperationException('''Unsupported binary operator feature: "«e.feature.class.simpleName»" - «e»''') + } + } + + def dispatch CharSequence translateExpression(XUnaryOperation e, Map valueName) { + val operand = e.operand.translateExpression(valueName) + val feature = e.feature.qualifiedName + if(feature.isN(N_MINUS1)) { return '''(-«operand»)'''} + else if(feature.isN(N_PLUS1)) { return '''(+«operand»)'''} + else{ + println("-> " + e.feature+","+e.class) + println("-> " + e.operand) + println("-> " + e.feature.qualifiedName) + throw new UnsupportedOperationException('''Unsupported unary operator feature: "«e.feature.class.simpleName»" - «e»''') + } + } + + def dispatch CharSequence translateExpression(XMemberFeatureCall e, Map valueName) { + val transformedArguments = e.actualArguments.map[translateExpression(valueName)] + val feature = e.feature.qualifiedName + if(feature == N_POWER2) { + return '''Math.pow(«transformedArguments.get(0)»,«transformedArguments.get(1)»)''' + }else { + println(e.feature+","+e.class) + println(e.actualArguments.join(", ")) + println(e.feature.qualifiedName) + throw new UnsupportedOperationException('''Unsupported feature call: "«e.feature.qualifiedName»" - «e»''') + } + } + + def dispatch CharSequence translateExpression(XFeatureCall e, Map valueName) { + val featureName = e.feature.qualifiedName + val entryWithName = valueName.entrySet.filter[it.key.name == featureName].head + if(entryWithName !== null) { + return entryWithName.value + } else { + throw new IllegalArgumentException('''Feature call reference to unavailable variable "«featureName»"''') + } + } + + def dispatch CharSequence translateExpression(XNumberLiteral l, Map valueName) '''«l.value»''' + + def dispatch CharSequence translateExpression(XExpression expression, Map valueName) { + throw new UnsupportedOperationException('''Unsupported expression in check or eval: «expression.class.name», «expression»"''') + } +} \ No newline at end of file -- cgit v1.2.3-54-g00ecf