diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-12 23:10:19 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-12 23:10:19 -0400 |
commit | e0fc38cb9a22bf0c21053361a22b8fa167f30625 (patch) | |
tree | 35b063b75bc970594ca496297fb57de2b9776776 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen | |
parent | VAMPIRE: complete testing setup (diff) | |
download | VIATRA-Generator-e0fc38cb9a22bf0c21053361a22b8fa167f30625.tar.gz VIATRA-Generator-e0fc38cb9a22bf0c21053361a22b8fa167f30625.tar.zst VIATRA-Generator-e0fc38cb9a22bf0c21053361a22b8fa167f30625.zip |
VAMPIRE: complete data collection and code setup
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen')
3 files changed, 11 insertions, 8 deletions
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", |