1 files changed, 148 insertions, 27 deletions

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