diff options
author | 2020-05-09 20:33:19 +0200 | |
---|---|---|
committer | 2020-05-09 20:33:19 +0200 | |
commit | 3776a7c6bc1d6fc3ebbdc9e8afb5ea99207798e0 (patch) | |
tree | 204cbd6fd1e7f439bc44e6210e684dbed8917e54 /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java | |
parent | Merge branch 'master' of https://github.com/viatra/VIATRA-Generator (diff) | |
download | VIATRA-Generator-3776a7c6bc1d6fc3ebbdc9e8afb5ea99207798e0.tar.gz VIATRA-Generator-3776a7c6bc1d6fc3ebbdc9e8afb5ea99207798e0.tar.zst VIATRA-Generator-3776a7c6bc1d6fc3ebbdc9e8afb5ea99207798e0.zip |
Numeric Solver integration to exploration
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java | 334 |
1 files changed, 173 insertions, 161 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 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; | |||
5 | import java.util.HashSet; | 5 | import java.util.HashSet; |
6 | import java.util.List; | 6 | import java.util.List; |
7 | import java.util.Map; | 7 | import java.util.Map; |
8 | import java.util.Map.Entry; | ||
8 | import java.util.Random; | 9 | import java.util.Random; |
9 | import java.util.Set; | 10 | import java.util.Set; |
10 | 11 | ||
12 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint; | ||
13 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation; | ||
11 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; | 14 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; |
12 | import org.eclipse.xtext.xbase.XBinaryOperation; | 15 | import org.eclipse.xtext.xbase.XBinaryOperation; |
13 | import org.eclipse.xtext.xbase.XExpression; | 16 | import 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 | } |