diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java | 34 |
1 files changed, 19 insertions, 15 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 f410cc6d..f6c0bc71 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 | |||
@@ -7,13 +7,11 @@ import java.io.FileInputStream; | |||
7 | import java.io.IOException; | 7 | import java.io.IOException; |
8 | import java.io.InputStream; | 8 | import java.io.InputStream; |
9 | import java.io.InputStreamReader; | 9 | import java.io.InputStreamReader; |
10 | import java.io.PrintWriter; | ||
11 | import java.util.ArrayList; | 10 | import java.util.ArrayList; |
12 | import java.util.Arrays; | 11 | import java.util.Arrays; |
13 | import java.util.HashMap; | 12 | import java.util.HashMap; |
14 | import java.util.List; | 13 | import java.util.List; |
15 | import java.util.Map; | 14 | import java.util.Map; |
16 | import java.util.Map.Entry; | ||
17 | import java.util.UUID; | 15 | import java.util.UUID; |
18 | import java.util.concurrent.TimeUnit; | 16 | import java.util.concurrent.TimeUnit; |
19 | import java.util.regex.Matcher; | 17 | import java.util.regex.Matcher; |
@@ -25,9 +23,6 @@ import org.eclipse.xtext.xbase.XExpression; | |||
25 | import org.eclipse.xtext.xbase.XFeatureCall; | 23 | import org.eclipse.xtext.xbase.XFeatureCall; |
26 | import org.eclipse.xtext.xbase.XNumberLiteral; | 24 | import org.eclipse.xtext.xbase.XNumberLiteral; |
27 | 25 | ||
28 | import com.microsoft.z3.IntExpr; | ||
29 | import com.microsoft.z3.RealExpr; | ||
30 | |||
31 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; | 26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; |
32 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | 27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; |
33 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; | 28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; |
@@ -168,6 +163,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
168 | } | 163 | } |
169 | } else { | 164 | } else { |
170 | //TODO unsure what it means if something gets in here | 165 | //TODO unsure what it means if something gets in here |
166 | System.err.println("Reached weird place"); | ||
171 | if (isInt) { | 167 | if (isInt) { |
172 | expr = Integer.toString(((IntegerElement) matchedObj).getValue()); | 168 | expr = Integer.toString(((IntegerElement) matchedObj).getValue()); |
173 | } else { | 169 | } else { |
@@ -342,20 +338,28 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
342 | if (result) { | 338 | if (result) { |
343 | long startFormingSolution = System.nanoTime(); | 339 | long startFormingSolution = System.nanoTime(); |
344 | Map<String, String> solMap = parseDrealOutput(outputs.get(0)); | 340 | Map<String, String> solMap = parseDrealOutput(outputs.get(0)); |
341 | |||
342 | // //DEBUG | ||
343 | // System.out.println("RESULT"); | ||
344 | // solMap.entrySet().forEach(System.out::println); | ||
345 | // System.out.println("SOLMAP"); | ||
346 | // varMap.forEach((k, v) -> System.out.println(v + "=" + k)); | ||
347 | // //END DEBUG | ||
348 | |||
345 | for (PrimitiveElement obj: objs) { | 349 | for (PrimitiveElement obj: objs) { |
346 | if(varMap.containsKey(obj)) { | 350 | if(varMap.containsKey(obj)) { |
347 | if (obj instanceof IntegerElement) { | 351 | String varName = varMap.get(obj); |
348 | String varName = varMap.get(obj); | 352 | String value = solMap.get(varName); |
349 | String value = solMap.get(varName); | 353 | if (value != null) { |
350 | sol.put(obj, Integer.parseInt(value)); | 354 | //this means that dreal actually worked on this and found a value for it |
351 | } else { | 355 | if (obj instanceof IntegerElement) { |
352 | String varName = varMap.get(obj); | 356 | sol.put(obj, Integer.parseInt(value)); |
353 | String value = solMap.get(varName); | 357 | } else { |
354 | sol.put(obj, Double.parseDouble(value)); | 358 | sol.put(obj, Double.parseDouble(value)); |
359 | } | ||
355 | } | 360 | } |
356 | |||
357 | } else { | 361 | } else { |
358 | // System.out.println(("variable " + obj + " is not used from Dreal"); | 362 | // System.err.println("variable " + obj + " is not used from Dreal"); |
359 | } | 363 | } |
360 | } | 364 | } |
361 | endFormingSolution = System.nanoTime() - startFormingSolution; | 365 | endFormingSolution = System.nanoTime() - startFormingSolution; |