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.xtend | 1 + .../Logic2VampireLanguageMapper_Support.xtend | 35 ++++++++++++++------- .../vampire/reasoner/.VampireSolver.xtendbin | Bin 10151 -> 10151 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 17151 -> 17151 bytes .../Logic2VampireLanguageMapper_Support.java | 19 ++++++----- 5 files changed, 36 insertions(+), 19 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner') 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 { ind = 0 while (!responseFound) { var line = response.get(ind) +// println(line) if (line.length >= 5 && line.substring(0, 5) == "ERROR") { done = false 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 { def getSolverSpecs(BackendSolver solver) { switch (solver) { - case BackendSolver::CVC4: return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT") - case BackendSolver::DARWINFM: return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s") - case BackendSolver::EDARWIN: return newArrayList("E-Darwin---1.5", "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s") - case BackendSolver::GEOIII: return newArrayList("Geo-III---2018C", "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s") - case BackendSolver::IPROVER: return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s") - case BackendSolver::PARADOX: return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s") - case BackendSolver::VAMPIRE: return newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s") - case BackendSolver::Z3: return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s") + case BackendSolver::CVC4: + return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT") + case BackendSolver::DARWINFM: + return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s") + case BackendSolver::EDARWIN: + return newArrayList("E-Darwin---1.5", + "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s") + case BackendSolver::GEOIII: + return newArrayList("Geo-III---2018C", + "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s") + case BackendSolver::IPROVER: + return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s") + case BackendSolver::PARADOX: + return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s") + case BackendSolver::VAMPIRE: + return newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s") + case BackendSolver::Z3: + return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:%d -file:%s") } } @@ -326,10 +336,12 @@ class Logic2VampireLanguageMapper_Support { val ID = solverSpecs.get(0) val cmd = solverSpecs.get(1) - return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID + + return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"TimeLimit___" + ID + + "\"\r\n\r\n" + 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" + cmd.replace("%d", time.toString) + "\r\n" + "\"\r\n\r\n" + cmd + "\r\n" } def addEnd() { @@ -338,7 +350,8 @@ class Logic2VampireLanguageMapper_Support { def sendPost(String formData) throws Exception { - val OkHttpClient client = new OkHttpClient.Builder().connectTimeout(350, TimeUnit.SECONDS).readTimeout(350, TimeUnit.SECONDS).build() + val OkHttpClient client = new OkHttpClient.Builder().connectTimeout(600, TimeUnit.SECONDS).readTimeout(350, + TimeUnit.SECONDS).build() val MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA") 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 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