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 ++++++----- .../dslreasoner/vampire/icse/YakinduTest.xtend | 16 +++++----- .../dslreasoner/vampire/icse/.YakinduTest.xtendbin | Bin 8992 -> 8997 bytes .../ecse/dslreasoner/vampire/icse/YakinduTest.java | 14 ++++----- 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 { 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", 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 { // val queries = null println("DSL loaded") - var SZ_TOP = 30 - var SZ_BOT = 5 - var INC = 5 - var REPS = 1 + var SZ_TOP = 150 + var SZ_BOT = 150 + var INC = 10 + var REPS = 10 - val RUNTIME = 20 + val RUNTIME = 300 val EXACT = -1 if (EXACT != -1) { @@ -82,13 +82,13 @@ class YakinduTest { // , // BackendSolver::GEOIII // , - BackendSolver::IPROVER +// BackendSolver::IPROVER // , // BackendSolver::PARADOX // , // BackendSolver::VAMPIRE // , -// BackendSolver::Z3 + BackendSolver::Z3 ) @@ -197,7 +197,7 @@ class YakinduTest { writer.append(satOut + ",") writer.append(satTime + ",") writer.append(modOut + ",") - writer.append(modTime + ",") + writer.append(modTime + "") writer.append("\n") // 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 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin 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 { final EList partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); InputOutput.println("DSL loaded"); - int SZ_TOP = 30; - int SZ_BOT = 5; - int INC = 5; - int REPS = 1; - final int RUNTIME = 20; + int SZ_TOP = 150; + int SZ_BOT = 150; + int INC = 10; + int REPS = 10; + final int RUNTIME = 300; final int EXACT = (-1); if ((EXACT != (-1))) { SZ_TOP = EXACT; @@ -98,7 +98,7 @@ public class YakinduTest { REPS = 10; } final ArrayList BACKENDSOLVERS = CollectionLiterals.newArrayList( - BackendSolver.IPROVER); + BackendSolver.Z3); String str = ""; for (final BackendSolver solver : BACKENDSOLVERS) { String _str = str; @@ -218,7 +218,7 @@ public class YakinduTest { String _plus_20 = (Double.valueOf(satTime) + ","); writer.append(_plus_20); writer.append((modOut + ",")); - String _plus_21 = (Double.valueOf(modTime) + ","); + String _plus_21 = (Double.valueOf(modTime) + ""); writer.append(_plus_21); writer.append("\n"); } -- cgit v1.2.3-54-g00ecf