From 635b4b6c3f9006847eb3d98c59cea3064f57979b Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Sat, 12 Oct 2019 23:10:19 -0400 Subject: VAMPIRE: complete data collection and code setup --- .../vampire/reasoner/.VampireSolver.xtendbin | Bin 10151 -> 10151 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 17151 -> 17151 bytes .../Logic2VampireLanguageMapper_Support.java | 19 +++++++++++-------- 3 files changed, 11 insertions(+), 8 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca') 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin 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 { case DARWINFM: return CollectionLiterals.newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s"); case EDARWIN: - return CollectionLiterals.newArrayList("E-Darwin---1.5", "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s"); + return CollectionLiterals.newArrayList("E-Darwin---1.5", + "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s"); case GEOIII: - return CollectionLiterals.newArrayList("Geo-III---2018C", "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s"); + return CollectionLiterals.newArrayList("Geo-III---2018C", + "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s"); case IPROVER: return CollectionLiterals.newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s"); case PARADOX: @@ -458,7 +460,7 @@ public class Logic2VampireLanguageMapper_Support { case VAMPIRE: return CollectionLiterals.newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s"); case Z3: - return CollectionLiterals.newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s"); + return CollectionLiterals.newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:%d -file:%s"); default: break; } @@ -482,12 +484,12 @@ public class Logic2VampireLanguageMapper_Support { final ArrayList solverSpecs = this.getSolverSpecs(solver); final String ID = solverSpecs.get(0); final String cmd = solverSpecs.get(1); - String _replace = cmd.replace("%d", Integer.valueOf(time).toString()); - String _plus = ((((((("------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID) + + return (((((((((((("------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"TimeLimit___" + ID) + + "\"\r\n\r\n") + Integer.valueOf(time)) + + "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___") + ID) + "\"\r\n\r\n") + ID) + "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___") + ID) + - "\"\r\n\r\n") + _replace); - return (_plus + "\r\n"); + "\"\r\n\r\n") + cmd) + "\r\n"); } public String addEnd() { @@ -495,7 +497,8 @@ public class Logic2VampireLanguageMapper_Support { } public ArrayList sendPost(final String formData) throws Exception { - final OkHttpClient client = new OkHttpClient.Builder().connectTimeout(350, TimeUnit.SECONDS).readTimeout(350, TimeUnit.SECONDS).build(); + final OkHttpClient client = new OkHttpClient.Builder().connectTimeout(600, TimeUnit.SECONDS).readTimeout(350, + TimeUnit.SECONDS).build(); final MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA"); final RequestBody body = RequestBody.create(mediaType, formData); 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", -- cgit v1.2.3-54-g00ecf