diff options
author | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2020-12-14 03:27:43 -0500 |
---|---|---|
committer | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-01-06 00:02:49 +0100 |
commit | 8fd50f7d4a979117a1e643f5384b76f4a3e36801 (patch) | |
tree | a5bb21af9c982f18bd216b1f9c98f9548169a2e2 /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner | |
parent | add numericProblemSolver supertype (diff) | |
download | VIATRA-Generator-8fd50f7d4a979117a1e643f5384b76f4a3e36801.tar.gz VIATRA-Generator-8fd50f7d4a979117a1e643f5384b76f4a3e36801.tar.zst VIATRA-Generator-8fd50f7d4a979117a1e643f5384b76f4a3e36801.zip |
implement isSatisfiable with Dreal integration
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner')
4 files changed, 252 insertions, 211 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java index 1e5742b7..9b9136c7 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java | |||
@@ -1,7 +1,10 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; | 1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; |
2 | 2 | ||
3 | import java.io.BufferedInputStream; | ||
3 | import java.io.BufferedReader; | 4 | import java.io.BufferedReader; |
4 | import java.io.File; | 5 | import java.io.File; |
6 | import java.io.FileInputStream; | ||
7 | import java.io.FileNotFoundException; | ||
5 | import java.io.IOException; | 8 | import java.io.IOException; |
6 | import java.io.InputStream; | 9 | import java.io.InputStream; |
7 | import java.io.InputStreamReader; | 10 | import java.io.InputStreamReader; |
@@ -12,55 +15,37 @@ import java.util.HashMap; | |||
12 | import java.util.List; | 15 | import java.util.List; |
13 | import java.util.Map; | 16 | import java.util.Map; |
14 | import java.util.UUID; | 17 | import java.util.UUID; |
18 | import java.util.concurrent.TimeUnit; | ||
15 | 19 | ||
16 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; | 20 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; |
21 | import org.eclipse.xtext.xbase.XBinaryOperation; | ||
17 | import org.eclipse.xtext.xbase.XExpression; | 22 | import org.eclipse.xtext.xbase.XExpression; |
23 | import org.eclipse.xtext.xbase.XFeatureCall; | ||
24 | import org.eclipse.xtext.xbase.XNumberLiteral; | ||
18 | 25 | ||
26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | 27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; |
28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; | ||
20 | 29 | ||
21 | public class NumericDrealProblemSolver extends NumericProblemSolver{ | 30 | public class NumericDrealProblemSolver extends NumericProblemSolver{ |
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 | 31 | ||
38 | private File tempFile; | 32 | private final String containerName; |
39 | private PrintWriter printer; | ||
40 | private String containerName; | ||
41 | private Map<Object, String> varMap; | 33 | private Map<Object, String> varMap; |
34 | private List<String> curVars; | ||
42 | 35 | ||
43 | public NumericDrealProblemSolver() throws IOException, InterruptedException { | 36 | public NumericDrealProblemSolver() throws IOException, InterruptedException { |
44 | //setup smt2 input file | ||
45 | tempFile = File.createTempFile("smt", ".smt2"); | ||
46 | printer = new PrintWriter(tempFile); | ||
47 | printer.println(";Header comment"); | ||
48 | printer.println("(set-logic QF_NRA)"); | ||
49 | |||
50 | //setup docker | 37 | //setup docker |
51 | File parentPath = tempFile.getParentFile(); | 38 | //TODO ENSURE that container name is not already in use???? |
52 | System.out.println(parentPath); | 39 | File tempDir = new File(System.getProperty("java.io.tmpdir")); |
53 | System.out.println(tempFile); | ||
54 | //TODO ENSURE that container name is not already in use | ||
55 | containerName = UUID.randomUUID().toString().replace("-", ""); | 40 | containerName = UUID.randomUUID().toString().replace("-", ""); |
56 | List<String> startDocker = new ArrayList<String>( | 41 | List<String> startDocker = new ArrayList<String>( |
57 | Arrays.asList("docker", "run", | 42 | Arrays.asList("docker", "run", |
58 | "-id", "--rm", | 43 | "-id", "--rm", |
59 | "--name", containerName, | 44 | "--name", containerName, |
60 | "-p", "8080:80", | 45 | // "-p", "8080:80", |
61 | "-v", parentPath + ":/mnt", | 46 | "-v", tempDir + ":/mnt", |
62 | "dreal/dreal4")); | 47 | "dreal/dreal4")); |
63 | Process p = runProcess(startDocker); | 48 | Process p = runProcess(startDocker); |
64 | 49 | ||
65 | //setup varmap | 50 | //setup varmap |
66 | varMap = new HashMap<Object, String>(); | 51 | varMap = new HashMap<Object, String>(); |
@@ -69,70 +54,235 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
69 | private Process runProcess(List<String> cmd) throws IOException, InterruptedException { | 54 | private Process runProcess(List<String> cmd) throws IOException, InterruptedException { |
70 | // println(cmd) | 55 | // println(cmd) |
71 | ProcessBuilder pb = new ProcessBuilder(cmd); | 56 | ProcessBuilder pb = new ProcessBuilder(cmd); |
72 | pb.redirectOutput(); | ||
73 | pb.redirectError(); | ||
74 | Process p = pb.start(); | 57 | Process p = pb.start(); |
75 | p.waitFor(); | 58 | // p.waitFor(); |
76 | //TODO timeout if needed | 59 | //TODO timeout if needed |
77 | // if (!p.waitFor(TIMEOUT, TimeUnit.SECONDS)) { | 60 | if (!p.waitFor(5, TimeUnit.SECONDS)) { |
78 | // p.destroy(); | 61 | p.destroy(); |
79 | // } | 62 | } |
80 | return p; | 63 | return p; |
81 | } | 64 | } |
82 | |||
83 | // | ||
84 | // private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) { | ||
85 | // ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); | ||
86 | // XExpression left = ((XBinaryOperation) expression).getLeftOperand(); | ||
87 | // XExpression right = ((XBinaryOperation) expression).getRightOperand(); | ||
88 | // | ||
89 | // getJvmIdentifiableElementsHelper(left, allElem); | ||
90 | // getJvmIdentifiableElementsHelper(right, allElem); | ||
91 | // return allElem; | ||
92 | // } | ||
93 | // | ||
94 | // private void getJvmIdentifiableElementsHelper(XExpression e, List<JvmIdentifiableElement> allElem) { | ||
95 | // if (e instanceof XFeatureCall) { | ||
96 | // allElem.add(((XFeatureCall) e).getFeature()); | ||
97 | // } else if (e instanceof XBinaryOperation) { | ||
98 | // getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getLeftOperand(), allElem); | ||
99 | // getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem); | ||
100 | // } | ||
101 | // } | ||
102 | 65 | ||
103 | private Process callDreal() throws IOException, InterruptedException { | 66 | private Process callDreal(String tempFileName) throws IOException, InterruptedException { |
104 | List<String> drealCmd = new ArrayList<String>( | 67 | List<String> drealCmd = new ArrayList<String>( |
105 | Arrays.asList("docker", "exec", | 68 | Arrays.asList("docker", "exec", |
106 | containerName, | 69 | containerName, |
107 | "dreal", | 70 | "dreal", |
108 | "--model", | 71 | "--model", |
109 | "mnt/" + tempFile.getName())); | 72 | "mnt/" + tempFileName)); |
110 | return runProcess(drealCmd); | 73 | return runProcess(drealCmd); |
111 | } | 74 | } |
112 | 75 | ||
113 | private boolean getDrealResult(Process p) throws IOException { | 76 | private List<String> getDrealStream(InputStream stream) throws IOException { |
114 | if (p.exitValue() == 1) {return false;} | 77 | List<String> output = new ArrayList<String>(); |
78 | BufferedReader r = new BufferedReader(new InputStreamReader(stream)); | ||
115 | 79 | ||
116 | BufferedReader output = new BufferedReader(new InputStreamReader(p.getInputStream())); | 80 | String rl = ""; |
81 | while ((rl = r.readLine()) != null) {output.add(rl);} | ||
82 | return output; | ||
83 | } | ||
84 | |||
85 | private List<List<String>> getProcessOutput(Process p) throws IOException { | ||
86 | List<List<String>> outputs = new ArrayList<List<String>>(); | ||
87 | outputs.add(getDrealStream(p.getInputStream())); | ||
88 | outputs.add(getDrealStream(p.getErrorStream())); | ||
89 | return outputs; | ||
90 | } | ||
91 | |||
92 | private boolean getDrealResult(int exitVal, List<List<String>> outputs) throws IOException { | ||
93 | //error at process-level | ||
94 | if (exitVal == 1) {printError(outputs.get(1)); return false;} | ||
95 | |||
96 | //error at dreal-level | ||
97 | if (! outputs.get(1).isEmpty()) {printError(outputs.get(1)); return false;} | ||
117 | 98 | ||
118 | String resultRaw = output.readLine(); | 99 | //print output |
100 | // printOutput(outputs.get(0)); | ||
101 | |||
102 | String resultRaw = outputs.get(0).get(0); | ||
119 | if (resultRaw.startsWith("unsat")) {return false;} | 103 | if (resultRaw.startsWith("unsat")) {return false;} |
120 | if (resultRaw.startsWith("delta-sat")) {return true;} | 104 | if (resultRaw.startsWith("delta-sat")) {return true;} |
121 | throw new IOException("Unknown dreal output first line"); | 105 | throw new IOException("Unknown dreal output first line"); |
122 | //TODO make the above better | 106 | //TODO make the above better |
107 | } | ||
108 | |||
109 | private String formNumericConstraint(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception { | ||
110 | //The check equation MUST be a binary operation | ||
111 | if (!(e instanceof XBinaryOperation)) { | ||
112 | throw new Exception ("error in check expression!!!"); | ||
113 | } | ||
114 | |||
115 | String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); | ||
116 | |||
117 | String operator = ""; | ||
118 | |||
119 | String left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); | ||
120 | String right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); | ||
121 | |||
122 | if (nameEndsWith(name, N_LESSTHAN)) { | ||
123 | operator = "<"; | ||
124 | } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) { | ||
125 | operator = "<="; | ||
126 | } else if (nameEndsWith(name, N_GREATERTHAN)) { | ||
127 | operator = ">"; | ||
128 | } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) { | ||
129 | operator = ">="; | ||
130 | } else if (nameEndsWith(name, N_EQUALS)) { | ||
131 | operator = "<"; | ||
132 | } else if (nameEndsWith(name, N_NOTEQUALS)) { | ||
133 | //Exceptional case | ||
134 | return "(not (=" + " " + left_operand + " " + right_operand + "))"; | ||
135 | // } else if (nameEndsWith(name, N_EQUALS3)) { | ||
136 | // operator = "<"; | ||
137 | // } else if (nameEndsWith(name, N_NOTEQUALS3)) { | ||
138 | // operator = "<"; | ||
139 | } else { | ||
140 | throw new Exception ("Unsupported binary operation " + name); | ||
141 | } | ||
142 | |||
143 | return "(" + operator + " " + left_operand + " " + right_operand + ")"; | ||
144 | } | ||
145 | |||
146 | private String formNumericConstraintHelper(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception { | ||
147 | String expr = ""; | ||
148 | // Variables | ||
149 | if (e instanceof XFeatureCall) { | ||
150 | PrimitiveElement matchedObj = aMatch.get(((XFeatureCall) e).getFeature()); | ||
151 | boolean isInt = matchedObj instanceof IntegerElement; | ||
152 | if (!matchedObj.isValueSet()) { | ||
153 | if (varMap.get(matchedObj) == null) { | ||
154 | expr = ((XFeatureCall) e).getFeature().getQualifiedName() + matchedObj.hashCode(); //TODO ISSUE | ||
155 | varMap.put(matchedObj, expr); | ||
156 | } else { | ||
157 | expr = varMap.get(matchedObj); | ||
158 | } | ||
159 | } else { | ||
160 | //TODO unsure what it means if something gets in here | ||
161 | if (isInt) { | ||
162 | expr = Integer.toString(((IntegerElement) matchedObj).getValue()); | ||
163 | } else { | ||
164 | expr = Double.toString(((RealElement) matchedObj).getValue().doubleValue()); | ||
165 | } | ||
166 | varMap.put(matchedObj, expr); | ||
167 | } | ||
168 | //Add variable declarations | ||
169 | if(! curVars.contains(expr)) { | ||
170 | String varDecl = "(declare-fun " + expr + " () "; | ||
171 | if (isInt) {varDecl += "Int)";} | ||
172 | else {varDecl += "Real)";} | ||
173 | curVars.add(varDecl); | ||
174 | } | ||
175 | } | ||
176 | // Constants | ||
177 | else if (e instanceof XNumberLiteral) { | ||
178 | //we do not care if it is an int or a real. | ||
179 | //We actually do not even check f the value parses into a number | ||
180 | expr = ((XNumberLiteral) e).getValue(); | ||
181 | //TODO ensure that the value is a valid number | ||
182 | // expr = Integer.parseInt(value) | ||
183 | } | ||
184 | // Expressions with operators | ||
185 | else if (e instanceof XBinaryOperation) { | ||
186 | String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); | ||
187 | String left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); | ||
188 | String right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); | ||
189 | |||
190 | String operator = ""; | ||
191 | if (nameEndsWith(name, N_PLUS)) { | ||
192 | operator = "+"; | ||
193 | } else if (nameEndsWith(name, N_MINUS)) { | ||
194 | operator = "-"; | ||
195 | } else if (nameEndsWith(name, N_POWER)) { | ||
196 | operator = "^"; | ||
197 | } else if (nameEndsWith(name, N_MULTIPLY)) { | ||
198 | operator = "*"; | ||
199 | } else if (nameEndsWith(name, N_DIVIDE)) { | ||
200 | operator = "/"; | ||
201 | // } else if (nameEndsWith(name, N_MODULO)) { | ||
202 | // expr = ctx.mkMod((IntExpr)left_operand, (IntExpr)right_operand); | ||
203 | } else { | ||
204 | throw new Exception ("Unsupported binary operation " + name); | ||
205 | } | ||
206 | |||
207 | expr = "(" + operator + " " + left_operand + " " + right_operand + ")"; | ||
208 | } else { | ||
209 | throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); | ||
210 | } | ||
211 | return expr; | ||
212 | |||
213 | } | ||
214 | |||
215 | private boolean nameEndsWith(String name, String end) { | ||
216 | return name.startsWith(N_Base) && name.endsWith(end); | ||
217 | } | ||
218 | |||
219 | private String formNumericProblemInstance(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | ||
220 | //CREATE SMT2 TEMP FILE | ||
221 | File tempFile = File.createTempFile("smt", ".smt2"); | ||
222 | String tempFileName = tempFile.getName(); | ||
223 | |||
224 | //STM2 FILE CONTENT CREATION | ||
225 | curVars = new ArrayList<String>(); | ||
226 | List<String> curConstraints = new ArrayList<String>(); | ||
227 | |||
228 | PrintWriter printer = new PrintWriter(tempFile); | ||
229 | printer.println(";Header comment"); | ||
230 | printer.println("(set-logic QF_NRA)"); | ||
231 | for (XExpression e: matches.keySet()) { | ||
232 | Iterable<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e); | ||
233 | for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) { | ||
234 | String constraint = formNumericConstraint(e, aMatch); | ||
235 | String negAssert = "(assert (not " + constraint + "))"; | ||
236 | curConstraints.add(negAssert); | ||
237 | } | ||
238 | } | ||
239 | //Add Content to SMT2 file | ||
240 | for (String varDecl : curVars) {printer.println(varDecl);} | ||
241 | for (String negAssert : curConstraints) {printer.println(negAssert);} | ||
242 | printer.println("(check-sat)"); | ||
243 | printer.close(); | ||
244 | return tempFileName; | ||
245 | } | ||
246 | |||
247 | private void printFileContent(String path) throws IOException { | ||
248 | InputStream input = new BufferedInputStream(new FileInputStream(path)); | ||
249 | byte[] buffer = new byte[8192]; | ||
250 | |||
251 | try { | ||
252 | for (int length = 0; (length = input.read(buffer)) != -1;) { | ||
253 | System.out.write(buffer, 0, length); | ||
254 | } | ||
255 | } finally { | ||
256 | input.close(); | ||
257 | } | ||
258 | } | ||
259 | |||
260 | private void printOutput(List<String> list) { | ||
261 | for (String line : list) { | ||
262 | System.out.println(line); | ||
263 | } | ||
264 | } | ||
265 | |||
266 | private void printError(List<String> list) { | ||
267 | for (String line : list) { | ||
268 | System.err.println(line); | ||
269 | } | ||
123 | } | 270 | } |
124 | 271 | ||
125 | public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | 272 | public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { |
273 | //CREATE DREAL STM2 FILE at this.tempfile location | ||
126 | long startformingProblem = System.nanoTime(); | 274 | long startformingProblem = System.nanoTime(); |
127 | //CREATE DREAL STM2 FILE | 275 | String tempFileName = formNumericProblemInstance(matches); |
128 | //TODO | ||
129 | |||
130 | printer.close(); | ||
131 | endformingProblem = System.nanoTime()-startformingProblem; | 276 | endformingProblem = System.nanoTime()-startformingProblem; |
277 | |||
278 | // printFileContent(System.getProperty("java.io.tmpdir") + tempFileName); | ||
279 | |||
280 | //CALL DREAL | ||
132 | long startSolvingProblem = System.nanoTime(); | 281 | long startSolvingProblem = System.nanoTime(); |
133 | //CALL DREAL | 282 | Process outputProcess = callDreal(tempFileName); |
134 | Process outputProcess = callDreal(); | 283 | List<List<String>> outputs = getProcessOutput(outputProcess); |
135 | boolean result = getDrealResult(outputProcess); | 284 | boolean result = getDrealResult(outputProcess.exitValue(), outputs); |
285 | System.out.println(result); | ||
136 | endSolvingProblem = System.nanoTime()-startSolvingProblem; | 286 | endSolvingProblem = System.nanoTime()-startSolvingProblem; |
137 | //CLOSE | 287 | //CLOSE |
138 | return result; | 288 | return result; |
@@ -177,124 +327,12 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
177 | // return sol; | 327 | // return sol; |
178 | return null; | 328 | return null; |
179 | } | 329 | } |
180 | // | 330 | |
181 | // private BoolExpr formNumericConstraint(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception { | 331 | public void teardown() throws IOException, InterruptedException { |
182 | // if (!(e instanceof XBinaryOperation)) { | 332 | List<String> stopDocker = new ArrayList<String>( |
183 | // throw new Exception ("error in check expression!!!"); | 333 | Arrays.asList("docker", "stop", containerName)); |
184 | // } | 334 | runProcess(stopDocker); |
185 | // | 335 | //TODO Check if above went well? |
186 | // String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); | 336 | } |
187 | // | 337 | |
188 | // BoolExpr constraint = null; | ||
189 | // | ||
190 | // ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); | ||
191 | // ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); | ||
192 | // | ||
193 | // if (nameEndsWith(name, N_LESSTHAN)) { | ||
194 | // constraint = ctx.mkLt(left_operand, right_operand); | ||
195 | // } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) { | ||
196 | // constraint = ctx.mkLe(left_operand, right_operand); | ||
197 | // } else if (nameEndsWith(name, N_GREATERTHAN)) { | ||
198 | // constraint = ctx.mkGt(left_operand, right_operand); | ||
199 | // } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) { | ||
200 | // constraint = ctx.mkGe(left_operand, right_operand); | ||
201 | // } else if (nameEndsWith(name, N_EQUALS)) { | ||
202 | // constraint = ctx.mkEq(left_operand, right_operand); | ||
203 | // } else if (nameEndsWith(name, N_NOTEQUALS)) { | ||
204 | // constraint = ctx.mkDistinct(left_operand, right_operand); | ||
205 | // } else if (nameEndsWith(name, N_EQUALS3)) { | ||
206 | // constraint = ctx.mkGe(left_operand, right_operand); // ??? | ||
207 | // } else if (nameEndsWith(name, N_NOTEQUALS3)) { | ||
208 | // constraint = ctx.mkGe(left_operand, right_operand); // ??? | ||
209 | // } else { | ||
210 | // throw new Exception ("Unsupported binary operation " + name); | ||
211 | // } | ||
212 | // | ||
213 | // return constraint; | ||
214 | // } | ||
215 | // | ||
216 | // private ArithExpr formNumericConstraintHelper(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception { | ||
217 | // ArithExpr expr = null; | ||
218 | // // Variables | ||
219 | // if (e instanceof XFeatureCall) { | ||
220 | // PrimitiveElement matchedObj = aMatch.get(((XFeatureCall) e).getFeature()); | ||
221 | // boolean isInt = matchedObj instanceof IntegerElement; | ||
222 | // if (!matchedObj.isValueSet()) { | ||
223 | // if (varMap.get(matchedObj) == null) { | ||
224 | // String var_name = ((XFeatureCall) e).getFeature().getQualifiedName() + matchedObj.toString(); | ||
225 | // if (isInt) { | ||
226 | // expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort()); | ||
227 | // } else { | ||
228 | // expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getRealSort()); | ||
229 | // } | ||
230 | // varMap.put(matchedObj, expr); | ||
231 | // } else { | ||
232 | // expr = (ArithExpr) varMap.get(matchedObj); | ||
233 | // } | ||
234 | // } else { | ||
235 | // if (isInt) { | ||
236 | // int value = ((IntegerElement) matchedObj).getValue(); | ||
237 | // expr = (ArithExpr) ctx.mkInt(value); | ||
238 | // } else { | ||
239 | // double value = ((RealElement) matchedObj).getValue().doubleValue(); | ||
240 | // expr = (ArithExpr) ctx.mkReal(String.valueOf(value)); | ||
241 | // } | ||
242 | // varMap.put(matchedObj, expr); | ||
243 | // } | ||
244 | // } | ||
245 | // // Constants | ||
246 | // else if (e instanceof XNumberLiteral) { | ||
247 | // String value = ((XNumberLiteral) e).getValue(); | ||
248 | // try{ | ||
249 | // int val = Integer.parseInt(value); | ||
250 | // expr = (ArithExpr) ctx.mkInt(val); | ||
251 | // } catch(NumberFormatException err){ | ||
252 | // try{ | ||
253 | // expr = (ArithExpr) ctx.mkReal(value); | ||
254 | // } catch(NumberFormatException err2){} | ||
255 | // } | ||
256 | // } | ||
257 | // // Expressions with operators | ||
258 | // else if (e instanceof XBinaryOperation) { | ||
259 | // String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); | ||
260 | // ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); | ||
261 | // ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); | ||
262 | // | ||
263 | // if (nameEndsWith(name, N_PLUS)) { | ||
264 | // expr = ctx.mkAdd(left_operand, right_operand); | ||
265 | // } else if (nameEndsWith(name, N_MINUS)) { | ||
266 | // expr = ctx.mkAdd(left_operand, ctx.mkUnaryMinus(right_operand)); | ||
267 | // } else if (nameEndsWith(name, N_POWER)) { | ||
268 | // expr = ctx.mkPower(left_operand, right_operand); | ||
269 | // } else if (nameEndsWith(name, N_MULTIPLY)) { | ||
270 | // expr = ctx.mkMul(left_operand, right_operand); | ||
271 | // } else if (nameEndsWith(name, N_DIVIDE)) { | ||
272 | // expr = ctx.mkDiv(left_operand, right_operand); | ||
273 | // } else if (nameEndsWith(name, N_MODULO)) { | ||
274 | // expr = ctx.mkMod((IntExpr)left_operand, (IntExpr)right_operand); | ||
275 | // } else { | ||
276 | // throw new Exception ("Unsupported binary operation " + name); | ||
277 | // } | ||
278 | // } else { | ||
279 | // throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); | ||
280 | // } | ||
281 | // return expr; | ||
282 | // | ||
283 | // } | ||
284 | // | ||
285 | // private boolean nameEndsWith(String name, String end) { | ||
286 | // return name.startsWith(N_Base) && name.endsWith(end); | ||
287 | // } | ||
288 | // | ||
289 | // private BoolExpr formNumericProblemInstance(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | ||
290 | // BoolExpr constraintInstances = ctx.mkTrue(); | ||
291 | // for (XExpression e: matches.keySet()) { | ||
292 | // Iterable<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e); | ||
293 | // for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) { | ||
294 | // BoolExpr constraintInstance = ctx.mkNot(formNumericConstraint(e, aMatch)); | ||
295 | // constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance); | ||
296 | // } | ||
297 | // } | ||
298 | // return constraintInstances; | ||
299 | // } | ||
300 | } | 338 | } |
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 d818ec91..5e823d9d 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 | |||
@@ -6,13 +6,30 @@ import java.util.Map; | |||
6 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; | 6 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; |
7 | import org.eclipse.xtext.xbase.XExpression; | 7 | import org.eclipse.xtext.xbase.XExpression; |
8 | 8 | ||
9 | import com.microsoft.z3.Expr; | ||
10 | |||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; |
10 | 12 | ||
11 | public abstract class NumericProblemSolver { | 13 | public abstract class NumericProblemSolver { |
14 | protected static final String N_Base = "org.eclipse.xtext.xbase.lib."; | ||
15 | protected static final String N_PLUS = "operator_plus"; | ||
16 | protected static final String N_MINUS = "operator_minus"; | ||
17 | protected static final String N_POWER = "operator_power"; | ||
18 | protected static final String N_MULTIPLY = "operator_multiply"; | ||
19 | protected static final String N_DIVIDE = "operator_divide"; | ||
20 | protected static final String N_MODULO = "operator_modulo"; | ||
21 | protected static final String N_LESSTHAN = "operator_lessThan"; | ||
22 | protected static final String N_LESSEQUALSTHAN = "operator_lessEqualsThan"; | ||
23 | protected static final String N_GREATERTHAN = "operator_greaterThan"; | ||
24 | protected static final String N_GREATEREQUALTHAN = "operator_greaterEqualsThan"; | ||
25 | protected static final String N_EQUALS = "operator_equals"; | ||
26 | protected static final String N_NOTEQUALS = "operator_notEquals"; | ||
27 | protected static final String N_EQUALS3 = "operator_tripleEquals"; | ||
28 | protected static final String N_NOTEQUALS3 = "operator_tripleNotEquals"; | ||
12 | 29 | ||
13 | long endformingProblem=0; | 30 | protected long endformingProblem=0; |
14 | long endSolvingProblem=0; | 31 | protected long endSolvingProblem=0; |
15 | long endFormingSolution=0; | 32 | protected long endFormingSolution=0; |
16 | 33 | ||
17 | public long getEndformingProblem() {return endformingProblem;} | 34 | public long getEndformingProblem() {return endformingProblem;} |
18 | public long getEndSolvingProblem() {return endSolvingProblem;} | 35 | public long getEndSolvingProblem() {return endSolvingProblem;} |
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 d63604b0..22ea41bf 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 | |||
@@ -16,6 +16,7 @@ import org.eclipse.xtext.xbase.XFeatureCall | |||
16 | class NumericTranslator { | 16 | class NumericTranslator { |
17 | 17 | ||
18 | private XExpressionExtractor extractor = new XExpressionExtractor(); | 18 | private XExpressionExtractor extractor = new XExpressionExtractor(); |
19 | private NumericDrealProblemSolver drealSolver = new NumericDrealProblemSolver(); | ||
19 | 20 | ||
20 | long formingProblemTime=0; | 21 | long formingProblemTime=0; |
21 | long solvingProblemTime=0; | 22 | long solvingProblemTime=0; |
@@ -52,7 +53,7 @@ class NumericTranslator { | |||
52 | 53 | ||
53 | def NumericProblemSolver selectProblemSolver() { | 54 | def NumericProblemSolver selectProblemSolver() { |
54 | // return new NumericProblemSolver | 55 | // return new NumericProblemSolver |
55 | return new NumericDrealProblemSolver | 56 | return drealSolver; |
56 | } | 57 | } |
57 | 58 | ||
58 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) { | 59 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) { |
@@ -80,4 +81,5 @@ class NumericTranslator { | |||
80 | def getFormingProblemTime() {formingProblemTime} | 81 | def getFormingProblemTime() {formingProblemTime} |
81 | def getSolvingProblemTime() {solvingProblemTime} | 82 | def getSolvingProblemTime() {solvingProblemTime} |
82 | def getFormingSolutionTime() {formingSolutionTime} | 83 | def getFormingSolutionTime() {formingSolutionTime} |
84 | def getDrealSolver(){return drealSolver} | ||
83 | } \ No newline at end of file | 85 | } \ No newline at end of file |
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java index a594eb60..ab7f6ddc 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java | |||
@@ -28,22 +28,6 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par | |||
28 | 28 | ||
29 | 29 | ||
30 | public class NumericZ3ProblemSolver extends NumericProblemSolver{ | 30 | public class NumericZ3ProblemSolver extends NumericProblemSolver{ |
31 | private static final String N_Base = "org.eclipse.xtext.xbase.lib."; | ||
32 | private static final String N_PLUS = "operator_plus"; | ||
33 | private static final String N_MINUS = "operator_minus"; | ||
34 | private static final String N_POWER = "operator_power"; | ||
35 | private static final String N_MULTIPLY = "operator_multiply"; | ||
36 | private static final String N_DIVIDE = "operator_divide"; | ||
37 | private static final String N_MODULO = "operator_modulo"; | ||
38 | private static final String N_LESSTHAN = "operator_lessThan"; | ||
39 | private static final String N_LESSEQUALSTHAN = "operator_lessEqualsThan"; | ||
40 | private static final String N_GREATERTHAN = "operator_greaterThan"; | ||
41 | private static final String N_GREATEREQUALTHAN = "operator_greaterEqualsThan"; | ||
42 | private static final String N_EQUALS = "operator_equals"; | ||
43 | private static final String N_NOTEQUALS = "operator_notEquals"; | ||
44 | private static final String N_EQUALS3 = "operator_tripleEquals"; | ||
45 | private static final String N_NOTEQUALS3 = "operator_tripleNotEquals"; | ||
46 | |||
47 | 31 | ||
48 | private Context ctx; | 32 | private Context ctx; |
49 | private Solver s; | 33 | private Solver s; |