1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
|
package hu.bme.mit.inf.dslreasoner.viatra2logic
import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
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 ExpressionEvaluation2Logic {
val extension LogicProblemBuilder builder = new LogicProblemBuilder
var NumericProblemSolver _numericSolver = null //new NumericProblemSolver
def getNumericSolver() {
if(_numericSolver === null) {
// it seems like this getter has no use
_numericSolver = (new NumericTranslator(null)).selectProblemSolver
}
return _numericSolver
}
def Term transformCheck(XExpression expression, Map<PVariable, Variable> variable2Variable) {
return expression.transform(variable2Variable)
}
def Term transformEval(PVariable target, XExpression expression, Map<PVariable, Variable> variable2Variable) {
// numericSolver.testIsNotSat(expression, expression.transform(variable2Variable));
// numericSolver.testGetOneSol(expression, expression.transform(variable2Variable));
// numericSolver.testGetOneSol2(expression, expression.transform(variable2Variable));
// numericSolver.testGetOneSol3(expression, expression.transform(variable2Variable));
// numericSolver.testIsSat(expression, expression.transform(variable2Variable));
return expression.transform(variable2Variable)
}
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 protected dispatch Term transform(XBinaryOperation e, Map<PVariable, Variable> variable2Variable) {
val left = e.leftOperand.transform(variable2Variable)
val right = e.rightOperand.transform(variable2Variable)
val feature = e.feature.qualifiedName
if(feature.isN(N_MINUS2)) { return Minus(left,right) }
else if(feature.isN(N_PLUS2)) { return Plus(left,right) }
else if(feature.isN(N_POWER)) { return Pow(left,right) }
else if(feature.isN(N_MULTIPLY)) { return Multiply(left,right) }
else if(feature.isN(N_DIVIDE)) { return Divide(left,right) }
else if(feature.isN(N_MODULO)) { return Modulo(left,right) }
else if(feature.isN(N_LESSTHAN)) { return LessThan(left,right) }
else if(feature.isN(N_LESSEQUALSTHAN)) { return LessOrEqual(left,right) }
else if(feature.isN(N_GREATERTHAN)) { return MoreThan(left,right) }
else if(feature.isN(N_GREATEREQUALTHAN)) { return MoreOrEqual(left,right) }
else if(feature.isN(N_EQUALS)) { return Equals(left,right) }
else if(feature.isN(N_NOTEQUALS)) { return Distinct(left,right) }
else if(feature.isN(N_EQUALS3)) { return Equals(left,right) }
else if(feature.isN(N_NOTEQUALS3)) { return Distinct(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 protected dispatch Term transform(XUnaryOperation e, Map<PVariable, Variable> variable2Variable) {
val operand = e.operand.transform(variable2Variable)
val feature = e.feature.qualifiedName
if(feature.isN(N_MINUS1)) { return Minus(0.asTerm,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 protected dispatch Term transform(XMemberFeatureCall e, Map<PVariable, Variable> variable2Variable) {
val transformedArguments = e.actualArguments.map[transform(variable2Variable)]
val feature = e.feature.qualifiedName
if(feature == N_POWER2) {
return 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 protected dispatch Term transform(XFeatureCall e, Map<PVariable,Variable> variable2Variable) {
val featureName = e.feature.qualifiedName
val entryWithName = variable2Variable.entrySet.filter[it.key.name == featureName].head
if(entryWithName !== null) {
return entryWithName.value.toTerm
} else {
throw new IllegalArgumentException('''Feature call reference to unavailable variable "«featureName»"''')
}
}
def protected dispatch Term transform(XNumberLiteral l, Map<PVariable, Variable> variable2Variable) {
val s = l.value
try{ return Integer.parseInt(s).asTerm } catch(NumberFormatException e){}
try{ return Short.parseShort(s).asTerm } catch(NumberFormatException e){}
try{ return Double.parseDouble(s).asTerm } catch(NumberFormatException e){}
try{ return Float.parseFloat(s).asTerm } catch(NumberFormatException e){}
throw new UnsupportedOperationException('''Unsupported numeric type: "«s»"''')
}
def protected dispatch Term transform(XExpression e, Map<PVariable, Variable> variable2Variable) {
throw new UnsupportedOperationException('''Unsupported expression: "«e.class.simpleName»" - «e»''')
}
}
|
