diff options
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java | 162 |
1 files changed, 117 insertions, 45 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java index a58bd855..2372177a 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,7 +1,13 @@ | |||
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.ArrayList; |
4 | import java.util.Arrays; | ||
5 | import java.util.Collections; | ||
4 | import java.util.HashMap; | 6 | import java.util.HashMap; |
7 | import java.util.HashSet; | ||
8 | import java.util.List; | ||
9 | import java.util.Map; | ||
10 | import java.util.Set; | ||
5 | 11 | ||
6 | import org.eclipse.xtext.xbase.XBinaryOperation; | 12 | import org.eclipse.xtext.xbase.XBinaryOperation; |
7 | import org.eclipse.xtext.xbase.XExpression; | 13 | import org.eclipse.xtext.xbase.XExpression; |
@@ -11,6 +17,7 @@ import org.eclipse.xtext.xbase.XNumberLiteral; | |||
11 | import com.microsoft.z3.ArithExpr; | 17 | import com.microsoft.z3.ArithExpr; |
12 | import com.microsoft.z3.BoolExpr; | 18 | import com.microsoft.z3.BoolExpr; |
13 | import com.microsoft.z3.Context; | 19 | import com.microsoft.z3.Context; |
20 | import com.microsoft.z3.Expr; | ||
14 | import com.microsoft.z3.IntExpr; | 21 | import com.microsoft.z3.IntExpr; |
15 | import com.microsoft.z3.Solver; | 22 | import com.microsoft.z3.Solver; |
16 | import com.microsoft.z3.Status; | 23 | import com.microsoft.z3.Status; |
@@ -32,34 +39,38 @@ public class NumericProblemSolver { | |||
32 | private static final String N_NOTEQUALS = "operator_notEquals"; | 39 | private static final String N_NOTEQUALS = "operator_notEquals"; |
33 | private static final String N_EQUALS3 = "operator_tripleEquals"; | 40 | private static final String N_EQUALS3 = "operator_tripleEquals"; |
34 | private static final String N_NOTEQUALS3 = "operator_tripleNotEquals"; | 41 | private static final String N_NOTEQUALS3 = "operator_tripleNotEquals"; |
35 | 42 | ||
36 | private static int counter = 0; | ||
37 | |||
38 | private Context ctx; | 43 | private Context ctx; |
39 | private ArithExpr[] vars = new ArithExpr[2]; | 44 | private Solver s; |
45 | private Map<XExpression, BoolExpr> templates; | ||
46 | private Map<XExpression, Map<Object, Expr>> bindings; | ||
47 | private BoolExpr test; | ||
40 | 48 | ||
41 | public NumericProblemSolver() { | 49 | public NumericProblemSolver() { |
42 | HashMap<String, String> cfg = new HashMap<String, String>(); | 50 | HashMap<String, String> cfg = new HashMap<String, String>(); |
43 | cfg.put("model", "true"); | 51 | cfg.put("model", "true"); |
44 | ctx = new Context(cfg); | 52 | ctx = new Context(cfg); |
53 | s = ctx.mkSolver(); | ||
54 | templates = new HashMap<XExpression, BoolExpr>(); | ||
55 | bindings = new HashMap<XExpression, Map<Object, Expr>>(); | ||
45 | } | 56 | } |
46 | 57 | ||
47 | public Context getNumericProblemContext() { | 58 | public Context getNumericProblemContext() { |
48 | return ctx; | 59 | return ctx; |
49 | } | 60 | } |
50 | 61 | ||
51 | public BoolExpr formNumericProblemTemplate(XExpression e) throws Exception { | 62 | public void formNumericProblemTemplate(XExpression e) throws Exception { |
52 | if (!(e instanceof XBinaryOperation)) { | 63 | if (!(e instanceof XBinaryOperation)) { |
53 | throw new Exception ("error in check expression!!!"); | 64 | throw new Exception ("error in check expression!!!"); |
54 | } | 65 | } |
55 | 66 | ||
56 | String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); | 67 | String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); |
57 | 68 | ||
58 | BoolExpr constraint = null; | 69 | BoolExpr constraint = null; |
59 | 70 | ||
60 | ArithExpr left_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getLeftOperand()); | 71 | ArithExpr left_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getLeftOperand()); |
61 | ArithExpr right_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getRightOperand()); | 72 | ArithExpr right_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getRightOperand()); |
62 | 73 | ||
63 | if (nameEndsWith(name, N_LESSTHAN)) { | 74 | if (nameEndsWith(name, N_LESSTHAN)) { |
64 | constraint = ctx.mkLt(left_operand, right_operand); | 75 | constraint = ctx.mkLt(left_operand, right_operand); |
65 | } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) { | 76 | } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) { |
@@ -80,57 +91,39 @@ public class NumericProblemSolver { | |||
80 | throw new Exception ("Unsupported binary operation " + name); | 91 | throw new Exception ("Unsupported binary operation " + name); |
81 | } | 92 | } |
82 | 93 | ||
83 | // To check the constraint | 94 | templates.put(e, constraint); |
84 | System.out.println(constraint.toString()); | 95 | HashMap<XExpression, Set<List<Object>>> matches = new HashMap<XExpression, Set<List<Object>>>(); |
85 | 96 | Object o1 = new Object(); | |
86 | int mage = 5; | 97 | Object o2 = new Object(); |
87 | int page = 25; | 98 | List<Object> list = new ArrayList<Object>(); |
88 | 99 | list.add(o1); | |
89 | BoolExpr inst = ctx.mkTrue(); | 100 | list.add(o2); |
90 | for (ArithExpr var: vars) { | 101 | Set<List<Object>> set = new HashSet<List<Object>>(); |
91 | inst = ctx.mkAnd(inst, ctx.mkEq(var, ctx.mkInt(mage))); | 102 | set.add(list); |
92 | } | 103 | matches.put(e, set); |
93 | System.out.println(inst.toString()); | 104 | System.out.println("************************"); |
94 | 105 | System.out.println(this.isSatisfiable(matches)); | |
95 | Solver s = ctx.mkSolver(); | ||
96 | s.add(constraint); | ||
97 | s.add(inst); | ||
98 | |||
99 | if (s.check() == Status.SATISFIABLE) { | ||
100 | System.out.println("satisfiable"); | ||
101 | } else { | ||
102 | System.out.println("not satisfiable"); | ||
103 | } | ||
104 | |||
105 | |||
106 | return constraint; | ||
107 | |||
108 | } | 106 | } |
109 | 107 | ||
108 | // TODO: add variable: state of the solver | ||
110 | private ArithExpr formNumericProblemTemplateHelper(XExpression e) throws Exception { | 109 | private ArithExpr formNumericProblemTemplateHelper(XExpression e) throws Exception { |
111 | ArithExpr expr = null; | 110 | ArithExpr expr = null; |
112 | // Variables | 111 | // Variables |
113 | // how to know the data type of this variable????? | ||
114 | if (e instanceof XFeatureCall) { | 112 | if (e instanceof XFeatureCall) { |
115 | String var_name = ((XFeatureCall) e).getFeature().getQualifiedName(); | 113 | String var_name = ((XFeatureCall) e).getFeature().getQualifiedName(); |
116 | vars[counter] = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort()); | 114 | expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort()); |
117 | expr = vars[counter]; | ||
118 | counter++; | ||
119 | } | 115 | } |
120 | // Constants | 116 | // Constants |
121 | else if (e instanceof XNumberLiteral) { | 117 | else if (e instanceof XNumberLiteral) { |
122 | String value = ((XNumberLiteral) e).getValue(); | 118 | String value = ((XNumberLiteral) e).getValue(); |
123 | try{ int val = Integer.parseInt(value); expr = (ArithExpr) ctx.mkInt(val);} catch(NumberFormatException err){} | 119 | try{ int val = Integer.parseInt(value); expr = (ArithExpr) ctx.mkInt(val);} catch(NumberFormatException err){} |
124 | // What to do with short / float / double??? | ||
125 | // e.g. For floats, need to use FPAdd instead of normal Add!! | ||
126 | } | 120 | } |
127 | // Expressions with operators | 121 | // Expressions with operators |
128 | else if (e instanceof XBinaryOperation) { | 122 | else if (e instanceof XBinaryOperation) { |
129 | String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); | 123 | String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); |
130 | |||
131 | ArithExpr left_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getLeftOperand()); | 124 | ArithExpr left_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getLeftOperand()); |
132 | ArithExpr right_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getRightOperand()); | 125 | ArithExpr right_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getRightOperand()); |
133 | 126 | ||
134 | if (nameEndsWith(name, N_PLUS)) { | 127 | if (nameEndsWith(name, N_PLUS)) { |
135 | expr = ctx.mkAdd(left_operand, right_operand); | 128 | expr = ctx.mkAdd(left_operand, right_operand); |
136 | } else if (nameEndsWith(name, N_MINUS)) { | 129 | } else if (nameEndsWith(name, N_MINUS)) { |
@@ -152,9 +145,88 @@ public class NumericProblemSolver { | |||
152 | return expr; | 145 | return expr; |
153 | 146 | ||
154 | } | 147 | } |
155 | 148 | ||
156 | private boolean nameEndsWith(String name, String end) { | 149 | private boolean nameEndsWith(String name, String end) { |
157 | return name.startsWith(N_Base) && name.endsWith(end); | 150 | return name.startsWith(N_Base) && name.endsWith(end); |
158 | } | 151 | } |
159 | 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 | |||
165 | // public Map<Object,Integer> getOneSolution(List<Object>, Map<XExpression, Set<List<Object>>> matches) { | ||
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(); | ||
177 | for (XExpression e: matches.keySet()) { | ||
178 | BoolExpr template = templates.get(e); | ||
179 | Set<List<Object>> matchSets = matches.get(e); | ||
180 | Map<Object, Expr> varMap = bindings.get(e); | ||
181 | |||
182 | if (varMap == null) { | ||
183 | varMap = new HashMap<Object, Expr>(); | ||
184 | bindings.put(e, varMap); | ||
185 | } | ||
186 | |||
187 | for (List<Object> aMatch: matchSets) { | ||
188 | Expr[] expressions = template.getArgs().clone(); | ||
189 | formNumericProblemInstance(expressions, aMatch, varMap, 0); | ||
190 | constraintInstances = ctx.mkAnd(constraintInstances, formConstraintInstance(template, expressions)); | ||
191 | } | ||
192 | } | ||
193 | return constraintInstances; | ||
194 | } | ||
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 | } | ||
160 | } | 232 | } |