diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme')
2 files changed, 67 insertions, 97 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 a1e18250..adecf1d4 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,6 +13,11 @@ 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 | ||
16 | 21 | ||
17 | class ExpressionEvaluation2Logic { | 22 | class ExpressionEvaluation2Logic { |
18 | val extension LogicProblemBuilder builder = new LogicProblemBuilder | 23 | val extension LogicProblemBuilder builder = new LogicProblemBuilder |
@@ -23,10 +28,9 @@ class ExpressionEvaluation2Logic { | |||
23 | } | 28 | } |
24 | 29 | ||
25 | def Term transformEval(PVariable target, XExpression expression, Map<PVariable, Variable> variable2Variable) { | 30 | def Term transformEval(PVariable target, XExpression expression, Map<PVariable, Variable> variable2Variable) { |
26 | val test = expression.transform(variable2Variable) | 31 | numericSolver.test(expression); |
27 | numericSolver.formNumericProblemTemplate(expression) | 32 | // numericSolver.isSatisfiable(null) |
28 | 33 | return expression.transform(variable2Variable) | |
29 | return test | ||
30 | } | 34 | } |
31 | 35 | ||
32 | static val N_Base = "org.eclipse.xtext.xbase.lib." | 36 | 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 index 2372177a..834cc2f0 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,14 +1,11 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; | 1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; |
2 | 2 | ||
3 | import java.util.ArrayList; | ||
4 | import java.util.Arrays; | ||
5 | import java.util.Collections; | ||
6 | import java.util.HashMap; | 3 | import java.util.HashMap; |
7 | import java.util.HashSet; | ||
8 | import java.util.List; | 4 | import java.util.List; |
9 | import java.util.Map; | 5 | import java.util.Map; |
10 | import java.util.Set; | 6 | import java.util.Set; |
11 | 7 | ||
8 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; | ||
12 | import org.eclipse.xtext.xbase.XBinaryOperation; | 9 | import org.eclipse.xtext.xbase.XBinaryOperation; |
13 | import org.eclipse.xtext.xbase.XExpression; | 10 | import org.eclipse.xtext.xbase.XExpression; |
14 | import org.eclipse.xtext.xbase.XFeatureCall; | 11 | import org.eclipse.xtext.xbase.XFeatureCall; |
@@ -22,6 +19,9 @@ import com.microsoft.z3.IntExpr; | |||
22 | import com.microsoft.z3.Solver; | 19 | import com.microsoft.z3.Solver; |
23 | import com.microsoft.z3.Status; | 20 | import com.microsoft.z3.Status; |
24 | 21 | ||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; | ||
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | ||
24 | |||
25 | 25 | ||
26 | public class NumericProblemSolver { | 26 | public class NumericProblemSolver { |
27 | private static final String N_Base = "org.eclipse.xtext.xbase.lib."; | 27 | private static final String N_Base = "org.eclipse.xtext.xbase.lib."; |
@@ -42,24 +42,50 @@ public class NumericProblemSolver { | |||
42 | 42 | ||
43 | private Context ctx; | 43 | private Context ctx; |
44 | private Solver s; | 44 | private Solver s; |
45 | private Map<XExpression, BoolExpr> templates; | ||
46 | private Map<XExpression, Map<Object, Expr>> bindings; | 45 | private Map<XExpression, Map<Object, Expr>> bindings; |
47 | private BoolExpr test; | ||
48 | 46 | ||
49 | public NumericProblemSolver() { | 47 | public NumericProblemSolver() { |
50 | HashMap<String, String> cfg = new HashMap<String, String>(); | 48 | HashMap<String, String> cfg = new HashMap<String, String>(); |
51 | cfg.put("model", "true"); | 49 | cfg.put("model", "true"); |
52 | ctx = new Context(cfg); | 50 | ctx = new Context(cfg); |
53 | s = ctx.mkSolver(); | 51 | s = ctx.mkSolver(); |
54 | templates = new HashMap<XExpression, BoolExpr>(); | ||
55 | bindings = new HashMap<XExpression, Map<Object, Expr>>(); | 52 | bindings = new HashMap<XExpression, Map<Object, Expr>>(); |
56 | } | 53 | } |
57 | 54 | ||
58 | public Context getNumericProblemContext() { | 55 | public Context getNumericProblemContext() { |
59 | return ctx; | 56 | return ctx; |
60 | } | 57 | } |
58 | |||
59 | // TODO: Remove this after integration | ||
60 | public void test(XExpression expression) throws Exception { | ||
61 | Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); | ||
62 | matches.put(expression, null); | ||
63 | isSatisfiable(matches); | ||
64 | } | ||
65 | |||
66 | public boolean isSatisfiable(Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | ||
67 | boolean sat = false; | ||
68 | BoolExpr problemInstance = formNumericProblemInstance(matches); | ||
69 | s.add(problemInstance); | ||
70 | if (s.check() == Status.SATISFIABLE) { | ||
71 | sat = true; | ||
72 | } else { | ||
73 | sat = false; | ||
74 | } | ||
75 | return sat; | ||
76 | } | ||
77 | |||
78 | public Map<Object,Integer> getOneSolution(List<Object> objs, Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | ||
79 | Map<Object,Integer> sol = new HashMap<Object, Integer>(); | ||
80 | BoolExpr problemInstance = formNumericProblemInstance(matches); | ||
81 | s.add(problemInstance); | ||
82 | if (s.check() == Status.SATISFIABLE) { | ||
83 | //TODO: Form the solution here | ||
84 | } | ||
85 | return sol; | ||
86 | } | ||
61 | 87 | ||
62 | public void formNumericProblemTemplate(XExpression e) throws Exception { | 88 | private BoolExpr formNumericConstraint(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch, Map<Object, Expr> varMap) throws Exception { |
63 | if (!(e instanceof XBinaryOperation)) { | 89 | if (!(e instanceof XBinaryOperation)) { |
64 | throw new Exception ("error in check expression!!!"); | 90 | throw new Exception ("error in check expression!!!"); |
65 | } | 91 | } |
@@ -68,8 +94,8 @@ public class NumericProblemSolver { | |||
68 | 94 | ||
69 | BoolExpr constraint = null; | 95 | BoolExpr constraint = null; |
70 | 96 | ||
71 | ArithExpr left_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getLeftOperand()); | 97 | ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch, varMap); |
72 | ArithExpr right_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getRightOperand()); | 98 | ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch, varMap); |
73 | 99 | ||
74 | if (nameEndsWith(name, N_LESSTHAN)) { | 100 | if (nameEndsWith(name, N_LESSTHAN)) { |
75 | constraint = ctx.mkLt(left_operand, right_operand); | 101 | constraint = ctx.mkLt(left_operand, right_operand); |
@@ -91,27 +117,28 @@ public class NumericProblemSolver { | |||
91 | throw new Exception ("Unsupported binary operation " + name); | 117 | throw new Exception ("Unsupported binary operation " + name); |
92 | } | 118 | } |
93 | 119 | ||
94 | templates.put(e, constraint); | 120 | return constraint; |
95 | HashMap<XExpression, Set<List<Object>>> matches = new HashMap<XExpression, Set<List<Object>>>(); | ||
96 | Object o1 = new Object(); | ||
97 | Object o2 = new Object(); | ||
98 | List<Object> list = new ArrayList<Object>(); | ||
99 | list.add(o1); | ||
100 | list.add(o2); | ||
101 | Set<List<Object>> set = new HashSet<List<Object>>(); | ||
102 | set.add(list); | ||
103 | matches.put(e, set); | ||
104 | System.out.println("************************"); | ||
105 | System.out.println(this.isSatisfiable(matches)); | ||
106 | } | 121 | } |
107 | 122 | ||
108 | // TODO: add variable: state of the solver | 123 | // TODO: add variable: state of the solver |
109 | private ArithExpr formNumericProblemTemplateHelper(XExpression e) throws Exception { | 124 | private ArithExpr formNumericConstraintHelper(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch, Map<Object, Expr> varMap) throws Exception { |
110 | ArithExpr expr = null; | 125 | ArithExpr expr = null; |
111 | // Variables | 126 | // Variables |
112 | if (e instanceof XFeatureCall) { | 127 | if (e instanceof XFeatureCall) { |
113 | String var_name = ((XFeatureCall) e).getFeature().getQualifiedName(); | 128 | PrimitiveElement matchedObj = aMatch.get(((XFeatureCall) e).getFeature()); |
114 | expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort()); | 129 | if (!matchedObj.isValueSet()) { |
130 | if (varMap.get(matchedObj) == null) { | ||
131 | String var_name = ((XFeatureCall) e).getFeature().getQualifiedName() + matchedObj.toString(); | ||
132 | expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort()); | ||
133 | varMap.put(matchedObj, expr); | ||
134 | } else { | ||
135 | expr = (ArithExpr) varMap.get(matchedObj); | ||
136 | } | ||
137 | } else { | ||
138 | int value = ((IntegerElement) matchedObj).getValue(); | ||
139 | expr = (ArithExpr) ctx.mkInt(value); | ||
140 | varMap.put(matchedObj, expr); | ||
141 | } | ||
115 | } | 142 | } |
116 | // Constants | 143 | // Constants |
117 | else if (e instanceof XNumberLiteral) { | 144 | else if (e instanceof XNumberLiteral) { |
@@ -121,8 +148,8 @@ public class NumericProblemSolver { | |||
121 | // Expressions with operators | 148 | // Expressions with operators |
122 | else if (e instanceof XBinaryOperation) { | 149 | else if (e instanceof XBinaryOperation) { |
123 | String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); | 150 | String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); |
124 | ArithExpr left_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getLeftOperand()); | 151 | ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch, varMap); |
125 | ArithExpr right_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getRightOperand()); | 152 | ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch, varMap); |
126 | 153 | ||
127 | if (nameEndsWith(name, N_PLUS)) { | 154 | if (nameEndsWith(name, N_PLUS)) { |
128 | expr = ctx.mkAdd(left_operand, right_operand); | 155 | expr = ctx.mkAdd(left_operand, right_operand); |
@@ -149,34 +176,11 @@ public class NumericProblemSolver { | |||
149 | private boolean nameEndsWith(String name, String end) { | 176 | private boolean nameEndsWith(String name, String end) { |
150 | return name.startsWith(N_Base) && name.endsWith(end); | 177 | return name.startsWith(N_Base) && name.endsWith(end); |
151 | } | 178 | } |
152 | |||
153 | public boolean isSatisfiable(Map<XExpression, Set<List<Object>>> matches) throws Exception { | ||
154 | boolean sat = false; | ||
155 | BoolExpr problemInstance = formNumericProblemInstance(matches); | ||
156 | s.add(problemInstance); | ||
157 | if (s.check() == Status.SATISFIABLE) { | ||
158 | sat = true; | ||
159 | } else { | ||
160 | sat = false; | ||
161 | } | ||
162 | return sat; | ||
163 | } | ||
164 | 179 | ||
165 | // public Map<Object,Integer> getOneSolution(List<Object>, Map<XExpression, Set<List<Object>>> matches) { | 180 | private BoolExpr formNumericProblemInstance(Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { |
166 | // Map<Object,Integer> sol = new HashMap<Object, Integer>(); | ||
167 | // BoolExpr problemInstance = formNumericProblemInstance(matches); | ||
168 | // s.add(problemInstance); | ||
169 | // if (s.check() == Status.SATISFIABLE) { | ||
170 | // //TODO: Form the map here | ||
171 | // } | ||
172 | // return sol; | ||
173 | // } | ||
174 | |||
175 | private BoolExpr formNumericProblemInstance(Map<XExpression, Set<List<Object>>> matches) throws Exception { | ||
176 | BoolExpr constraintInstances = ctx.mkTrue(); | 181 | BoolExpr constraintInstances = ctx.mkTrue(); |
177 | for (XExpression e: matches.keySet()) { | 182 | for (XExpression e: matches.keySet()) { |
178 | BoolExpr template = templates.get(e); | 183 | Set<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e); |
179 | Set<List<Object>> matchSets = matches.get(e); | ||
180 | Map<Object, Expr> varMap = bindings.get(e); | 184 | Map<Object, Expr> varMap = bindings.get(e); |
181 | 185 | ||
182 | if (varMap == null) { | 186 | if (varMap == null) { |
@@ -184,49 +188,11 @@ public class NumericProblemSolver { | |||
184 | bindings.put(e, varMap); | 188 | bindings.put(e, varMap); |
185 | } | 189 | } |
186 | 190 | ||
187 | for (List<Object> aMatch: matchSets) { | 191 | for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) { |
188 | Expr[] expressions = template.getArgs().clone(); | 192 | BoolExpr constraintInstance = formNumericConstraint(e, aMatch, varMap); |
189 | formNumericProblemInstance(expressions, aMatch, varMap, 0); | 193 | constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance); |
190 | constraintInstances = ctx.mkAnd(constraintInstances, formConstraintInstance(template, expressions)); | ||
191 | } | 194 | } |
192 | } | 195 | } |
193 | return constraintInstances; | 196 | return constraintInstances; |
194 | } | 197 | } |
195 | |||
196 | // TODO: Create a new exception class?? | ||
197 | private BoolExpr formConstraintInstance(BoolExpr template, Expr[] expressions) throws Exception { | ||
198 | if (expressions.length != 2) { | ||
199 | throw new Exception("Wrong format"); | ||
200 | } | ||
201 | BoolExpr inst = ctx.mkTrue(); | ||
202 | ArithExpr leftOperand = (ArithExpr) expressions[0]; | ||
203 | ArithExpr rightOperand = (ArithExpr) expressions[1]; | ||
204 | if (template.isLE()) { | ||
205 | inst = ctx.mkLe(leftOperand, rightOperand); | ||
206 | } else if (template.isLT()) { | ||
207 | inst = ctx.mkLt(leftOperand, rightOperand); | ||
208 | } else if (template.isGE()) { | ||
209 | inst = ctx.mkGe(leftOperand, rightOperand); | ||
210 | } else if (template.isGT()) { | ||
211 | inst = ctx.mkGt(leftOperand, rightOperand); | ||
212 | } else if (template.isEq()) { | ||
213 | inst = ctx.mkEq(leftOperand, rightOperand); | ||
214 | } else if (template.isDistinct()) { | ||
215 | inst = ctx.mkDistinct(leftOperand, rightOperand); | ||
216 | } else { | ||
217 | throw new Exception("Something went wrong"); | ||
218 | } | ||
219 | return inst; | ||
220 | } | ||
221 | |||
222 | // TODO: This is not gonna work....How to plug in matched objects to the template??? | ||
223 | private void formNumericProblemInstance(Expr[] expr, List<Object> match, Map<Object, Expr> varMap, int ind) { | ||
224 | for (int i = 0; i < expr.length; i++) { | ||
225 | if (expr[i].isConst()) { | ||
226 | expr[i] = ctx.mkConst(expr[i].toString(), ctx.getIntSort()); | ||
227 | } else if (expr[i].getArgs().length > 0) { | ||
228 | formNumericProblemInstance(expr[i].getArgs(), match, varMap, ind); | ||
229 | } | ||
230 | } | ||
231 | } | ||
232 | } | 198 | } |