5 files changed, 196 insertions, 39 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
index 4e9737cb..4c2f1952 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
@@ -2,21 +2,29 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner
 
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
 
-class VampireSolverConfiguration extends LogicSolverConfiguration {
+class VampireSolverConfiguration
+ extends LogicSolverConfiguration {
         
         public var int contCycleLevel = 0
         public var boolean uniquenessDuplicates = false
         public var int iteration = -1
-        public var BackendSolver solver = BackendSolver::VAMP
+        public var BackendSolver solver = BackendSolver::VAMPIRE
         public var genModel = true
+        public var server = false
         //choose needed backend solver
 //      public var VampireBackendSolver solver = VampireBackendSolver.SAT4J
 }
 
 
 enum BackendSolver {
-        VAMP,
-        CVC4
+        CVC4,
+        DARWINFM,
+        EDARWIN,
+        GEOIII,
+        IPROVER,
+        PARADOX,
+        VAMPIRE,
+        Z3
         //add needed things
 }
 
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) {
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
index 39862c65..a9516cc4 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
@@ -40,7 +40,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                 // Equals the number of elements in te initial model

                 var elemsInIM = trace.definedElement2String.size

                 val ABSOLUTE_MIN = 0

-                val ABSOLUTE_MAX = -1-elemsInIM

+                val ABSOLUTE_MAX = Integer.MAX_VALUE-elemsInIM

 //              var elemsInIM = 0

 //              

 //              for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) {

@@ -60,7 +60,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 

                 // Handling Minimum_General

                 if (GLOBAL_MIN != ABSOLUTE_MIN) {

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

+                        getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, consistant)//may make not consistent here 

                         if (consistant) {

                                 for (i : trace.uniqueInstances) {

                                         localInstances.add(support.duplicate(i))

@@ -73,7 +73,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 

                 // Handling Maximum_General

                 if (GLOBAL_MAX != ABSOLUTE_MAX) {

-                        getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant)

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

                         if (consistant) {

                                 makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null)

                         } else {

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 680213ab..7b1c7d9a 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
@@ -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.vampireLanguage.VLSConstant
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm
@@ -16,6 +17,12 @@ import java.util.ArrayList
 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 static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
@@ -77,13 +84,13 @@ class Logic2VampireLanguageMapper_Support {
                         it.terms += duplicate(v)
                 ]
         }
-        
+
         def protected List<VLSVariable> duplicate(List<VLSVariable> vars) {
-                        var newList = newArrayList
-                        for (v : vars) {
-                                newList.add(duplicate(v))
-                        }
-                        return newList
+                var newList = newArrayList
+                for (v : vars) {
+                        newList.add(duplicate(v))
+                }
+                return newList
         }
 
         def protected VLSConstant toConstant(VLSFunctionAsTerm term) {
@@ -117,7 +124,7 @@ class Logic2VampireLanguageMapper_Support {
 
 // TODO Make more general
         def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) {
-                
+
 //              OLD
 //              val List<VLSInequality> eqs = newArrayList
 //              for (t1 : terms.subList(1, terms.length)) {
@@ -133,7 +140,6 @@ class Logic2VampireLanguageMapper_Support {
 //              }
 //              return unfoldAnd(eqs)
 //              END OLD
-
                 val List<VLSInequality> eqs = newArrayList
                 for (t1 : terms) {
                         if (t1 != t2) {
@@ -257,7 +263,8 @@ class Logic2VampireLanguageMapper_Support {
                         }
                 }
         }
-        //TODO rewrite such that it uses "listSubTypes"
+
+        // TODO rewrite such that it uses "listSubTypes"
         def protected boolean dfsSubtypeCheck(Type type, Type type2) {
                 // There is surely a better way to do this
                 if (type.subtypes.isEmpty)
@@ -284,4 +291,74 @@ class Logic2VampireLanguageMapper_Support {
                 new HashMap(map1) => [putAll(map2)]
         }
 
+        // SERVERS
+        def makeForm(String formula, BackendSolver solver, int time) {
+                return header + formula + addOptions + addSolver(solver, time) + addEnd
+        }
+
+        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")
+                }
+        }
+
+        def 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"
+        }
+
+        def addSpec(String spec) {
+                return spec.replace("\n", "\\r\\n")
+        }
+
+        def 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"
+        }
+
+        def addSolver(BackendSolver solver, int time) {
+                val solverSpecs = getSolverSpecs(solver)
+                val ID = solverSpecs.get(0)
+                val cmd = solverSpecs.get(1)
+
+                return "------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"
+        }
+
+        def addEnd() {
+                return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--"
+        }
+
+        def sendPost(String formData) throws Exception {
+
+                val OkHttpClient client = new OkHttpClient.Builder().connectTimeout(350, TimeUnit.SECONDS).readTimeout(350, TimeUnit.SECONDS).build()
+
+                val MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA")
+                val RequestBody body = RequestBody.create(mediaType, formData)
+                val 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()
+
+                val Response response = client.newCall(request).execute()
+//              TimeUnit.SECONDS.sleep(5)
+                return newArrayList(response.body.string.split("\n"))
+//              return response.body.string
+        // case 1: 
+        }
+
 }
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
index 47eae807..6d301442 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
@@ -70,7 +70,7 @@ class VampireHandler {
                 var long startTime = -1 as long

                 var long solverTime = -1 as long

                 var Process p = null

-                if (configuration.solver == BackendSolver::VAMP) {

+                if (configuration.solver == BackendSolver::VAMPIRE) {

 

                         var OPTION = " --mode casc_sat "

                         if (configuration.runtimeLimit != -1) {