aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-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
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend7
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend1
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend6
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java32
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend114
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend3
10 files changed, 387 insertions, 178 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
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
index e7342ff7..975ace2f 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
@@ -17,6 +17,8 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
17import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery 17import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
18import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule 18import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule
19import org.eclipse.xtend.lib.annotations.Data 19import org.eclipse.xtend.lib.annotations.Data
20import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
21import java.util.Map
20 22
21class ModelGenerationStatistics { 23class ModelGenerationStatistics {
22 public var long transformationExecutionTime = 0 24 public var long transformationExecutionTime = 0
@@ -36,6 +38,8 @@ class ModelGenerationStatistics {
36 38
37 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF 39 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF
38 40
41 Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unitPropagationPreconditions
42
39 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns 43 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns
40} 44}
41enum TypeInferenceMethod { 45enum TypeInferenceMethod {
@@ -77,6 +81,8 @@ class ModelGenerationMethodProvider {
77 81
78 val invalidWF = queries.getInvalidWFQueries.values 82 val invalidWF = queries.getInvalidWFQueries.values
79 83
84 val unitPropagationPreconditions = queries.getUnitPropagationPreconditionPatterns
85
80 return new ModelGenerationMethod( 86 return new ModelGenerationMethod(
81 statistics, 87 statistics,
82 objectRefinementRules.values, 88 objectRefinementRules.values,
@@ -84,6 +90,7 @@ class ModelGenerationMethodProvider {
84 unfinishedMultiplicities, 90 unfinishedMultiplicities,
85 unfinishedWF, 91 unfinishedWF,
86 invalidWF, 92 invalidWF,
93 unitPropagationPreconditions,
87 queries.allQueries 94 queries.allQueries
88 ) 95 )
89 } 96 }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
index f576d1a1..18e3018a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
@@ -93,7 +93,6 @@ class PatternProvider {
93 refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] 93 refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)]
94 val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 94 val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
95 unitPropagationPreconditionPatterns = unitPropagationTrace.mapValues[it.lookup(queries)] 95 unitPropagationPreconditionPatterns = unitPropagationTrace.mapValues[it.lookup(queries)]
96 unitPropagationPreconditionPatterns.entrySet.forEach[println(it.key + "->" +it.value)]
97 return new GeneratedPatterns( 96 return new GeneratedPatterns(
98 invalidWFQueries, 97 invalidWFQueries,
99 unfinishedWFQueries, 98 unfinishedWFQueries,
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend
index 6c68ec94..d487db64 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend
@@ -100,11 +100,9 @@ class UnitPropagationPreconditionGenerator {
100 val preconditions = new LinkedList 100 val preconditions = new LinkedList
101 val constraint2Precondition = new HashMap 101 val constraint2Precondition = new HashMap
102 for(entry : mainPropagationNames.entrySet) { 102 for(entry : mainPropagationNames.entrySet) {
103 val name = '''UPMUSTPropagate«res.getOrGenerateConstraintName(entry.key)»'''; 103 val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»''';
104 val def = ''' 104 val def = '''
105 pattern «name»( 105 pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»)
106 problem:LogicProblem, interpretation:PartialInterpretation,
107 «FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»)
108 «FOR propagation : entry.value SEPARATOR " or "» 106 «FOR propagation : entry.value SEPARATOR " or "»
109 { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); } 107 { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); }
110 «ENDFOR»''' 108 «ENDFOR»'''
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
index 1e623823..cb73f4e8 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
@@ -77,7 +77,7 @@ class ViatraReasoner extends LogicReasoner{
77 scopePropagator, 77 scopePropagator,
78 viatraConfig.documentationLevel 78 viatraConfig.documentationLevel
79 ) 79 )
80 println("parsed") 80 //println("parsed")
81 81
82 dse.addObjective(new ModelGenerationCompositeObjective( 82 dse.addObjective(new ModelGenerationCompositeObjective(
83 new ScopeObjective, 83 new ScopeObjective,
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
index 60f46033..1cd61e9a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
@@ -17,10 +17,12 @@ import java.util.Comparator;
17import java.util.Iterator; 17import java.util.Iterator;
18import java.util.LinkedList; 18import java.util.LinkedList;
19import java.util.List; 19import java.util.List;
20import java.util.Map;
20import java.util.PriorityQueue; 21import java.util.PriorityQueue;
21import java.util.Random; 22import java.util.Random;
22 23
23import org.apache.log4j.Logger; 24import org.apache.log4j.Logger;
25import org.eclipse.emf.ecore.EObject;
24import org.eclipse.emf.ecore.util.EcoreUtil; 26import org.eclipse.emf.ecore.util.EcoreUtil;
25import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy; 27import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy;
26import org.eclipse.viatra.dse.base.ThreadContext; 28import org.eclipse.viatra.dse.base.ThreadContext;
@@ -38,6 +40,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
38import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult; 40import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult;
39import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; 41import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
40import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; 42import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;
43import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver;
41import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod; 44import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod;
42import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; 45import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic;
43import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; 46import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation;
@@ -80,12 +83,14 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
80 private volatile boolean isInterrupted = false; 83 private volatile boolean isInterrupted = false;
81 private ModelResult modelResultByInternalSolver = null; 84 private ModelResult modelResultByInternalSolver = null;
82 private Random random = new Random(); 85 private Random random = new Random();
83 private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers; 86 //private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers;
84 87
85 // Statistics 88 // Statistics
86 private int numberOfStatecoderFail = 0; 89 private int numberOfStatecoderFail = 0;
87 private int numberOfPrintedModel = 0; 90 private int numberOfPrintedModel = 0;
88 private int numberOfSolverCalls = 0; 91 private int numberOfSolverCalls = 0;
92
93 private NumericSolver numericSolver = null;
89 94
90 public BestFirstStrategyForModelGeneration( 95 public BestFirstStrategyForModelGeneration(
91 ReasonerWorkspace workspace, 96 ReasonerWorkspace workspace,
@@ -112,14 +117,14 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
112 this.context = context; 117 this.context = context;
113 this.solutionStore = context.getGlobalContext().getSolutionStore(); 118 this.solutionStore = context.getGlobalContext().getSolutionStore();
114 119
115 ViatraQueryEngine engine = context.getQueryEngine(); 120// ViatraQueryEngine engine = context.getQueryEngine();
116// // TODO: visualisation 121// // TODO: visualisation
117 matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>(); 122// matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>();
118 for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) { 123// for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) {
119 //System.out.println(p.getSimpleName()); 124// //System.out.println(p.getSimpleName());
120 ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine); 125// ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine);
121 matchers.add(matcher); 126// matchers.add(matcher);
122 } 127// }
123 128
124 this.solutionStoreWithCopy = new SolutionStoreWithCopy(); 129 this.solutionStoreWithCopy = new SolutionStoreWithCopy();
125 this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement); 130 this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement);
@@ -131,6 +136,8 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
131 return objectiveComparatorHelper.compare(o2.fitness, o1.fitness); 136 return objectiveComparatorHelper.compare(o2.fitness, o1.fitness);
132 } 137 }
133 }; 138 };
139
140 this.numericSolver = new NumericSolver(context, method);
134 141
135 trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator); 142 trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator);
136 } 143 }
@@ -140,6 +147,9 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
140 if (!context.checkGlobalConstraints()) { 147 if (!context.checkGlobalConstraints()) {
141 logger.info("Global contraint is not satisifed in the first state. Terminate."); 148 logger.info("Global contraint is not satisifed in the first state. Terminate.");
142 return; 149 return;
150 } else if(!numericSolver.isSatisfiable()) {
151 logger.info("Numeric contraints are not satisifed in the first state. Terminate.");
152 return;
143 } 153 }
144 if (configuration.searchSpaceConstraints.maxDepth == 0) { 154 if (configuration.searchSpaceConstraints.maxDepth == 0) {
145 logger.info("Maximal depth is reached in the initial solution. Terminate."); 155 logger.info("Maximal depth is reached in the initial solution. Terminate.");
@@ -218,6 +228,9 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
218 } else if (!context.checkGlobalConstraints()) { 228 } else if (!context.checkGlobalConstraints()) {
219 logger.debug("Global contraint is not satisifed."); 229 logger.debug("Global contraint is not satisifed.");
220 context.backtrack(); 230 context.backtrack();
231 } else if (!numericSolver.isSatisfiable()) {
232 logger.debug("Numeric constraints are not satisifed.");
233 context.backtrack();
221 } else { 234 } else {
222 final Fitness nextFitness = context.calculateFitness(); 235 final Fitness nextFitness = context.calculateFitness();
223 checkForSolution(nextFitness); 236 checkForSolution(nextFitness);
@@ -272,7 +285,8 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
272 private void checkForSolution(final Fitness fittness) { 285 private void checkForSolution(final Fitness fittness) {
273 if (fittness.isSatisifiesHardObjectives()) { 286 if (fittness.isSatisifiesHardObjectives()) {
274 if (solutionStoreWithDiversityDescriptor.isDifferent(context)) { 287 if (solutionStoreWithDiversityDescriptor.isDifferent(context)) {
275 solutionStoreWithCopy.newSolution(context); 288 Map<EObject, EObject> trace = solutionStoreWithCopy.newSolution(context);
289 numericSolver.fillSolutionCopy(trace);
276 solutionStoreWithDiversityDescriptor.newSolution(context); 290 solutionStoreWithDiversityDescriptor.newSolution(context);
277 solutionStore.newSolution(context); 291 solutionStore.newSolution(context);
278 configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution); 292 configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution);
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
new file mode 100644
index 00000000..b72bdb44
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
@@ -0,0 +1,114 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
5import java.util.HashMap
6import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
7import org.eclipse.viatra.query.runtime.api.IPatternMatch
8import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
9import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
10import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator
11import org.eclipse.viatra.dse.base.ThreadContext
12import org.eclipse.emf.ecore.EObject
13import java.util.Map
14import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
15import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
16import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement
17import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement
18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement
19import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement
20import java.util.List
21import java.math.BigDecimal
22
23class NumericSolver {
24 val ThreadContext threadContext;
25 val constraint2UnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>
26 NumericTranslator t = new NumericTranslator
27
28 new(ThreadContext threadContext, ModelGenerationMethod method) {
29 this.threadContext = threadContext
30 val engine = threadContext.queryEngine
31 for(entry : method.unitPropagationPreconditions.entrySet) {
32 val constraint = entry.key
33 val querySpec = entry.value
34 val matcher = querySpec.getMatcher(engine);
35 constraint2UnitPropagationPrecondition.put(constraint,matcher)
36 }
37 }
38
39 def boolean isSatisfiable() {
40 if(constraint2UnitPropagationPrecondition.empty) return true
41 else {
42 val propagatedConstraints = new HashMap
43 for(entry : constraint2UnitPropagationPrecondition.entrySet) {
44 val constraint = entry.key
45 //println(constraint)
46 val allMatches = entry.value.allMatches.map[it.toArray]
47 //println(allMatches.toList)
48 propagatedConstraints.put(constraint,allMatches)
49 }
50
51 if(propagatedConstraints.values.forall[empty]) {
52 return true
53 } else {
54 val res = t.delegateIsSatisfiable(propagatedConstraints)
55 //println(res)
56 return res
57 }
58 }
59 }
60
61 def fillSolutionCopy(Map<EObject, EObject> trace) {
62 val model = threadContext.getModel as PartialInterpretation
63 val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList
64 if(constraint2UnitPropagationPrecondition.empty) {
65 fillWithDefaultValues(dataObjects,trace)
66 } else {
67 val propagatedConstraints = new HashMap
68 for(entry : constraint2UnitPropagationPrecondition.entrySet) {
69 val constraint = entry.key
70 val allMatches = entry.value.allMatches.map[it.toArray]
71 propagatedConstraints.put(constraint,allMatches)
72 }
73
74 if(propagatedConstraints.values.forall[empty]) {
75 fillWithDefaultValues(dataObjects,trace)
76 } else {
77 val solution = t.delegateGetSolution(dataObjects,propagatedConstraints)
78 fillWithSolutions(dataObjects,solution,trace)
79 }
80 }
81 }
82
83 def protected fillWithDefaultValues(List<PrimitiveElement> elements, Map<EObject, EObject> trace) {
84 for(element : elements) {
85 if(element.valueSet==false) {
86 val value = getDefaultValue(element)
87 val target = trace.get(element) as PrimitiveElement
88 target.fillWithValue(value)
89 }
90 }
91 }
92
93 def protected dispatch getDefaultValue(BooleanElement e) {false}
94 def protected dispatch getDefaultValue(IntegerElement e) {0}
95 def protected dispatch getDefaultValue(RealElement e) {0.0}
96 def protected dispatch getDefaultValue(StringElement e) {""}
97
98 def protected fillWithSolutions(List<PrimitiveElement> elements, Map<PrimitiveElement, Integer> solution, Map<EObject, EObject> trace) {
99 for(element : elements) {
100 if(element.valueSet==false) {
101 if(solution.containsKey(element)) {
102 val value = solution.get(element)
103 val target = trace.get(element) as PrimitiveElement
104 target.fillWithValue(value)
105 }
106 }
107 }
108 }
109
110 def protected dispatch fillWithValue(BooleanElement e, Object value) {e.valueSet=true e.value=value as Boolean}
111 def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer}
112 def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=BigDecimal.valueOf(value as Double) }
113 def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String}
114} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
index a8b7301e..21867a4e 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
@@ -25,7 +25,7 @@ class SolutionStoreWithCopy {
25 newSolution(context) 25 newSolution(context)
26 }*/ 26 }*/
27 27
28 def newSolution(ThreadContext context) { 28 def Map<EObject,EObject> newSolution(ThreadContext context) {
29 //print(System.nanoTime-initTime + ";") 29 //print(System.nanoTime-initTime + ";")
30 val copyStart = System.nanoTime 30 val copyStart = System.nanoTime
31 val solution = context.model as PartialInterpretation 31 val solution = context.model as PartialInterpretation
@@ -36,6 +36,7 @@ class SolutionStoreWithCopy {
36 copyTraces.add(copier) 36 copyTraces.add(copier)
37 runtime += System.nanoTime - copyStart 37 runtime += System.nanoTime - copyStart
38 solutionTimes.add(System.nanoTime-sartTime) 38 solutionTimes.add(System.nanoTime-sartTime)
39 return copier
39 } 40 }
40 def getSumRuntime() { 41 def getSumRuntime() {
41 return runtime 42 return runtime
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-29 16:19:07 +0000