19 files changed, 243 insertions, 32 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
index e50e6812..b26c1ded 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
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 e4925e24..fb8f872d 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/VampireSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
index 432b14c3..3e3bd688 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
@@ -5,12 +5,15 @@ import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation;

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;

+import com.google.common.base.Objects;

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation;

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;

@@ -19,13 +22,25 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration;
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput;

 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;

 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory;

 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry;

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry;

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics;

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry;

 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;

+import java.util.ArrayList;

 import java.util.List;

 import org.eclipse.emf.common.util.EList;

 import org.eclipse.xtend2.lib.StringConcatenation;

+import org.eclipse.xtext.xbase.lib.CollectionLiterals;

+import org.eclipse.xtext.xbase.lib.Exceptions;

+import org.eclipse.xtext.xbase.lib.Extension;

 import org.eclipse.xtext.xbase.lib.Functions.Function1;

+import org.eclipse.xtext.xbase.lib.InputOutput;

 import org.eclipse.xtext.xbase.lib.ListExtensions;

+import org.eclipse.xtext.xbase.lib.ObjectExtensions;

+import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;

 

 @SuppressWarnings("all")

 public class VampireSolver extends LogicReasoner {

@@ -41,36 +56,142 @@ public class VampireSolver extends LogicReasoner {
   

   private final VampireHandler handler = new VampireHandler();

   

+  private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();

+  

+  @Extension

+  private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE;

+  

+  @Extension

+  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

+  

   @Override

   public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException {

-    final VampireSolverConfiguration vampireConfig = this.asConfig(config);

-    String fileName = (((("problem_" + Integer.valueOf(vampireConfig.typeScopes.minNewElements)) + "-") + Integer.valueOf(vampireConfig.typeScopes.maxNewElements)) + ".tptp");

-    final long transformationStart = System.currentTimeMillis();

-    final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig);

-    long _currentTimeMillis = System.currentTimeMillis();

-    final long transformationTime = (_currentTimeMillis - transformationStart);

-    final VampireModel vampireProblem = result.getOutput();

-    final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace();

-    String fileURI = null;

-    String vampireCode = null;

-    vampireCode = workspace.writeModelToString(vampireProblem, fileName);

-    final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || 

-      (vampireConfig.documentationLevel == DocumentationLevel.FULL));

-    if (writeFile) {

-      fileURI = workspace.writeModel(vampireProblem, fileName).toFileString();

-    }

-    if (vampireConfig.genModel) {

-      final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig);

-      final long backTransformationStart = System.currentTimeMillis();

-      final ModelResult logicResult = this.backwardMapper.transformOutput(problem, 

-        vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime);

-      long _currentTimeMillis_1 = System.currentTimeMillis();

-      final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart);

-      return logicResult;

+    try {

+      final VampireSolverConfiguration vampireConfig = this.asConfig(config);

+      String fileName = (((("problem_" + Integer.valueOf(vampireConfig.typeScopes.minNewElements)) + "-") + 

+        Integer.valueOf(vampireConfig.typeScopes.maxNewElements)) + ".tptp");

+      final long transformationStart = System.currentTimeMillis();

+      final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig);

+      long _currentTimeMillis = System.currentTimeMillis();

+      final long transformationTime = (_currentTimeMillis - transformationStart);

+      final VampireModel vampireProblem = result.getOutput();

+      final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace();

+      String fileURI = null;

+      String vampireCode = null;

+      vampireCode = workspace.writeModelToString(vampireProblem, fileName);

+      final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || 

+        (vampireConfig.documentationLevel == DocumentationLevel.FULL));

+      if (writeFile) {

+        fileURI = workspace.writeModel(vampireProblem, fileName).toFileString();

+      }

