aboutsummaryrefslogtreecommitdiffstats
path: root/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic
diff options
context:
space:
mode:
authorLibravatar 20001LastOrder <boqi.chen@mail.mcgill.ca>2020-11-04 01:33:58 -0500
committerLibravatar 20001LastOrder <boqi.chen@mail.mcgill.ca>2020-11-04 01:33:58 -0500
commita20af4d0dbf5eab84ee271d426528aabb5a8ac3b (patch)
treea9ab772ee313125aaf3a941d66e131b408d949ba /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic
parentchanges in settings of measurements (diff)
parentmerge with current master, comment numerical solver related logging (diff)
downloadVIATRA-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/hu/bme/mit/inf/dslreasoner/viatra2logic')
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Constraint2Logic.xtend73
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExampleRecreation.java120
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend140
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/FakeIntegerElement.java169
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java473
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend80
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend335
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeInferer.xtend392
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeResult.xtend47
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/XExpressionExtractor.xtend24
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
31import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 31import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
32import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint 32import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint
33import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.AggregatorConstraint
34import org.eclipse.viatra.query.runtime.matchers.aggregators.DoubleSumOperator
35import org.eclipse.viatra.query.runtime.matchers.aggregators.IntegerSumOperator
36import org.eclipse.viatra.query.runtime.matchers.aggregators.LongSumOperator
37import org.eclipse.viatra.query.runtime.matchers.aggregators.ExtremumOperator
38import org.eclipse.viatra.query.runtime.matchers.aggregators.ExtremumOperator.Extreme
39import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.PatternMatchCounter
40import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
33 41
34class Constraint2Logic { 42class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic;
2
3import java.util.HashMap;
4
5import com.microsoft.z3.*;
6
7public 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 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic
2
3import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
6import java.util.Map
7import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
8import org.eclipse.xtext.xbase.XBinaryOperation
9import org.eclipse.xtext.xbase.XExpression
10import org.eclipse.xtext.xbase.XFeatureCall
11import org.eclipse.xtext.xbase.XMemberFeatureCall
12import org.eclipse.xtext.xbase.XNumberLiteral
13import org.eclipse.xtext.xbase.XUnaryOperation
14
15import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
16
17class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic;
2
3import java.lang.reflect.InvocationTargetException;
4
5import org.eclipse.emf.common.notify.Adapter;
6import org.eclipse.emf.common.notify.Notification;
7import org.eclipse.emf.common.util.EList;
8import org.eclipse.emf.common.util.TreeIterator;
9import org.eclipse.emf.ecore.EClass;
10import org.eclipse.emf.ecore.EObject;
11import org.eclipse.emf.ecore.EOperation;
12import org.eclipse.emf.ecore.EReference;
13import org.eclipse.emf.ecore.EStructuralFeature;
14import org.eclipse.emf.ecore.resource.Resource;
15
16import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition;
17import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement;
18
19public 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 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic;
2
3import java.math.BigDecimal;
4import java.util.ArrayList;
5import java.util.HashMap;
6import java.util.HashSet;
7import java.util.List;
8import java.util.Map;
9import java.util.Map.Entry;
10import java.util.Random;
11import java.util.Set;
12
13import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint;
14import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation;
15import org.eclipse.xtext.common.types.JvmIdentifiableElement;
16import org.eclipse.xtext.xbase.XBinaryOperation;
17import org.eclipse.xtext.xbase.XExpression;
18import org.eclipse.xtext.xbase.XFeatureCall;
19import org.eclipse.xtext.xbase.XNumberLiteral;
20
21import com.microsoft.z3.ArithExpr;
22import com.microsoft.z3.BoolExpr;
23import com.microsoft.z3.Context;
24import com.microsoft.z3.Expr;
25import com.microsoft.z3.IntExpr;
26import com.microsoft.z3.Model;
27import com.microsoft.z3.RealExpr;
28import com.microsoft.z3.Solver;
29import com.microsoft.z3.Status;
30import com.microsoft.z3.enumerations.Z3_ast_print_mode;
31
32import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term;
33import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement;
34import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement;
35import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement;
36
37
38public 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 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic
2
3import org.eclipse.xtext.xbase.XExpression
4import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
5import org.eclipse.xtext.common.types.JvmIdentifiableElement
6import java.util.Set
7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
8import java.util.Map
9import com.microsoft.z3.BoolExpr
10import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
11import java.util.Map.Entry
12import org.eclipse.xtext.xbase.XFeatureCall
13import java.util.Comparator
14import java.util.ArrayList
15import java.util.HashMap
16import java.util.List
17
18class 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
4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace 4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
5import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder 5import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
6import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput 6import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition 7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable 8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
13import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem 9import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
14import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery 10import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
15import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsFactory 11import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsFactory
16import java.util.ArrayList 12import java.util.ArrayList
17import java.util.HashMap 13import java.util.HashMap
18import java.util.HashSet
19import java.util.LinkedList 14import java.util.LinkedList
20import java.util.List 15import java.util.List
21import java.util.Map 16import java.util.Map
22import java.util.Set 17import java.util.Set
23import org.eclipse.emf.ecore.EAttribute 18import org.eclipse.emf.ecore.EAttribute
24import org.eclipse.emf.ecore.EClassifier
25import org.eclipse.emf.ecore.EEnum
26import org.eclipse.emf.ecore.EReference 19import org.eclipse.emf.ecore.EReference
27import org.eclipse.emf.ecore.EStructuralFeature 20import org.eclipse.emf.ecore.EStructuralFeature
28import org.eclipse.emf.ecore.EcorePackage 21import org.eclipse.emf.ecore.util.EcoreUtil
29import org.eclipse.viatra.query.runtime.api.IQuerySpecification 22import org.eclipse.viatra.query.runtime.api.IQuerySpecification
30import org.eclipse.viatra.query.runtime.emf.EMFQueryMetaContext 23import org.eclipse.viatra.query.runtime.emf.EMFQueryMetaContext
31import org.eclipse.viatra.query.runtime.emf.types.BaseEMFTypeKey
32import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
33import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
34import org.eclipse.viatra.query.runtime.matchers.context.IInputKey
35import org.eclipse.viatra.query.runtime.matchers.context.common.JavaTransitiveInstancesKey
36import org.eclipse.viatra.query.runtime.matchers.planning.helpers.TypeHelper
37import org.eclipse.viatra.query.runtime.matchers.psystem.PBody 24import org.eclipse.viatra.query.runtime.matchers.psystem.PBody
25import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
38import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable 26import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
27import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.AggregatorConstraint
39import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall 28import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
29import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.PatternMatchCounter
30import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction
40import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter 31import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter
41import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery 32import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
42import org.eclipse.viatra.query.runtime.matchers.psystem.rewriters.PBodyNormalizer 33import org.eclipse.viatra.query.runtime.matchers.psystem.rewriters.PBodyNormalizer
43import org.eclipse.xtend.lib.annotations.Data 34import org.eclipse.xtend.lib.annotations.Data
44 35
45import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 36import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
46import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction
47import org.eclipse.emf.ecore.util.EcoreUtil
48import 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}
62class Viatra2LogicConfiguration { 49class Viatra2LogicConfiguration {
63 public var normalize = true 50 public var normalize = true
64 public var transitiveClosureDepth = 3
65} 51}
66 52
67class Viatra2Logic { 53class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic
2
3import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
5import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
6import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
13import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
14import java.util.HashMap
15import java.util.HashSet
16import java.util.List
17import java.util.Set
18import org.eclipse.emf.ecore.EEnum
19import org.eclipse.emf.ecore.EcorePackage
20import org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguageStandaloneSetup
21import org.eclipse.viatra.query.patternlanguage.emf.specification.XBaseEvaluator
22import org.eclipse.viatra.query.runtime.emf.EMFQueryMetaContext
23import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
24import org.eclipse.viatra.query.runtime.emf.types.EClassUnscopedTransitiveInstancesKey
25import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
26import org.eclipse.viatra.query.runtime.matchers.context.IInputKey
27import org.eclipse.viatra.query.runtime.matchers.context.common.JavaTransitiveInstancesKey
28import org.eclipse.viatra.query.runtime.matchers.planning.helpers.TypeHelper
29import org.eclipse.viatra.query.runtime.matchers.psystem.IExpressionEvaluator
30import org.eclipse.viatra.query.runtime.matchers.psystem.PBody
31import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
32import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.AggregatorConstraint
33import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
34import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.PatternCallBasedDeferred
35import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.PatternMatchCounter
36import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter
37import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
38import org.eclipse.xtext.xbase.XExpression
39import org.eclipse.xtext.xbase.typesystem.IBatchTypeResolver
40import org.eclipse.xtext.xbase.typesystem.references.UnknownTypeReference
41
42import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
43import org.eclipse.xtext.xbase.typesystem.references.InnerTypeReference
44
45class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic
2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
4import java.util.Map
5import org.eclipse.viatra.query.runtime.matchers.psystem.PBody
6import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
7import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter
8import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
9import org.eclipse.xtend.lib.annotations.Data
10import org.eclipse.xtext.xbase.lib.Functions.Function0
11import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
14import org.eclipse.emf.ecore.util.EcoreUtil
15import 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 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic
2
3import org.eclipse.viatra.query.patternlanguage.emf.specification.XBaseEvaluator
4import org.eclipse.viatra.query.runtime.matchers.psystem.IExpressionEvaluator
5import org.eclipse.xtext.xbase.XExpression
6
7class 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
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-29 17:15:56 +0000