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
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
|
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.IfThenElse
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.XIfExpression
import org.eclipse.xtext.xbase.XMemberFeatureCall
import org.eclipse.xtext.xbase.XNumberLiteral
import org.eclipse.xtext.xbase.XUnaryOperation
import org.eclipse.xtext.xbase.XBlockExpression
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("z3")
}
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(XIfExpression i, Map<PVariable, Variable> variable2Variable) {
val cond_op = i.^if.transform(variable2Variable)
val then_op = i.then.transform(variable2Variable)
val else_op = i.^else.transform(variable2Variable)
if (cond_op === null) {
println("-> " + i.^if)
println("-> " + i.then)
println("-> " + i.^else)
throw new UnsupportedOperationException('''Your ITE statement has a null condition.''')
}
if (then_op === null) {
println("-> " + i.^if)
println("-> " + i.then)
println("-> " + i.^else)
throw new UnsupportedOperationException('''Your ITE statement has a null "then" statement"".''')
}
return ITE(cond_op, then_op, else_op)
}
def protected dispatch Term transform(XBlockExpression b, Map<PVariable, Variable> variable2Variable) {
val exprs = newArrayList
for(e:b.expressions){ exprs.add(transform(e, variable2Variable)) }
if (exprs.size > 1)
throw new UnsupportedOperationException('''blocks with more than 1 statement are not currently supportes: "«exprs»"''')
if (exprs.isEmpty)
throw new UnsupportedOperationException('''blocks is empty: "«exprs»"''')
return exprs.get(0)
}
def protected dispatch Term transform(XExpression e, Map<PVariable, Variable> variable2Variable) {
throw new UnsupportedOperationException('''Unsupported expression: "«e.class.simpleName»" - «e»''')
}
}
|
