diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic')
2 files changed, 323 insertions, 3 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/DrealProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/DrealProblemSolver.java new file mode 100644 index 00000000..d13990be --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/DrealProblemSolver.java | |||
@@ -0,0 +1,315 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; | ||
2 | |||
3 | import java.io.BufferedReader; | ||
4 | import java.io.File; | ||
5 | import java.io.IOException; | ||
6 | import java.io.InputStream; | ||
7 | import java.io.InputStreamReader; | ||
8 | import java.io.PrintWriter; | ||
9 | import java.util.ArrayList; | ||
10 | import java.util.Arrays; | ||
11 | import java.util.HashMap; | ||
12 | import java.util.List; | ||
13 | import java.util.Map; | ||
14 | import java.util.UUID; | ||
15 | |||
16 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; | ||
17 | import org.eclipse.xtext.xbase.XExpression; | ||
18 | |||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | ||
20 | |||
21 | public class DrealProblemSolver { | ||
22 | private static final String N_Base = "org.eclipse.xtext.xbase.lib."; | ||
23 | private static final String N_PLUS = "operator_plus"; | ||
24 | private static final String N_MINUS = "operator_minus"; | ||
25 | private static final String N_POWER = "operator_power"; | ||
26 | private static final String N_MULTIPLY = "operator_multiply"; | ||
27 | private static final String N_DIVIDE = "operator_divide"; | ||
28 | private static final String N_MODULO = "operator_modulo"; | ||
29 | private static final String N_LESSTHAN = "operator_lessThan"; | ||
30 | private static final String N_LESSEQUALSTHAN = "operator_lessEqualsThan"; | ||
31 | private static final String N_GREATERTHAN = "operator_greaterThan"; | ||
32 | private static final String N_GREATEREQUALTHAN = "operator_greaterEqualsThan"; | ||
33 | private static final String N_EQUALS = "operator_equals"; | ||
34 | private static final String N_NOTEQUALS = "operator_notEquals"; | ||
35 | private static final String N_EQUALS3 = "operator_tripleEquals"; | ||
36 | private static final String N_NOTEQUALS3 = "operator_tripleNotEquals"; | ||
37 | |||
38 | private File tempFile; | ||
39 | private PrintWriter printer; | ||
40 | private String containerName; | ||
41 | private Map<Object, String> varMap; | ||
42 | |||
43 | long endformingProblem=0; | ||
44 | long endSolvingProblem=0; | ||
45 | long endFormingSolution=0; | ||
46 | |||
47 | public DrealProblemSolver() throws IOException, InterruptedException { | ||
48 | //setup smt2 input file | ||
49 | tempFile = File.createTempFile("smt", ".smt2"); | ||
50 | printer = new PrintWriter(tempFile); | ||
51 | printer.println(";Header comment"); | ||
52 | printer.println("(set-logic QF_NRA)"); | ||
53 | |||
54 | //setup docker | ||
55 | File parentPath = tempFile.getParentFile(); | ||
56 | System.out.println(parentPath); | ||
57 | System.out.println(tempFile); | ||
58 | //TODO ENSURE that container name is not already in use | ||
59 | containerName = UUID.randomUUID().toString().replace("-", ""); | ||
60 | List<String> startDocker = new ArrayList<String>( | ||
61 | Arrays.asList("docker", "run", | ||
62 | "-id", "--rm", | ||
63 | "--name", containerName, | ||
64 | "-p", "8080:80", | ||
65 | "-v", parentPath + ":/mnt", | ||
66 | "dreal/dreal4")); | ||
67 | Process p = runProcess(startDocker); | ||
68 | |||
69 | //setup varmap | ||
70 | varMap = new HashMap<Object, String>(); | ||
71 | } | ||
72 | |||
73 | public Process runProcess(List<String> cmd) throws IOException, InterruptedException { | ||
74 | // println(cmd) | ||
75 | ProcessBuilder pb = new ProcessBuilder(cmd); | ||
76 | pb.redirectOutput(); | ||
77 | pb.redirectError(); | ||
78 | Process p = pb.start(); | ||
79 | p.waitFor(); | ||
80 | //TODO timeout if needed | ||
81 | // if (!p.waitFor(TIMEOUT, TimeUnit.SECONDS)) { | ||
82 | // p.destroy(); | ||
83 | // } | ||
84 | return p; | ||
85 | } | ||
86 | |||
87 | public long getEndformingProblem() { | ||
88 | return endformingProblem; | ||
89 | } | ||
90 | |||
91 | public long getEndSolvingProblem() { | ||
92 | return endSolvingProblem; | ||
93 | } | ||
94 | |||
95 | public long getEndFormingSolution() { | ||
96 | return endFormingSolution; | ||
97 | } | ||
98 | // | ||
99 | // private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) { | ||
100 | // ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); | ||
101 | // XExpression left = ((XBinaryOperation) expression).getLeftOperand(); | ||
102 | // XExpression right = ((XBinaryOperation) expression).getRightOperand(); | ||
103 | // | ||
104 | // getJvmIdentifiableElementsHelper(left, allElem); | ||
105 | // getJvmIdentifiableElementsHelper(right, allElem); | ||
106 | // return allElem; | ||
107 | // } | ||
108 | // | ||
109 | // private void getJvmIdentifiableElementsHelper(XExpression e, List<JvmIdentifiableElement> allElem) { | ||
110 | // if (e instanceof XFeatureCall) { | ||
111 | // allElem.add(((XFeatureCall) e).getFeature()); | ||
112 | // } else if (e instanceof XBinaryOperation) { | ||
113 | // getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getLeftOperand(), allElem); | ||
114 | // getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem); | ||
115 | // } | ||
116 | // } | ||
117 | |||
118 | public Process callDreal() throws IOException, InterruptedException { | ||
119 | List<String> drealCmd = new ArrayList<String>( | ||
120 | Arrays.asList("docker", "exec", | ||
121 | containerName, | ||
122 | "dreal", | ||
123 | "--model", | ||
124 | "mnt/" + tempFile.getName())); | ||
125 | return runProcess(drealCmd); | ||
126 | } | ||
127 | |||
128 | public boolean getDrealResult(Process p) throws IOException { | ||
129 | if (p.exitValue() == 1) {return false;} | ||
130 | |||
131 | BufferedReader output = new BufferedReader(new InputStreamReader(p.getInputStream())); | ||
132 | |||
133 | String resultRaw = output.readLine(); | ||
134 | if (resultRaw.startsWith("unsat")) {return false;} | ||
135 | if (resultRaw.startsWith("delta-sat")) {return true;} | ||
136 | throw new IOException("Unknown dreal output first line"); | ||
137 | //TODO make the above better | ||
138 | } | ||
139 | |||
140 | public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | ||
141 | long startformingProblem = System.nanoTime(); | ||
142 | //CREATE DREAL STM2 FILE | ||
143 | //TODO | ||
144 | |||
145 | printer.close(); | ||
146 | endformingProblem = System.nanoTime()-startformingProblem; | ||
147 | long startSolvingProblem = System.nanoTime(); | ||
148 | //CALL DREAL | ||
149 | Process outputProcess = callDreal(); | ||
150 | boolean result = getDrealResult(outputProcess); | ||
151 | endSolvingProblem = System.nanoTime()-startSolvingProblem; | ||
152 | //CLOSE | ||
153 | return result; | ||
154 | } | ||
155 | |||
156 | public Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | ||
157 | // Map<PrimitiveElement,Number> sol = new HashMap<PrimitiveElement, Number>(); | ||
158 | // long startformingProblem = System.nanoTime(); | ||
159 | // BoolExpr problemInstance = formNumericProblemInstance(matches); | ||
160 | // endformingProblem = System.nanoTime()-startformingProblem; | ||
161 | // //System.out.println("Forming problem: " + (endformingProblem - startformingProblem)); | ||
162 | // s.add(problemInstance); | ||
163 | // long startSolvingProblem = System.nanoTime(); | ||
164 | // if (s.check() == Status.SATISFIABLE) { | ||
165 | // Model m = s.getModel(); | ||
166 | // endSolvingProblem = System.nanoTime()-startSolvingProblem; | ||
167 | // //System.out.println("Solving problem: " + (endSolvingProblem - startSolvingProblem)); | ||
168 | // long startFormingSolution = System.nanoTime(); | ||
169 | // for (PrimitiveElement o: objs) { | ||
170 | // if(varMap.containsKey(o)) { | ||
171 | // if (o instanceof IntegerElement) { | ||
172 | // IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false); | ||
173 | // Integer oSol = Integer.parseInt(val.toString()); | ||
174 | // sol.put(o, oSol); | ||
175 | // } else { | ||
176 | // RealExpr val = (RealExpr) m.evaluate(varMap.get(o), false); | ||
177 | // Double oSol = Double.parseDouble(val.toString()); | ||
178 | // sol.put(o, oSol); | ||
179 | // } | ||
180 | // //System.out.println("Solution:" + o + "->" + oSol); | ||
181 | // | ||
182 | // } else { | ||
183 | // //System.out.println("not used var:" + o); | ||
184 | // } | ||
185 | // } | ||
186 | // endFormingSolution = System.nanoTime()-startFormingSolution; | ||
187 | // //System.out.println("Forming solution: " + (endFormingSolution - startFormingSolution)); | ||
188 | // } else { | ||
189 | // System.out.println("Unsatisfiable numerical problem"); | ||
190 | // } | ||
191 | // this.ctx.close(); | ||
192 | // return sol; | ||
193 | return null; | ||
194 | } | ||
195 | // | ||
196 | // private BoolExpr formNumericConstraint(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception { | ||
197 | // if (!(e instanceof XBinaryOperation)) { | ||
198 | // throw new Exception ("error in check expression!!!"); | ||
199 | // } | ||
200 | // | ||
201 | // String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); | ||
202 | // | ||
203 | // BoolExpr constraint = null; | ||
204 | // | ||
205 | // ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); | ||
206 | // ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); | ||
207 | // | ||
208 | // if (nameEndsWith(name, N_LESSTHAN)) { | ||
209 | // constraint = ctx.mkLt(left_operand, right_operand); | ||
210 | // } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) { | ||
211 | // constraint = ctx.mkLe(left_operand, right_operand); | ||
212 | // } else if (nameEndsWith(name, N_GREATERTHAN)) { | ||
213 | // constraint = ctx.mkGt(left_operand, right_operand); | ||
214 | // } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) { | ||
215 | // constraint = ctx.mkGe(left_operand, right_operand); | ||
216 | // } else if (nameEndsWith(name, N_EQUALS)) { | ||
217 | // constraint = ctx.mkEq(left_operand, right_operand); | ||
218 | // } else if (nameEndsWith(name, N_NOTEQUALS)) { | ||
219 | // constraint = ctx.mkDistinct(left_operand, right_operand); | ||
220 | // } else if (nameEndsWith(name, N_EQUALS3)) { | ||
221 | // constraint = ctx.mkGe(left_operand, right_operand); // ??? | ||
222 | // } else if (nameEndsWith(name, N_NOTEQUALS3)) { | ||
223 | // constraint = ctx.mkGe(left_operand, right_operand); // ??? | ||
224 | // } else { | ||
225 | // throw new Exception ("Unsupported binary operation " + name); | ||
226 | // } | ||
227 | // | ||
228 | // return constraint; | ||
229 | // } | ||
230 | // | ||
231 | // private ArithExpr formNumericConstraintHelper(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception { | ||
232 | // ArithExpr expr = null; | ||
233 | // // Variables | ||
234 | // if (e instanceof XFeatureCall) { | ||
235 | // PrimitiveElement matchedObj = aMatch.get(((XFeatureCall) e).getFeature()); | ||
236 | // boolean isInt = matchedObj instanceof IntegerElement; | ||
237 | // if (!matchedObj.isValueSet()) { | ||
238 | // if (varMap.get(matchedObj) == null) { | ||
239 | // String var_name = ((XFeatureCall) e).getFeature().getQualifiedName() + matchedObj.toString(); | ||
240 | // if (isInt) { | ||
241 | // expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort()); | ||
242 | // } else { | ||
243 | // expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getRealSort()); | ||
244 | // } | ||
245 | // varMap.put(matchedObj, expr); | ||
246 | // } else { | ||
247 | // expr = (ArithExpr) varMap.get(matchedObj); | ||
248 | // } | ||
249 | // } else { | ||
250 | // if (isInt) { | ||
251 | // int value = ((IntegerElement) matchedObj).getValue(); | ||
252 | // expr = (ArithExpr) ctx.mkInt(value); | ||
253 | // } else { | ||
254 | // double value = ((RealElement) matchedObj).getValue().doubleValue(); | ||
255 | // expr = (ArithExpr) ctx.mkReal(String.valueOf(value)); | ||
256 | // } | ||
257 | // varMap.put(matchedObj, expr); | ||
258 | // } | ||
259 | // } | ||
260 | // // Constants | ||
261 | // else if (e instanceof XNumberLiteral) { | ||
262 | // String value = ((XNumberLiteral) e).getValue(); | ||
263 | // try{ | ||
264 | // int val = Integer.parseInt(value); | ||
265 | // expr = (ArithExpr) ctx.mkInt(val); | ||
266 | // } catch(NumberFormatException err){ | ||
267 | // try{ | ||
268 | // expr = (ArithExpr) ctx.mkReal(value); | ||
269 | // } catch(NumberFormatException err2){} | ||
270 | // } | ||
271 | // } | ||
272 | // // Expressions with operators | ||
273 | // else if (e instanceof XBinaryOperation) { | ||
274 | // String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); | ||
275 | // ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); | ||
276 | // ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); | ||
277 | // | ||
278 | // if (nameEndsWith(name, N_PLUS)) { | ||
279 | // expr = ctx.mkAdd(left_operand, right_operand); | ||
280 | // } else if (nameEndsWith(name, N_MINUS)) { | ||
281 | // expr = ctx.mkAdd(left_operand, ctx.mkUnaryMinus(right_operand)); | ||
282 | // } else if (nameEndsWith(name, N_POWER)) { | ||
283 | // expr = ctx.mkPower(left_operand, right_operand); | ||
284 | // } else if (nameEndsWith(name, N_MULTIPLY)) { | ||
285 | // expr = ctx.mkMul(left_operand, right_operand); | ||
286 | // } else if (nameEndsWith(name, N_DIVIDE)) { | ||
287 | // expr = ctx.mkDiv(left_operand, right_operand); | ||
288 | // } else if (nameEndsWith(name, N_MODULO)) { | ||
289 | // expr = ctx.mkMod((IntExpr)left_operand, (IntExpr)right_operand); | ||
290 | // } else { | ||
291 | // throw new Exception ("Unsupported binary operation " + name); | ||
292 | // } | ||
293 | // } else { | ||
294 | // throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); | ||
295 | // } | ||
296 | // return expr; | ||
297 | // | ||
298 | // } | ||
299 | // | ||
300 | // private boolean nameEndsWith(String name, String end) { | ||
301 | // return name.startsWith(N_Base) && name.endsWith(end); | ||
302 | // } | ||
303 | // | ||
304 | // private BoolExpr formNumericProblemInstance(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | ||
305 | // BoolExpr constraintInstances = ctx.mkTrue(); | ||
306 | // for (XExpression e: matches.keySet()) { | ||
307 | // Iterable<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e); | ||
308 | // for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) { | ||
309 | // BoolExpr constraintInstance = ctx.mkNot(formNumericConstraint(e, aMatch)); | ||
310 | // constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance); | ||
311 | // } | ||
312 | // } | ||
313 | // return constraintInstances; | ||
314 | // } | ||
315 | } | ||
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 index b9eda7b3..21fbe589 100644 --- 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 | |||
@@ -50,9 +50,14 @@ class NumericTranslator { | |||
50 | return res | 50 | return res |
51 | } | 51 | } |
52 | 52 | ||
53 | def selectProblemSolver() { | ||
54 | // return new NumericProblemSolver | ||
55 | return new DrealProblemSolver | ||
56 | } | ||
57 | |||
53 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) { | 58 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) { |
54 | val input = formNumericProblemInstance(matches) | 59 | val input = formNumericProblemInstance(matches) |
55 | val solver = new NumericProblemSolver | 60 | val solver = selectProblemSolver |
56 | val satisfiability = solver.isSatisfiable(input) | 61 | val satisfiability = solver.isSatisfiable(input) |
57 | solver.updateTimes | 62 | solver.updateTimes |
58 | return satisfiability | 63 | return satisfiability |
@@ -60,13 +65,13 @@ class NumericTranslator { | |||
60 | 65 | ||
61 | def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches) { | 66 | def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches) { |
62 | val input = formNumericProblemInstance(matches) | 67 | val input = formNumericProblemInstance(matches) |
63 | val solver = new NumericProblemSolver | 68 | val solver = selectProblemSolver |
64 | val solution = solver.getOneSolution(primitiveElements,input) | 69 | val solution = solver.getOneSolution(primitiveElements,input) |
65 | solver.updateTimes | 70 | solver.updateTimes |
66 | return solution | 71 | return solution |
67 | } | 72 | } |
68 | 73 | ||
69 | private def updateTimes(NumericProblemSolver s) { | 74 | private def updateTimes(DrealProblemSolver s) { |
70 | this.formingProblemTime += s.getEndformingProblem | 75 | this.formingProblemTime += s.getEndformingProblem |
71 | this.solvingProblemTime += s.getEndSolvingProblem | 76 | this.solvingProblemTime += s.getEndSolvingProblem |
72 | this.formingSolutionTime += s.getEndFormingSolution | 77 | this.formingSolutionTime += s.getEndFormingSolution |