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