diff options
8 files changed, 51 insertions, 34 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend index 31aa091c..9ec08163 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend | |||
@@ -90,6 +90,7 @@ class VampireSolver extends LogicReasoner { | |||
90 | ind = 0 | 90 | ind = 0 |
91 | while (!responseFound) { | 91 | while (!responseFound) { |
92 | var line = response.get(ind) | 92 | var line = response.get(ind) |
93 | // println(line) | ||
93 | if (line.length >= 5 && line.substring(0, 5) == "ERROR") { | 94 | if (line.length >= 5 && line.substring(0, 5) == "ERROR") { |
94 | done = false | 95 | done = false |
95 | responseFound = true | 96 | responseFound = true |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend index 7b1c7d9a..44efd84e 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend | |||
@@ -298,14 +298,24 @@ class Logic2VampireLanguageMapper_Support { | |||
298 | 298 | ||
299 | def getSolverSpecs(BackendSolver solver) { | 299 | def getSolverSpecs(BackendSolver solver) { |
300 | switch (solver) { | 300 | switch (solver) { |
301 | case BackendSolver::CVC4: return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT") | 301 | case BackendSolver::CVC4: |
302 | case BackendSolver::DARWINFM: return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s") | 302 | return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT") |
303 | case BackendSolver::EDARWIN: return newArrayList("E-Darwin---1.5", "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s") | 303 | case BackendSolver::DARWINFM: |
304 | case BackendSolver::GEOIII: return newArrayList("Geo-III---2018C", "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s") | 304 | return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s") |
305 | case BackendSolver::IPROVER: return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s") | 305 | case BackendSolver::EDARWIN: |
306 | case BackendSolver::PARADOX: return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s") | 306 | return newArrayList("E-Darwin---1.5", |
307 | case BackendSolver::VAMPIRE: return newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s") | 307 | "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s") |
308 | case BackendSolver::Z3: return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s") | 308 | case BackendSolver::GEOIII: |
309 | return newArrayList("Geo-III---2018C", | ||
310 | "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s") | ||
311 | case BackendSolver::IPROVER: | ||
312 | return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s") | ||
313 | case BackendSolver::PARADOX: | ||
314 | return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s") | ||
315 | case BackendSolver::VAMPIRE: | ||
316 | return newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s") | ||
317 | case BackendSolver::Z3: | ||
318 | return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:%d -file:%s") | ||
309 | } | 319 | } |
310 | } | 320 | } |
311 | 321 | ||
@@ -326,10 +336,12 @@ class Logic2VampireLanguageMapper_Support { | |||
326 | val ID = solverSpecs.get(0) | 336 | val ID = solverSpecs.get(0) |
327 | val cmd = solverSpecs.get(1) | 337 | val cmd = solverSpecs.get(1) |
328 | 338 | ||
329 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID + | 339 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"TimeLimit___" + ID + |
340 | "\"\r\n\r\n" + time + | ||
341 | "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID + | ||
330 | "\"\r\n\r\n" + ID + | 342 | "\"\r\n\r\n" + ID + |
331 | "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___" + ID + | 343 | "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___" + ID + |
332 | "\"\r\n\r\n" + cmd.replace("%d", time.toString) + "\r\n" | 344 | "\"\r\n\r\n" + cmd + "\r\n" |
333 | } | 345 | } |
334 | 346 | ||
335 | def addEnd() { | 347 | def addEnd() { |
@@ -338,7 +350,8 @@ class Logic2VampireLanguageMapper_Support { | |||
338 | 350 | ||
339 | def sendPost(String formData) throws Exception { | 351 | def sendPost(String formData) throws Exception { |
340 | 352 | ||
341 | val OkHttpClient client = new OkHttpClient.Builder().connectTimeout(350, TimeUnit.SECONDS).readTimeout(350, TimeUnit.SECONDS).build() | 353 | val OkHttpClient client = new OkHttpClient.Builder().connectTimeout(600, TimeUnit.SECONDS).readTimeout(350, |
354 | TimeUnit.SECONDS).build() | ||
342 | 355 | ||
343 | val MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA") | 356 | val MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA") |
344 | val RequestBody body = RequestBody.create(mediaType, formData) | 357 | val RequestBody body = RequestBody.create(mediaType, formData) |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin index fb8f872d..7fedcc30 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin index 6c7c7522..9caad4ea 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java index 1255b25c..d757212a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java | |||
@@ -448,9 +448,11 @@ public class Logic2VampireLanguageMapper_Support { | |||
448 | case DARWINFM: | 448 | case DARWINFM: |
449 | return CollectionLiterals.<String>newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s"); | 449 | return CollectionLiterals.<String>newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s"); |
450 | case EDARWIN: | 450 | case EDARWIN: |
451 | return CollectionLiterals.<String>newArrayList("E-Darwin---1.5", "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s"); | 451 | return CollectionLiterals.<String>newArrayList("E-Darwin---1.5", |
452 | "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s"); | ||
452 | case GEOIII: | 453 | case GEOIII: |
453 | return CollectionLiterals.<String>newArrayList("Geo-III---2018C", "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s"); | 454 | return CollectionLiterals.<String>newArrayList("Geo-III---2018C", |
455 | "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s"); | ||
454 | case IPROVER: | 456 | case IPROVER: |
455 | return CollectionLiterals.<String>newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s"); | 457 | return CollectionLiterals.<String>newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s"); |
456 | case PARADOX: | 458 | case PARADOX: |
@@ -458,7 +460,7 @@ public class Logic2VampireLanguageMapper_Support { | |||
458 | case VAMPIRE: | 460 | case VAMPIRE: |
459 | return CollectionLiterals.<String>newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s"); | 461 | return CollectionLiterals.<String>newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s"); |
460 | case Z3: | 462 | case Z3: |
461 | return CollectionLiterals.<String>newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s"); | 463 | return CollectionLiterals.<String>newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:%d -file:%s"); |
462 | default: | 464 | default: |
463 | break; | 465 | break; |
464 | } | 466 | } |
@@ -482,12 +484,12 @@ public class Logic2VampireLanguageMapper_Support { | |||
482 | final ArrayList<String> solverSpecs = this.getSolverSpecs(solver); | 484 | final ArrayList<String> solverSpecs = this.getSolverSpecs(solver); |
483 | final String ID = solverSpecs.get(0); | 485 | final String ID = solverSpecs.get(0); |
484 | final String cmd = solverSpecs.get(1); | 486 | final String cmd = solverSpecs.get(1); |
485 | String _replace = cmd.replace("%d", Integer.valueOf(time).toString()); | 487 | return (((((((((((("------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"TimeLimit___" + ID) + |
486 | String _plus = ((((((("------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID) + | 488 | "\"\r\n\r\n") + Integer.valueOf(time)) + |
489 | "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___") + ID) + | ||
487 | "\"\r\n\r\n") + ID) + | 490 | "\"\r\n\r\n") + ID) + |
488 | "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___") + ID) + | 491 | "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___") + ID) + |
489 | "\"\r\n\r\n") + _replace); | 492 | "\"\r\n\r\n") + cmd) + "\r\n"); |
490 | return (_plus + "\r\n"); | ||
491 | } | 493 | } |
492 | 494 | ||
493 | public String addEnd() { | 495 | public String addEnd() { |
@@ -495,7 +497,8 @@ public class Logic2VampireLanguageMapper_Support { | |||
495 | } | 497 | } |
496 | 498 | ||
497 | public ArrayList<String> sendPost(final String formData) throws Exception { | 499 | public ArrayList<String> sendPost(final String formData) throws Exception { |
498 | final OkHttpClient client = new OkHttpClient.Builder().connectTimeout(350, TimeUnit.SECONDS).readTimeout(350, TimeUnit.SECONDS).build(); | 500 | final OkHttpClient client = new OkHttpClient.Builder().connectTimeout(600, TimeUnit.SECONDS).readTimeout(350, |
501 | TimeUnit.SECONDS).build(); | ||
499 | final MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA"); | 502 | final MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA"); |
500 | final RequestBody body = RequestBody.create(mediaType, formData); | 503 | final RequestBody body = RequestBody.create(mediaType, formData); |
501 | final Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body).addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin", | 504 | final Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body).addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin", |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend index 9121367b..26b91525 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend | |||
@@ -59,12 +59,12 @@ class YakinduTest { | |||
59 | // val queries = null | 59 | // val queries = null |
60 | println("DSL loaded") | 60 | println("DSL loaded") |
61 | 61 | ||
62 | var SZ_TOP = 30 | 62 | var SZ_TOP = 150 |
63 | var SZ_BOT = 5 | 63 | var SZ_BOT = 150 |
64 | var INC = 5 | 64 | var INC = 10 |
65 | var REPS = 1 | 65 | var REPS = 10 |
66 | 66 | ||
67 | val RUNTIME = 20 | 67 | val RUNTIME = 300 |
68 | 68 | ||
69 | val EXACT = -1 | 69 | val EXACT = -1 |
70 | if (EXACT != -1) { | 70 | if (EXACT != -1) { |
@@ -82,13 +82,13 @@ class YakinduTest { | |||
82 | // , | 82 | // , |
83 | // BackendSolver::GEOIII | 83 | // BackendSolver::GEOIII |
84 | // , | 84 | // , |
85 | BackendSolver::IPROVER | 85 | // BackendSolver::IPROVER |
86 | // , | 86 | // , |
87 | // BackendSolver::PARADOX | 87 | // BackendSolver::PARADOX |
88 | // , | 88 | // , |
89 | // BackendSolver::VAMPIRE | 89 | // BackendSolver::VAMPIRE |
90 | // , | 90 | // , |
91 | // BackendSolver::Z3 | 91 | BackendSolver::Z3 |
92 | ) | 92 | ) |
93 | 93 | ||
94 | 94 | ||
@@ -197,7 +197,7 @@ class YakinduTest { | |||
197 | writer.append(satOut + ",") | 197 | writer.append(satOut + ",") |
198 | writer.append(satTime + ",") | 198 | writer.append(satTime + ",") |
199 | writer.append(modOut + ",") | 199 | writer.append(modOut + ",") |
200 | writer.append(modTime + ",") | 200 | writer.append(modTime + "") |
201 | writer.append("\n") | 201 | writer.append("\n") |
202 | 202 | ||
203 | // print("(" + tTime + "/" + sTime + "s)..") | 203 | // print("(" + tTime + "/" + sTime + "s)..") |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin index cf52d6a6..b29e18b1 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java index 1837b768..c2aaee03 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java | |||
@@ -85,11 +85,11 @@ public class YakinduTest { | |||
85 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); | 85 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); |
86 | final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); | 86 | final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); |
87 | InputOutput.<String>println("DSL loaded"); | 87 | InputOutput.<String>println("DSL loaded"); |
88 | int SZ_TOP = 30; | 88 | int SZ_TOP = 150; |
89 | int SZ_BOT = 5; | 89 | int SZ_BOT = 150; |
90 | int INC = 5; | 90 | int INC = 10; |
91 | int REPS = 1; | 91 | int REPS = 10; |
92 | final int RUNTIME = 20; | 92 | final int RUNTIME = 300; |
93 | final int EXACT = (-1); | 93 | final int EXACT = (-1); |
94 | if ((EXACT != (-1))) { | 94 | if ((EXACT != (-1))) { |
95 | SZ_TOP = EXACT; | 95 | SZ_TOP = EXACT; |
@@ -98,7 +98,7 @@ public class YakinduTest { | |||
98 | REPS = 10; | 98 | REPS = 10; |
99 | } | 99 | } |
100 | final ArrayList<BackendSolver> BACKENDSOLVERS = CollectionLiterals.<BackendSolver>newArrayList( | 100 | final ArrayList<BackendSolver> BACKENDSOLVERS = CollectionLiterals.<BackendSolver>newArrayList( |
101 | BackendSolver.IPROVER); | 101 | BackendSolver.Z3); |
102 | String str = ""; | 102 | String str = ""; |
103 | for (final BackendSolver solver : BACKENDSOLVERS) { | 103 | for (final BackendSolver solver : BACKENDSOLVERS) { |
104 | String _str = str; | 104 | String _str = str; |
@@ -218,7 +218,7 @@ public class YakinduTest { | |||
218 | String _plus_20 = (Double.valueOf(satTime) + ","); | 218 | String _plus_20 = (Double.valueOf(satTime) + ","); |
219 | writer.append(_plus_20); | 219 | writer.append(_plus_20); |
220 | writer.append((modOut + ",")); | 220 | writer.append((modOut + ",")); |
221 | String _plus_21 = (Double.valueOf(modTime) + ","); | 221 | String _plus_21 = (Double.valueOf(modTime) + ""); |
222 | writer.append(_plus_21); | 222 | writer.append(_plus_21); |
223 | writer.append("\n"); | 223 | writer.append("\n"); |
224 | } | 224 | } |