VAMPIRE: complete data collection and code setup

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
--- 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", 

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
--- 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
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<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi");

       final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance());

       InputOutput.<String>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<BackendSolver> BACKENDSOLVERS = CollectionLiterals.<BackendSolver>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");

                 }