aboutsummaryrefslogtreecommitdiffstats
path: root/Framework
diff options
context:
space:
mode:
authorLibravatar anqili426 <mollisterkl@outlook.com>2020-04-25 20:49:55 -0400
committerLibravatar anqili426 <mollisterkl@outlook.com>2020-04-25 20:49:55 -0400
commit1a9e2a01329fb3bea0bc4c4eb89472040967b7b9 (patch)
tree6ae752432602bd8f0b95765eeb77cba5b6d35b45 /Framework
parentcheck expressions are mapped to WF constraints (diff)
parentAdded new test (diff)
downloadVIATRA-Generator-1a9e2a01329fb3bea0bc4c4eb89472040967b7b9.tar.gz
VIATRA-Generator-1a9e2a01329fb3bea0bc4c4eb89472040967b7b9.tar.zst
VIATRA-Generator-1a9e2a01329fb3bea0bc4c4eb89472040967b7b9.zip
Merge branch 'Attribute-Solver'
Diffstat (limited to 'Framework')
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend10
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java414
2 files changed, 423 insertions, 1 deletions
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
index f474ded4..a27e8904 100644
--- 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
@@ -16,12 +16,20 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
16 16
17class ExpressionEvaluation2Logic { 17class ExpressionEvaluation2Logic {
18 val extension LogicProblemBuilder builder = new LogicProblemBuilder 18 val extension LogicProblemBuilder builder = new LogicProblemBuilder
19 val NumericProblemSolver numericSolver = new NumericProblemSolver
19 20
20 def Term transformCheck(XExpression expression, Map<PVariable, Variable> variable2Variable) { 21 def Term transformCheck(XExpression expression, Map<PVariable, Variable> variable2Variable) {
21 return expression.transform(variable2Variable) 22 return expression.transform(variable2Variable)
22 } 23 }
24
23 def Term transformEval(PVariable target, XExpression expression, Map<PVariable, Variable> variable2Variable) { 25 def Term transformEval(PVariable target, XExpression expression, Map<PVariable, Variable> variable2Variable) {
24 return target.lookup(variable2Variable) == expression.transform(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)
25 } 33 }
26 34
27 static val N_Base = "org.eclipse.xtext.xbase.lib." 35 static val N_Base = "org.eclipse.xtext.xbase.lib."
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..ff3a85eb
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java
@@ -0,0 +1,414 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic;
2
3import java.util.ArrayList;
4import java.util.HashMap;
5import java.util.HashSet;
6import java.util.List;
7import java.util.Map;
8import java.util.Random;
9import java.util.Set;
10
11import org.eclipse.xtext.common.types.JvmIdentifiableElement;
12import org.eclipse.xtext.xbase.XBinaryOperation;
13import org.eclipse.xtext.xbase.XExpression;
14import org.eclipse.xtext.xbase.XFeatureCall;
15import org.eclipse.xtext.xbase.XNumberLiteral;
16
17import com.microsoft.z3.ArithExpr;
18import com.microsoft.z3.BoolExpr;
19import com.microsoft.z3.Context;
20import com.microsoft.z3.Expr;
21import com.microsoft.z3.IntExpr;
22import com.microsoft.z3.Model;
23import com.microsoft.z3.Solver;
24import com.microsoft.z3.Status;
25import com.microsoft.z3.enumerations.Z3_ast_print_mode;
26
27import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term;
28import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement;
29import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement;
30
31
32public class NumericProblemSolver {
33 private static final String N_Base = "org.eclipse.xtext.xbase.lib.";
34 private static final String N_PLUS = "operator_plus";
35 private static final String N_MINUS = "operator_minus";
36 private static final String N_POWER = "operator_power";
37 private static final String N_MULTIPLY = "operator_multiply";
38 private static final String N_DIVIDE = "operator_divide";
39 private static final String N_MODULO = "operator_modulo";
40 private static final String N_LESSTHAN = "operator_lessThan";
41 private static final String N_LESSEQUALSTHAN = "operator_lessEqualsThan";
42 private static final String N_GREATERTHAN = "operator_greaterThan";
43 private static final String N_GREATEREQUALTHAN = "operator_greaterEqualsThan";
44 private static final String N_EQUALS = "operator_equals";
45 private static final String N_NOTEQUALS = "operator_notEquals";
46 private static final String N_EQUALS3 = "operator_tripleEquals";
47 private static final String N_NOTEQUALS3 = "operator_tripleNotEquals";
48
49 private Context ctx;
50 private Solver s;
51 private Map<Object, Expr> varMap;
52
53 public NumericProblemSolver() {
54 HashMap<String, String> cfg = new HashMap<String, String>();
55 cfg.put("model", "true");
56 ctx = new Context(cfg);
57 ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL);
58 s = ctx.mkSolver();
59 varMap = new HashMap<Object, Expr>();
60 }
61
62 public Context getNumericProblemContext() {
63 return ctx;
64 }
65
66 public void testIsSat(XExpression expression, Term t) throws Exception {
67 int count = 10000;
68 Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>();
69 Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>();
70 ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression);
71
72 for (int i = 0; i < count; i++) {
73 Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>();
74 for (JvmIdentifiableElement e: allElem) {
75 FakeIntegerElement intE = new FakeIntegerElement();
76 match.put(e, intE);
77 }
78 matchSet.add(match);
79 }
80
81 matches.put(expression, matchSet);
82 long start = System.currentTimeMillis();
83 boolean sat = isSatisfiable(matches);
84 long end = System.currentTimeMillis();
85 System.out.println(sat);
86 System.out.println("Number of matches: " + count);
87 System.out.println("Running time:" + (end - start));
88 }
89
90
91 public void testIsNotSat(XExpression expression, Term t) throws Exception {
92 Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>();
93 Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>();
94 Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>();
95 ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression);
96 FakeIntegerElement int1 = null;
97 FakeIntegerElement int2 = null;
98 boolean first = true;
99 for (JvmIdentifiableElement e: allElem) {
100 FakeIntegerElement intE = new FakeIntegerElement();
101 if (first) {
102 int1 = intE;
103 first = false;
104 } else {
105 int2 = intE;
106 }
107
108 match.put(e, intE);
109 }
110 matchSet.add(match);
111
112 Map<JvmIdentifiableElement,PrimitiveElement> match2 = new HashMap<JvmIdentifiableElement,PrimitiveElement>();
113 boolean first2 = true;
114 for (JvmIdentifiableElement e: allElem) {
115 if (first2) {
116 match2.put(e, int2);
117 first2 = false;
118 } else {
119 match2.put(e, int1);
120 }
121 }
122 matchSet.add(match2);
123
124 matches.put(expression, matchSet);
125 long start = System.currentTimeMillis();
126 boolean sat = isSatisfiable(matches);
127 long end = System.currentTimeMillis();
128 System.out.println(sat);
129 System.out.println("Number of matches: ");
130 System.out.println("Running time:" + (end - start));
131 }
132
133
134 public void testGetOneSol(XExpression expression, Term t) throws Exception {
135 int count = 10;
136 Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>();
137 Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>();
138
139 ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression);
140 List<Object> obj = new ArrayList<Object>();
141
142 for (int i = 0; i < count; i++) {
143 Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>();
144 for (JvmIdentifiableElement e: allElem) {
145 FakeIntegerElement intE = new FakeIntegerElement();
146 obj.add(intE);
147 match.put(e, intE);
148 }
149 matchSet.add(match);
150 matches.put(expression, matchSet);
151 }
152
153 long start = System.currentTimeMillis();
154 Map<Object,Integer> sol = getOneSolution(obj, matches);
155 long end = System.currentTimeMillis();
156
157
158 // Print sol
159 for (Object o: sol.keySet()) {
160 System.out.println(o + " :" + sol.get(o));
161 }
162
163
164 System.out.println("Number of matches: " + count);
165 System.out.println("Running time:" + (end - start));
166 }
167
168 public void testGetOneSol2(XExpression expression, Term t) throws Exception {
169 int count = 250;
170 Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>();
171 Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>();
172 ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression);
173 List<Object> obj = new ArrayList<Object>();
174 for (int i = 0; i < count; i++) {
175 Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>();
176 FakeIntegerElement int2 = null;
177 boolean first = false;
178 for (JvmIdentifiableElement e: allElem) {
179 FakeIntegerElement intE = new FakeIntegerElement();
180 if (first) {
181 first = false;
182 } else {
183 int2 = intE;
184 }
185 obj.add(intE);
186 match.put(e, intE);
187 }
188
189 Map<JvmIdentifiableElement,PrimitiveElement> match2 = new HashMap<JvmIdentifiableElement,PrimitiveElement>();
190 boolean first2 = true;
191 for (JvmIdentifiableElement e: allElem) {
192 FakeIntegerElement intE = null;
193 if (first2) {
194 intE = int2;
195 first2 = false;
196 } else {
197 intE = new FakeIntegerElement();
198 }
199 obj.add(intE);
200 match2.put(e, intE);
201 }
202
203
204 matchSet.add(match);
205 matchSet.add(match2);
206 }
207 matches.put(expression, matchSet);
208
209 System.out.println("Number of matches: " + matchSet.size());
210 for (int i = 0; i < 10; i++) {
211 Map<Object,Integer> sol = getOneSolution(obj, matches);
212 System.out.println("**********************");
213 Thread.sleep(3000);
214 }
215 }
216
217 public void testGetOneSol3(XExpression expression, Term t) throws Exception {
218 int count = 15000;
219 Random rand = new Random();
220 Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>();
221 Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>();
222 ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression);
223 List<Object> obj = new ArrayList<Object>();
224 for (int i = 0; i < count; i++) {
225 Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>();
226 if (obj.size() > 1) {
227 for (JvmIdentifiableElement e: allElem) {
228 FakeIntegerElement intE = null;
229 int useOld = rand.nextInt(10);
230 if (useOld == 1) {
231 System.out.println("here ");
232 int index = rand.nextInt(obj.size());
233 intE = (FakeIntegerElement) obj.get(index);
234 } else {
235 intE = new FakeIntegerElement();
236 }
237 obj.add(intE);
238 match.put(e, intE);
239 }
240 } else {
241 for (JvmIdentifiableElement e: allElem) {
242 FakeIntegerElement intE = new FakeIntegerElement();
243 obj.add(intE);
244 match.put(e, intE);
245 }
246 }
247 matchSet.add(match);
248 }
249 matches.put(expression, matchSet);
250
251 System.out.println("Number of matches: " + matchSet.size());
252 for (int i = 0; i < 10; i++) {
253 Map<Object,Integer> sol = getOneSolution(obj, matches);
254 System.out.println("**********************");
255 Thread.sleep(3000);
256 }
257 }
258
259 private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) {
260 ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>();
261 XExpression left = ((XBinaryOperation) expression).getLeftOperand();
262 XExpression right = ((XBinaryOperation) expression).getRightOperand();
263
264 getJvmIdentifiableElementsHelper(left, allElem);
265 getJvmIdentifiableElementsHelper(right, allElem);
266 return allElem;
267 }
268
269 private void getJvmIdentifiableElementsHelper(XExpression e, List<JvmIdentifiableElement> allElem) {
270 if (e instanceof XFeatureCall) {
271 allElem.add(((XFeatureCall) e).getFeature());
272 } else if (e instanceof XBinaryOperation) {
273 getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getLeftOperand(), allElem);
274 getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem);
275 }
276 }
277
278 public boolean isSatisfiable(Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception {
279 BoolExpr problemInstance = formNumericProblemInstance(matches);
280 s.add(problemInstance);
281 return s.check() == Status.SATISFIABLE;
282 }
283
284 public Map<Object,Integer> getOneSolution(List<Object> objs, Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception {
285 Map<Object,Integer> sol = new HashMap<Object, Integer>();
286 long startformingProblem = System.currentTimeMillis();
287 BoolExpr problemInstance = formNumericProblemInstance(matches);
288 long endformingProblem = System.currentTimeMillis();
289 System.out.println("Forming problem: " + (endformingProblem - startformingProblem));
290 s.add(problemInstance);
291 long startSolvingProblem = System.currentTimeMillis();
292 if (s.check() == Status.SATISFIABLE) {
293 Model m = s.getModel();
294 long endSolvingProblem = System.currentTimeMillis();
295 System.out.println("Solving problem: " + (endSolvingProblem - startSolvingProblem));
296 long startFormingSolution = System.currentTimeMillis();
297 for (Object o: objs) {
298 IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false);
299 Integer oSol = Integer.parseInt(val.toString());
300 sol.put(o, oSol);
301 }
302 long endFormingSolution = System.currentTimeMillis();
303 System.out.println("Forming solution: " + (endFormingSolution - startFormingSolution));
304 } else {
305 System.out.println("Unsatisfiable");
306 }
307
308 return sol;
309 }
310
311 private BoolExpr formNumericConstraint(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception {
312 if (!(e instanceof XBinaryOperation)) {
313 throw new Exception ("error in check expression!!!");
314 }
315
316 String name = ((XBinaryOperation) e).getFeature().getQualifiedName();
317
318 BoolExpr constraint = null;
319
320 ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch);
321 ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch);
322
323 if (nameEndsWith(name, N_LESSTHAN)) {
324 constraint = ctx.mkLt(left_operand, right_operand);
325 } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) {
326 constraint = ctx.mkLe(left_operand, right_operand);
327 } else if (nameEndsWith(name, N_GREATERTHAN)) {
328 constraint = ctx.mkGt(left_operand, right_operand);
329 } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) {
330 constraint = ctx.mkGe(left_operand, right_operand);
331 } else if (nameEndsWith(name, N_EQUALS)) {
332 constraint = ctx.mkEq(left_operand, right_operand);
333 } else if (nameEndsWith(name, N_NOTEQUALS)) {
334 constraint = ctx.mkDistinct(left_operand, right_operand);
335 } else if (nameEndsWith(name, N_EQUALS3)) {
336 constraint = ctx.mkGe(left_operand, right_operand); // ???
337 } else if (nameEndsWith(name, N_NOTEQUALS3)) {
338 constraint = ctx.mkGe(left_operand, right_operand); // ???
339 } else {
340 throw new Exception ("Unsupported binary operation " + name);
341 }
342
343 return constraint;
344 }
345
346 // TODO: add variable: state of the solver
347 private ArithExpr formNumericConstraintHelper(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception {
348 ArithExpr expr = null;
349 // Variables
350 if (e instanceof XFeatureCall) {
351 PrimitiveElement matchedObj = aMatch.get(((XFeatureCall) e).getFeature());
352 if (!matchedObj.isValueSet()) {
353 if (varMap.get(matchedObj) == null) {
354 String var_name = ((XFeatureCall) e).getFeature().getQualifiedName() + matchedObj.toString();
355 expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort());
356 varMap.put(matchedObj, expr);
357 } else {
358 expr = (ArithExpr) varMap.get(matchedObj);
359 }
360 } else {
361 int value = ((IntegerElement) matchedObj).getValue();
362 expr = (ArithExpr) ctx.mkInt(value);
363 varMap.put(matchedObj, expr);
364 }
365 }
366 // Constants
367 else if (e instanceof XNumberLiteral) {
368 String value = ((XNumberLiteral) e).getValue();
369 try{ int val = Integer.parseInt(value); expr = (ArithExpr) ctx.mkInt(val);} catch(NumberFormatException err){}
370 }
371 // Expressions with operators
372 else if (e instanceof XBinaryOperation) {
373 String name = ((XBinaryOperation) e).getFeature().getQualifiedName();
374 ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch);
375 ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch);
376
377 if (nameEndsWith(name, N_PLUS)) {
378 expr = ctx.mkAdd(left_operand, right_operand);
379 } else if (nameEndsWith(name, N_MINUS)) {
380 expr = ctx.mkAdd(left_operand, ctx.mkUnaryMinus(right_operand));
381 } else if (nameEndsWith(name, N_POWER)) {
382 expr = ctx.mkPower(left_operand, right_operand);
383 } else if (nameEndsWith(name, N_MULTIPLY)) {
384 expr = ctx.mkMul(left_operand, right_operand);
385 } else if (nameEndsWith(name, N_DIVIDE)) {
386 expr = ctx.mkDiv(left_operand, right_operand);
387 } else if (nameEndsWith(name, N_MODULO)) {
388 expr = ctx.mkMod((IntExpr)left_operand, (IntExpr)right_operand);
389 } else {
390 throw new Exception ("Unsupported binary operation " + name);
391 }
392 } else {
393 throw new Exception ("Unsupported expression " + e.getClass().getSimpleName());
394 }
395 return expr;
396
397 }
398
399 private boolean nameEndsWith(String name, String end) {
400 return name.startsWith(N_Base) && name.endsWith(end);
401 }
402
403 private BoolExpr formNumericProblemInstance(Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception {
404 BoolExpr constraintInstances = ctx.mkTrue();
405 for (XExpression e: matches.keySet()) {
406 Set<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e);
407 for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) {
408 BoolExpr constraintInstance = formNumericConstraint(e, aMatch);
409 constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance);
410 }
411 }
412 return constraintInstances;
413 }
414}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-26 20:43:46 +0000