check expressions are mapped to WF constraints

author: Oszkar Semerath <semerath@mit.bme.hu> 2020-04-17 00:17:45 +0200
committer: Oszkar Semerath <semerath@mit.bme.hu> 2020-04-17 00:17:45 +0200
commit: 6e56760734f62857d437cbb54746e9ff487f46d3 (patch)
tree: 541f68b6e9da4c4badbf42d4a9e0c191dfcd1978 /Solvers
parent: variable mapping trace is created after mapping (diff)
download: VIATRA-Generator-6e56760734f62857d437cbb54746e9ff487f46d3.tar.gz
VIATRA-Generator-6e56760734f62857d437cbb54746e9ff487f46d3.tar.zst
VIATRA-Generator-6e56760734f62857d437cbb54746e9ff487f46d3.zip
2 files changed, 183 insertions, 23 deletions
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> 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> 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> 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> 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> variableMapping) {
                val params = (0..<pcall.actualParametersTuple.size).map[index | 
                        val variable = pcall.actualParametersTuple.get(index) as PVariable
                        return variable.canonizeName
@@ -119,24 +128,24 @@ class PConstraintTransformer {
                return referPattern(pcall.referredQuery,params,modality.dual,false,false)
        }
        
-        dispatch def transformConstraint(PositivePatternCall pcall, Modality modality) {
+        dispatch def transformConstraint(PositivePatternCall pcall, Modality modality, List<VariableMapping> variableMapping) {
                val params = (0..<pcall.variablesTuple.size).map[index | 
                        val variable = pcall.variablesTuple.get(index) as PVariable
                        return variable.canonizeName
                ]
                return referPattern(pcall.referredQuery,params,modality,true,false)
        }
-        dispatch def transformConstraint(BinaryTransitiveClosure pcall, Modality modality) {
+        dispatch def transformConstraint(BinaryTransitiveClosure pcall, Modality modality, List<VariableMapping> 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> variableMapping) {
                return '''// «e.parameterName» is exported'''
        }
-        dispatch def transformConstraint(ConstantValue c, Modality modality) {
+        dispatch def transformConstraint(ConstantValue c, Modality modality, List<VariableMapping> 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'''
+                        targetString = '''const_«target»_Real'''
-                        additionalDefinition = '''RealElement.value(«targetString»,"«target»");'''
+                        additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); RealElement.value(«targetString»,«target»);'''
                } else if(target instanceof Float) {
-                        targetString = '''const_«target»_Number'''
+                        targetString = '''const_«target»_Real'''
-                        additionalDefinition = '''RealElement.value(«targetString»,"«target»");'''
+                        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> 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> 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> 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) {
+                        if(modality.isMay) {
-                                return ''''''
+                                return '''
-                        } else if(modality.isMay) {
+                                        «FOR variable: e.affectedVariables»
-                                return ''''''
+                                                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> 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<PVariable,String> 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<PVariable,String> 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<PVariable,String> 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<PVariable,String> 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<PVariable,String> valueName) '''«l.value»'''
+        
+        def dispatch CharSequence translateExpression(XExpression expression, Map<PVariable,String> valueName) {
+                throw new UnsupportedOperationException('''Unsupported expression in check or eval: «expression.class.name», «expression»"''')
+        }
+}
+\ No newline at end of file
author	Oszkar Semerath <semerath@mit.bme.hu>	2020-04-17 00:17:45 +0200
committer	Oszkar Semerath <semerath@mit.bme.hu>	2020-04-17 00:17:45 +0200
commit	6e56760734f62857d437cbb54746e9ff487f46d3 (patch)
tree	541f68b6e9da4c4badbf42d4a9e0c191dfcd1978 /Solvers
parent	variable mapping trace is created after mapping (diff)
download	VIATRA-Generator-6e56760734f62857d437cbb54746e9ff487f46d3.tar.gz VIATRA-Generator-6e56760734f62857d437cbb54746e9ff487f46d3.tar.zst VIATRA-Generator-6e56760734f62857d437cbb54746e9ff487f46d3.zip

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
20	import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue	20	import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue
21	import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall	21	import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall
22	import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint	22	import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint
		23	import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.VariableMapping
		24	import java.util.List
		25	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
		26	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
		27	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference
		28	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
		29	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
		30	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
23		31
24	class PConstraintTransformer {	32	class PConstraintTransformer {
25	val extension RelationDefinitionIndexer relationDefinitionIndexer;	33	val extension RelationDefinitionIndexer relationDefinitionIndexer;
26	val expressionExtractor = new XExpressionExtractor	34	val expressionExtractor = new XExpressionExtractor
		35	val expressionGenerator = new PExpressionGenerator
27		36
28	new(RelationDefinitionIndexer relationDefinitionIndexer) {	37	new(RelationDefinitionIndexer relationDefinitionIndexer) {
29	this.relationDefinitionIndexer = relationDefinitionIndexer	38	this.relationDefinitionIndexer = relationDefinitionIndexer
30	}	39	}
31		40
32	dispatch def transformConstraint(TypeConstraint constraint, Modality modality) {	41	dispatch def transformConstraint(TypeConstraint constraint, Modality modality, List<VariableMapping> variableMapping) {
33	val touple = constraint.variablesTuple	42	val touple = constraint.variablesTuple
34	if(touple.size == 1) {	43	if(touple.size == 1) {
35	val inputKey = constraint.equivalentJudgement.inputKey	44	val inputKey = constraint.equivalentJudgement.inputKey
@@ -58,7 +67,7 @@ class PConstraintTransformer {
58	throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')	67	throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
59	}	68	}
60	}	69	}
61	dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality) {	70	dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality, List<VariableMapping> variableMapping) {
62	val touple = constraint.variablesTuple	71	val touple = constraint.variablesTuple
63	if(touple.size == 1) {	72	if(touple.size == 1) {
64	val inputKey = constraint.equivalentJudgement.inputKey	73	val inputKey = constraint.equivalentJudgement.inputKey
@@ -88,7 +97,7 @@ class PConstraintTransformer {
88	}	97	}
89	}	98	}
90		99
91	dispatch def transformConstraint(Equality equality, Modality modality) {	100	dispatch def transformConstraint(Equality equality, Modality modality, List<VariableMapping> variableMapping) {
92	val a = equality.who	101	val a = equality.who
93	val b = equality.withWhom	102	val b = equality.withWhom
94	transformEquality(modality.toMustMay, a, b)	103	transformEquality(modality.toMustMay, a, b)
@@ -99,7 +108,7 @@ class PConstraintTransformer {
99	else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''	108	else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
100	}	109	}
101		110
102	dispatch def transformConstraint(Inequality inequality, Modality modality) {	111	dispatch def transformConstraint(Inequality inequality, Modality modality, List<VariableMapping> variableMapping) {
103	val a = inequality.who	112	val a = inequality.who
104	val b = inequality.withWhom	113	val b = inequality.withWhom
105	if(modality.isCurrent) {	114	if(modality.isCurrent) {
@@ -111,7 +120,7 @@ class PConstraintTransformer {
111	}	120	}
112	}	121	}
113		122
114	dispatch def transformConstraint(NegativePatternCall pcall, Modality modality) {	123	dispatch def transformConstraint(NegativePatternCall pcall, Modality modality, List<VariableMapping> variableMapping) {
115	val params = (0..<pcall.actualParametersTuple.size).map[index \|	124	val params = (0..<pcall.actualParametersTuple.size).map[index \|
116	val variable = pcall.actualParametersTuple.get(index) as PVariable	125	val variable = pcall.actualParametersTuple.get(index) as PVariable
117	return variable.canonizeName	126	return variable.canonizeName
@@ -119,24 +128,24 @@ class PConstraintTransformer {
119	return referPattern(pcall.referredQuery,params,modality.dual,false,false)	128	return referPattern(pcall.referredQuery,params,modality.dual,false,false)
120	}	129	}
121		130
122	dispatch def transformConstraint(PositivePatternCall pcall, Modality modality) {	131	dispatch def transformConstraint(PositivePatternCall pcall, Modality modality, List<VariableMapping> variableMapping) {
123	val params = (0..<pcall.variablesTuple.size).map[index \|	132	val params = (0..<pcall.variablesTuple.size).map[index \|
124	val variable = pcall.variablesTuple.get(index) as PVariable	133	val variable = pcall.variablesTuple.get(index) as PVariable
125	return variable.canonizeName	134	return variable.canonizeName
126	]	135	]
127	return referPattern(pcall.referredQuery,params,modality,true,false)	136	return referPattern(pcall.referredQuery,params,modality,true,false)
128	}	137	}
129	dispatch def transformConstraint(BinaryTransitiveClosure pcall, Modality modality) {	138	dispatch def transformConstraint(BinaryTransitiveClosure pcall, Modality modality, List<VariableMapping> variableMapping) {
130	val params = (0..1).map[index \|	139	val params = (0..1).map[index \|
131	val variable = pcall.getVariableInTuple(index) as PVariable	140	val variable = pcall.getVariableInTuple(index) as PVariable
132	return variable.canonizeName	141	return variable.canonizeName
133	]	142	]
134	return referPattern(pcall.referredQuery,params,modality,true,true)	143	return referPattern(pcall.referredQuery,params,modality,true,true)
135	}	144	}
136	dispatch def transformConstraint(ExportedParameter e, Modality modality) {	145	dispatch def transformConstraint(ExportedParameter e, Modality modality, List<VariableMapping> variableMapping) {
137	return '''// «e.parameterName» is exported'''	146	return '''// «e.parameterName» is exported'''
138	}	147	}
139	dispatch def transformConstraint(ConstantValue c, Modality modality) {	148	dispatch def transformConstraint(ConstantValue c, Modality modality, List<VariableMapping> variableMapping) {
140	val target = c.supplierKey	149	val target = c.supplierKey
141		150
142	var String targetString;	151	var String targetString;
@@ -146,19 +155,19 @@ class PConstraintTransformer {
146	additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» «target.EEnum.name»"); //LogicProblem.elements(problem,«targetString»);'''	155	additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» «target.EEnum.name»"); //LogicProblem.elements(problem,«targetString»);'''
147	} else if(target instanceof Integer) {	156	} else if(target instanceof Integer) {
148	targetString = '''const_«target»_Integer'''	157	targetString = '''const_«target»_Integer'''
149	additionalDefinition = '''IntegerElement.value(«targetString»,«target»);'''	158	additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); IntegerElement.value(«targetString»,«target»);'''
150	} else if(target instanceof Boolean) {	159	} else if(target instanceof Boolean) {
151	targetString = '''const_«target»_Boolean'''	160	targetString = '''const_«target»_Boolean'''
152	additionalDefinition = '''BooleanElement.value(«targetString»,«target»);'''	161	additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); BooleanElement.value(«targetString»,«target»);'''
153	} else if(target instanceof String) {	162	} else if(target instanceof String) {
154	targetString = '''const_«target»_String'''	163	targetString = '''const_«target»_String'''
155	additionalDefinition = '''StringElement.value(«targetString»,"«target»");'''	164	additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); StringElement.value(«targetString»,"«target»");'''
156	} else if(target instanceof Double) {	165	} else if(target instanceof Double) {
157	targetString = '''const_«target»_Number'''	166	targetString = '''const_«target»_Real'''
158	additionalDefinition = '''RealElement.value(«targetString»,"«target»");'''	167	additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); RealElement.value(«targetString»,«target»);'''
159	} else if(target instanceof Float) {	168	} else if(target instanceof Float) {
160	targetString = '''const_«target»_Number'''	169	targetString = '''const_«target»_Real'''
161	additionalDefinition = '''RealElement.value(«targetString»,"«target»");'''	170	additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); RealElement.value(«targetString»,«target»);'''
162	} else {	171	} else {
163	throw new UnsupportedOperationException('''Unknown constant type: «target.class»''')	172	throw new UnsupportedOperationException('''Unknown constant type: «target.class»''')
164	}	173	}
@@ -171,22 +180,64 @@ class PConstraintTransformer {
171	return '''«sourceName» == «targetString»;«additionalDefinition»''';	180	return '''«sourceName» == «targetString»;«additionalDefinition»''';
172	}	181	}
173		182
		183	protected def valueVariable(PVariable v) {
		184	"value_"+v.canonizeName
		185	}
		186	protected def valueSetted(PVariable v) {
		187	"setted_"+v.canonizeName
		188	}
		189	def hasValue(PVariable v, String target, Modality m, List<VariableMapping> variableMapping) {
		190	val typeReference = variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range as PrimitiveTypeReference
		191	if(m.isMay) {
		192	'''PrimitiveElement.valueSet(«v.canonizeName»,«v.valueSetted»); «hasValueExpression(typeReference,v,v.valueVariable)» check(!«v.valueSetted»\|\|«v.valueVariable»==«target»));'''
		193	} else { // Must or current
		194	'''PrimitiveElement.valueSet(«v.canonizeName»,true);«hasValueExpression(typeReference,v,target)»'''
		195	}
		196	}
174		197
		198	private def hasValueExpression(List<VariableMapping> variableMapping, PVariable v, String target) {
		199	hasValueExpression(
		200	variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range,
		201	v,
		202	target
		203	)
		204	}
		205	private def dispatch hasValueExpression(BoolTypeReference typeReference, PVariable v, String target) '''BooleanElement.value(«v.canonizeName»,«target»);'''
		206	private def dispatch hasValueExpression(IntTypeReference typeReference, PVariable v, String target) '''IntegerElement.value(«v.canonizeName»,«target»);'''
		207	private def dispatch hasValueExpression(RealTypeReference typeReference, PVariable v, String target) '''RealElement.value(«v.canonizeName»,«target»);'''
		208	private def dispatch hasValueExpression(StringTypeReference typeReference, PVariable v, String target) '''StringElement.value(«v.canonizeName»,«target»);'''
		209	private def dispatch hasValueExpression(TypeReference typeReference, PVariable v, String target) {
		210	throw new UnsupportedOperationException('''Unsupported primitive type reference: «typeReference.class»''')
		211	}
175		212
176	dispatch def transformConstrait(ExpressionEvaluation e, Modality modality) {	213	dispatch def transformConstraint(ExpressionEvaluation e, Modality modality, List<VariableMapping> variableMapping) {
177	if(e.outputVariable!==null) {	214	if(e.outputVariable!==null) {
178	throw new UnsupportedOperationException('''Only check expressions are supported "«e.class.name»"!''')	215	throw new UnsupportedOperationException('''Only check expressions are supported "«e.class.name»"!''')
179	} else {	216	} else {
180	val expression = expressionExtractor.extractExpression(e.evaluator)	217	val expression = expressionExtractor.extractExpression(e.evaluator)
181	if(modality.isMust) {	218	if(modality.isMay) {
182	return ''''''	219	return '''
183	} else if(modality.isMay) {	220	«FOR variable: e.affectedVariables»
184	return ''''''	221	PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
		222	«ENDFOR»
		223	check(
		224	«FOR variable: e.affectedVariables SEPARATOR " \|\| "»!«variable.valueSetted»«ENDFOR»
		225	\|\|
		226	(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable])»)
		227	);
		228	'''
		229	} else { // Must or Current
		230	return '''
		231	«FOR variable: e.affectedVariables»
		232	PrimitiveElement.valueSet(«variable.canonizeName»,true); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
		233	«ENDFOR»
		234	check(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable])»);
		235	'''
185	}	236	}
186	}	237	}
187	}	238	}
188		239
189	dispatch def transformConstraint(PConstraint c, Modality modality) {	240	dispatch def transformConstraint(PConstraint c, Modality modality, List<VariableMapping> variableMapping) {
190	throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''')	241	throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''')
191	}	242	}
192	} \ No newline at end of file	243	} \ 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 @@
		1	package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
		2
		3	import java.util.Map
		4	import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
		5	import org.eclipse.xtext.xbase.XBinaryOperation
		6	import org.eclipse.xtext.xbase.XExpression
		7	import org.eclipse.xtext.xbase.XFeatureCall
		8	import org.eclipse.xtext.xbase.XMemberFeatureCall
		9	import org.eclipse.xtext.xbase.XNumberLiteral
		10	import org.eclipse.xtext.xbase.XUnaryOperation
		11
		12	class PExpressionGenerator {
		13	static val N_Base = "org.eclipse.xtext.xbase.lib."
		14
		15	static val N_PLUS1 = "operator_plus"
		16	static val N_MINUS1 = "operator_minus"
		17
		18	static val N_MINUS2 = "operator_minus"
		19	static val N_PLUS2 = "operator_plus"
		20	static val N_POWER = "operator_power"
		21	static val N_MULTIPLY = "operator_multiply"
		22	static val N_DIVIDE = "operator_divide"
		23	static val N_MODULO = "operator_modulo"
		24	static val N_LESSTHAN = "operator_lessThan"
		25	static val N_LESSEQUALSTHAN = "operator_lessEqualsThan"
		26	static val N_GREATERTHAN = "operator_greaterThan"
		27	static val N_GREATEREQUALTHAN = "operator_greaterEqualsThan"
		28	static val N_EQUALS = "operator_equals"
		29	static val N_NOTEQUALS = "operator_notEquals"
		30	static val N_EQUALS3 = "operator_tripleEquals"
		31	static val N_NOTEQUALS3 = "operator_tripleNotEquals"
		32
		33	protected def isN(String name, String s) {
		34	val res = name.startsWith(N_Base) && name.endsWith(s)
		35	//println('''[«res»] «name» ?= «N_Base»*«s»''')
		36	return res
		37	}
		38
		39	static val N_POWER2 = "java.lang.Math.pow"
		40
		41	def dispatch CharSequence translateExpression(XBinaryOperation e, Map<PVariable,String> valueName) {
		42	val left = e.leftOperand.translateExpression(valueName)
		43	val right = e.rightOperand.translateExpression(valueName)
		44	val feature = e.feature.qualifiedName
		45	if(feature.isN(N_MINUS2)) { return '''(«left»-«right»)'''}
		46	else if(feature.isN(N_PLUS2)) { return '''(«left»+«right»)''' }
		47	else if(feature.isN(N_POWER)) { return '''(«left»^«right»)''' }
		48	else if(feature.isN(N_MULTIPLY)) { return '''(«left»*«right»)''' }
		49	else if(feature.isN(N_DIVIDE)) { return '''(«left»/«right»)''' }
		50	else if(feature.isN(N_MODULO)) { return '''(«left»%«right»)''' }
		51	else if(feature.isN(N_LESSTHAN)) { return '''(«left»<«right»)''' }
		52	else if(feature.isN(N_LESSEQUALSTHAN)) { return '''(«left»<=«right»)''' }
		53	else if(feature.isN(N_GREATERTHAN)) { return '''(«left»>«right»)''' }
		54	else if(feature.isN(N_GREATEREQUALTHAN)) { return '''(«left»>=«right»)''' }
		55	else if(feature.isN(N_EQUALS)) { return '''(«left»==«right»)''' }
		56	else if(feature.isN(N_NOTEQUALS)) { return '''(«left»!=«right»)''' }
		57	else if(feature.isN(N_EQUALS3)) { return '''(«left»===«right»)''' }
		58	else if(feature.isN(N_NOTEQUALS3)) { return '''(«left»!==«right»)''' }
		59	else {
		60	println("-> " + e.feature+","+e.class)
		61	println("-> " + e.leftOperand)
		62	println("-> " + e.rightOperand)
		63	println("-> " + e.feature.qualifiedName)
		64	throw new UnsupportedOperationException('''Unsupported binary operator feature: "«e.feature.class.simpleName»" - «e»''')
		65	}
		66	}
		67
		68	def dispatch CharSequence translateExpression(XUnaryOperation e, Map<PVariable,String> valueName) {
		69	val operand = e.operand.translateExpression(valueName)
		70	val feature = e.feature.qualifiedName
		71	if(feature.isN(N_MINUS1)) { return '''(-«operand»)'''}
		72	else if(feature.isN(N_PLUS1)) { return '''(+«operand»)'''}
		73	else{
		74	println("-> " + e.feature+","+e.class)
		75	println("-> " + e.operand)
		76	println("-> " + e.feature.qualifiedName)
		77	throw new UnsupportedOperationException('''Unsupported unary operator feature: "«e.feature.class.simpleName»" - «e»''')
		78	}
		79	}
		80
		81	def dispatch CharSequence translateExpression(XMemberFeatureCall e, Map<PVariable,String> valueName) {
		82	val transformedArguments = e.actualArguments.map[translateExpression(valueName)]
		83	val feature = e.feature.qualifiedName
		84	if(feature == N_POWER2) {
		85	return '''Math.pow(«transformedArguments.get(0)»,«transformedArguments.get(1)»)'''
		86	}else {
		87	println(e.feature+","+e.class)
		88	println(e.actualArguments.join(", "))
		89	println(e.feature.qualifiedName)
		90	throw new UnsupportedOperationException('''Unsupported feature call: "«e.feature.qualifiedName»" - «e»''')
		91	}
		92	}
		93
		94	def dispatch CharSequence translateExpression(XFeatureCall e, Map<PVariable,String> valueName) {
		95	val featureName = e.feature.qualifiedName
		96	val entryWithName = valueName.entrySet.filter[it.key.name == featureName].head
		97	if(entryWithName !== null) {
		98	return entryWithName.value
		99	} else {
		100	throw new IllegalArgumentException('''Feature call reference to unavailable variable "«featureName»"''')
		101	}
		102	}
		103
		104	def dispatch CharSequence translateExpression(XNumberLiteral l, Map<PVariable,String> valueName) '''«l.value»'''
		105
		106	def dispatch CharSequence translateExpression(XExpression expression, Map<PVariable,String> valueName) {
		107	throw new UnsupportedOperationException('''Unsupported expression in check or eval: «expression.class.name», «expression»"''')
		108	}
		109	} \ No newline at end of file