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 | 27 |
1 files changed, 15 insertions, 12 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 575a9224..b8ab8e95 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 | |||
@@ -193,15 +193,24 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
193 | PrimitiveElement matchedObj = aMatch.get(((XFeatureCall) e).getFeature()); | 193 | PrimitiveElement matchedObj = aMatch.get(((XFeatureCall) e).getFeature()); |
194 | boolean isInt = matchedObj instanceof IntegerElement; | 194 | boolean isInt = matchedObj instanceof IntegerElement; |
195 | if (!matchedObj.isValueSet()) { | 195 | if (!matchedObj.isValueSet()) { |
196 | //e is UNDEFINED term | ||
196 | if (varMap.get(matchedObj) == null) { | 197 | if (varMap.get(matchedObj) == null) { |
198 | //define and store the name of the matchedObj | ||
197 | expr = ((XFeatureCall) e).getFeature().getQualifiedName() + matchedObj.hashCode(); //TODO ISSUE | 199 | expr = ((XFeatureCall) e).getFeature().getQualifiedName() + matchedObj.hashCode(); //TODO ISSUE |
198 | varMap.put(matchedObj, expr); | 200 | varMap.put(matchedObj, expr); |
199 | } else { | 201 | } else { |
202 | //get name if already seen | ||
200 | expr = varMap.get(matchedObj); | 203 | expr = varMap.get(matchedObj); |
201 | } | 204 | } |
205 | //Add variable declarations, only for UNDEFINED | ||
206 | if(! curVar2Decl.keySet().contains(expr)) { | ||
207 | String varDecl = "(declare-fun " + expr + " () "; | ||
208 | if (isInt) {varDecl += "Int)";} | ||
209 | else {varDecl += "Real)";} | ||
210 | curVar2Decl.put(expr, varDecl); | ||
211 | } | ||
202 | } else { | 212 | } else { |
203 | //TODO unsure what it means if something gets in here | 213 | //e is DEFINED term (has a value) |
204 | System.err.println("Reached weird place"); | ||
205 | if (isInt) { | 214 | if (isInt) { |
206 | expr = Integer.toString(((IntegerElement) matchedObj).getValue()); | 215 | expr = Integer.toString(((IntegerElement) matchedObj).getValue()); |
207 | } else { | 216 | } else { |
@@ -210,13 +219,6 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
210 | } | 219 | } |
211 | varMap.put(matchedObj, expr); | 220 | varMap.put(matchedObj, expr); |
212 | } | 221 | } |
213 | //Add variable declarations | ||
214 | if(! curVar2Decl.keySet().contains(expr)) { | ||
215 | String varDecl = "(declare-fun " + expr + " () "; | ||
216 | if (isInt) {varDecl += "Int)";} | ||
217 | else {varDecl += "Real)";} | ||
218 | curVar2Decl.put(expr, varDecl); | ||
219 | } | ||
220 | } | 222 | } |
221 | // Constants | 223 | // Constants |
222 | else if (e instanceof XNumberLiteral) { | 224 | else if (e instanceof XNumberLiteral) { |
@@ -375,8 +377,9 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
375 | //DEBUG - Print things | 377 | //DEBUG - Print things |
376 | if (outputProcess == null) { | 378 | if (outputProcess == null) { |
377 | System.err.println("TIMEOUT"); | 379 | System.err.println("TIMEOUT"); |
378 | // printOutput(numProbContent); | 380 | printOutput(numProbContent); |
379 | } | 381 | } |
382 | |||
380 | // printOutput(numProbContent); | 383 | // printOutput(numProbContent); |
381 | // if (outputs != null) printOutput(outputs.get(0)); | 384 | // if (outputs != null) printOutput(outputs.get(0)); |
382 | // System.out.println(result); | 385 | // System.out.println(result); |
@@ -434,8 +437,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
434 | 437 | ||
435 | //DEBUG - Print things | 438 | //DEBUG - Print things |
436 | System.out.println("Getting Solution!"); | 439 | System.out.println("Getting Solution!"); |
437 | // printOutput(numProbContent); | 440 | printOutput(numProbContent); |
438 | // printOutput(outputs.get(0)); | 441 | printOutput(outputs.get(0)); |
439 | // System.out.println(result); | 442 | // System.out.println(result); |
440 | //END DEBUG | 443 | //END DEBUG |
441 | 444 | ||