1 files changed, 94 insertions, 22 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 85b81a8c..31aa091c 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
@@ -4,18 +4,20 @@ import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup
 import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated
 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 ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+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.workspace.ReasonerWorkspace
 
@@ -30,18 +32,20 @@ class VampireSolver extends LogicReasoner {
         val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper
         val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
         val VampireHandler handler = new VampireHandler
+        val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
+        val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
+        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
 
 //      var fileName = "problem.tptp"
-
 //      def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) {
 //              fileName = location + fileName
 //              solve(problem, config, workspace)
 //      }
-
         override solve(LogicProblem problem, LogicSolverConfiguration config,
                 ReasonerWorkspace workspace) throws LogicReasonerException {
                 val vampireConfig = config.asConfig
-                var fileName = "problem_" + vampireConfig.typeScopes.minNewElements + "-" + vampireConfig.typeScopes.maxNewElements + ".tptp"
+                var fileName = "problem_" + vampireConfig.typeScopes.minNewElements + "-" +
+                        vampireConfig.typeScopes.maxNewElements + ".tptp"
 
                 // Start: Logic -> Vampire mapping
                 val transformationStart = System.currentTimeMillis
@@ -55,8 +59,6 @@ class VampireSolver extends LogicReasoner {
                 var String fileURI = null;
                 var String vampireCode = null;
                 vampireCode = workspace.writeModelToString(vampireProblem, fileName)
-                
-                
 
                 val writeFile = (
                         vampireConfig.documentationLevel === DocumentationLevel::NORMAL ||
@@ -73,24 +75,94 @@ class VampireSolver extends LogicReasoner {
 //              println(model)
                 // Finish: Logic -> Vampire mapping
                 if (vampireConfig.genModel) {
-
-                        // Start: Solving .tptp problem
-                        val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig)
-                        // Finish: Solving .tptp problem
-                        // Start: Vampire -> Logic mapping
-                        val backTransformationStart = System.currentTimeMillis
-                        // Backwards Mapper
-                        val logicResult = backwardMapper.transformOutput(problem,
-                                vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime)
-
-                        val backTransformationTime = System.currentTimeMillis - backTransformationStart
-                        // Finish: Vampire -> Logic Mapping
+                        if (vampireConfig.server) {
+                                val form = support.makeForm(vampireCode, vampireConfig.solver, vampireConfig.runtimeLimit)
+                                var response = newArrayList
+                                var ind = 0
+                                var done = false
+                                print(" ")
+                                while (!done) {
+                                        print("(x)")
+                                        done = false
+                                        response = support.sendPost(form)
+
+                                        var responseFound = false
+                                        ind = 0
+                                        while (!responseFound) {
+                                                var line = response.get(ind)
+                                                if (line.length >= 5 && line.substring(0, 5) == "ERROR") {
+                                                        done = false
+                                                        responseFound = true
+                                                } else {
+                                                        if (line == "</PRE>") {
+                                                                done = true
+                                                                responseFound = true
+                                                        }
+                                                }
+                                                ind++
+                                        }
+                                }
+                                val satRaw = response.get(ind - 3)
+                                val modRaw = response.get(ind - 2)
+
+                                val sat = newArrayList(satRaw.split(" "))
+                                val mod = newArrayList(modRaw.split(" "))
+
+                                val satOut = sat.get(1)
+                                val modOut = mod.get(1)
+                                val satTime = sat.get(2)
+                                val modTime = mod.get(2)
+
+                                println()
+                                println(sat)
+                                println(mod)
+
+                                return createModelResult => [
+                                        it.problem = null
+                                        it.representation += createVampireModel => []
+                                        it.trace = trace
+                                        it.statistics = createStatistics => [
+                                                it.transformationTime = transformationTime as int
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "satOut"
+                                                        it.value = satOut
+                                                ]
+                                                it.entries += createRealStatisticEntry => [
+                                                        it.name = "satTime"
+                                                        it.value = Double.parseDouble(satTime)
+                                                ]
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "modOut"
+                                                        it.value = modOut
+                                                ]
+                                                it.entries += createRealStatisticEntry => [
+                                                        it.name = "modTime"
+                                                        it.value = Double.parseDouble(modTime)
+                                                ]
+
+                                        ]
+                                ]
+
+//                              return newArrayList(line1, line2)
+                        } else {
+
+                                // Start: Solving .tptp problem
+                                val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig)
+                                // Finish: Solving .tptp problem
+                                // Start: Vampire -> Logic mapping
+                                val backTransformationStart = System.currentTimeMillis
+                                // Backwards Mapper
+                                val logicResult = backwardMapper.transformOutput(problem,
+                                        vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime)
+
+                                val backTransformationTime = System.currentTimeMillis - backTransformationStart
+                                // Finish: Vampire -> Logic Mapping
 //              print(vampSol.generatedModel.tfformulas.size)
-                        return logicResult // currently only a ModelResult
+                                return logicResult // currently only a ModelResult
+                        }
                 }
-                
-                return backwardMapper.transformOutput(problem,
-                                vampireConfig.solutionScope.numberOfRequiredSolution, new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime)
+                return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution,
+                        new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime)
         }
 
         def asConfig(LogicSolverConfiguration configuration) {