aboutsummaryrefslogtreecommitdiffstats
path: root/Framework
diff options
context:
space:
mode:
authorLibravatar Oszkar Semerath <semerath@mit.bme.hu>2020-05-09 20:33:19 +0200
committerLibravatar Oszkar Semerath <semerath@mit.bme.hu>2020-05-09 20:33:19 +0200
commit3776a7c6bc1d6fc3ebbdc9e8afb5ea99207798e0 (patch)
tree204cbd6fd1e7f439bc44e6210e684dbed8917e54 /Framework
parentMerge branch 'master' of https://github.com/viatra/VIATRA-Generator (diff)
downloadVIATRA-Generator-3776a7c6bc1d6fc3ebbdc9e8afb5ea99207798e0.tar.gz
VIATRA-Generator-3776a7c6bc1d6fc3ebbdc9e8afb5ea99207798e0.tar.zst
VIATRA-Generator-3776a7c6bc1d6fc3ebbdc9e8afb5ea99207798e0.zip
Numeric Solver integration to exploration
Diffstat (limited to 'Framework')
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend2
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java334
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend64
3 files changed, 238 insertions, 162 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 a27e8904..b4303739 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
@@ -26,7 +26,7 @@ class ExpressionEvaluation2Logic {
26// numericSolver.testIsNotSat(expression, expression.transform(variable2Variable)); 26// numericSolver.testIsNotSat(expression, expression.transform(variable2Variable));
27// numericSolver.testGetOneSol(expression, expression.transform(variable2Variable)); 27// numericSolver.testGetOneSol(expression, expression.transform(variable2Variable));
28// numericSolver.testGetOneSol2(expression, expression.transform(variable2Variable)); 28// numericSolver.testGetOneSol2(expression, expression.transform(variable2Variable));
29 numericSolver.testGetOneSol3(expression, expression.transform(variable2Variable)); 29// numericSolver.testGetOneSol3(expression, expression.transform(variable2Variable));
30// numericSolver.testIsSat(expression, expression.transform(variable2Variable)); 30// numericSolver.testIsSat(expression, expression.transform(variable2Variable));
31 31
32 return expression.transform(variable2Variable) 32 return expression.transform(variable2Variable)
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
index ff3a85eb..0e6e824c 100644
--- 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
@@ -5,9 +5,12 @@ import java.util.HashMap;
5import java.util.HashSet; 5import java.util.HashSet;
6import java.util.List; 6import java.util.List;
7import java.util.Map; 7import java.util.Map;
8import java.util.Map.Entry;
8import java.util.Random; 9import java.util.Random;
9import java.util.Set; 10import java.util.Set;
10 11
12import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint;
13import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation;
11import org.eclipse.xtext.common.types.JvmIdentifiableElement; 14import org.eclipse.xtext.common.types.JvmIdentifiableElement;
12import org.eclipse.xtext.xbase.XBinaryOperation; 15import org.eclipse.xtext.xbase.XBinaryOperation;
13import org.eclipse.xtext.xbase.XExpression; 16import org.eclipse.xtext.xbase.XExpression;
@@ -46,6 +49,7 @@ public class NumericProblemSolver {
46 private static final String N_EQUALS3 = "operator_tripleEquals"; 49 private static final String N_EQUALS3 = "operator_tripleEquals";
47 private static final String N_NOTEQUALS3 = "operator_tripleNotEquals"; 50 private static final String N_NOTEQUALS3 = "operator_tripleNotEquals";
48 51
52
49 private Context ctx; 53 private Context ctx;
50 private Solver s; 54 private Solver s;
51 private Map<Object, Expr> varMap; 55 private Map<Object, Expr> varMap;
@@ -63,6 +67,170 @@ public class NumericProblemSolver {
63 return ctx; 67 return ctx;
64 } 68 }
65 69
70
71 private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) {
72 ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>();
73 XExpression left = ((XBinaryOperation) expression).getLeftOperand();
74 XExpression right = ((XBinaryOperation) expression).getRightOperand();
75
76 getJvmIdentifiableElementsHelper(left, allElem);
77 getJvmIdentifiableElementsHelper(right, allElem);
78 return allElem;
79 }
80
81 private void getJvmIdentifiableElementsHelper(XExpression e, List<JvmIdentifiableElement> allElem) {
82 if (e instanceof XFeatureCall) {
83 allElem.add(((XFeatureCall) e).getFeature());
84 } else if (e instanceof XBinaryOperation) {
85 getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getLeftOperand(), allElem);
86 getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem);
87 }
88 }
89
90 public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception {
91 BoolExpr problemInstance = formNumericProblemInstance(matches);
92 s.add(problemInstance);
93 return s.check() == Status.SATISFIABLE;
94 }
95
96 public Map<PrimitiveElement,Integer> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception {
97 Map<PrimitiveElement,Integer> sol = new HashMap<PrimitiveElement, Integer>();
98 long startformingProblem = System.currentTimeMillis();
99 BoolExpr problemInstance = formNumericProblemInstance(matches);
100 long endformingProblem = System.currentTimeMillis();
101 System.out.println("Forming problem: " + (endformingProblem - startformingProblem));
102 s.add(problemInstance);
103 long startSolvingProblem = System.currentTimeMillis();
104 if (s.check() == Status.SATISFIABLE) {
105 Model m = s.getModel();
106 long endSolvingProblem = System.currentTimeMillis();
107 System.out.println("Solving problem: " + (endSolvingProblem - startSolvingProblem));
108 long startFormingSolution = System.currentTimeMillis();
109 for (PrimitiveElement o: objs) {
110 if(varMap.containsKey(o)) {
111 IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false);
112 Integer oSol = Integer.parseInt(val.toString());
113 //System.out.println("Solution:" + o + "->" + oSol);
114 sol.put(o, oSol);
115 } else {
116 //System.out.println("not used var:" + o);
117 }
118 }
119 long endFormingSolution = System.currentTimeMillis();
120 System.out.println("Forming solution: " + (endFormingSolution - startFormingSolution));
121 } else {
122 System.out.println("Unsatisfiable");
123 }
124
125 return sol;
126 }
127
128 private BoolExpr formNumericConstraint(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception {
129 if (!(e instanceof XBinaryOperation)) {
130 throw new Exception ("error in check expression!!!");
131 }
132
133 String name = ((XBinaryOperation) e).getFeature().getQualifiedName();
134
135 BoolExpr constraint = null;
136
137 ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch);
138 ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch);
139
140 if (nameEndsWith(name, N_LESSTHAN)) {
141 constraint = ctx.mkLt(left_operand, right_operand);
142 } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) {
143 constraint = ctx.mkLe(left_operand, right_operand);
144 } else if (nameEndsWith(name, N_GREATERTHAN)) {
145 constraint = ctx.mkGt(left_operand, right_operand);
146 } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) {
147 constraint = ctx.mkGe(left_operand, right_operand);
148 } else if (nameEndsWith(name, N_EQUALS)) {
149 constraint = ctx.mkEq(left_operand, right_operand);
150 } else if (nameEndsWith(name, N_NOTEQUALS)) {
151 constraint = ctx.mkDistinct(left_operand, right_operand);
152 } else if (nameEndsWith(name, N_EQUALS3)) {
153 constraint = ctx.mkGe(left_operand, right_operand); // ???
154 } else if (nameEndsWith(name, N_NOTEQUALS3)) {
155 constraint = ctx.mkGe(left_operand, right_operand); // ???
156 } else {
157 throw new Exception ("Unsupported binary operation " + name);
158 }
159
160 return constraint;
161 }
162
163 // TODO: add variable: state of the solver
164 private ArithExpr formNumericConstraintHelper(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception {
165 ArithExpr expr = null;
166 // Variables
167 if (e instanceof XFeatureCall) {
168 PrimitiveElement matchedObj = aMatch.get(((XFeatureCall) e).getFeature());
169 if (!matchedObj.isValueSet()) {
170 if (varMap.get(matchedObj) == null) {
171 String var_name = ((XFeatureCall) e).getFeature().getQualifiedName() + matchedObj.toString();
172 expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort());
173 varMap.put(matchedObj, expr);
174 } else {
175 expr = (ArithExpr) varMap.get(matchedObj);
176 }
177 } else {
178 int value = ((IntegerElement) matchedObj).getValue();
179 expr = (ArithExpr) ctx.mkInt(value);
180 varMap.put(matchedObj, expr);
181 }
182 }
183 // Constants
184 else if (e instanceof XNumberLiteral) {
185 String value = ((XNumberLiteral) e).getValue();
186 try{ int val = Integer.parseInt(value); expr = (ArithExpr) ctx.mkInt(val);} catch(NumberFormatException err){}
187 }
188 // Expressions with operators
189 else if (e instanceof XBinaryOperation) {
190 String name = ((XBinaryOperation) e).getFeature().getQualifiedName();
191 ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch);
192 ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch);
193
194 if (nameEndsWith(name, N_PLUS)) {
195 expr = ctx.mkAdd(left_operand, right_operand);
196 } else if (nameEndsWith(name, N_MINUS)) {
197 expr = ctx.mkAdd(left_operand, ctx.mkUnaryMinus(right_operand));
198 } else if (nameEndsWith(name, N_POWER)) {
199 expr = ctx.mkPower(left_operand, right_operand);
200 } else if (nameEndsWith(name, N_MULTIPLY)) {
201 expr = ctx.mkMul(left_operand, right_operand);
202 } else if (nameEndsWith(name, N_DIVIDE)) {
203 expr = ctx.mkDiv(left_operand, right_operand);
204 } else if (nameEndsWith(name, N_MODULO)) {
205 expr = ctx.mkMod((IntExpr)left_operand, (IntExpr)right_operand);
206 } else {
207 throw new Exception ("Unsupported binary operation " + name);
208 }
209 } else {
210 throw new Exception ("Unsupported expression " + e.getClass().getSimpleName());
211 }
212 return expr;
213
214 }
215
216 private boolean nameEndsWith(String name, String end) {
217 return name.startsWith(N_Base) && name.endsWith(end);
218 }
219
220 private BoolExpr formNumericProblemInstance(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception {
221 BoolExpr constraintInstances = ctx.mkTrue();
222 for (XExpression e: matches.keySet()) {
223 Iterable<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e);
224 for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) {
225 BoolExpr constraintInstance = ctx.mkNot(formNumericConstraint(e, aMatch));
226 constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance);
227 }
228 }
229 return constraintInstances;
230 }
231
232
233 /*
66 public void testIsSat(XExpression expression, Term t) throws Exception { 234 public void testIsSat(XExpression expression, Term t) throws Exception {
67 int count = 10000; 235 int count = 10000;
68 Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); 236 Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>();
@@ -87,7 +255,6 @@ public class NumericProblemSolver {
87 System.out.println("Running time:" + (end - start)); 255 System.out.println("Running time:" + (end - start));
88 } 256 }
89 257
90
91 public void testIsNotSat(XExpression expression, Term t) throws Exception { 258 public void testIsNotSat(XExpression expression, Term t) throws Exception {
92 Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); 259 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>>(); 260 Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>();
@@ -129,9 +296,9 @@ public class NumericProblemSolver {
129 System.out.println("Number of matches: "); 296 System.out.println("Number of matches: ");
130 System.out.println("Running time:" + (end - start)); 297 System.out.println("Running time:" + (end - start));
131 } 298 }
132 299 */
133 300
134 public void testGetOneSol(XExpression expression, Term t) throws Exception { 301 /*public void testGetOneSol(XExpression expression, Term t) throws Exception {
135 int count = 10; 302 int count = 10;
136 Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); 303 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>>(); 304 Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>();
@@ -163,8 +330,8 @@ public class NumericProblemSolver {
163 330
164 System.out.println("Number of matches: " + count); 331 System.out.println("Number of matches: " + count);
165 System.out.println("Running time:" + (end - start)); 332 System.out.println("Running time:" + (end - start));
166 } 333 }*/
167 334 /*
168 public void testGetOneSol2(XExpression expression, Term t) throws Exception { 335 public void testGetOneSol2(XExpression expression, Term t) throws Exception {
169 int count = 250; 336 int count = 250;
170 Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); 337 Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>();
@@ -255,160 +422,5 @@ public class NumericProblemSolver {
255 Thread.sleep(3000); 422 Thread.sleep(3000);
256 } 423 }
257 } 424 }
258 425 */
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} 426}
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..89719b91
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend
@@ -0,0 +1,64 @@
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 val comparator = new Comparator<JvmIdentifiableElement>(){
23 override compare(JvmIdentifiableElement o1, JvmIdentifiableElement o2) {
24 //println('''«o1.simpleName» - «o2.simpleName»''')
25 o1.simpleName.compareTo(o2.simpleName)
26 }
27 }
28 def Map<JvmIdentifiableElement, PrimitiveElement> arrayToMap(Object[] tuple, ArrayList<JvmIdentifiableElement> variablesInOrder) {
29 val res = new HashMap
30 for(var i=0; i<tuple.length; i++) {
31 res.put(variablesInOrder.get(i),tuple.get(i) as PrimitiveElement)
32 }
33 return res
34 }
35 def formNumericProblemInstance(Map<PConstraint, Iterable<Object[]>> matches) throws Exception {
36 val res = new HashMap
37 for (Entry<PConstraint, Iterable<Object[]>> entry: matches.entrySet()) {
38 val ExpressionEvaluation constraint = entry.getKey() as ExpressionEvaluation;
39 val XExpression expression = extractor.extractExpression(constraint.getEvaluator());
40 val Iterable<Object[]> tuples = entry.getValue();
41 val features = expression.eAllContents.filter(XFeatureCall).map[it.feature].toSet
42 val variablesInOrder = new ArrayList(features)
43 variablesInOrder.toList.sort(comparator)
44 //println(variablesInOrder)
45 val map = tuples.map[it.arrayToMap(variablesInOrder)]
46 res.put(expression,map)
47 }
48 return res
49 }
50
51 def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) {
52 val input = formNumericProblemInstance(matches)
53 val solver = new NumericProblemSolver
54 val satisfiability = solver.isSatisfiable(input)
55 return satisfiability
56 }
57
58 def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches) {
59 val input = formNumericProblemInstance(matches)
60 val solver = new NumericProblemSolver
61 val solution = solver.getOneSolution(primitiveElements,input)
62 return solution
63 }
64} \ No newline at end of file
generated by cgit v1.2.3-54-g00ecf (git 2.45.1) at 2024-06-03 05:47:31 +0000