aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2020-12-13 00:53:36 -0500
committerLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2020-12-13 00:53:36 -0500
commit8c2930129730fd2319902c29f873f6ced33fd0d6 (patch)
treecdc29c36d4b724f6c0f3819a26b5851cbd45d945
parentremove auto-generated files and fix gitignores (diff)
downloadVIATRA-Generator-8c2930129730fd2319902c29f873f6ced33fd0d6.tar.gz
VIATRA-Generator-8c2930129730fd2319902c29f873f6ced33fd0d6.tar.zst
VIATRA-Generator-8c2930129730fd2319902c29f873f6ced33fd0d6.zip
implement setup for dreal calls
Diffstat
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/DrealProblemSolver.java315
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend11
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 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic;
2
3import java.io.BufferedReader;
4import java.io.File;
5import java.io.IOException;
6import java.io.InputStream;
7import java.io.InputStreamReader;
8import java.io.PrintWriter;
9import java.util.ArrayList;
10import java.util.Arrays;
11import java.util.HashMap;
12import java.util.List;
13import java.util.Map;
14import java.util.UUID;
15
16import org.eclipse.xtext.common.types.JvmIdentifiableElement;
17import org.eclipse.xtext.xbase.XExpression;
18
19import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement;
20
21public 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
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-05 22:57:49 +0000