diff options
author | anqili426 <mollisterkl@outlook.com> | 2020-04-25 20:49:55 -0400 |
---|---|---|
committer | anqili426 <mollisterkl@outlook.com> | 2020-04-25 20:49:55 -0400 |
commit | 1a9e2a01329fb3bea0bc4c4eb89472040967b7b9 (patch) | |
tree | 6ae752432602bd8f0b95765eeb77cba5b6d35b45 /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner | |
parent | check expressions are mapped to WF constraints (diff) | |
parent | Added new test (diff) | |
download | VIATRA-Generator-1a9e2a01329fb3bea0bc4c4eb89472040967b7b9.tar.gz VIATRA-Generator-1a9e2a01329fb3bea0bc4c4eb89472040967b7b9.tar.zst VIATRA-Generator-1a9e2a01329fb3bea0bc4c4eb89472040967b7b9.zip |
Merge branch 'Attribute-Solver'
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner')
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 | ||
17 | class ExpressionEvaluation2Logic { | 17 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; | ||
2 | |||
3 | import java.util.ArrayList; | ||
4 | import java.util.HashMap; | ||
5 | import java.util.HashSet; | ||
6 | import java.util.List; | ||
7 | import java.util.Map; | ||
8 | import java.util.Random; | ||
9 | import java.util.Set; | ||
10 | |||
11 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; | ||
12 | import org.eclipse.xtext.xbase.XBinaryOperation; | ||
13 | import org.eclipse.xtext.xbase.XExpression; | ||
14 | import org.eclipse.xtext.xbase.XFeatureCall; | ||
15 | import org.eclipse.xtext.xbase.XNumberLiteral; | ||
16 | |||
17 | import com.microsoft.z3.ArithExpr; | ||
18 | import com.microsoft.z3.BoolExpr; | ||
19 | import com.microsoft.z3.Context; | ||
20 | import com.microsoft.z3.Expr; | ||
21 | import com.microsoft.z3.IntExpr; | ||
22 | import com.microsoft.z3.Model; | ||
23 | import com.microsoft.z3.Solver; | ||
24 | import com.microsoft.z3.Status; | ||
25 | import com.microsoft.z3.enumerations.Z3_ast_print_mode; | ||
26 | |||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | ||
28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; | ||
29 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | ||
30 | |||
31 | |||
32 | public 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 | } | ||