aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar anqili426 <mollisterkl@outlook.com>2020-03-31 10:15:44 -0400
committerLibravatar anqili426 <mollisterkl@outlook.com>2020-03-31 10:15:44 -0400
commit7b3ec6bfed2581cd3bb5bbb497bfc518d19f21c3 (patch)
treeff7f39d8712d2c7fbbb33b09628317bcf237be02
parentAdded call to form numeric problem templates (diff)
downloadVIATRA-Generator-7b3ec6bfed2581cd3bb5bbb497bfc518d19f21c3.tar.gz
VIATRA-Generator-7b3ec6bfed2581cd3bb5bbb497bfc518d19f21c3.tar.zst
VIATRA-Generator-7b3ec6bfed2581cd3bb5bbb497bfc518d19f21c3.zip
Added logic to form numeric problem templates
Diffstat
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java160
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 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic;
2
3import java.util.ArrayList;
4import java.util.HashMap;
5
6import org.eclipse.xtext.xbase.XBinaryOperation;
7import org.eclipse.xtext.xbase.XExpression;
8import org.eclipse.xtext.xbase.XFeatureCall;
9import org.eclipse.xtext.xbase.XNumberLiteral;
10
11import com.microsoft.z3.ArithExpr;
12import com.microsoft.z3.BoolExpr;
13import com.microsoft.z3.Context;
14import com.microsoft.z3.IntExpr;
15import com.microsoft.z3.Solver;
16import com.microsoft.z3.Status;
17
18
19public 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}
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-06 16:32:45 +0000