diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src')
2 files changed, 185 insertions, 28 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 adecf1d4..569414f0 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 | |||
@@ -13,11 +13,6 @@ import org.eclipse.xtext.xbase.XNumberLiteral | |||
13 | import org.eclipse.xtext.xbase.XUnaryOperation | 13 | import org.eclipse.xtext.xbase.XUnaryOperation |
14 | 14 | ||
15 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 15 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
16 | import com.microsoft.z3.BoolExpr | ||
17 | import java.util.Set | ||
18 | import java.util.List | ||
19 | import org.eclipse.xtext.common.types.JvmIdentifiableElement | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement | ||
21 | 16 | ||
22 | class ExpressionEvaluation2Logic { | 17 | class ExpressionEvaluation2Logic { |
23 | val extension LogicProblemBuilder builder = new LogicProblemBuilder | 18 | val extension LogicProblemBuilder builder = new LogicProblemBuilder |
@@ -28,8 +23,11 @@ class ExpressionEvaluation2Logic { | |||
28 | } | 23 | } |
29 | 24 | ||
30 | def Term transformEval(PVariable target, XExpression expression, Map<PVariable, Variable> variable2Variable) { | 25 | def Term transformEval(PVariable target, XExpression expression, Map<PVariable, Variable> variable2Variable) { |
31 | numericSolver.test(expression); | 26 | // numericSolver.testIsNotSat(expression, expression.transform(variable2Variable)); |
32 | // numericSolver.isSatisfiable(null) | 27 | // numericSolver.testGetOneSol(expression, expression.transform(variable2Variable)); |
28 | numericSolver.testGetOneSol2(expression, expression.transform(variable2Variable)); | ||
29 | // numericSolver.testIsSat(expression, expression.transform(variable2Variable)); | ||
30 | |||
33 | return expression.transform(variable2Variable) | 31 | return expression.transform(variable2Variable) |
34 | } | 32 | } |
35 | 33 | ||
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 b9532c46..28fa2c64 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 | |||
@@ -1,6 +1,8 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; | 1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; |
2 | 2 | ||
3 | import java.util.ArrayList; | ||
3 | import java.util.HashMap; | 4 | import java.util.HashMap; |
5 | import java.util.HashSet; | ||
4 | import java.util.List; | 6 | import java.util.List; |
5 | import java.util.Map; | 7 | import java.util.Map; |
6 | import java.util.Set; | 8 | import java.util.Set; |
@@ -21,6 +23,7 @@ import com.microsoft.z3.Solver; | |||
21 | import com.microsoft.z3.Status; | 23 | import com.microsoft.z3.Status; |
22 | import com.microsoft.z3.enumerations.Z3_ast_print_mode; | 24 | import com.microsoft.z3.enumerations.Z3_ast_print_mode; |
23 | 25 | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | ||
24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; | 27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; |
25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | 28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; |
26 | 29 | ||
@@ -59,23 +62,181 @@ public class NumericProblemSolver { | |||
59 | return ctx; | 62 | return ctx; |
60 | } | 63 | } |
61 | 64 | ||
62 | // TODO: Remove this after integration | 65 | public void testIsSat(XExpression expression, Term t) throws Exception { |
63 | public void test(XExpression expression) throws Exception { | 66 | int count = 10000; |
64 | Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); | 67 | Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); |
65 | matches.put(expression, null); | 68 | Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>(); |
66 | isSatisfiable(matches); | 69 | ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression); |
70 | |||
71 | for (int i = 0; i < count; i++) { | ||
72 | Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); | ||
73 | for (JvmIdentifiableElement e: allElem) { | ||
74 | FakeIntegerElement intE = new FakeIntegerElement(); | ||
75 | match.put(e, intE); | ||
76 | } | ||
77 | matchSet.add(match); | ||
78 | } | ||
79 | |||
80 | matches.put(expression, matchSet); | ||
81 | long start = System.currentTimeMillis(); | ||
82 | boolean sat = isSatisfiable(matches); | ||
83 | long end = System.currentTimeMillis(); | ||
84 | System.out.println(sat); | ||
85 | System.out.println("Number of matches: " + count); | ||
86 | System.out.println("Running time:" + (end - start)); | ||
87 | } | ||
88 | |||
89 | |||
90 | public void testIsNotSat(XExpression expression, Term t) throws Exception { | ||
91 | Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); | ||
92 | Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>(); | ||
93 | Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); | ||
94 | ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression); | ||
95 | FakeIntegerElement int1 = null; | ||
96 | FakeIntegerElement int2 = null; | ||
97 | boolean first = true; | ||
98 | for (JvmIdentifiableElement e: allElem) { | ||
99 | FakeIntegerElement intE = new FakeIntegerElement(); | ||
100 | if (first) { | ||
101 | int1 = intE; | ||
102 | first = false; | ||
103 | } else { | ||
104 | int2 = intE; | ||
105 | } | ||
106 | |||
107 | match.put(e, intE); | ||
108 | } | ||
109 | matchSet.add(match); | ||
110 | |||
111 | Map<JvmIdentifiableElement,PrimitiveElement> match2 = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); | ||
112 | boolean first2 = true; | ||
113 | for (JvmIdentifiableElement e: allElem) { | ||
114 | if (first2) { | ||
115 | match2.put(e, int2); | ||
116 | first2 = false; | ||
117 | } else { | ||
118 | match2.put(e, int1); | ||
119 | } | ||
120 | } | ||
121 | matchSet.add(match2); | ||
122 | |||
123 | matches.put(expression, matchSet); | ||
124 | long start = System.currentTimeMillis(); | ||
125 | boolean sat = isSatisfiable(matches); | ||
126 | long end = System.currentTimeMillis(); | ||
127 | System.out.println(sat); | ||
128 | System.out.println("Number of matches: "); | ||
129 | System.out.println("Running time:" + (end - start)); | ||
130 | } | ||
131 | |||
132 | |||
133 | public void testGetOneSol(XExpression expression, Term t) throws Exception { | ||
134 | int count = 10; | ||
135 | Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); | ||
136 | Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>(); | ||
137 | |||
138 | ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression); | ||
139 | List<Object> obj = new ArrayList<Object>(); | ||
140 | |||
141 | for (int i = 0; i < count; i++) { | ||
142 | Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); | ||
143 | for (JvmIdentifiableElement e: allElem) { | ||
144 | FakeIntegerElement intE = new FakeIntegerElement(); | ||
145 | obj.add(intE); | ||
146 | match.put(e, intE); | ||
147 | } | ||
148 | matchSet.add(match); | ||
149 | matches.put(expression, matchSet); | ||
150 | } | ||
151 | |||
152 | long start = System.currentTimeMillis(); | ||
153 | Map<Object,Integer> sol = getOneSolution(obj, matches); | ||
154 | long end = System.currentTimeMillis(); | ||
155 | |||
156 | |||
157 | // Print sol | ||
158 | for (Object o: sol.keySet()) { | ||
159 | System.out.println(o + " :" + sol.get(o)); | ||
160 | } | ||
161 | |||
162 | |||
163 | System.out.println("Number of matches: " + count); | ||
164 | System.out.println("Running time:" + (end - start)); | ||
165 | } | ||
166 | |||
167 | |||
168 | public void testGetOneSol2(XExpression expression, Term t) throws Exception { | ||
169 | int count = 50; | ||
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 | long start = System.currentTimeMillis(); | ||
210 | Map<Object,Integer> sol = getOneSolution(obj, matches); | ||
211 | long end = System.currentTimeMillis(); | ||
212 | |||
213 | System.out.println("Number of matches: " + matchSet.size()); | ||
214 | System.out.println("Running time:" + (end - start)); | ||
215 | } | ||
216 | |||
217 | private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) { | ||
218 | ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); | ||
219 | XExpression left = ((XBinaryOperation) expression).getLeftOperand(); | ||
220 | XExpression right = ((XBinaryOperation) expression).getRightOperand(); | ||
221 | |||
222 | getJvmIdentifiableElementsHelper(left, allElem); | ||
223 | getJvmIdentifiableElementsHelper(right, allElem); | ||
224 | return allElem; | ||
225 | } | ||
226 | |||
227 | private void getJvmIdentifiableElementsHelper(XExpression e, List<JvmIdentifiableElement> allElem) { | ||
228 | if (e instanceof XFeatureCall) { | ||
229 | allElem.add(((XFeatureCall) e).getFeature()); | ||
230 | } else if (e instanceof XBinaryOperation) { | ||
231 | getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getLeftOperand(), allElem); | ||
232 | getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem); | ||
233 | } | ||
67 | } | 234 | } |
68 | 235 | ||
69 | public boolean isSatisfiable(Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | 236 | public boolean isSatisfiable(Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { |
70 | boolean sat = false; | ||
71 | BoolExpr problemInstance = formNumericProblemInstance(matches); | 237 | BoolExpr problemInstance = formNumericProblemInstance(matches); |
72 | s.add(problemInstance); | 238 | s.add(problemInstance); |
73 | if (s.check() == Status.SATISFIABLE) { | 239 | return s.check() == Status.SATISFIABLE; |
74 | sat = true; | ||
75 | } else { | ||
76 | sat = false; | ||
77 | } | ||
78 | return sat; | ||
79 | } | 240 | } |
80 | 241 | ||
81 | public Map<Object,Integer> getOneSolution(List<Object> objs, Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | 242 | public Map<Object,Integer> getOneSolution(List<Object> objs, Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { |
@@ -84,8 +245,7 @@ public class NumericProblemSolver { | |||
84 | s.add(problemInstance); | 245 | s.add(problemInstance); |
85 | if (s.check() == Status.SATISFIABLE) { | 246 | if (s.check() == Status.SATISFIABLE) { |
86 | Model m = s.getModel(); | 247 | Model m = s.getModel(); |
87 | Set<Object> allObj = varMap.keySet(); | 248 | for (Object o: objs) { |
88 | for (Object o: allObj) { | ||
89 | IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false); | 249 | IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false); |
90 | Integer oSol = Integer.parseInt(val.toString()); | 250 | Integer oSol = Integer.parseInt(val.toString()); |
91 | sol.put(o, oSol); | 251 | sol.put(o, oSol); |
@@ -94,7 +254,7 @@ public class NumericProblemSolver { | |||
94 | return sol; | 254 | return sol; |
95 | } | 255 | } |
96 | 256 | ||
97 | private BoolExpr formNumericConstraint(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch, Map<Object, Expr> varMap) throws Exception { | 257 | private BoolExpr formNumericConstraint(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception { |
98 | if (!(e instanceof XBinaryOperation)) { | 258 | if (!(e instanceof XBinaryOperation)) { |
99 | throw new Exception ("error in check expression!!!"); | 259 | throw new Exception ("error in check expression!!!"); |
100 | } | 260 | } |
@@ -103,8 +263,8 @@ public class NumericProblemSolver { | |||
103 | 263 | ||
104 | BoolExpr constraint = null; | 264 | BoolExpr constraint = null; |
105 | 265 | ||
106 | ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch, varMap); | 266 | ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); |
107 | ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch, varMap); | 267 | ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); |
108 | 268 | ||
109 | if (nameEndsWith(name, N_LESSTHAN)) { | 269 | if (nameEndsWith(name, N_LESSTHAN)) { |
110 | constraint = ctx.mkLt(left_operand, right_operand); | 270 | constraint = ctx.mkLt(left_operand, right_operand); |
@@ -126,12 +286,11 @@ public class NumericProblemSolver { | |||
126 | throw new Exception ("Unsupported binary operation " + name); | 286 | throw new Exception ("Unsupported binary operation " + name); |
127 | } | 287 | } |
128 | 288 | ||
129 | System.out.println(constraint.toString()); | ||
130 | return constraint; | 289 | return constraint; |
131 | } | 290 | } |
132 | 291 | ||
133 | // TODO: add variable: state of the solver | 292 | // TODO: add variable: state of the solver |
134 | private ArithExpr formNumericConstraintHelper(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch, Map<Object, Expr> varMap) throws Exception { | 293 | private ArithExpr formNumericConstraintHelper(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception { |
135 | ArithExpr expr = null; | 294 | ArithExpr expr = null; |
136 | // Variables | 295 | // Variables |
137 | if (e instanceof XFeatureCall) { | 296 | if (e instanceof XFeatureCall) { |
@@ -158,8 +317,8 @@ public class NumericProblemSolver { | |||
158 | // Expressions with operators | 317 | // Expressions with operators |
159 | else if (e instanceof XBinaryOperation) { | 318 | else if (e instanceof XBinaryOperation) { |
160 | String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); | 319 | String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); |
161 | ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch, varMap); | 320 | ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); |
162 | ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch, varMap); | 321 | ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); |
163 | 322 | ||
164 | if (nameEndsWith(name, N_PLUS)) { | 323 | if (nameEndsWith(name, N_PLUS)) { |
165 | expr = ctx.mkAdd(left_operand, right_operand); | 324 | expr = ctx.mkAdd(left_operand, right_operand); |
@@ -192,7 +351,7 @@ public class NumericProblemSolver { | |||
192 | for (XExpression e: matches.keySet()) { | 351 | for (XExpression e: matches.keySet()) { |
193 | Set<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e); | 352 | Set<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e); |
194 | for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) { | 353 | for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) { |
195 | BoolExpr constraintInstance = formNumericConstraint(e, aMatch, varMap); | 354 | BoolExpr constraintInstance = formNumericConstraint(e, aMatch); |
196 | constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance); | 355 | constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance); |
197 | } | 356 | } |
198 | } | 357 | } |