diff options
author | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-01-07 23:23:37 -0500 |
---|---|---|
committer | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-01-07 23:23:37 -0500 |
commit | 2fd7b130fe5d05137e162ede499d5cc661d83424 (patch) | |
tree | 8242c120c51dc4030e43959336e17ed65b38b204 /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner | |
parent | crlf fix (diff) | |
download | VIATRA-Generator-2fd7b130fe5d05137e162ede499d5cc661d83424.tar.gz VIATRA-Generator-2fd7b130fe5d05137e162ede499d5cc661d83424.tar.zst VIATRA-Generator-2fd7b130fe5d05137e162ede499d5cc661d83424.zip |
fix dup decl bug + adjust famTree case study
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java | 12 |
1 files changed, 7 insertions, 5 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 d7268bb9..7dedfaeb 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 | |||
@@ -13,6 +13,7 @@ import java.util.Arrays; | |||
13 | import java.util.HashMap; | 13 | import java.util.HashMap; |
14 | import java.util.List; | 14 | import java.util.List; |
15 | import java.util.Map; | 15 | import java.util.Map; |
16 | import java.util.Map.Entry; | ||
16 | import java.util.UUID; | 17 | import java.util.UUID; |
17 | import java.util.concurrent.TimeUnit; | 18 | import java.util.concurrent.TimeUnit; |
18 | import java.util.regex.Matcher; | 19 | import java.util.regex.Matcher; |
@@ -35,7 +36,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
35 | 36 | ||
36 | private final String containerName; | 37 | private final String containerName; |
37 | private Map<Object, String> varMap; | 38 | private Map<Object, String> varMap; |
38 | private List<String> curVars; | 39 | private Map<String, String> curVar2Decl; |
39 | 40 | ||
40 | public NumericDrealProblemSolver() throws IOException, InterruptedException { | 41 | public NumericDrealProblemSolver() throws IOException, InterruptedException { |
41 | //setup docker | 42 | //setup docker |
@@ -64,6 +65,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
64 | //TODO timeout if needed | 65 | //TODO timeout if needed |
65 | if (!p.waitFor(5, TimeUnit.SECONDS)) { | 66 | if (!p.waitFor(5, TimeUnit.SECONDS)) { |
66 | p.destroy(); | 67 | p.destroy(); |
68 | System.err.println("TIMEOUT"); | ||
67 | } | 69 | } |
68 | return p; | 70 | return p; |
69 | } | 71 | } |
@@ -171,11 +173,11 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
171 | varMap.put(matchedObj, expr); | 173 | varMap.put(matchedObj, expr); |
172 | } | 174 | } |
173 | //Add variable declarations | 175 | //Add variable declarations |
174 | if(! curVars.contains(expr)) { | 176 | if(! curVar2Decl.keySet().contains(expr)) { |
175 | String varDecl = "(declare-fun " + expr + " () "; | 177 | String varDecl = "(declare-fun " + expr + " () "; |
176 | if (isInt) {varDecl += "Int)";} | 178 | if (isInt) {varDecl += "Int)";} |
177 | else {varDecl += "Real)";} | 179 | else {varDecl += "Real)";} |
178 | curVars.add(varDecl); | 180 | curVar2Decl.put(expr, varDecl); |
179 | } | 181 | } |
180 | } | 182 | } |
181 | // Constants | 183 | // Constants |
@@ -227,7 +229,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
227 | String tempFileName = tempFile.getName(); | 229 | String tempFileName = tempFile.getName(); |
228 | 230 | ||
229 | //STM2 FILE CONTENT CREATION | 231 | //STM2 FILE CONTENT CREATION |
230 | curVars = new ArrayList<String>(); | 232 | curVar2Decl = new HashMap<String, String>(); |
231 | List<String> curConstraints = new ArrayList<String>(); | 233 | List<String> curConstraints = new ArrayList<String>(); |
232 | 234 | ||
233 | PrintWriter printer = new PrintWriter(tempFile); | 235 | PrintWriter printer = new PrintWriter(tempFile); |
@@ -242,7 +244,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
242 | } | 244 | } |
243 | } | 245 | } |
244 | //Add Content to SMT2 file | 246 | //Add Content to SMT2 file |
245 | for (String varDecl : curVars) {printer.println(varDecl);} | 247 | for (String varDecl : curVar2Decl.values()) {printer.println(varDecl);} |
246 | for (String negAssert : curConstraints) {printer.println(negAssert);} | 248 | for (String negAssert : curConstraints) {printer.println(negAssert);} |
247 | printer.println("(check-sat)"); | 249 | printer.println("(check-sat)"); |
248 | printer.close(); | 250 | printer.close(); |