diff options
author | 20001LastOrder <boqi.chen@mail.mcgill.ca> | 2020-11-04 01:33:58 -0500 |
---|---|---|
committer | 20001LastOrder <boqi.chen@mail.mcgill.ca> | 2020-11-04 01:33:58 -0500 |
commit | a20af4d0dbf5eab84ee271d426528aabb5a8ac3b (patch) | |
tree | a9ab772ee313125aaf3a941d66e131b408d949ba /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src | |
parent | changes in settings of measurements (diff) | |
parent | merge with current master, comment numerical solver related logging (diff) | |
download | VIATRA-Generator-a20af4d0dbf5eab84ee271d426528aabb5a8ac3b.tar.gz VIATRA-Generator-a20af4d0dbf5eab84ee271d426528aabb5a8ac3b.tar.zst VIATRA-Generator-a20af4d0dbf5eab84ee271d426528aabb5a8ac3b.zip |
fix merging issue
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src')
10 files changed, 1587 insertions, 266 deletions
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 index 3e8b3366..b8c52af4 100644 --- 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 | |||
@@ -30,10 +30,20 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeCo | |||
30 | 30 | ||
31 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 31 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
32 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint | 32 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint |
33 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.AggregatorConstraint | ||
34 | import org.eclipse.viatra.query.runtime.matchers.aggregators.DoubleSumOperator | ||
35 | import org.eclipse.viatra.query.runtime.matchers.aggregators.IntegerSumOperator | ||
36 | import org.eclipse.viatra.query.runtime.matchers.aggregators.LongSumOperator | ||
37 | import org.eclipse.viatra.query.runtime.matchers.aggregators.ExtremumOperator | ||
38 | import org.eclipse.viatra.query.runtime.matchers.aggregators.ExtremumOperator.Extreme | ||
39 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.PatternMatchCounter | ||
40 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation | ||
33 | 41 | ||
34 | class Constraint2Logic { | 42 | class Constraint2Logic { |
35 | val extension LogicProblemBuilder builder = new LogicProblemBuilder | 43 | val extension LogicProblemBuilder builder = new LogicProblemBuilder |
36 | val Ecore2Logic ecore2Logic | 44 | val Ecore2Logic ecore2Logic |
45 | val ExpressionEvaluation2Logic expressionEvaliation2Logic = new ExpressionEvaluation2Logic | ||
46 | val expressionExtractor = new XExpressionExtractor | ||
37 | 47 | ||
38 | new(Ecore2Logic ecore2Logic) { | 48 | new(Ecore2Logic ecore2Logic) { |
39 | this.ecore2Logic = ecore2Logic | 49 | this.ecore2Logic = ecore2Logic |
@@ -269,6 +279,69 @@ class Constraint2Logic { | |||
269 | } else throw new IllegalArgumentException('''unknown tuple: «tuple»''') | 279 | } else throw new IllegalArgumentException('''unknown tuple: «tuple»''') |
270 | } | 280 | } |
271 | 281 | ||
282 | def dispatch Term transformConstraint(AggregatorConstraint constraint, | ||
283 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
284 | Viatra2LogicTrace viatra2LogicTrace, | ||
285 | Map<PVariable, Variable> variable2Variable, | ||
286 | Viatra2LogicConfiguration config) | ||
287 | { | ||
288 | val logicReferred = constraint.referredQuery.lookup(viatra2LogicTrace.query2Relation) | ||
289 | val parameterSubstitution = new LinkedList | ||
290 | for(index : 0..<constraint.actualParametersTuple.size) { | ||
291 | val term = (constraint.actualParametersTuple.get(index) as PVariable).lookup(variable2Variable) | ||
292 | parameterSubstitution += term | ||
293 | } | ||
294 | val aggregatorIndex = constraint.aggregatedColumn | ||
295 | val logicResultVariable = constraint.resultVariable.lookup(variable2Variable) | ||
296 | val type = constraint.aggregator.operator | ||
297 | if(type === null) { | ||
298 | return Count(logicReferred,parameterSubstitution,logicResultVariable) | ||
299 | } else if(type instanceof IntegerSumOperator || type instanceof DoubleSumOperator || type instanceof LongSumOperator){ | ||
300 | return Sum(logicReferred,parameterSubstitution,aggregatorIndex,logicResultVariable) | ||
301 | } else if(type instanceof ExtremumOperator) { | ||
302 | if(type.name == Extreme.MIN.name.toLowerCase) { | ||
303 | return Min(logicReferred,parameterSubstitution,aggregatorIndex,logicResultVariable) | ||
304 | } else if(type.name == Extreme.MAX.name.toLowerCase){ | ||
305 | return Max(logicReferred,parameterSubstitution,aggregatorIndex,logicResultVariable) | ||
306 | } else { | ||
307 | throw new UnsupportedOperationException('''Unkown Extremum aggregator type: «type.name»''') | ||
308 | } | ||
309 | } else { | ||
310 | throw new UnsupportedOperationException('''Unkown aggregator type: «type.name»''') | ||
311 | } | ||
312 | } | ||
313 | |||
314 | def dispatch Term transformConstraint(PatternMatchCounter constraint, | ||
315 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
316 | Viatra2LogicTrace viatra2LogicTrace, | ||
317 | Map<PVariable, Variable> variable2Variable, | ||
318 | Viatra2LogicConfiguration config) | ||
319 | { | ||
320 | val logicReferred = constraint.referredQuery.lookup(viatra2LogicTrace.query2Relation) | ||
321 | val parameterSubstitution = new LinkedList | ||
322 | for(index : 0..<constraint.actualParametersTuple.size) { | ||
323 | val term = (constraint.actualParametersTuple.get(index) as PVariable).lookup(variable2Variable) | ||
324 | parameterSubstitution += term | ||
325 | } | ||
326 | val logicResultVariable = constraint.resultVariable.lookup(variable2Variable) | ||
327 | return Count(logicReferred,parameterSubstitution,logicResultVariable) | ||
328 | } | ||
329 | |||
330 | def dispatch Term transformConstraint(ExpressionEvaluation constraint, | ||
331 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
332 | Viatra2LogicTrace viatra2LogicTrace, | ||
333 | Map<PVariable, Variable> variable2Variable, | ||
334 | Viatra2LogicConfiguration config) | ||
335 | { | ||
336 | val outputVariable = constraint.outputVariable | ||
337 | val expression = expressionExtractor.extractExpression(constraint.evaluator) | ||
338 | if(outputVariable === null) { | ||
339 | return expressionEvaliation2Logic.transformCheck(expression,variable2Variable) | ||
340 | } else { | ||
341 | return expressionEvaliation2Logic.transformEval(outputVariable,expression,variable2Variable) | ||
342 | } | ||
343 | } | ||
344 | |||
272 | def dispatch Term transformConstraint(PConstraint constraint, | 345 | def dispatch Term transformConstraint(PConstraint constraint, |
273 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | 346 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, |
274 | Viatra2LogicTrace viatra2LogicTrace, | 347 | Viatra2LogicTrace viatra2LogicTrace, |
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExampleRecreation.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExampleRecreation.java new file mode 100644 index 00000000..a3d25ccf --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExampleRecreation.java | |||
@@ -0,0 +1,120 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; | ||
2 | |||
3 | import java.util.HashMap; | ||
4 | |||
5 | import com.microsoft.z3.*; | ||
6 | |||
7 | public class ExampleRecreation { | ||
8 | |||
9 | |||
10 | public static void sudoku(Context ctx) { | ||
11 | |||
12 | // 9 * 9 int matrix | ||
13 | IntExpr[][] X = new IntExpr[9][]; | ||
14 | for (int i = 0; i < 9; i++) { | ||
15 | X[i] = new IntExpr[9]; | ||
16 | for (int j = 0; j < 9; j++) { | ||
17 | X[i][j] = (IntExpr) ctx.mkConst(ctx.mkSymbol("x_" + (i + 1) + "_" + (j + 1)), ctx.getIntSort()); | ||
18 | } | ||
19 | } | ||
20 | |||
21 | // Cell value from 1 - 9 | ||
22 | BoolExpr[][] cells = new BoolExpr[9][]; | ||
23 | for (int i = 0; i < 9; i++) { | ||
24 | cells[i] = new BoolExpr[9]; | ||
25 | for (int j = 0; j < 9; j++) { | ||
26 | cells[i][j] = ctx.mkAnd(ctx.mkLe(ctx.mkInt(1), X[i][j]), ctx.mkLe(X[i][j], ctx.mkInt(9))); | ||
27 | } | ||
28 | } | ||
29 | |||
30 | // Each value in a row is distinct | ||
31 | BoolExpr[] row = new BoolExpr[9]; | ||
32 | for (int i = 0; i < 9; i++) { | ||
33 | row[i] = ctx.mkDistinct(X[i]); | ||
34 | } | ||
35 | |||
36 | // Each value in a col is distinct | ||
37 | BoolExpr[] col = new BoolExpr[9]; | ||
38 | for (int j = 0; j < 9; j++) { | ||
39 | IntExpr[] one_col = new IntExpr[9]; | ||
40 | for (int i = 0; i < 9; i++) { | ||
41 | one_col[i] = X[i][j]; | ||
42 | } | ||
43 | col[j] = ctx.mkDistinct(one_col); | ||
44 | } | ||
45 | |||
46 | |||
47 | // Each value in a 3*3 square is distinct | ||
48 | BoolExpr[][] squares = new BoolExpr[3][]; | ||
49 | for (int x = 0; x < 3; x++) { | ||
50 | squares[x] = new BoolExpr[3]; | ||
51 | for (int y = 0; y < 3; y++) { | ||
52 | IntExpr[] square = new IntExpr[9]; | ||
53 | for (int i = 0; i < 3; i++) { | ||
54 | for (int j = 0; j < 3; j++) { | ||
55 | square[3 * i + j] = X[3 * x + i][3 * y + j]; | ||
56 | } | ||
57 | } | ||
58 | squares[x][y] = ctx.mkDistinct(square); | ||
59 | } | ||
60 | } | ||
61 | |||
62 | // Combine all conditions | ||
63 | BoolExpr sudoku = ctx.mkTrue(); | ||
64 | for (BoolExpr[] e: cells) { | ||
65 | sudoku = ctx.mkAnd(ctx.mkAnd(e), sudoku); | ||
66 | } | ||
67 | sudoku = ctx.mkAnd(ctx.mkAnd(row), sudoku); | ||
68 | sudoku = ctx.mkAnd(ctx.mkAnd(col), sudoku); | ||
69 | for (BoolExpr[] e: squares) { | ||
70 | sudoku = ctx.mkAnd(ctx.mkAnd(e), sudoku); | ||
71 | } | ||
72 | |||
73 | int[][] instance = { { 0, 0, 0, 0, 9, 4, 0, 3, 0 }, | ||
74 | { 0, 0, 0, 5, 1, 0, 0, 0, 7 }, { 0, 8, 9, 0, 0, 0, 0, 4, 0 }, | ||
75 | { 0, 0, 0, 0, 0, 0, 2, 0, 8 }, { 0, 6, 0, 2, 0, 1, 0, 5, 0 }, | ||
76 | { 1, 0, 2, 0, 0, 0, 0, 0, 0 }, { 0, 7, 0, 0, 0, 0, 5, 2, 0 }, | ||
77 | { 9, 0, 0, 0, 6, 5, 0, 0, 0 }, { 0, 4, 0, 9, 7, 0, 0, 0, 0 } }; | ||
78 | |||
79 | // Set assertions enforced by the instance | ||
80 | BoolExpr inst = ctx.mkTrue(); | ||
81 | for (int i = 0; i < 9; i++) { | ||
82 | for (int j = 0; j < 9; j++) { | ||
83 | inst = ctx.mkAnd(inst, (BoolExpr) ctx.mkITE(ctx.mkEq(ctx.mkInt(instance[i][j]), ctx.mkInt(0)), ctx.mkTrue(), ctx.mkEq(X[i][j], ctx.mkInt(instance[i][j])))); | ||
84 | } | ||
85 | } | ||
86 | |||
87 | Solver s = ctx.mkSolver(); | ||
88 | s.add(sudoku); | ||
89 | s.add(inst); | ||
90 | |||
91 | if (s.check() == Status.SATISFIABLE) { | ||
92 | Model m = s.getModel(); | ||
93 | Expr[][] solution = new Expr[9][9]; | ||
94 | for (int i = 0; i < 9; i++) { | ||
95 | for (int j = 0; j < 9; j++) { | ||
96 | solution[i][j] = m.evaluate(X[i][j], false); | ||
97 | } | ||
98 | } | ||
99 | |||
100 | System.out.println("Sudoku solution:\n"); | ||
101 | for (int i = 0; i < 9; i++) { | ||
102 | for (int j = 0; j < 9; j++) { | ||
103 | System.out.print(solution[i][j] + " "); | ||
104 | } | ||
105 | System.out.println(); | ||
106 | } | ||
107 | } | ||
108 | else { | ||
109 | System.out.println("No solution"); | ||
110 | } | ||
111 | } | ||
112 | |||
113 | public static void main (String []args) { | ||
114 | HashMap<String, String> cfg = new HashMap<String, String>(); | ||
115 | cfg.put("model", "true"); | ||
116 | Context ctx = new Context(cfg); | ||
117 | sudoku(ctx); | ||
118 | } | ||
119 | |||
120 | } \ No newline at end of file | ||
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend new file mode 100644 index 00000000..b4303739 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend | |||
@@ -0,0 +1,140 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
6 | import java.util.Map | ||
7 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable | ||
8 | import org.eclipse.xtext.xbase.XBinaryOperation | ||
9 | import org.eclipse.xtext.xbase.XExpression | ||
10 | import org.eclipse.xtext.xbase.XFeatureCall | ||
11 | import org.eclipse.xtext.xbase.XMemberFeatureCall | ||
12 | import org.eclipse.xtext.xbase.XNumberLiteral | ||
13 | import org.eclipse.xtext.xbase.XUnaryOperation | ||
14 | |||
15 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
16 | |||
17 | class ExpressionEvaluation2Logic { | ||
18 | val extension LogicProblemBuilder builder = new LogicProblemBuilder | ||
19 | val NumericProblemSolver numericSolver = new NumericProblemSolver | ||
20 | |||
21 | def Term transformCheck(XExpression expression, Map<PVariable, Variable> variable2Variable) { | ||
22 | return expression.transform(variable2Variable) | ||
23 | } | ||
24 | |||
25 | def Term transformEval(PVariable target, XExpression expression, Map<PVariable, Variable> variable2Variable) { | ||
26 | // numericSolver.testIsNotSat(expression, expression.transform(variable2Variable)); | ||
27 | // numericSolver.testGetOneSol(expression, expression.transform(variable2Variable)); | ||
28 | // numericSolver.testGetOneSol2(expression, expression.transform(variable2Variable)); | ||
29 | // numericSolver.testGetOneSol3(expression, expression.transform(variable2Variable)); | ||
30 | // numericSolver.testIsSat(expression, expression.transform(variable2Variable)); | ||
31 | |||
32 | return expression.transform(variable2Variable) | ||
33 | } | ||
34 | |||
35 | static val N_Base = "org.eclipse.xtext.xbase.lib." | ||
36 | |||
37 | static val N_PLUS1 = "operator_plus" | ||
38 | static val N_MINUS1 = "operator_minus" | ||
39 | |||
40 | static val N_MINUS2 = "operator_minus" | ||
41 | static val N_PLUS2 = "operator_plus" | ||
42 | static val N_POWER = "operator_power" | ||
43 | static val N_MULTIPLY = "operator_multiply" | ||
44 | static val N_DIVIDE = "operator_divide" | ||
45 | static val N_MODULO = "operator_modulo" | ||
46 | static val N_LESSTHAN = "operator_lessThan" | ||
47 | static val N_LESSEQUALSTHAN = "operator_lessEqualsThan" | ||
48 | static val N_GREATERTHAN = "operator_greaterThan" | ||
49 | static val N_GREATEREQUALTHAN = "operator_greaterEqualsThan" | ||
50 | static val N_EQUALS = "operator_equals" | ||
51 | static val N_NOTEQUALS = "operator_notEquals" | ||
52 | static val N_EQUALS3 = "operator_tripleEquals" | ||
53 | static val N_NOTEQUALS3 = "operator_tripleNotEquals" | ||
54 | |||
55 | |||
56 | |||
57 | protected def isN(String name, String s) { | ||
58 | val res = name.startsWith(N_Base) && name.endsWith(s) | ||
59 | //println('''[«res»] «name» ?= «N_Base»*«s»''') | ||
60 | return res | ||
61 | } | ||
62 | |||
63 | static val N_POWER2 = "java.lang.Math.pow" | ||
64 | |||
65 | def protected dispatch Term transform(XBinaryOperation e, Map<PVariable, Variable> variable2Variable) { | ||
66 | val left = e.leftOperand.transform(variable2Variable) | ||
67 | val right = e.rightOperand.transform(variable2Variable) | ||
68 | val feature = e.feature.qualifiedName | ||
69 | if(feature.isN(N_MINUS2)) { return Minus(left,right) } | ||
70 | else if(feature.isN(N_PLUS2)) { return Plus(left,right) } | ||
71 | else if(feature.isN(N_POWER)) { return Pow(left,right) } | ||
72 | else if(feature.isN(N_MULTIPLY)) { return Multiply(left,right) } | ||
73 | else if(feature.isN(N_DIVIDE)) { return Divide(left,right) } | ||
74 | else if(feature.isN(N_MODULO)) { return Modulo(left,right) } | ||
75 | else if(feature.isN(N_LESSTHAN)) { return LessThan(left,right) } | ||
76 | else if(feature.isN(N_LESSEQUALSTHAN)) { return LessOrEqual(left,right) } | ||
77 | else if(feature.isN(N_GREATERTHAN)) { return MoreThan(left,right) } | ||
78 | else if(feature.isN(N_GREATEREQUALTHAN)) { return MoreOrEqual(left,right) } | ||
79 | else if(feature.isN(N_EQUALS)) { return Equals(left,right) } | ||
80 | else if(feature.isN(N_NOTEQUALS)) { return Distinct(left,right) } | ||
81 | else if(feature.isN(N_EQUALS3)) { return Equals(left,right) } | ||
82 | else if(feature.isN(N_NOTEQUALS3)) { return Distinct(left,right) } | ||
83 | else { | ||
84 | println("-> " + e.feature+","+e.class) | ||
85 | println("-> " + e.leftOperand) | ||
86 | println("-> " + e.rightOperand) | ||
87 | println("-> " + e.feature.qualifiedName) | ||
88 | throw new UnsupportedOperationException('''Unsupported binary operator feature: "«e.feature.class.simpleName»" - «e»''') | ||
89 | } | ||
90 | } | ||
91 | |||
92 | def protected dispatch Term transform(XUnaryOperation e, Map<PVariable, Variable> variable2Variable) { | ||
93 | val operand = e.operand.transform(variable2Variable) | ||
94 | val feature = e.feature.qualifiedName | ||
95 | if(feature.isN(N_MINUS1)) { return Minus(0.asTerm,operand)} | ||
96 | else if(feature.isN(N_PLUS1)) { return operand} | ||
97 | else{ | ||
98 | println("-> " + e.feature+","+e.class) | ||
99 | println("-> " + e.operand) | ||
100 | println("-> " + e.feature.qualifiedName) | ||
101 | throw new UnsupportedOperationException('''Unsupported unary operator feature: "«e.feature.class.simpleName»" - «e»''') | ||
102 | } | ||
103 | } | ||
104 | |||
105 | def protected dispatch Term transform(XMemberFeatureCall e, Map<PVariable, Variable> variable2Variable) { | ||
106 | val transformedArguments = e.actualArguments.map[transform(variable2Variable)] | ||
107 | val feature = e.feature.qualifiedName | ||
108 | if(feature == N_POWER2) { | ||
109 | return Pow(transformedArguments.get(0),transformedArguments.get(1)) | ||
110 | }else { | ||
111 | println(e.feature+","+e.class) | ||
112 | println(e.actualArguments.join(", ")) | ||
113 | println(e.feature.qualifiedName) | ||
114 | throw new UnsupportedOperationException('''Unsupported feature call: "«e.feature.qualifiedName»" - «e»''') | ||
115 | } | ||
116 | } | ||
117 | |||
118 | def protected dispatch Term transform(XFeatureCall e, Map<PVariable,Variable> variable2Variable) { | ||
119 | val featureName = e.feature.qualifiedName | ||
120 | val entryWithName = variable2Variable.entrySet.filter[it.key.name == featureName].head | ||
121 | if(entryWithName !== null) { | ||
122 | return entryWithName.value.toTerm | ||
123 | } else { | ||
124 | throw new IllegalArgumentException('''Feature call reference to unavailable variable "«featureName»"''') | ||
125 | } | ||
126 | } | ||
127 | |||
128 | def protected dispatch Term transform(XNumberLiteral l, Map<PVariable, Variable> variable2Variable) { | ||
129 | val s = l.value | ||
130 | try{ return Integer.parseInt(s).asTerm } catch(NumberFormatException e){} | ||
131 | try{ return Short.parseShort(s).asTerm } catch(NumberFormatException e){} | ||
132 | try{ return Double.parseDouble(s).asTerm } catch(NumberFormatException e){} | ||
133 | try{ return Float.parseFloat(s).asTerm } catch(NumberFormatException e){} | ||
134 | throw new UnsupportedOperationException('''Unsupported numeric type: "«s»"''') | ||
135 | } | ||
136 | |||
137 | def protected dispatch Term transform(XExpression e, Map<PVariable, Variable> variable2Variable) { | ||
138 | throw new UnsupportedOperationException('''Unsupported expression: "«e.class.simpleName»" - «e»''') | ||
139 | } | ||
140 | } \ No newline at end of file | ||
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/FakeIntegerElement.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/FakeIntegerElement.java new file mode 100644 index 00000000..7b8634c4 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/FakeIntegerElement.java | |||
@@ -0,0 +1,169 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; | ||
2 | |||
3 | import java.lang.reflect.InvocationTargetException; | ||
4 | |||
5 | import org.eclipse.emf.common.notify.Adapter; | ||
6 | import org.eclipse.emf.common.notify.Notification; | ||
7 | import org.eclipse.emf.common.util.EList; | ||
8 | import org.eclipse.emf.common.util.TreeIterator; | ||
9 | import org.eclipse.emf.ecore.EClass; | ||
10 | import org.eclipse.emf.ecore.EObject; | ||
11 | import org.eclipse.emf.ecore.EOperation; | ||
12 | import org.eclipse.emf.ecore.EReference; | ||
13 | import org.eclipse.emf.ecore.EStructuralFeature; | ||
14 | import org.eclipse.emf.ecore.resource.Resource; | ||
15 | |||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | ||
18 | |||
19 | public class FakeIntegerElement implements PrimitiveElement{ | ||
20 | |||
21 | public FakeIntegerElement() { | ||
22 | |||
23 | } | ||
24 | |||
25 | @Override | ||
26 | public EList<TypeDefinition> getDefinedInType() { | ||
27 | // TODO Auto-generated method stub | ||
28 | return null; | ||
29 | } | ||
30 | |||
31 | @Override | ||
32 | public String getName() { | ||
33 | // TODO Auto-generated method stub | ||
34 | return null; | ||
35 | } | ||
36 | |||
37 | @Override | ||
38 | public void setName(String value) { | ||
39 | // TODO Auto-generated method stub | ||
40 | |||
41 | } | ||
42 | |||
43 | @Override | ||
44 | public EClass eClass() { | ||
45 | // TODO Auto-generated method stub | ||
46 | return null; | ||
47 | } | ||
48 | |||
49 | @Override | ||
50 | public Resource eResource() { | ||
51 | // TODO Auto-generated method stub | ||
52 | return null; | ||
53 | } | ||
54 | |||
55 | @Override | ||
56 | public EObject eContainer() { | ||
57 | // TODO Auto-generated method stub | ||
58 | return null; | ||
59 | } | ||
60 | |||
61 | @Override | ||
62 | public EStructuralFeature eContainingFeature() { | ||
63 | // TODO Auto-generated method stub | ||
64 | return null; | ||
65 | } | ||
66 | |||
67 | @Override | ||
68 | public EReference eContainmentFeature() { | ||
69 | // TODO Auto-generated method stub | ||
70 | return null; | ||
71 | } | ||
72 | |||
73 | @Override | ||
74 | public EList<EObject> eContents() { | ||
75 | // TODO Auto-generated method stub | ||
76 | return null; | ||
77 | } | ||
78 | |||
79 | @Override | ||
80 | public TreeIterator<EObject> eAllContents() { | ||
81 | // TODO Auto-generated method stub | ||
82 | return null; | ||
83 | } | ||
84 | |||
85 | @Override | ||
86 | public boolean eIsProxy() { | ||
87 | // TODO Auto-generated method stub | ||
88 | return false; | ||
89 | } | ||
90 | |||
91 | @Override | ||
92 | public EList<EObject> eCrossReferences() { | ||
93 | // TODO Auto-generated method stub | ||
94 | return null; | ||
95 | } | ||
96 | |||
97 | @Override | ||
98 | public Object eGet(EStructuralFeature feature) { | ||
99 | // TODO Auto-generated method stub | ||
100 | return null; | ||
101 | } | ||
102 | |||
103 | @Override | ||
104 | public Object eGet(EStructuralFeature feature, boolean resolve) { | ||
105 | // TODO Auto-generated method stub | ||
106 | return null; | ||
107 | } | ||
108 | |||
109 | @Override | ||
110 | public void eSet(EStructuralFeature feature, Object newValue) { | ||
111 | // TODO Auto-generated method stub | ||
112 | |||
113 | } | ||
114 | |||
115 | @Override | ||
116 | public boolean eIsSet(EStructuralFeature feature) { | ||
117 | // TODO Auto-generated method stub | ||
118 | return false; | ||
119 | } | ||
120 | |||
121 | @Override | ||
122 | public void eUnset(EStructuralFeature feature) { | ||
123 | // TODO Auto-generated method stub | ||
124 | |||
125 | } | ||
126 | |||
127 | @Override | ||
128 | public Object eInvoke(EOperation operation, EList<?> arguments) throws InvocationTargetException { | ||
129 | // TODO Auto-generated method stub | ||
130 | return null; | ||
131 | } | ||
132 | |||
133 | @Override | ||
134 | public EList<Adapter> eAdapters() { | ||
135 | // TODO Auto-generated method stub | ||
136 | return null; | ||
137 | } | ||
138 | |||
139 | @Override | ||
140 | public boolean eDeliver() { | ||
141 | // TODO Auto-generated method stub | ||
142 | return false; | ||
143 | } | ||
144 | |||
145 | @Override | ||
146 | public void eSetDeliver(boolean deliver) { | ||
147 | // TODO Auto-generated method stub | ||
148 | |||
149 | } | ||
150 | |||
151 | @Override | ||
152 | public void eNotify(Notification notification) { | ||
153 | // TODO Auto-generated method stub | ||
154 | |||
155 | } | ||
156 | |||
157 | @Override | ||
158 | public boolean isValueSet() { | ||
159 | // TODO Auto-generated method stub | ||
160 | return false; | ||
161 | } | ||
162 | |||
163 | @Override | ||
164 | public void setValueSet(boolean value) { | ||
165 | // TODO Auto-generated method stub | ||
166 | |||
167 | } | ||
168 | |||
169 | } | ||
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java new file mode 100644 index 00000000..0b249962 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java | |||
@@ -0,0 +1,473 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; | ||
2 | |||
3 | import java.math.BigDecimal; | ||
4 | import java.util.ArrayList; | ||
5 | import java.util.HashMap; | ||
6 | import java.util.HashSet; | ||
7 | import java.util.List; | ||
8 | import java.util.Map; | ||
9 | import java.util.Map.Entry; | ||
10 | import java.util.Random; | ||
11 | import java.util.Set; | ||
12 | |||
13 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint; | ||
14 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation; | ||
15 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; | ||
16 | import org.eclipse.xtext.xbase.XBinaryOperation; | ||
17 | import org.eclipse.xtext.xbase.XExpression; | ||
18 | import org.eclipse.xtext.xbase.XFeatureCall; | ||
19 | import org.eclipse.xtext.xbase.XNumberLiteral; | ||
20 | |||
21 | import com.microsoft.z3.ArithExpr; | ||
22 | import com.microsoft.z3.BoolExpr; | ||
23 | import com.microsoft.z3.Context; | ||
24 | import com.microsoft.z3.Expr; | ||
25 | import com.microsoft.z3.IntExpr; | ||
26 | import com.microsoft.z3.Model; | ||
27 | import com.microsoft.z3.RealExpr; | ||
28 | import com.microsoft.z3.Solver; | ||
29 | import com.microsoft.z3.Status; | ||
30 | import com.microsoft.z3.enumerations.Z3_ast_print_mode; | ||
31 | |||
32 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | ||
33 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; | ||
34 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; | ||
35 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | ||
36 | |||
37 | |||
38 | public class NumericProblemSolver { | ||
39 | private static final String N_Base = "org.eclipse.xtext.xbase.lib."; | ||
40 | private static final String N_PLUS = "operator_plus"; | ||
41 | private static final String N_MINUS = "operator_minus"; | ||
42 | private static final String N_POWER = "operator_power"; | ||
43 | private static final String N_MULTIPLY = "operator_multiply"; | ||
44 | private static final String N_DIVIDE = "operator_divide"; | ||
45 | private static final String N_MODULO = "operator_modulo"; | ||
46 | private static final String N_LESSTHAN = "operator_lessThan"; | ||
47 | private static final String N_LESSEQUALSTHAN = "operator_lessEqualsThan"; | ||
48 | private static final String N_GREATERTHAN = "operator_greaterThan"; | ||
49 | private static final String N_GREATEREQUALTHAN = "operator_greaterEqualsThan"; | ||
50 | private static final String N_EQUALS = "operator_equals"; | ||
51 | private static final String N_NOTEQUALS = "operator_notEquals"; | ||
52 | private static final String N_EQUALS3 = "operator_tripleEquals"; | ||
53 | private static final String N_NOTEQUALS3 = "operator_tripleNotEquals"; | ||
54 | |||
55 | |||
56 | private Context ctx; | ||
57 | private Solver s; | ||
58 | private Map<Object, Expr> varMap; | ||
59 | |||
60 | long endformingProblem=0; | ||
61 | long endSolvingProblem=0; | ||
62 | long endFormingSolution=0; | ||
63 | |||
64 | public NumericProblemSolver() { | ||
65 | HashMap<String, String> cfg = new HashMap<String, String>(); | ||
66 | cfg.put("model", "true"); | ||
67 | ctx = new Context(cfg); | ||
68 | ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL); | ||
69 | s = ctx.mkSolver(); | ||
70 | varMap = new HashMap<Object, Expr>(); | ||
71 | } | ||
72 | |||
73 | public Context getNumericProblemContext() { | ||
74 | return ctx; | ||
75 | } | ||
76 | |||
77 | public long getEndformingProblem() { | ||
78 | return endformingProblem; | ||
79 | } | ||
80 | |||
81 | public long getEndSolvingProblem() { | ||
82 | return endSolvingProblem; | ||
83 | } | ||
84 | |||
85 | public long getEndFormingSolution() { | ||
86 | return endFormingSolution; | ||
87 | } | ||
88 | |||
89 | private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) { | ||
90 | ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); | ||
91 | XExpression left = ((XBinaryOperation) expression).getLeftOperand(); | ||
92 | XExpression right = ((XBinaryOperation) expression).getRightOperand(); | ||
93 | |||
94 | getJvmIdentifiableElementsHelper(left, allElem); | ||
95 | getJvmIdentifiableElementsHelper(right, allElem); | ||
96 | return allElem; | ||
97 | } | ||
98 | |||
99 | private void getJvmIdentifiableElementsHelper(XExpression e, List<JvmIdentifiableElement> allElem) { | ||
100 | if (e instanceof XFeatureCall) { | ||
101 | allElem.add(((XFeatureCall) e).getFeature()); | ||
102 | } else if (e instanceof XBinaryOperation) { | ||
103 | getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getLeftOperand(), allElem); | ||
104 | getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem); | ||
105 | } | ||
106 | } | ||
107 | |||
108 | public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | ||
109 | long startformingProblem = System.nanoTime(); | ||
110 | BoolExpr problemInstance = formNumericProblemInstance(matches); | ||
111 | s.add(problemInstance); | ||
112 | endformingProblem = System.nanoTime()-startformingProblem; | ||
113 | long startSolvingProblem = System.nanoTime(); | ||
114 | boolean result = (s.check() == Status.SATISFIABLE); | ||
115 | endSolvingProblem = System.nanoTime()-startSolvingProblem; | ||
116 | this.ctx.close(); | ||
117 | return result; | ||
118 | } | ||
119 | |||
120 | public Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | ||
121 | Map<PrimitiveElement,Number> sol = new HashMap<PrimitiveElement, Number>(); | ||
122 | long startformingProblem = System.nanoTime(); | ||
123 | BoolExpr problemInstance = formNumericProblemInstance(matches); | ||
124 | endformingProblem = System.nanoTime()-startformingProblem; | ||
125 | //System.out.println("Forming problem: " + (endformingProblem - startformingProblem)); | ||
126 | s.add(problemInstance); | ||
127 | long startSolvingProblem = System.nanoTime(); | ||
128 | if (s.check() == Status.SATISFIABLE) { | ||
129 | Model m = s.getModel(); | ||
130 | endSolvingProblem = System.nanoTime()-startSolvingProblem; | ||
131 | //System.out.println("Solving problem: " + (endSolvingProblem - startSolvingProblem)); | ||
132 | long startFormingSolution = System.nanoTime(); | ||
133 | for (PrimitiveElement o: objs) { | ||
134 | if(varMap.containsKey(o)) { | ||
135 | if (o instanceof IntegerElement) { | ||
136 | IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false); | ||
137 | Integer oSol = Integer.parseInt(val.toString()); | ||
138 | sol.put(o, oSol); | ||
139 | } else { | ||
140 | RealExpr val = (RealExpr) m.evaluate(varMap.get(o), false); | ||
141 | Double oSol = Double.parseDouble(val.toString()); | ||
142 | sol.put(o, oSol); | ||
143 | } | ||
144 | //System.out.println("Solution:" + o + "->" + oSol); | ||
145 | |||
146 | } else { | ||
147 | //System.out.println("not used var:" + o); | ||
148 | } | ||
149 | } | ||
150 | endFormingSolution = System.nanoTime()-startFormingSolution; | ||
151 | //System.out.println("Forming solution: " + (endFormingSolution - startFormingSolution)); | ||
152 | } else { | ||
153 | System.out.println("Unsatisfiable numerical problem"); | ||
154 | } | ||
155 | this.ctx.close(); | ||
156 | return sol; | ||
157 | } | ||
158 | |||
159 | private BoolExpr formNumericConstraint(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception { | ||
160 | if (!(e instanceof XBinaryOperation)) { | ||
161 | throw new Exception ("error in check expression!!!"); | ||
162 | } | ||
163 | |||
164 | String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); | ||
165 | |||
166 | BoolExpr constraint = null; | ||
167 | |||
168 | ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); | ||
169 | ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); | ||
170 | |||
171 | if (nameEndsWith(name, N_LESSTHAN)) { | ||
172 | constraint = ctx.mkLt(left_operand, right_operand); | ||
173 | } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) { | ||
174 | constraint = ctx.mkLe(left_operand, right_operand); | ||
175 | } else if (nameEndsWith(name, N_GREATERTHAN)) { | ||
176 | constraint = ctx.mkGt(left_operand, right_operand); | ||
177 | } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) { | ||
178 | constraint = ctx.mkGe(left_operand, right_operand); | ||
179 | } else if (nameEndsWith(name, N_EQUALS)) { | ||
180 | constraint = ctx.mkEq(left_operand, right_operand); | ||
181 | } else if (nameEndsWith(name, N_NOTEQUALS)) { | ||
182 | constraint = ctx.mkDistinct(left_operand, right_operand); | ||
183 | } else if (nameEndsWith(name, N_EQUALS3)) { | ||
184 | constraint = ctx.mkGe(left_operand, right_operand); // ??? | ||
185 | } else if (nameEndsWith(name, N_NOTEQUALS3)) { | ||
186 | constraint = ctx.mkGe(left_operand, right_operand); // ??? | ||
187 | } else { | ||
188 | throw new Exception ("Unsupported binary operation " + name); | ||
189 | } | ||
190 | |||
191 | return constraint; | ||
192 | } | ||
193 | |||
194 | private ArithExpr formNumericConstraintHelper(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception { | ||
195 | ArithExpr expr = null; | ||
196 | // Variables | ||
197 | if (e instanceof XFeatureCall) { | ||
198 | PrimitiveElement matchedObj = aMatch.get(((XFeatureCall) e).getFeature()); | ||
199 | boolean isInt = matchedObj instanceof IntegerElement; | ||
200 | if (!matchedObj.isValueSet()) { | ||
201 | if (varMap.get(matchedObj) == null) { | ||
202 | String var_name = ((XFeatureCall) e).getFeature().getQualifiedName() + matchedObj.toString(); | ||
203 | if (isInt) { | ||
204 | expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort()); | ||
205 | } else { | ||
206 | expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getRealSort()); | ||
207 | } | ||
208 | varMap.put(matchedObj, expr); | ||
209 | } else { | ||
210 | expr = (ArithExpr) varMap.get(matchedObj); | ||
211 | } | ||
212 | } else { | ||
213 | if (isInt) { | ||
214 | int value = ((IntegerElement) matchedObj).getValue(); | ||
215 | expr = (ArithExpr) ctx.mkInt(value); | ||
216 | } else { | ||
217 | double value = ((RealElement) matchedObj).getValue().doubleValue(); | ||
218 | expr = (ArithExpr) ctx.mkReal(String.valueOf(value)); | ||
219 | } | ||
220 | varMap.put(matchedObj, expr); | ||
221 | } | ||
222 | } | ||
223 | // Constants | ||
224 | else if (e instanceof XNumberLiteral) { | ||
225 | String value = ((XNumberLiteral) e).getValue(); | ||
226 | try{ | ||
227 | int val = Integer.parseInt(value); | ||
228 | expr = (ArithExpr) ctx.mkInt(val); | ||
229 | } catch(NumberFormatException err){ | ||
230 | try{ | ||
231 | expr = (ArithExpr) ctx.mkReal(value); | ||
232 | } catch(NumberFormatException err2){} | ||
233 | } | ||
234 | } | ||
235 | // Expressions with operators | ||
236 | else if (e instanceof XBinaryOperation) { | ||
237 | String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); | ||
238 | ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); | ||
239 | ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); | ||
240 | |||
241 | if (nameEndsWith(name, N_PLUS)) { | ||
242 | expr = ctx.mkAdd(left_operand, right_operand); | ||
243 | } else if (nameEndsWith(name, N_MINUS)) { | ||
244 | expr = ctx.mkAdd(left_operand, ctx.mkUnaryMinus(right_operand)); | ||
245 | } else if (nameEndsWith(name, N_POWER)) { | ||
246 | expr = ctx.mkPower(left_operand, right_operand); | ||
247 | } else if (nameEndsWith(name, N_MULTIPLY)) { | ||
248 | expr = ctx.mkMul(left_operand, right_operand); | ||
249 | } else if (nameEndsWith(name, N_DIVIDE)) { | ||
250 | expr = ctx.mkDiv(left_operand, right_operand); | ||
251 | } else if (nameEndsWith(name, N_MODULO)) { | ||
252 | expr = ctx.mkMod((IntExpr)left_operand, (IntExpr)right_operand); | ||
253 | } else { | ||
254 | throw new Exception ("Unsupported binary operation " + name); | ||
255 | } | ||
256 | } else { | ||
257 | throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); | ||
258 | } | ||
259 | return expr; | ||
260 | |||
261 | } | ||
262 | |||
263 | private boolean nameEndsWith(String name, String end) { | ||
264 | return name.startsWith(N_Base) && name.endsWith(end); | ||
265 | } | ||
266 | |||
267 | private BoolExpr formNumericProblemInstance(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | ||
268 | BoolExpr constraintInstances = ctx.mkTrue(); | ||
269 | for (XExpression e: matches.keySet()) { | ||
270 | Iterable<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e); | ||
271 | for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) { | ||
272 | BoolExpr constraintInstance = ctx.mkNot(formNumericConstraint(e, aMatch)); | ||
273 | constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance); | ||
274 | } | ||
275 | } | ||
276 | return constraintInstances; | ||
277 | } | ||
278 | |||
279 | |||
280 | /* | ||
281 | public void testIsSat(XExpression expression, Term t) throws Exception { | ||
282 | int count = 10000; | ||
283 | Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); | ||
284 | Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>(); | ||
285 | ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression); | ||
286 | |||
287 | for (int i = 0; i < count; i++) { | ||
288 | Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); | ||
289 | for (JvmIdentifiableElement e: allElem) { | ||
290 | FakeIntegerElement intE = new FakeIntegerElement(); | ||
291 | match.put(e, intE); | ||
292 | } | ||
293 | matchSet.add(match); | ||
294 | } | ||
295 | |||
296 | matches.put(expression, matchSet); | ||
297 | long start = System.currentTimeMillis(); | ||
298 | boolean sat = isSatisfiable(matches); | ||
299 | long end = System.currentTimeMillis(); | ||
300 | System.out.println(sat); | ||
301 | System.out.println("Number of matches: " + count); | ||
302 | System.out.println("Running time:" + (end - start)); | ||
303 | } | ||
304 | |||
305 | public void testIsNotSat(XExpression expression, Term t) throws Exception { | ||
306 | Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); | ||
307 | Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>(); | ||
308 | Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); | ||
309 | ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression); | ||
310 | FakeIntegerElement int1 = null; | ||
311 | FakeIntegerElement int2 = null; | ||
312 | boolean first = true; | ||
313 | for (JvmIdentifiableElement e: allElem) { | ||
314 | FakeIntegerElement intE = new FakeIntegerElement(); | ||
315 | if (first) { | ||
316 | int1 = intE; | ||
317 | first = false; | ||
318 | } else { | ||
319 | int2 = intE; | ||
320 | } | ||
321 | |||
322 | match.put(e, intE); | ||
323 | } | ||
324 | matchSet.add(match); | ||
325 | |||
326 | Map<JvmIdentifiableElement,PrimitiveElement> match2 = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); | ||
327 | boolean first2 = true; | ||
328 | for (JvmIdentifiableElement e: allElem) { | ||
329 | if (first2) { | ||
330 | match2.put(e, int2); | ||
331 | first2 = false; | ||
332 | } else { | ||
333 | match2.put(e, int1); | ||
334 | } | ||
335 | } | ||
336 | matchSet.add(match2); | ||
337 | |||
338 | matches.put(expression, matchSet); | ||
339 | long start = System.currentTimeMillis(); | ||
340 | boolean sat = isSatisfiable(matches); | ||
341 | long end = System.currentTimeMillis(); | ||
342 | System.out.println(sat); | ||
343 | System.out.println("Number of matches: "); | ||
344 | System.out.println("Running time:" + (end - start)); | ||
345 | } | ||
346 | */ | ||
347 | |||
348 | /* public void testGetOneSol(XExpression expression, Term t) throws Exception { | ||
349 | int count = 10; | ||
350 | Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>>(); | ||
351 | Iterable<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new ArrayList<Map<JvmIdentifiableElement,PrimitiveElement>>(); | ||
352 | |||
353 | ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression); | ||
354 | List<PrimitiveElement> obj = new ArrayList<PrimitiveElement>(); | ||
355 | |||
356 | for (int i = 0; i < count; i++) { | ||
357 | Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); | ||
358 | for (JvmIdentifiableElement e: allElem) { | ||
359 | FakeIntegerElement intE = new FakeIntegerElement(); | ||
360 | obj.add(intE); | ||
361 | match.put(e, intE); | ||
362 | } | ||
363 | ((ArrayList) matchSet).add(match); | ||
364 | matches.put(expression, matchSet); | ||
365 | } | ||
366 | |||
367 | long start = System.currentTimeMillis(); | ||
368 | Map<PrimitiveElement,Integer> sol = getOneSolution(obj, matches); | ||
369 | long end = System.currentTimeMillis(); | ||
370 | |||
371 | |||
372 | // Print sol | ||
373 | for (Object o: sol.keySet()) { | ||
374 | System.out.println(o + " :" + sol.get(o)); | ||
375 | } | ||
376 | |||
377 | |||
378 | System.out.println("Number of matches: " + count); | ||
379 | System.out.println("Running time:" + (end - start)); | ||
380 | }*/ | ||
381 | /* | ||
382 | public void testGetOneSol2(XExpression expression, Term t) throws Exception { | ||
383 | int count = 250; | ||
384 | Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); | ||
385 | Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>(); | ||
386 | ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression); | ||
387 | List<Object> obj = new ArrayList<Object>(); | ||
388 | for (int i = 0; i < count; i++) { | ||
389 | Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); | ||
390 | FakeIntegerElement int2 = null; | ||
391 | boolean first = false; | ||
392 | for (JvmIdentifiableElement e: allElem) { | ||
393 | FakeIntegerElement intE = new FakeIntegerElement(); | ||
394 | if (first) { | ||
395 | first = false; | ||
396 | } else { | ||
397 | int2 = intE; | ||
398 | } | ||
399 | obj.add(intE); | ||
400 | match.put(e, intE); | ||
401 | } | ||
402 | |||
403 | Map<JvmIdentifiableElement,PrimitiveElement> match2 = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); | ||
404 | boolean first2 = true; | ||
405 | for (JvmIdentifiableElement e: allElem) { | ||
406 | FakeIntegerElement intE = null; | ||
407 | if (first2) { | ||
408 | intE = int2; | ||
409 | first2 = false; | ||
410 | } else { | ||
411 | intE = new FakeIntegerElement(); | ||
412 | } | ||
413 | obj.add(intE); | ||
414 | match2.put(e, intE); | ||
415 | } | ||
416 | |||
417 | |||
418 | matchSet.add(match); | ||
419 | matchSet.add(match2); | ||
420 | } | ||
421 | matches.put(expression, matchSet); | ||
422 | |||
423 | System.out.println("Number of matches: " + matchSet.size()); | ||
424 | for (int i = 0; i < 10; i++) { | ||
425 | Map<Object,Integer> sol = getOneSolution(obj, matches); | ||
426 | System.out.println("**********************"); | ||
427 | Thread.sleep(3000); | ||
428 | } | ||
429 | } | ||
430 | |||
431 | public void testGetOneSol3(XExpression expression, Term t) throws Exception { | ||
432 | int count = 15000; | ||
433 | Random rand = new Random(); | ||
434 | Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); | ||
435 | Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>(); | ||
436 | ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression); | ||
437 | List<Object> obj = new ArrayList<Object>(); | ||
438 | for (int i = 0; i < count; i++) { | ||
439 | Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); | ||
440 | if (obj.size() > 1) { | ||
441 | for (JvmIdentifiableElement e: allElem) { | ||
442 | FakeIntegerElement intE = null; | ||
443 | int useOld = rand.nextInt(10); | ||
444 | if (useOld == 1) { | ||
445 | System.out.println("here "); | ||
446 | int index = rand.nextInt(obj.size()); | ||
447 | intE = (FakeIntegerElement) obj.get(index); | ||
448 | } else { | ||
449 | intE = new FakeIntegerElement(); | ||
450 | } | ||
451 | obj.add(intE); | ||
452 | match.put(e, intE); | ||
453 | } | ||
454 | } else { | ||
455 | for (JvmIdentifiableElement e: allElem) { | ||
456 | FakeIntegerElement intE = new FakeIntegerElement(); | ||
457 | obj.add(intE); | ||
458 | match.put(e, intE); | ||
459 | } | ||
460 | } | ||
461 | matchSet.add(match); | ||
462 | } | ||
463 | matches.put(expression, matchSet); | ||
464 | |||
465 | System.out.println("Number of matches: " + matchSet.size()); | ||
466 | for (int i = 0; i < 10; i++) { | ||
467 | Map<Object,Integer> sol = getOneSolution(obj, matches); | ||
468 | System.out.println("**********************"); | ||
469 | Thread.sleep(3000); | ||
470 | } | ||
471 | } | ||
472 | */ | ||
473 | } | ||
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend new file mode 100644 index 00000000..81bc1796 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend | |||
@@ -0,0 +1,80 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic | ||
2 | |||
3 | import org.eclipse.xtext.xbase.XExpression | ||
4 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation | ||
5 | import org.eclipse.xtext.common.types.JvmIdentifiableElement | ||
6 | import java.util.Set | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement | ||
8 | import java.util.Map | ||
9 | import com.microsoft.z3.BoolExpr | ||
10 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
11 | import java.util.Map.Entry | ||
12 | import org.eclipse.xtext.xbase.XFeatureCall | ||
13 | import java.util.Comparator | ||
14 | import java.util.ArrayList | ||
15 | import java.util.HashMap | ||
16 | import java.util.List | ||
17 | |||
18 | class NumericTranslator { | ||
19 | |||
20 | private XExpressionExtractor extractor = new XExpressionExtractor(); | ||
21 | |||
22 | long formingProblemTime=0; | ||
23 | long solvingProblemTime=0; | ||
24 | long formingSolutionTime=0; | ||
25 | |||
26 | val comparator = new Comparator<JvmIdentifiableElement>(){ | ||
27 | override compare(JvmIdentifiableElement o1, JvmIdentifiableElement o2) { | ||
28 | //println('''«o1.simpleName» - «o2.simpleName»''') | ||
29 | o1.simpleName.compareTo(o2.simpleName) | ||
30 | } | ||
31 | } | ||
32 | def Map<JvmIdentifiableElement, PrimitiveElement> arrayToMap(Object[] tuple, ArrayList<JvmIdentifiableElement> variablesInOrder) { | ||
33 | val res = new HashMap | ||
34 | for(var i=0; i<tuple.length; i++) { | ||
35 | res.put(variablesInOrder.get(i),tuple.get(i) as PrimitiveElement) | ||
36 | } | ||
37 | return res | ||
38 | } | ||
39 | def formNumericProblemInstance(Map<PConstraint, Iterable<Object[]>> matches) throws Exception { | ||
40 | val res = new HashMap | ||
41 | for (Entry<PConstraint, Iterable<Object[]>> entry: matches.entrySet()) { | ||
42 | val ExpressionEvaluation constraint = entry.getKey() as ExpressionEvaluation; | ||
43 | val XExpression expression = extractor.extractExpression(constraint.getEvaluator()); | ||
44 | val Iterable<Object[]> tuples = entry.getValue(); | ||
45 | val features = expression.eAllContents.filter(XFeatureCall).map[it.feature].toSet | ||
46 | val variablesInOrder = new ArrayList(features) | ||
47 | variablesInOrder.toList.sort(comparator) | ||
48 | //println(variablesInOrder) | ||
49 | val map = tuples.map[it.arrayToMap(variablesInOrder)] | ||
50 | res.put(expression,map) | ||
51 | } | ||
52 | return res | ||
53 | } | ||
54 | |||
55 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) { | ||
56 | val input = formNumericProblemInstance(matches) | ||
57 | val solver = new NumericProblemSolver | ||
58 | val satisfiability = solver.isSatisfiable(input) | ||
59 | solver.updateTimes | ||
60 | return satisfiability | ||
61 | } | ||
62 | |||
63 | def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches) { | ||
64 | val input = formNumericProblemInstance(matches) | ||
65 | val solver = new NumericProblemSolver | ||
66 | val solution = solver.getOneSolution(primitiveElements,input) | ||
67 | solver.updateTimes | ||
68 | return solution | ||
69 | } | ||
70 | |||
71 | private def updateTimes(NumericProblemSolver s) { | ||
72 | this.formingProblemTime += s.getEndformingProblem | ||
73 | this.solvingProblemTime += s.getEndSolvingProblem | ||
74 | this.formingSolutionTime += s.getEndFormingSolution | ||
75 | } | ||
76 | |||
77 | def getFormingProblemTime() {formingProblemTime} | ||
78 | def getSolvingProblemTime() {solvingProblemTime} | ||
79 | def getFormingSolutionTime() {formingSolutionTime} | ||
80 | } \ 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 index 3b828170..74e03f71 100644 --- 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 | |||
@@ -4,48 +4,36 @@ import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | |||
4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace | 4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition |
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
14 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | 10 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery |
15 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsFactory | 11 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsFactory |
16 | import java.util.ArrayList | 12 | import java.util.ArrayList |
17 | import java.util.HashMap | 13 | import java.util.HashMap |
18 | import java.util.HashSet | ||
19 | import java.util.LinkedList | 14 | import java.util.LinkedList |
20 | import java.util.List | 15 | import java.util.List |
21 | import java.util.Map | 16 | import java.util.Map |
22 | import java.util.Set | 17 | import java.util.Set |
23 | import org.eclipse.emf.ecore.EAttribute | 18 | import org.eclipse.emf.ecore.EAttribute |
24 | import org.eclipse.emf.ecore.EClassifier | ||
25 | import org.eclipse.emf.ecore.EEnum | ||
26 | import org.eclipse.emf.ecore.EReference | 19 | import org.eclipse.emf.ecore.EReference |
27 | import org.eclipse.emf.ecore.EStructuralFeature | 20 | import org.eclipse.emf.ecore.EStructuralFeature |
28 | import org.eclipse.emf.ecore.EcorePackage | 21 | import org.eclipse.emf.ecore.util.EcoreUtil |
29 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | 22 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification |
30 | import org.eclipse.viatra.query.runtime.emf.EMFQueryMetaContext | 23 | import org.eclipse.viatra.query.runtime.emf.EMFQueryMetaContext |
31 | import org.eclipse.viatra.query.runtime.emf.types.BaseEMFTypeKey | ||
32 | import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey | ||
33 | import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey | ||
34 | import org.eclipse.viatra.query.runtime.matchers.context.IInputKey | ||
35 | import org.eclipse.viatra.query.runtime.matchers.context.common.JavaTransitiveInstancesKey | ||
36 | import org.eclipse.viatra.query.runtime.matchers.planning.helpers.TypeHelper | ||
37 | import org.eclipse.viatra.query.runtime.matchers.psystem.PBody | 24 | import org.eclipse.viatra.query.runtime.matchers.psystem.PBody |
25 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
38 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable | 26 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable |
27 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.AggregatorConstraint | ||
39 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall | 28 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall |
29 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.PatternMatchCounter | ||
30 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction | ||
40 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter | 31 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter |
41 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 32 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
42 | import org.eclipse.viatra.query.runtime.matchers.psystem.rewriters.PBodyNormalizer | 33 | import org.eclipse.viatra.query.runtime.matchers.psystem.rewriters.PBodyNormalizer |
43 | import org.eclipse.xtend.lib.annotations.Data | 34 | import org.eclipse.xtend.lib.annotations.Data |
44 | 35 | ||
45 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 36 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
46 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction | ||
47 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
48 | import org.eclipse.viatra.query.runtime.emf.types.EClassUnscopedTransitiveInstancesKey | ||
49 | 37 | ||
50 | @Data class ViatraQuerySetDescriptor { | 38 | @Data class ViatraQuerySetDescriptor { |
51 | val List<? extends IQuerySpecification<?>> patterns | 39 | val List<? extends IQuerySpecification<?>> patterns |
@@ -57,24 +45,24 @@ class Viatra2LogicTrace { | |||
57 | public val Map<PQuery, RelationDefinition> query2Relation = new HashMap | 45 | public val Map<PQuery, RelationDefinition> query2Relation = new HashMap |
58 | public val Map<PQuery, TransfomedViatraQuery> query2Annotation = new HashMap | 46 | public val Map<PQuery, TransfomedViatraQuery> query2Annotation = new HashMap |
59 | public val Map<Pair<PQuery,PParameter>, Variable> parameter2Variable = new HashMap | 47 | public val Map<Pair<PQuery,PParameter>, Variable> parameter2Variable = new HashMap |
60 | //public val Map<PVariable, Variable> variable2Variable = new HashMap | ||
61 | } | 48 | } |
62 | class Viatra2LogicConfiguration { | 49 | class Viatra2LogicConfiguration { |
63 | public var normalize = true | 50 | public var normalize = true |
64 | public var transitiveClosureDepth = 3 | ||
65 | } | 51 | } |
66 | 52 | ||
67 | class Viatra2Logic { | 53 | class Viatra2Logic { |
68 | val extension LogicProblemBuilder builder = new LogicProblemBuilder | 54 | val extension LogicProblemBuilder builder = new LogicProblemBuilder |
69 | val extension Viatra2LogicAnnotationsFactory factory = Viatra2LogicAnnotationsFactory.eINSTANCE | 55 | val extension Viatra2LogicAnnotationsFactory factory = Viatra2LogicAnnotationsFactory.eINSTANCE |
70 | val normalizer = new PBodyNormalizer(EMFQueryMetaContext.DEFAULT) | 56 | val normalizer = new PBodyNormalizer(EMFQueryMetaContext.DEFAULT) |
57 | val Viatra2LogicTypeInferer typeInferer | ||
71 | 58 | ||
72 | val Ecore2Logic ecore2Logic | 59 | val Ecore2Logic ecore2Logic |
73 | Constraint2Logic constraint2Logic | 60 | Constraint2Logic constraint2Logic |
74 | 61 | ||
75 | new(Ecore2Logic ecore2Logic) { | 62 | new(Ecore2Logic ecore2Logic) { |
76 | this.ecore2Logic = ecore2Logic | 63 | this.ecore2Logic = ecore2Logic |
77 | constraint2Logic = new Constraint2Logic(ecore2Logic) | 64 | this.typeInferer = new Viatra2LogicTypeInferer(ecore2Logic) |
65 | this.constraint2Logic = new Constraint2Logic(ecore2Logic) | ||
78 | } | 66 | } |
79 | 67 | ||
80 | def TracedOutput<LogicProblem,Viatra2LogicTrace> transformQueries( | 68 | def TracedOutput<LogicProblem,Viatra2LogicTrace> transformQueries( |
@@ -82,65 +70,55 @@ class Viatra2Logic { | |||
82 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | 70 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, |
83 | Viatra2LogicConfiguration config) | 71 | Viatra2LogicConfiguration config) |
84 | { | 72 | { |
73 | // Create trace | ||
85 | val viatra2LogicTrace = new Viatra2LogicTrace | 74 | val viatra2LogicTrace = new Viatra2LogicTrace |
86 | val typeAlanysis = new HashMap | 75 | |
76 | // Translation works on PQueries. QuerySpecification -> PQuery. | ||
87 | val pQueries = queries.patterns.map[it.internalQueryRepresentation] | 77 | val pQueries = queries.patterns.map[it.internalQueryRepresentation] |
88 | 78 | ||
89 | for(query: pQueries) { | 79 | // If requested, the queries are normalized |
90 | val disjunction = normalizer.rewrite(query) | 80 | for(query: pQueries) { |
81 | val disjunction = normalizer.rewrite(query) | ||
91 | viatra2LogicTrace.query2Disjunction.put(query,disjunction) | 82 | viatra2LogicTrace.query2Disjunction.put(query,disjunction) |
92 | } | 83 | } |
93 | 84 | ||
94 | for(query: pQueries) { | 85 | // The types are calculated |
95 | val types = query.lookup(viatra2LogicTrace.query2Disjunction).bodies.toInvertedMap[ | 86 | val types = typeInferer.inferTypes(pQueries,ecore2LogicTrace,viatra2LogicTrace) |
96 | TypeHelper::inferUnaryTypesFor(it.uniqueVariables,it.constraints,EMFQueryMetaContext.DEFAULT) | ||
97 | ] | ||
98 | // for(m : types.values) { | ||
99 | // for(n: m.entrySet) { | ||
100 | // val variable = n.key | ||
101 | // println(''' - «variable.name»''') | ||
102 | // for(type : n.value) { | ||
103 | // println('''«variable.name» - «type»''') | ||
104 | // } | ||
105 | // } | ||
106 | // | ||
107 | // } | ||
108 | |||
109 | typeAlanysis.put(query,types) | ||
110 | } | ||
111 | 87 | ||
88 | // First, the signature of the queries are translated, ... | ||
112 | for(query: pQueries) { | 89 | for(query: pQueries) { |
113 | try { | 90 | try { |
114 | this.transformQueryHeader(query,query.lookup(typeAlanysis),ecore2LogicTrace,viatra2LogicTrace,config) | 91 | this.transformQueryHeader(query,types,ecore2LogicTrace,viatra2LogicTrace,config) |
115 | } catch(IllegalArgumentException e) { | 92 | } catch(IllegalArgumentException e) { |
116 | throw new IllegalArgumentException(''' | 93 | throw new IllegalArgumentException(''' |
117 | Unable to translate query "«query.fullyQualifiedName»". | 94 | Unable to translate query "«query.fullyQualifiedName»". |
118 | Reason: «e.class.simpleName», «e.message»''',e) | 95 | Reason: «e.class.simpleName», «e.message»''',e) |
119 | } | 96 | } |
120 | } | 97 | } |
98 | |||
99 | // ...then the bodies, ... | ||
121 | for(query: pQueries) { | 100 | for(query: pQueries) { |
122 | try { | 101 | try { |
123 | this.transformQuerySpecification(query,query.lookup(typeAlanysis),ecore2LogicTrace,viatra2LogicTrace,config) | 102 | this.transformQuerySpecification(query,types,ecore2LogicTrace,viatra2LogicTrace,config) |
124 | } catch (IllegalArgumentException e){ | 103 | } catch (IllegalArgumentException e){ |
125 | throw new IllegalArgumentException(''' | 104 | throw new IllegalArgumentException(''' |
126 | Unable to translate query "«query.fullyQualifiedName»". | 105 | Unable to translate query "«query.fullyQualifiedName»". |
127 | Reason: «e.class.simpleName», «e.message»''',e) | 106 | Reason: «e.class.simpleName», «e.message»''',e) |
128 | } | 107 | } |
129 | } | 108 | } |
130 | /*for(d : viatra2LogicTrace.query2Relation.values) { | ||
131 | checkDefinition(d) | ||
132 | }*/ | ||
133 | 109 | ||
110 | // ... and finally, the annotations. | ||
134 | transformQueryConstraints( | 111 | transformQueryConstraints( |
135 | queries.validationPatterns.map[internalQueryRepresentation], | 112 | queries.validationPatterns.map[internalQueryRepresentation], |
136 | queries.derivedFeatures, | 113 | queries.derivedFeatures, |
137 | ecore2LogicTrace,viatra2LogicTrace) | 114 | ecore2LogicTrace,viatra2LogicTrace) |
115 | |||
138 | return new TracedOutput(ecore2LogicTrace.output,viatra2LogicTrace) | 116 | return new TracedOutput(ecore2LogicTrace.output,viatra2LogicTrace) |
139 | } | 117 | } |
140 | 118 | ||
141 | def protected transformQueryHeader( | 119 | def protected transformQueryHeader( |
142 | PQuery pquery, | 120 | PQuery pquery, |
143 | Map<PBody, Map<PVariable, Set<IInputKey>>> types, | 121 | Viatra2LogicTypeResult types, |
144 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | 122 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, |
145 | Viatra2LogicTrace viatra2LogicTrace, | 123 | Viatra2LogicTrace viatra2LogicTrace, |
146 | Viatra2LogicConfiguration config) | 124 | Viatra2LogicConfiguration config) |
@@ -149,7 +127,7 @@ class Viatra2Logic { | |||
149 | val parameters = new ArrayList<Variable>(pquery.parameters.size) | 127 | val parameters = new ArrayList<Variable>(pquery.parameters.size) |
150 | for(vParam: pquery.parameters) { | 128 | for(vParam: pquery.parameters) { |
151 | val parameterName = '''parameter «vParam.name»''' | 129 | val parameterName = '''parameter «vParam.name»''' |
152 | val parameterType = getType(vParam,types,ecore2LogicTrace) | 130 | val parameterType = types.getType(pquery,vParam) |
153 | if(parameterType === null) { | 131 | if(parameterType === null) { |
154 | throw new AssertionError('''null type for parameter «vParam.name» in pattern «pquery.fullyQualifiedName»''') | 132 | throw new AssertionError('''null type for parameter «vParam.name» in pattern «pquery.fullyQualifiedName»''') |
155 | } | 133 | } |
@@ -166,6 +144,7 @@ class Viatra2Logic { | |||
166 | it.target = lRelation | 144 | it.target = lRelation |
167 | it.patternFullyQualifiedName = pquery.fullyQualifiedName | 145 | it.patternFullyQualifiedName = pquery.fullyQualifiedName |
168 | it.patternPQuery = pquery | 146 | it.patternPQuery = pquery |
147 | it.optimizedDisjunction = viatra2LogicTrace.query2Disjunction.get(pquery) | ||
169 | ] | 148 | ] |
170 | viatra2LogicTrace.query2Annotation.put(pquery,annotation) | 149 | viatra2LogicTrace.query2Annotation.put(pquery,annotation) |
171 | ecore2LogicTrace.output.annotations += annotation | 150 | ecore2LogicTrace.output.annotations += annotation |
@@ -175,7 +154,7 @@ class Viatra2Logic { | |||
175 | 154 | ||
176 | def protected transformQuerySpecification( | 155 | def protected transformQuerySpecification( |
177 | PQuery pquery, | 156 | PQuery pquery, |
178 | Map<PBody, Map<PVariable, Set<IInputKey>>> types, | 157 | Viatra2LogicTypeResult types, |
179 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | 158 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, |
180 | Viatra2LogicTrace viatra2LogicTrace, | 159 | Viatra2LogicTrace viatra2LogicTrace, |
181 | Viatra2LogicConfiguration config) | 160 | Viatra2LogicConfiguration config) |
@@ -233,7 +212,7 @@ class Viatra2Logic { | |||
233 | } | 212 | } |
234 | 213 | ||
235 | def transformBody(PBody body, | 214 | def transformBody(PBody body, |
236 | Map<PBody, Map<PVariable, Set<IInputKey>>> types, | 215 | Viatra2LogicTypeResult types, |
237 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | 216 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, |
238 | Viatra2LogicTrace viatra2LogicTrace, | 217 | Viatra2LogicTrace viatra2LogicTrace, |
239 | Viatra2LogicConfiguration config) | 218 | Viatra2LogicConfiguration config) |
@@ -248,19 +227,33 @@ class Viatra2Logic { | |||
248 | // Inner Variables | 227 | // Inner Variables |
249 | val innerPositiveVariables = new LinkedList | 228 | val innerPositiveVariables = new LinkedList |
250 | val innerNegativeVariables = new LinkedList | 229 | val innerNegativeVariables = new LinkedList |
230 | val innerAggreatedVariables = new LinkedList | ||
231 | //println(body.uniqueVariables) | ||
251 | for(innerVariable : body.uniqueVariables) { | 232 | for(innerVariable : body.uniqueVariables) { |
252 | 233 | ||
253 | if(!variable2Variable.containsKey(innerVariable)) { | 234 | if(!variable2Variable.containsKey(innerVariable)) { |
254 | val name = '''variable «innerVariable.name.normalizeName»''' | 235 | if(innerVariable.aggregateOnly) { |
255 | //println(body.pattern.fullyQualifiedName + "-") | 236 | // do not create variable |
256 | val logicType = getType(innerVariable,types,ecore2LogicTrace) | 237 | innerAggreatedVariables.add(innerVariable) |
257 | val logicVariable = createVar(name,logicType) | 238 | variable2Variable.put(innerVariable,null) |
258 | if(innerVariable.isPositiveVariable) { | ||
259 | innerPositiveVariables += logicVariable | ||
260 | } else { | 239 | } else { |
261 | innerNegativeVariables += logicVariable | 240 | val name = '''variable «innerVariable.name.normalizeName»''' |
241 | val logicType = types.getType(body,innerVariable) | ||
242 | if(logicType === null) { | ||
243 | throw new IllegalArgumentException('''Variable «innerVariable.name.normalizeName» has no type!''') | ||
244 | } | ||
245 | val logicVariable = createVar(name,logicType) | ||
246 | if(innerVariable.negativeOnly) { | ||
247 | innerNegativeVariables += logicVariable | ||
248 | } else { | ||
249 | innerPositiveVariables += logicVariable | ||
250 | } | ||
251 | variable2Variable.put(innerVariable,logicVariable) | ||
252 | body.pattern.lookup(viatra2LogicTrace.query2Annotation).variableTrace += createVariableMapping=>[ | ||
253 | it.sourcePVariable = innerVariable | ||
254 | it.targetLogicVariable = logicVariable | ||
255 | ] | ||
262 | } | 256 | } |
263 | variable2Variable.put(innerVariable,logicVariable) | ||
264 | } | 257 | } |
265 | } | 258 | } |
266 | 259 | ||
@@ -279,229 +272,39 @@ class Viatra2Logic { | |||
279 | } else { | 272 | } else { |
280 | Exists(innerPositiveVariables,allNegativeVariablesAreSatisfied); | 273 | Exists(innerPositiveVariables,allNegativeVariablesAreSatisfied); |
281 | } | 274 | } |
282 | 275 | ||
283 | return allVariablesAreExisting | 276 | return allVariablesAreExisting |
284 | } | 277 | } |
285 | // def toTypeJudgement(PVariable v, IInputKey key) { | ||
286 | // new TypeJudgement(key,new Tuple1) | ||
287 | // } | ||
288 | 278 | ||
289 | def private normalizeName(String variableName) { | 279 | def private normalizeName(String variableName) { |
290 | return variableName.replaceAll("[\\W]|_", "") | 280 | return variableName.replaceAll("[\\W]|_", "") |
291 | } | 281 | } |
292 | |||
293 | /** | ||
294 | * Translates the type of a parameter variable in a pattern | ||
295 | */ | ||
296 | def TypeReference getType(PParameter v, Map<PBody, Map<PVariable, Set<IInputKey>>> types, TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
297 | // If parameter type is specified then the specified type is used | ||
298 | if(v.declaredUnaryType !== null) { | ||
299 | val res = transformTypeReference(v.declaredUnaryType,ecore2LogicTrace) | ||
300 | if(res === null) { | ||
301 | throw new AssertionError(''' | ||
302 | Unable to translate declared type «v.declaredUnaryType». | ||
303 | ''') | ||
304 | } else { | ||
305 | return res | ||
306 | } | ||
307 | } | ||
308 | // Otherwise, calculate the type based on the type of the variable in the bodies | ||
309 | else { | ||
310 | val bodies = types.keySet | ||
311 | val typesFromBodies = new ArrayList(bodies.size) | ||
312 | for(body : bodies) { | ||
313 | // collect the variable in the body | ||
314 | val exported = body.symbolicParameters.filter[it.patternParameter === v] | ||
315 | if(exported.size !== 1) { | ||
316 | throw new AssertionError('''Parameter «v.name» has no reference in body!''') | ||
317 | } | ||
318 | val variable = exported.head.parameterVariable | ||
319 | typesFromBodies+=variable.getType(types,ecore2LogicTrace) | ||
320 | } | ||
321 | return typesFromBodies.calculateCommonSupertype | ||
322 | } | ||
323 | } | ||
324 | |||
325 | /** | ||
326 | * Translates the type of a variable in a pattern body | ||
327 | */ | ||
328 | def TypeReference getType(PVariable v, Map<PBody, Map<PVariable, Set<IInputKey>>> types ,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
329 | if (v.isPositiveVariable) { | ||
330 | val keys = getTypesFromCollection(v,types) | ||
331 | val logicTypes = keys.map[transformTypeReference(it,ecore2LogicTrace)].filterNull | ||
332 | return logicTypes.calculateCommonSubtype | ||
333 | } else { | ||
334 | val onlyConstraint = v.referringConstraints.head as NegativePatternCall | ||
335 | val indexOfVariable = v.lookup(onlyConstraint.actualParametersTuple.invertIndex) | ||
336 | val parameter = onlyConstraint.referredQuery.parameters.get(indexOfVariable) | ||
337 | val declaredUnaryType = parameter.declaredUnaryType as BaseEMFTypeKey<? extends EClassifier> | ||
338 | if (declaredUnaryType === null) { | ||
339 | throw new UnsupportedOperationException( | ||
340 | '''parameter «parameter.name» in pattern «onlyConstraint.referredQuery.fullyQualifiedName» does not have type!''') | ||
341 | } else | ||
342 | return declaredUnaryType.transformTypeReference(ecore2LogicTrace) | ||
343 | } | ||
344 | } | ||
345 | |||
346 | def getTypesFromCollection(PVariable v, Map<PBody, Map<PVariable, Set<IInputKey>>> types) { | ||
347 | for(entry : types.entrySet) { | ||
348 | if(entry.key.uniqueVariables.contains(v)) { | ||
349 | return v.lookup(entry.value) | ||
350 | } | ||
351 | } | ||
352 | throw new IllegalArgumentException('''Variable «v.name» is not present in neither of the bodies!''') | ||
353 | } | ||
354 | |||
355 | 282 | ||
356 | def TypeReference calculateCommonSubtype(Iterable<TypeReference> types) { | 283 | def isNegativeOnly(PVariable variable) { |
357 | val primitiveTypeReferences = types.filter(PrimitiveTypeReference) | 284 | if(variable.referringConstraints.size == 1) { |
358 | val complexTypeReferences = types.filter(ComplexTypeReference) | 285 | val PConstraint onlyConstraint = variable.referringConstraints.head |
359 | if(complexTypeReferences.isEmpty) { | 286 | if(onlyConstraint instanceof NegativePatternCall) { |
360 | val head = primitiveTypeReferences.head | 287 | return true |
361 | if(primitiveTypeReferences.exists[it.eClass !== head.eClass]) { | 288 | } else { |
362 | throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''') | 289 | return false |
363 | } | ||
364 | return head | ||
365 | } else if(primitiveTypeReferences.isEmpty) { | ||
366 | val complexTypes = complexTypeReferences.map[it.referred].toSet | ||
367 | if(complexTypes.size === 1) { | ||
368 | return builder.toTypeReference(complexTypes.head) | ||
369 | } | ||
370 | // Collect possible subtypes | ||
371 | val subtypeSets = complexTypes.map[it.transitiveClosureStar[it.subtypes].toSet] | ||
372 | val commonTypeSet = new HashSet(subtypeSets.head) | ||
373 | val otherSets = subtypeSets.tail | ||
374 | for(otherSet : otherSets) { | ||
375 | commonTypeSet.retainAll(otherSet) | ||
376 | } | ||
377 | if(commonTypeSet.empty) { | ||
378 | throw new IllegalArgumentException('''Inconsistent types: «complexTypes.map[name].toList»''') | ||
379 | } | ||
380 | |||
381 | return calculateCommonComplexSupertype(commonTypeSet) | ||
382 | |||
383 | } else { | ||
384 | throw new IllegalArgumentException(''' | ||
385 | Inconsistent types, mixing primitive and complex types: | ||
386 | «primitiveTypeReferences.map[eClass.name].toSet.toList» | ||
387 | and | ||
388 | «complexTypeReferences.map[it.referred].toSet.map[name].toList»''') | ||
389 | |||
390 | } | ||
391 | } | ||
392 | def TypeReference calculateCommonSupertype(Iterable<TypeReference> types) { | ||
393 | val primitiveTypeReferences = types.filter(PrimitiveTypeReference) | ||
394 | val complexTypeReferences = types.filter(ComplexTypeReference) | ||
395 | if(complexTypeReferences.isEmpty) { | ||
396 | val head = primitiveTypeReferences.head | ||
397 | if(primitiveTypeReferences.exists[it.eClass !== head.eClass]) { | ||
398 | throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''') | ||
399 | } | ||
400 | return head | ||
401 | } else if(primitiveTypeReferences.isEmpty) { | ||
402 | val complexTypes = complexTypeReferences.map[it.referred].toSet | ||
403 | return calculateCommonComplexSupertype(complexTypes) | ||
404 | |||
405 | } else { | ||
406 | throw new IllegalArgumentException(''' | ||
407 | Inconsistent types, mixing primitive and complex types: | ||
408 | «primitiveTypeReferences.map[eClass.name].toSet.toList» | ||
409 | and | ||
410 | «complexTypeReferences.map[it.referred].toSet.map[name].toList»''') | ||
411 | |||
412 | } | ||
413 | } | ||
414 | def TypeReference calculateCommonComplexSupertype(Set<Type> complexTypes) { | ||
415 | if(complexTypes.size === 1) { | ||
416 | return builder.toTypeReference(complexTypes.head) | ||
417 | } | ||
418 | // Collect possible supertypes | ||
419 | val supertypeSets = complexTypes.map[it.transitiveClosureStar[it.supertypes].toSet] | ||
420 | val commonTypeSet = new HashSet(supertypeSets.head) | ||
421 | val otherSets = supertypeSets.tail | ||
422 | for(otherSet : otherSets) { | ||
423 | commonTypeSet.retainAll(otherSet) | ||
424 | } | ||
425 | if(commonTypeSet.empty) { | ||
426 | throw new IllegalArgumentException('''Inconsistent types: «complexTypes.map[name].toList»''') | ||
427 | } | ||
428 | // Remove type that already have covered | ||
429 | val coveredTypes = commonTypeSet.map[it.supertypes].flatten | ||
430 | commonTypeSet.removeAll(coveredTypes) | ||
431 | return builder.toTypeReference(commonTypeSet.head) | ||
432 | } | ||
433 | |||
434 | /** | ||
435 | * Transforms a Viatra type reference to a logic type. | ||
436 | */ | ||
437 | def dispatch TypeReference transformTypeReference(EDataTypeInSlotsKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
438 | val w = k.wrappedKey | ||
439 | if(w == EcorePackage.Literals.EINT || w == EcorePackage.Literals.ESHORT || w == EcorePackage.Literals.ELONG) { | ||
440 | return builder.LogicInt | ||
441 | } else if(w == EcorePackage.Literals.EDOUBLE || w == EcorePackage.Literals.EFLOAT) { | ||
442 | return builder.LogicReal | ||
443 | } else if(w == EcorePackage.Literals.EBOOLEAN) { | ||
444 | return builder.LogicBool | ||
445 | } else if(w == EcorePackage.Literals.ESTRING) { | ||
446 | return builder.LogicString | ||
447 | } else if(w instanceof EEnum) { | ||
448 | val c = this.ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,w) | ||
449 | return builder.toTypeReference(c); | ||
450 | } else throw new UnsupportedOperationException('''Unknown reference type «w.class.name»''') | ||
451 | } | ||
452 | def dispatch TypeReference transformTypeReference(JavaTransitiveInstancesKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
453 | val c = k.wrapperInstanceClass | ||
454 | if(c == Integer || c == Long || c == Short) { | ||
455 | return LogicInt | ||
456 | } else if(c == Float || c == Double) { | ||
457 | return LogicReal | ||
458 | } else if(c == Boolean) { | ||
459 | return LogicBool | ||
460 | } else if(c == String) { | ||
461 | return LogicString | ||
462 | } else if(c.superclass == java.lang.Enum){ | ||
463 | val enums = ecore2Logic.allEnumsInScope(ecore2LogicTrace.trace) | ||
464 | for(enum : enums) { | ||
465 | if(c == enum.instanceClass) { | ||
466 | return builder.toTypeReference(ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,enum)) | ||
467 | } | ||
468 | } | 290 | } |
469 | throw new IllegalArgumentException('''Enum type «c.simpleName» is not mapped to logic!''') | ||
470 | } | ||
471 | return null | ||
472 | } | ||
473 | def dispatch TypeReference transformTypeReference(EClassTransitiveInstancesKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
474 | val c = k.wrappedKey | ||
475 | |||
476 | if(this.ecore2Logic.allClassesInScope(ecore2LogicTrace.trace).toList.contains(c)) { | ||
477 | return builder.toTypeReference(this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,k.wrappedKey)) | ||
478 | } else { | 291 | } else { |
479 | return null | 292 | return false |
480 | } | 293 | } |
481 | } | 294 | } |
482 | def dispatch TypeReference transformTypeReference(EClassUnscopedTransitiveInstancesKey k, TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
483 | val c = k.wrappedKey | ||
484 | |||
485 | if(this.ecore2Logic.allClassesInScope(ecore2LogicTrace.trace).toList.contains(c)) { | ||
486 | return builder.toTypeReference(this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,k.wrappedKey)) | ||
487 | } else { | ||
488 | return null | ||
489 | } | ||
490 | } | ||
491 | |||
492 | def dispatch TypeReference transformTypeReference(IInputKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
493 | //println(k) | ||
494 | throw new IllegalArgumentException('''Unsupported type: «k.class.simpleName»''') | ||
495 | } | ||
496 | 295 | ||
497 | def boolean isPositiveVariable(PVariable v) { | 296 | def isAggregateOnly(PVariable variable) { |
498 | val constraints = v.referringConstraints | 297 | if(variable.referringConstraints.size == 1) { |
499 | if(constraints.size == 1) { | 298 | val PConstraint onlyConstraint = variable.referringConstraints.head |
500 | val onlyConstraint = constraints.head | 299 | if(onlyConstraint instanceof AggregatorConstraint) { |
501 | if(onlyConstraint instanceof NegativePatternCall) { | 300 | return true |
301 | } else if(onlyConstraint instanceof PatternMatchCounter) { | ||
302 | return true | ||
303 | } else { | ||
502 | return false | 304 | return false |
503 | } | 305 | } |
306 | } else { | ||
307 | return false | ||
504 | } | 308 | } |
505 | return true | ||
506 | } | 309 | } |
507 | } \ No newline at end of file | 310 | } \ No newline at end of file |
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeInferer.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeInferer.xtend new file mode 100644 index 00000000..b8a6b9c1 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeInferer.xtend | |||
@@ -0,0 +1,392 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
14 | import java.util.HashMap | ||
15 | import java.util.HashSet | ||
16 | import java.util.List | ||
17 | import java.util.Set | ||
18 | import org.eclipse.emf.ecore.EEnum | ||
19 | import org.eclipse.emf.ecore.EcorePackage | ||
20 | import org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguageStandaloneSetup | ||
21 | import org.eclipse.viatra.query.patternlanguage.emf.specification.XBaseEvaluator | ||
22 | import org.eclipse.viatra.query.runtime.emf.EMFQueryMetaContext | ||
23 | import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey | ||
24 | import org.eclipse.viatra.query.runtime.emf.types.EClassUnscopedTransitiveInstancesKey | ||
25 | import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey | ||
26 | import org.eclipse.viatra.query.runtime.matchers.context.IInputKey | ||
27 | import org.eclipse.viatra.query.runtime.matchers.context.common.JavaTransitiveInstancesKey | ||
28 | import org.eclipse.viatra.query.runtime.matchers.planning.helpers.TypeHelper | ||
29 | import org.eclipse.viatra.query.runtime.matchers.psystem.IExpressionEvaluator | ||
30 | import org.eclipse.viatra.query.runtime.matchers.psystem.PBody | ||
31 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable | ||
32 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.AggregatorConstraint | ||
33 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation | ||
34 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.PatternCallBasedDeferred | ||
35 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.PatternMatchCounter | ||
36 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter | ||
37 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
38 | import org.eclipse.xtext.xbase.XExpression | ||
39 | import org.eclipse.xtext.xbase.typesystem.IBatchTypeResolver | ||
40 | import org.eclipse.xtext.xbase.typesystem.references.UnknownTypeReference | ||
41 | |||
42 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
43 | import org.eclipse.xtext.xbase.typesystem.references.InnerTypeReference | ||
44 | |||
45 | class Viatra2LogicTypeInferer{ | ||
46 | val Ecore2Logic ecore2Logic | ||
47 | val extension LogicProblemBuilder builder = new LogicProblemBuilder | ||
48 | /**Typeresolver uses the same resolver as EMFPatternLanguageStandaloneSetup.*/ | ||
49 | val IBatchTypeResolver typeResolver = | ||
50 | (new EMFPatternLanguageStandaloneSetup).createInjector.getInstance(IBatchTypeResolver) | ||
51 | val expressionExtractor = new XExpressionExtractor | ||
52 | |||
53 | new(Ecore2Logic ecore2Logic) { | ||
54 | this.ecore2Logic = ecore2Logic | ||
55 | } | ||
56 | |||
57 | def Viatra2LogicTypeResult inferTypes(List<PQuery> pQueries, TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, Viatra2LogicTrace viatra2LogicTrace) { | ||
58 | val Viatra2LogicTypeResult result = new Viatra2LogicTypeResult(new HashMap,new HashMap); | ||
59 | for(query : pQueries) { | ||
60 | for(body: query.lookup(viatra2LogicTrace.query2Disjunction).bodies) { | ||
61 | for(variable : body.uniqueVariables) { | ||
62 | getOrMakeTypeDecision(result,variable,body,ecore2LogicTrace,viatra2LogicTrace,emptySet) | ||
63 | } | ||
64 | } | ||
65 | for(parameter: query.parameters) { | ||
66 | getOrMakeTypeDecision(result,query,parameter,ecore2LogicTrace,viatra2LogicTrace,emptySet) | ||
67 | } | ||
68 | } | ||
69 | return result | ||
70 | } | ||
71 | |||
72 | private def TypeReference getOrMakeTypeDecision( | ||
73 | Viatra2LogicTypeResult result, | ||
74 | PVariable variable, PBody body, | ||
75 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
76 | Viatra2LogicTrace viatra2LogicTrace, | ||
77 | Set<? extends PParameter> checkedInDecisionMaking) | ||
78 | { | ||
79 | if(result.containsSolution(body,variable)) { | ||
80 | return result.getType(body,variable) | ||
81 | } else { | ||
82 | val inferredTypesByViatra = TypeHelper::inferUnaryTypesFor(body.uniqueVariables, body.constraints, EMFQueryMetaContext.DEFAULT) | ||
83 | val constraintsForVariable = variable.lookup(inferredTypesByViatra) | ||
84 | |||
85 | val typeConstraintsDerivedByTypeHelper = constraintsForVariable.map[transformTypeReference(ecore2LogicTrace)] | ||
86 | val typesFromEval = variable.getTypesFromEval(typeResolver) | ||
87 | val typesFromAggregatorResult = variable.getTypeFromPassivePatternCallConstraintResult( | ||
88 | result, | ||
89 | ecore2LogicTrace, | ||
90 | viatra2LogicTrace, | ||
91 | checkedInDecisionMaking) | ||
92 | |||
93 | val typesFromPositiveReasoning = (typeConstraintsDerivedByTypeHelper + typesFromEval + typesFromAggregatorResult).filterNull | ||
94 | |||
95 | val types = if(!typesFromPositiveReasoning.empty) { | ||
96 | typesFromPositiveReasoning | ||
97 | } else { | ||
98 | variable.getTypeFromPassivePatternCallConstraints( | ||
99 | result, | ||
100 | ecore2LogicTrace, | ||
101 | viatra2LogicTrace, | ||
102 | checkedInDecisionMaking) | ||
103 | } | ||
104 | |||
105 | val commonSubtype = this.calculateCommonSubtype(types) | ||
106 | |||
107 | result.addType(body,variable,commonSubtype) | ||
108 | return commonSubtype | ||
109 | } | ||
110 | } | ||
111 | |||
112 | private def TypeReference getOrMakeTypeDecision( | ||
113 | Viatra2LogicTypeResult result, | ||
114 | PQuery query, | ||
115 | PParameter parameter, | ||
116 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
117 | Viatra2LogicTrace viatra2LogicTrace, | ||
118 | Set<? extends PParameter> checkedInDecisionMaking) | ||
119 | { | ||
120 | if(checkedInDecisionMaking.contains(parameter)) { | ||
121 | return null | ||
122 | } | ||
123 | if(result.containsSolution(parameter)) { | ||
124 | return result.getType(query, parameter) | ||
125 | } | ||
126 | |||
127 | var TypeReference typeReference; | ||
128 | |||
129 | if(parameter.declaredUnaryType !== null) { | ||
130 | val key = parameter.declaredUnaryType | ||
131 | typeReference = key.transformTypeReference(ecore2LogicTrace) | ||
132 | } else { | ||
133 | val bodies = query.lookup(viatra2LogicTrace.query2Disjunction).bodies | ||
134 | val newChecked = new HashSet(checkedInDecisionMaking) => [add(parameter)] | ||
135 | val Iterable<TypeReference> variableTypes = bodies.map[body| | ||
136 | val symbolicParameter = body.symbolicParameters.filter[patternParameter === parameter].head | ||
137 | val variable = symbolicParameter.parameterVariable | ||
138 | getOrMakeTypeDecision(result,variable,body,ecore2LogicTrace,viatra2LogicTrace,newChecked) | ||
139 | ] | ||
140 | typeReference = calculateCommonSupertype(variableTypes) | ||
141 | } | ||
142 | result.addType(query,parameter,typeReference) | ||
143 | return typeReference | ||
144 | } | ||
145 | |||
146 | private def Iterable<? extends TypeReference> getTypesFromEval(PVariable v, IBatchTypeResolver typeResolver) { | ||
147 | val constraints = v.getReferringConstraintsOfType( | ||
148 | typeof(ExpressionEvaluation) | ||
149 | ).filter[ | ||
150 | it.outputVariable === v | ||
151 | ] | ||
152 | val res = constraints.map[getTypeFromEval] | ||
153 | return res | ||
154 | } | ||
155 | |||
156 | def TypeReference getTypeFromEval(ExpressionEvaluation evaluation) { | ||
157 | val XExpression expression = expressionExtractor.extractExpression(evaluation.evaluator) | ||
158 | val returnType = typeResolver.resolveTypes(expression).getReturnType(expression); | ||
159 | if(returnType === null || returnType instanceof UnknownTypeReference) { | ||
160 | return null | ||
161 | } else { | ||
162 | val javaIdentifier = returnType.wrapperTypeIfPrimitive.javaIdentifier | ||
163 | if(javaIdentifier == Boolean.name) { | ||
164 | return LogicBool | ||
165 | } else if(javaIdentifier == Integer.name || javaIdentifier == Short.name) { | ||
166 | return LogicInt | ||
167 | } else if(javaIdentifier == Double.name || javaIdentifier == Float.name){ | ||
168 | return LogicReal | ||
169 | } else if(javaIdentifier == String.name) { | ||
170 | return LogicString | ||
171 | } else { | ||
172 | throw new UnsupportedOperationException('''Unsupported eval type: "«javaIdentifier»"!''') | ||
173 | } | ||
174 | } | ||
175 | } | ||
176 | |||
177 | private def getTypeFromPassivePatternCallConstraintResult( | ||
178 | PVariable v, | ||
179 | Viatra2LogicTypeResult result, | ||
180 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
181 | Viatra2LogicTrace viatra2LogicTrace, | ||
182 | Set<? extends PParameter> checkedInDecisionMaking | ||
183 | ) { | ||
184 | val referringConstraints = v.referringConstraints | ||
185 | |||
186 | val referringCountMatcherTargeting = referringConstraints | ||
187 | .filter(PatternMatchCounter) | ||
188 | .filter[it.resultVariable === v] | ||
189 | .map[builder.LogicInt] | ||
190 | val referringAggregatorConstraintsTargeting = referringConstraints | ||
191 | .filter(AggregatorConstraint) | ||
192 | .filter[it.resultVariable === v] | ||
193 | .map[ // get the type of the referred column | ||
194 | getOrMakeTypeDecision( | ||
195 | result, | ||
196 | it.referredQuery, | ||
197 | it.referredQuery.parameters.get(aggregatedColumn), | ||
198 | ecore2LogicTrace, | ||
199 | viatra2LogicTrace, | ||
200 | checkedInDecisionMaking)] | ||
201 | |||
202 | return referringCountMatcherTargeting + referringAggregatorConstraintsTargeting | ||
203 | } | ||
204 | |||
205 | private def getTypeFromPassivePatternCallConstraints( | ||
206 | PVariable v, | ||
207 | Viatra2LogicTypeResult result, | ||
208 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | ||
209 | Viatra2LogicTrace viatra2LogicTrace, | ||
210 | Set<? extends PParameter> checkedInDecisionMaking | ||
211 | ) { | ||
212 | val referringConstraints = v.referringConstraints | ||
213 | if(referringConstraints.size === 1) { | ||
214 | val onlyConstraint = referringConstraints.head | ||
215 | |||
216 | if(onlyConstraint instanceof PatternCallBasedDeferred) { | ||
217 | val indexOfVariable = v.lookup(onlyConstraint.actualParametersTuple.invertIndex) | ||
218 | val parameter = onlyConstraint.referredQuery.parameters.get(indexOfVariable) | ||
219 | val res = getOrMakeTypeDecision(result, onlyConstraint.referredQuery, parameter, ecore2LogicTrace,viatra2LogicTrace,checkedInDecisionMaking) | ||
220 | return #[res] | ||
221 | } else { | ||
222 | throw new IllegalArgumentException('''A non-PatternCallBasedDeferred type constraint is referring to the variable "«v.name»"!''') | ||
223 | } | ||
224 | } else { | ||
225 | throw new IllegalArgumentException('''Multiple («referringConstraints.size», «FOR c:referringConstraints SEPARATOR ", "»«c»«ENDFOR») constraints are referring to variable "«v.name»", but no type is inferred!''') | ||
226 | } | ||
227 | } | ||
228 | |||
229 | def TypeReference calculateCommonSubtype(Iterable<TypeReference> types) { | ||
230 | val primitiveTypeReferences = types.filter(PrimitiveTypeReference) | ||
231 | val complexTypeReferences = types.filter(ComplexTypeReference) | ||
232 | if(complexTypeReferences.isEmpty) { | ||
233 | // If there is an int type, ... | ||
234 | if(primitiveTypeReferences.exists[it instanceof IntTypeReference]) { | ||
235 | // ... and all types are either real or int, then return int! | ||
236 | if(primitiveTypeReferences.forall[it instanceof RealTypeReference || it instanceof IntTypeReference]) { | ||
237 | return primitiveTypeReferences.filter(IntTypeReference).head | ||
238 | } | ||
239 | // Otherwise, the types are inconsistent, because they mixing numeric and non-numeric types. | ||
240 | else throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''') | ||
241 | } | ||
242 | // If there is no Real, then the types should be homogenious | ||
243 | val head = primitiveTypeReferences.head | ||
244 | if(primitiveTypeReferences.exists[it.eClass !== head.eClass]) { | ||
245 | throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''') | ||
246 | } | ||
247 | return head | ||
248 | } else if(primitiveTypeReferences.isEmpty) { | ||
249 | val complexTypes = complexTypeReferences.map[it.referred].toSet | ||
250 | if(complexTypes.size === 1) { | ||
251 | return builder.toTypeReference(complexTypes.head) | ||
252 | } | ||
253 | // Collect possible subtypes | ||
254 | val subtypeSets = complexTypes.map[it.transitiveClosureStar[it.subtypes].toSet] | ||
255 | val commonTypeSet = new HashSet(subtypeSets.head) | ||
256 | val otherSets = subtypeSets.tail | ||
257 | for(otherSet : otherSets) { | ||
258 | commonTypeSet.retainAll(otherSet) | ||
259 | } | ||
260 | if(commonTypeSet.empty) { | ||
261 | throw new IllegalArgumentException('''Inconsistent types: «complexTypes.map[name].toList»''') | ||
262 | } | ||
263 | |||
264 | |||
265 | return calculateCommonComplexSupertype(commonTypeSet) | ||
266 | |||
267 | } else { | ||
268 | throw new IllegalArgumentException(''' | ||
269 | Inconsistent types, mixing primitive and complex types: | ||
270 | «primitiveTypeReferences.map[eClass.name].toSet.toList» | ||
271 | and | ||
272 | «complexTypeReferences.map[it.referred].toSet.map[name].toList»''') | ||
273 | |||
274 | } | ||
275 | } | ||
276 | |||
277 | |||
278 | def TypeReference calculateCommonSupertype(Iterable<TypeReference> types) { | ||
279 | val primitiveTypeReferences = types.filter(PrimitiveTypeReference) | ||
280 | val complexTypeReferences = types.filter(ComplexTypeReference) | ||
281 | if(complexTypeReferences.isEmpty) { | ||
282 | // If there is a real type, ... | ||
283 | if(primitiveTypeReferences.exists[it instanceof RealTypeReference]) { | ||
284 | // ... and all types are either real or int, then return real! | ||
285 | if(primitiveTypeReferences.forall[it instanceof RealTypeReference || it instanceof IntTypeReference]) { | ||
286 | return primitiveTypeReferences.filter(RealTypeReference).head | ||
287 | } | ||
288 | // Otherwise, the types are inconsistent, because they mixing numeric and non-numeric types. | ||
289 | else throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''') | ||
290 | } | ||
291 | // If there is no Real, then the types should be homogenious | ||
292 | val head = primitiveTypeReferences.head | ||
293 | if(primitiveTypeReferences.exists[it.eClass !== head.eClass]) { | ||
294 | throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''') | ||
295 | } | ||
296 | return head | ||
297 | } else if(primitiveTypeReferences.isEmpty) { | ||
298 | val complexTypes = complexTypeReferences.map[it.referred].toSet | ||
299 | return calculateCommonComplexSupertype(complexTypes) | ||
300 | |||
301 | } else { | ||
302 | throw new IllegalArgumentException(''' | ||
303 | Inconsistent types, mixing primitive and complex types: | ||
304 | «primitiveTypeReferences.map[eClass.name].toSet.toList» | ||
305 | and | ||
306 | «complexTypeReferences.map[it.referred].toSet.map[name].toList»''') | ||
307 | |||
308 | } | ||
309 | } | ||
310 | def TypeReference calculateCommonComplexSupertype(Set<Type> complexTypes) { | ||
311 | if(complexTypes.size === 1) { | ||
312 | return builder.toTypeReference(complexTypes.head) | ||
313 | } | ||
314 | // Collect possible supertypes | ||
315 | val supertypeSets = complexTypes.map[it.transitiveClosureStar[it.supertypes].toSet] | ||
316 | val commonTypeSet = new HashSet(supertypeSets.head) | ||
317 | val otherSets = supertypeSets.tail | ||
318 | for(otherSet : otherSets) { | ||
319 | commonTypeSet.retainAll(otherSet) | ||
320 | } | ||
321 | if(commonTypeSet.empty) { | ||
322 | throw new IllegalArgumentException('''Inconsistent types: «complexTypes.map[name].toList»''') | ||
323 | } | ||
324 | // Remove type that already have covered | ||
325 | val coveredTypes = commonTypeSet.map[it.supertypes].flatten | ||
326 | commonTypeSet.removeAll(coveredTypes) | ||
327 | return builder.toTypeReference(commonTypeSet.head) | ||
328 | } | ||
329 | |||
330 | /** | ||
331 | * Transforms a Viatra type reference to a logic type. | ||
332 | */ | ||
333 | def dispatch TypeReference transformTypeReference(EDataTypeInSlotsKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
334 | val w = k.wrappedKey | ||
335 | if(w == EcorePackage.Literals.EINT || w == EcorePackage.Literals.ESHORT || w == EcorePackage.Literals.ELONG) { | ||
336 | return builder.LogicInt | ||
337 | } else if(w == EcorePackage.Literals.EDOUBLE || w == EcorePackage.Literals.EFLOAT) { | ||
338 | return builder.LogicReal | ||
339 | } else if(w == EcorePackage.Literals.EBOOLEAN) { | ||
340 | return builder.LogicBool | ||
341 | } else if(w == EcorePackage.Literals.ESTRING) { | ||
342 | return builder.LogicString | ||
343 | } else if(w instanceof EEnum) { | ||
344 | val c = this.ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,w) | ||
345 | return builder.toTypeReference(c); | ||
346 | } else throw new UnsupportedOperationException('''Unknown reference type «w.class.name»''') | ||
347 | } | ||
348 | def dispatch TypeReference transformTypeReference(JavaTransitiveInstancesKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
349 | val c = k.wrapperInstanceClass | ||
350 | if(c == Integer || c == Long || c == Short) { | ||
351 | return LogicInt | ||
352 | } else if(c == Float || c == Double) { | ||
353 | return LogicReal | ||
354 | } else if(c == Boolean) { | ||
355 | return LogicBool | ||
356 | } else if(c == String) { | ||
357 | return LogicString | ||
358 | } else if(c.superclass == Enum){ | ||
359 | val enums = ecore2Logic.allEnumsInScope(ecore2LogicTrace.trace) | ||
360 | for(enum : enums) { | ||
361 | if(c == enum.instanceClass) { | ||
362 | return builder.toTypeReference(ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,enum)) | ||
363 | } | ||
364 | } | ||
365 | throw new IllegalArgumentException('''Enum type «c.simpleName» is not mapped to logic!''') | ||
366 | } else { | ||
367 | return null | ||
368 | } | ||
369 | } | ||
370 | def dispatch TypeReference transformTypeReference(EClassTransitiveInstancesKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
371 | val c = k.wrappedKey | ||
372 | |||
373 | if(this.ecore2Logic.allClassesInScope(ecore2LogicTrace.trace).toList.contains(c)) { | ||
374 | return builder.toTypeReference(this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,k.wrappedKey)) | ||
375 | } else { | ||
376 | return null | ||
377 | } | ||
378 | } | ||
379 | def dispatch TypeReference transformTypeReference(EClassUnscopedTransitiveInstancesKey k, TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
380 | val c = k.wrappedKey | ||
381 | |||
382 | if(this.ecore2Logic.allClassesInScope(ecore2LogicTrace.trace).toList.contains(c)) { | ||
383 | return builder.toTypeReference(this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,k.wrappedKey)) | ||
384 | } else { | ||
385 | return null | ||
386 | } | ||
387 | } | ||
388 | |||
389 | def dispatch TypeReference transformTypeReference(IInputKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
390 | throw new IllegalArgumentException('''Unsupported type: «k.class.simpleName»''') | ||
391 | } | ||
392 | } \ No newline at end of file | ||
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeResult.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeResult.xtend new file mode 100644 index 00000000..7ba90724 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeResult.xtend | |||
@@ -0,0 +1,47 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference | ||
4 | import java.util.Map | ||
5 | import org.eclipse.viatra.query.runtime.matchers.psystem.PBody | ||
6 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable | ||
7 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter | ||
8 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
9 | import org.eclipse.xtend.lib.annotations.Data | ||
10 | import org.eclipse.xtext.xbase.lib.Functions.Function0 | ||
11 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
14 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference | ||
16 | |||
17 | @Data class Viatra2LogicTypeResult{ | ||
18 | Map<Pair<PQuery,PParameter>,Function0<TypeReference>> typesInParameters | ||
19 | Map<Pair<PBody,PVariable>,Function0<TypeReference>> typesInBodies; | ||
20 | |||
21 | def addType(PBody body, PVariable variable, TypeReference typeConstructor) { | ||
22 | typesInBodies.put(body->variable,typeConstructor.createTypeConstructor) | ||
23 | } | ||
24 | def addType(PQuery query, PParameter variable, TypeReference typeConstructor) { | ||
25 | typesInParameters.put(query->variable,typeConstructor.createTypeConstructor) | ||
26 | } | ||
27 | def getType(PBody body, PVariable variable) { | ||
28 | return (body->variable).lookup(typesInBodies).apply | ||
29 | } | ||
30 | def getType(PQuery query, PParameter variable) { | ||
31 | return (query->variable).lookup(typesInParameters).apply | ||
32 | } | ||
33 | |||
34 | def containsSolution(PBody body, PVariable variable) { | ||
35 | return typesInBodies.containsKey(body->variable) | ||
36 | } | ||
37 | def containsSolution(PParameter variable) { | ||
38 | return typesInParameters.containsKey(variable) | ||
39 | } | ||
40 | |||
41 | def dispatch Function0<TypeReference> createTypeConstructor(ComplexTypeReference ref) { | ||
42 | return [LogiclanguageFactory.eINSTANCE.createComplexTypeReference=>[it.referred = ref.referred]] | ||
43 | } | ||
44 | def dispatch Function0<TypeReference> createTypeConstructor(PrimitiveTypeReference ref) { | ||
45 | return [EcoreUtil.copy(ref)] | ||
46 | } | ||
47 | } \ No newline at end of file | ||
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/XExpressionExtractor.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/XExpressionExtractor.xtend new file mode 100644 index 00000000..ea8d0b23 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/XExpressionExtractor.xtend | |||
@@ -0,0 +1,24 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic | ||
2 | |||
3 | import org.eclipse.viatra.query.patternlanguage.emf.specification.XBaseEvaluator | ||
4 | import org.eclipse.viatra.query.runtime.matchers.psystem.IExpressionEvaluator | ||
5 | import org.eclipse.xtext.xbase.XExpression | ||
6 | |||
7 | class XExpressionExtractor { | ||
8 | def dispatch XExpression extractExpression(XBaseEvaluator evaluator) { evaluator.expression } | ||
9 | def dispatch XExpression extractExpression(IExpressionEvaluator evaluator) { | ||
10 | val clazz = evaluator.class | ||
11 | if(clazz.name == "org.eclipse.viatra.query.runtime.matchers.psystem.rewriters.VariableMappingExpressionEvaluatorWrapper") { | ||
12 | val field = clazz.declaredFields.filter[it.name == "wrapped"].head | ||
13 | if(field === null) { | ||
14 | throw new IllegalArgumentException('''Class «clazz.simpleName» has no field "wrapped"!''') | ||
15 | } else { | ||
16 | field.setAccessible(true); | ||
17 | val wrappedEvaluator = field.get(evaluator) as XBaseEvaluator | ||
18 | return wrappedEvaluator.extractExpression | ||
19 | } | ||
20 | } else { | ||
21 | throw new IllegalArgumentException('''Unsupported expression evaluation form: «clazz.simpleName»!''') | ||
22 | } | ||
23 | } | ||
24 | } \ No newline at end of file | ||