+      if (vampireConfig.genModel) {

+        if (vampireConfig.server) {

+          final String form = this.support.makeForm(vampireCode, vampireConfig.solver, vampireConfig.runtimeLimit);

+          ArrayList<String> response = CollectionLiterals.<String>newArrayList();

+          int ind = 0;

+          boolean done = false;

+          InputOutput.<String>print(" ");

+          while ((!done)) {

+            {

+              InputOutput.<String>print("(x)");

+              done = false;

+              response = this.support.sendPost(form);

+              boolean responseFound = false;

+              ind = 0;

+              while ((!responseFound)) {

+                {

+                  String line = response.get(ind);

+                  if (((line.length() >= 5) && Objects.equal(line.substring(0, 5), "ERROR"))) {

+                    done = false;

+                    responseFound = true;

+                  } else {

+                    boolean _equals = Objects.equal(line, "</PRE>");

+                    if (_equals) {

+                      done = true;

+                      responseFound = true;

+                    }

+                  }

+                  ind++;

+                }

+              }

+            }

+          }

+          final String satRaw = response.get((ind - 3));

+          final String modRaw = response.get((ind - 2));

+          final ArrayList<String> sat = CollectionLiterals.<String>newArrayList(satRaw.split(" "));

+          final ArrayList<String> mod = CollectionLiterals.<String>newArrayList(modRaw.split(" "));

+          final String satOut = sat.get(1);

+          final String modOut = mod.get(1);

+          final String satTime = sat.get(2);

+          final String modTime = mod.get(2);

+          InputOutput.println();

+          InputOutput.<ArrayList<String>>println(sat);

+          InputOutput.<ArrayList<String>>println(mod);

+          ModelResult _createModelResult = this.resultFactory.createModelResult();

+          final Procedure1<ModelResult> _function = (ModelResult it) -> {

+            it.setProblem(null);

+            EList<Object> _representation = it.getRepresentation();

+            VampireModel _createVampireModel = this.factory.createVampireModel();

+            final Procedure1<VampireModel> _function_1 = (VampireModel it_1) -> {

+            };

+            VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_1);

+            _representation.add(_doubleArrow);

+            it.setTrace(it.getTrace());

+            Statistics _createStatistics = this.resultFactory.createStatistics();

+            final Procedure1<Statistics> _function_2 = (Statistics it_1) -> {

+              it_1.setTransformationTime(((int) transformationTime));

+              EList<StatisticEntry> _entries = it_1.getEntries();

+              StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry();

+              final Procedure1<StringStatisticEntry> _function_3 = (StringStatisticEntry it_2) -> {

+                it_2.setName("satOut");

+                it_2.setValue(satOut);

+              };

+              StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_3);

+              _entries.add(_doubleArrow_1);

+              EList<StatisticEntry> _entries_1 = it_1.getEntries();

+              RealStatisticEntry _createRealStatisticEntry = this.resultFactory.createRealStatisticEntry();

+              final Procedure1<RealStatisticEntry> _function_4 = (RealStatisticEntry it_2) -> {

+                it_2.setName("satTime");

+                it_2.setValue(Double.parseDouble(satTime));

+              };

+              RealStatisticEntry _doubleArrow_2 = ObjectExtensions.<RealStatisticEntry>operator_doubleArrow(_createRealStatisticEntry, _function_4);

+              _entries_1.add(_doubleArrow_2);

+              EList<StatisticEntry> _entries_2 = it_1.getEntries();

+              StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry();

+              final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> {

+                it_2.setName("modOut");

+                it_2.setValue(modOut);

+              };

+              StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_5);

+              _entries_2.add(_doubleArrow_3);

+              EList<StatisticEntry> _entries_3 = it_1.getEntries();

+              RealStatisticEntry _createRealStatisticEntry_1 = this.resultFactory.createRealStatisticEntry();

+              final Procedure1<RealStatisticEntry> _function_6 = (RealStatisticEntry it_2) -> {

+                it_2.setName("modTime");

+                it_2.setValue(Double.parseDouble(modTime));

+              };

+              RealStatisticEntry _doubleArrow_4 = ObjectExtensions.<RealStatisticEntry>operator_doubleArrow(_createRealStatisticEntry_1, _function_6);

+              _entries_3.add(_doubleArrow_4);

+            };

+            Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_2);

+            it.setStatistics(_doubleArrow_1);

+          };

+          return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult, _function);

+        } else {

+          final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig);

+          final long backTransformationStart = System.currentTimeMillis();

+          final ModelResult logicResult = this.backwardMapper.transformOutput(problem, 

+            vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime);

+          long _currentTimeMillis_1 = System.currentTimeMillis();

+          final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart);

+          return logicResult;

+        }

+      }

+      MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null);

+      return this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, _monitoredVampireSolution, forwardTrace, transformationTime);

+    } catch (Throwable _e) {

+      throw Exceptions.sneakyThrow(_e);

     }

-    MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null);

-    return this.backwardMapper.transformOutput(problem, 

-      vampireConfig.solutionScope.numberOfRequiredSolution, _monitoredVampireSolution, forwardTrace, transformationTime);

   }

   

   public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) {

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
index dd66e910..c094872e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
@@ -11,7 +11,9 @@ public class VampireSolverConfiguration extends LogicSolverConfiguration {
   

   public int iteration = (-1);

   

-  public BackendSolver solver = BackendSolver.VAMP;

+  public BackendSolver solver = BackendSolver.VAMPIRE;

   

   public boolean genModel = true;

+  

+  public boolean server = false;

 }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
index 8d2ec6ab..8b7f031e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
index 515b4b3c..1b6e8f80 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
index 46ad8c79..f523f1af 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
index 169aedc2..30ba1843 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
index 699ce6e2..174c7362 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
index 799515d4..affa3754 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.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 2a112ae7..6c7c7522 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_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
index 7f32e055..5be67889 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
index a2dd469b..192c9d1a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
index 98c355ab..0495ab53 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
index 246c08c8..c438f1e5 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
index 9e55bac4..5fb9b455 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
index bc39a068..c09d929e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
@@ -55,13 +55,13 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
   public void _transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {

     int elemsInIM = trace.definedElement2String.size();

     final int ABSOLUTE_MIN = 0;

-    final int ABSOLUTE_MAX = ((-1) - elemsInIM);

+    final int ABSOLUTE_MAX = (Integer.MAX_VALUE - elemsInIM);

     final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM);

     final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM);

     final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList();

     final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN);

     if ((GLOBAL_MIN != ABSOLUTE_MIN)) {

-      this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, (!consistant));

