diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src')
2 files changed, 5 insertions, 4 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 55d52031..f410cc6d 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 | |||
@@ -171,7 +171,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
171 | if (isInt) { | 171 | if (isInt) { |
172 | expr = Integer.toString(((IntegerElement) matchedObj).getValue()); | 172 | expr = Integer.toString(((IntegerElement) matchedObj).getValue()); |
173 | } else { | 173 | } else { |
174 | expr = Double.toString(((RealElement) matchedObj).getValue().doubleValue()); | 174 | expr = Double.toString(((RealElement) matchedObj).getValue()); |
175 | // expr = Double.toString(((RealElement) matchedObj).getValue().doubleValue()); | ||
175 | } | 176 | } |
176 | varMap.put(matchedObj, expr); | 177 | varMap.put(matchedObj, expr); |
177 | } | 178 | } |
@@ -301,7 +302,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
301 | 302 | ||
302 | private Map<String, String> parseDrealOutput(List<String> output) { | 303 | private Map<String, String> parseDrealOutput(List<String> output) { |
303 | Map<String, String> res = new HashMap<String, String>(); | 304 | Map<String, String> res = new HashMap<String, String>(); |
304 | String re = "(\\w+) : \\[([0-9\\-.e]+), ([0-9\\-.e]+)\\]"; | 305 | String re = "(\\w+) : \\[([0-9\\-+.e]+), ([0-9\\-+.e]+)\\]"; |
305 | Pattern p = Pattern.compile(re); | 306 | Pattern p = Pattern.compile(re); |
306 | for (String varVal : output) { | 307 | for (String varVal : output) { |
307 | Matcher m = p.matcher(varVal); | 308 | Matcher m = p.matcher(varVal); |
@@ -350,7 +351,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
350 | } else { | 351 | } else { |
351 | String varName = varMap.get(obj); | 352 | String varName = varMap.get(obj); |
352 | String value = solMap.get(varName); | 353 | String value = solMap.get(varName); |
353 | sol.put(obj, Integer.parseInt(value)); | 354 | sol.put(obj, Double.parseDouble(value)); |
354 | } | 355 | } |
355 | 356 | ||
356 | } else { | 357 | } else { |
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 ab7f6ddc..db33804e 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 | |||
@@ -174,7 +174,7 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ | |||
174 | int value = ((IntegerElement) matchedObj).getValue(); | 174 | int value = ((IntegerElement) matchedObj).getValue(); |
175 | expr = (ArithExpr) ctx.mkInt(value); | 175 | expr = (ArithExpr) ctx.mkInt(value); |
176 | } else { | 176 | } else { |
177 | double value = ((RealElement) matchedObj).getValue().doubleValue(); | 177 | double value = ((RealElement) matchedObj).getValue(); |
178 | expr = (ArithExpr) ctx.mkReal(String.valueOf(value)); | 178 | expr = (ArithExpr) ctx.mkReal(String.valueOf(value)); |
179 | } | 179 | } |
180 | varMap.put(matchedObj, expr); | 180 | varMap.put(matchedObj, expr); |