5 files changed, 36 insertions, 19 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
--- 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
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
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.<String>newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s");

         case EDARWIN:

-          return CollectionLiterals.<String>newArrayList("E-Darwin---1.5", "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s");

+          return CollectionLiterals.<String>newArrayList("E-Darwin---1.5", 

+            "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s");

         case GEOIII:

-          return CollectionLiterals.<String>newArrayList("Geo-III---2018C", "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s");

+          return CollectionLiterals.<String>newArrayList("Geo-III---2018C", 

+            "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s");

         case IPROVER:

           return CollectionLiterals.<String>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.<String>newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s");

         case Z3:

-          return CollectionLiterals.<String>newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s");

+          return CollectionLiterals.<String>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<String> 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<String> 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",