+      this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, consistant);

       if (consistant) {

         for (final VLSConstant i : trace.uniqueInstances) {

           localInstances.add(this.support.duplicate(i));

@@ -72,7 +72,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
       }

     }

     if ((GLOBAL_MAX != ABSOLUTE_MAX)) {

-      this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant);

+      this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, (!consistant));

       if (consistant) {

         this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null);

       } else {

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 dae0df6e..1255b25c 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
@@ -1,5 +1,6 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

 

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd;

@@ -29,6 +30,12 @@ import java.util.Collection;
 import java.util.HashMap;

 import java.util.List;

 import java.util.Map;

+import java.util.concurrent.TimeUnit;

+import okhttp3.MediaType;

+import okhttp3.OkHttpClient;

+import okhttp3.Request;

+import okhttp3.RequestBody;

+import okhttp3.Response;

 import org.eclipse.emf.common.util.EList;

 import org.eclipse.xtend2.lib.StringConcatenation;

 import org.eclipse.xtext.xbase.lib.CollectionLiterals;

@@ -421,4 +428,85 @@ public class Logic2VampireLanguageMapper_Support {
     };

     return ObjectExtensions.<HashMap<Variable, VLSVariable>>operator_doubleArrow(_hashMap, _function);

   }

+  

+  public String makeForm(final String formula, final BackendSolver solver, final int time) {

+    String _header = this.getHeader();

+    String _plus = (_header + formula);

+    String _addOptions = this.addOptions();

+    String _plus_1 = (_plus + _addOptions);

+    String _addSolver = this.addSolver(solver, time);

+    String _plus_2 = (_plus_1 + _addSolver);

+    String _addEnd = this.addEnd();

+    return (_plus_2 + _addEnd);

+  }

+  

+  public ArrayList<String> getSolverSpecs(final BackendSolver solver) {

+    if (solver != null) {

+      switch (solver) {

+        case CVC4:

+          return CollectionLiterals.<String>newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT");

+        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");

+        case GEOIII:

+          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:

+          return CollectionLiterals.<String>newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s");

+        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");

+        default:

+          break;

+      }

+    }

+    return null;

+  }

+  

+  public String getHeader() {

+    return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"ProblemSource\"\r\n\r\nFORMULAE\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"FORMULAEProblem\"\r\n\r\n\r\n";

+  }

+  

+  public String addSpec(final String spec) {

+    return spec.replace("\n", "\\r\\n");

+  }

+  

+  public String addOptions() {

+    return "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"QuietFlag\"\r\n\r\n-q3\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"SubmitButton\"\r\n\r\nRunSelectedSystems\r\n";

+  }

+  

+  public String addSolver(final BackendSolver solver, final int time) {

+    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) + 

+      "\"\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");

+  }

+  

+  public String addEnd() {

+    return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--";

+  }

+  

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

+      "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", 

+      "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent", 

+      "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36").addHeader("Accept", 

+      "text/html,application/xhtml+xml,application/xmlq=0.9,image/webp,image/apng,*/*q=0.8,application/signed-exchangev=b3").addHeader("Referer", "http://tptp.cs.miami.edu/cgi-bin/SystemOnTPTP").addHeader("Accept-Encoding", 

+      "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", 

+      "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", 

+      "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build();

+    final Response response = client.newCall(request).execute();

+    return CollectionLiterals.<String>newArrayList(response.body().string().split("\n"));

+  }

 }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
index fcbdfde7..e32530cb 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
@@ -41,7 +41,7 @@ public class VampireHandler {
       long startTime = (-((long) 1));

       long solverTime = (-((long) 1));

       Process p = null;

-      boolean _equals = Objects.equal(configuration.solver, BackendSolver.VAMP);

+      boolean _equals = Objects.equal(configuration.solver, BackendSolver.VAMPIRE);

       if (_equals) {

         String OPTION = " --mode casc_sat ";

         if ((configuration.runtimeLimit != (-1))) {