diff options
author | anqili426 <mollisterkl@outlook.com> | 2020-03-31 10:15:44 -0400 |
---|---|---|
committer | anqili426 <mollisterkl@outlook.com> | 2020-03-31 10:15:44 -0400 |
commit | 7b3ec6bfed2581cd3bb5bbb497bfc518d19f21c3 (patch) | |
tree | ff7f39d8712d2c7fbbb33b09628317bcf237be02 /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic | |
parent | Added call to form numeric problem templates (diff) | |
download | VIATRA-Generator-7b3ec6bfed2581cd3bb5bbb497bfc518d19f21c3.tar.gz VIATRA-Generator-7b3ec6bfed2581cd3bb5bbb497bfc518d19f21c3.tar.zst VIATRA-Generator-7b3ec6bfed2581cd3bb5bbb497bfc518d19f21c3.zip |
Added logic to form numeric problem templates
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java | 160 |
1 files changed, 160 insertions, 0 deletions
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..a58bd855 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java | |||
@@ -0,0 +1,160 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; | ||
2 | |||
3 | import java.util.ArrayList; | ||
4 | import java.util.HashMap; | ||
5 | |||
6 | import org.eclipse.xtext.xbase.XBinaryOperation; | ||
7 | import org.eclipse.xtext.xbase.XExpression; | ||
8 | import org.eclipse.xtext.xbase.XFeatureCall; | ||
9 | import org.eclipse.xtext.xbase.XNumberLiteral; | ||
10 | |||
11 | import com.microsoft.z3.ArithExpr; | ||
12 | import com.microsoft.z3.BoolExpr; | ||
13 | import com.microsoft.z3.Context; | ||
14 | import com.microsoft.z3.IntExpr; | ||
15 | import com.microsoft.z3.Solver; | ||
16 | import com.microsoft.z3.Status; | ||
17 | |||
18 | |||
19 | public class NumericProblemSolver { | ||
20 | private static final String N_Base = "org.eclipse.xtext.xbase.lib."; | ||
21 | private static final String N_PLUS = "operator_plus"; | ||
22 | private static final String N_MINUS = "operator_minus"; | ||
23 | private static final String N_POWER = "operator_power"; | ||
24 | private static final String N_MULTIPLY = "operator_multiply"; | ||
25 | private static final String N_DIVIDE = "operator_divide"; | ||
26 | private static final String N_MODULO = "operator_modulo"; | ||
27 | private static final String N_LESSTHAN = "operator_lessThan"; | ||
28 | private static final String N_LESSEQUALSTHAN = "operator_lessEqualsThan"; | ||
29 | private static final String N_GREATERTHAN = "operator_greaterThan"; | ||
30 | private static final String N_GREATEREQUALTHAN = "operator_greaterEqualsThan"; | ||
31 | private static final String N_EQUALS = "operator_equals"; | ||
32 | private static final String N_NOTEQUALS = "operator_notEquals"; | ||
33 | private static final String N_EQUALS3 = "operator_tripleEquals"; | ||
34 | private static final String N_NOTEQUALS3 = "operator_tripleNotEquals"; | ||
35 | |||
36 | private static int counter = 0; | ||
37 | |||
38 | private Context ctx; | ||
39 | private ArithExpr[] vars = new ArithExpr[2]; | ||
40 | |||
41 | public NumericProblemSolver() { | ||
42 | HashMap<String, String> cfg = new HashMap<String, String>(); | ||
43 | cfg.put("model", "true"); | ||
44 | ctx = new Context(cfg); | ||
45 | } | ||
46 | |||
47 | public Context getNumericProblemContext() { | ||
48 | return ctx; | ||
49 | } | ||
50 | |||
51 | public BoolExpr formNumericProblemTemplate(XExpression e) throws Exception { | ||
52 | if (!(e instanceof XBinaryOperation)) { | ||
53 | throw new Exception ("error in check expression!!!"); | ||
54 | } | ||
55 | |||
56 | String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); | ||
57 | |||
58 | BoolExpr constraint = null; | ||
59 | |||
60 | ArithExpr left_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getLeftOperand()); | ||
61 | ArithExpr right_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getRightOperand()); | ||
62 | |||
63 | if (nameEndsWith(name, N_LESSTHAN)) { | ||
64 | constraint = ctx.mkLt(left_operand, right_operand); | ||
65 | } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) { | ||
66 | constraint = ctx.mkLe(left_operand, right_operand); | ||
67 | } else if (nameEndsWith(name, N_GREATERTHAN)) { | ||
68 | constraint = ctx.mkGt(left_operand, right_operand); | ||
69 | } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) { | ||
70 | constraint = ctx.mkGe(left_operand, right_operand); | ||
71 | } else if (nameEndsWith(name, N_EQUALS)) { | ||
72 | constraint = ctx.mkEq(left_operand, right_operand); | ||
73 | } else if (nameEndsWith(name, N_NOTEQUALS)) { | ||
74 | constraint = ctx.mkDistinct(left_operand, right_operand); | ||
75 | } else if (nameEndsWith(name, N_EQUALS3)) { | ||
76 | constraint = ctx.mkGe(left_operand, right_operand); // ??? | ||
77 | } else if (nameEndsWith(name, N_NOTEQUALS3)) { | ||
78 | constraint = ctx.mkGe(left_operand, right_operand); // ??? | ||
79 | } else { | ||
80 | throw new Exception ("Unsupported binary operation " + name); | ||
81 | } | ||
82 | |||
83 | // To check the constraint | ||
84 | System.out.println(constraint.toString()); | ||
85 | |||
86 | int mage = 5; | ||
87 | int page = 25; | ||
88 | |||
89 | BoolExpr inst = ctx.mkTrue(); | ||
90 | for (ArithExpr var: vars) { | ||
91 | inst = ctx.mkAnd(inst, ctx.mkEq(var, ctx.mkInt(mage))); | ||
92 | } | ||
93 | System.out.println(inst.toString()); | ||
94 | |||
95 | Solver s = ctx.mkSolver(); | ||
96 | s.add(constraint); | ||
97 | s.add(inst); | ||
98 | |||
99 | if (s.check() == Status.SATISFIABLE) { | ||
100 | System.out.println("satisfiable"); | ||
101 | } else { | ||
102 | System.out.println("not satisfiable"); | ||
103 | } | ||
104 | |||
105 | |||
106 | return constraint; | ||
107 | |||
108 | } | ||
109 | |||
110 | private ArithExpr formNumericProblemTemplateHelper(XExpression e) throws Exception { | ||
111 | ArithExpr expr = null; | ||
112 | // Variables | ||
113 | // how to know the data type of this variable????? | ||
114 | if (e instanceof XFeatureCall) { | ||
115 | String var_name = ((XFeatureCall) e).getFeature().getQualifiedName(); | ||
116 | vars[counter] = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort()); | ||
117 | expr = vars[counter]; | ||
118 | counter++; | ||
119 | } | ||
120 | // Constants | ||
121 | else if (e instanceof XNumberLiteral) { | ||
122 | String value = ((XNumberLiteral) e).getValue(); | ||
123 | try{ int val = Integer.parseInt(value); expr = (ArithExpr) ctx.mkInt(val);} catch(NumberFormatException err){} | ||
124 | // What to do with short / float / double??? | ||
125 | // e.g. For floats, need to use FPAdd instead of normal Add!! | ||
126 | } | ||
127 | // Expressions with operators | ||
128 | else if (e instanceof XBinaryOperation) { | ||
129 | String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); | ||
130 | |||
131 | ArithExpr left_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getLeftOperand()); | ||
132 | ArithExpr right_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getRightOperand()); | ||
133 | |||
134 | if (nameEndsWith(name, N_PLUS)) { | ||
135 | expr = ctx.mkAdd(left_operand, right_operand); | ||
136 | } else if (nameEndsWith(name, N_MINUS)) { | ||
137 | expr = ctx.mkAdd(left_operand, ctx.mkUnaryMinus(right_operand)); | ||
138 | } else if (nameEndsWith(name, N_POWER)) { | ||
139 | expr = ctx.mkPower(left_operand, right_operand); | ||
140 | } else if (nameEndsWith(name, N_MULTIPLY)) { | ||
141 | expr = ctx.mkMul(left_operand, right_operand); | ||
142 | } else if (nameEndsWith(name, N_DIVIDE)) { | ||
143 | expr = ctx.mkDiv(left_operand, right_operand); | ||
144 | } else if (nameEndsWith(name, N_MODULO)) { | ||
145 | expr = ctx.mkMod((IntExpr)left_operand, (IntExpr)right_operand); | ||
146 | } else { | ||
147 | throw new Exception ("Unsupported binary operation " + name); | ||
148 | } | ||
149 | } else { | ||
150 | throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); | ||
151 | } | ||
152 | return expr; | ||
153 | |||
154 | } | ||
155 | |||
156 | private boolean nameEndsWith(String name, String end) { | ||
157 | return name.startsWith(N_Base) && name.endsWith(end); | ||
158 | } | ||
159 | |||
160 | } | ||