From 17d6aa5028bff14c80f0be6a042c6a68fe8b61b0 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Fri, 11 Oct 2019 15:51:49 -0400 Subject: VAMPIRE: complete testing setup --- .../reasoner/VampireAnalyzerConfiguration.xtend | 16 ++- .../vampire/reasoner/VampireSolver.xtend | 116 +++++++++++++++++---- .../Logic2VampireLanguageMapper_ScopeMapper.xtend | 6 +- .../Logic2VampireLanguageMapper_Support.xtend | 95 +++++++++++++++-- .../vampire/reasoner/builder/VampireHandler.xtend | 2 +- 5 files changed, 196 insertions(+), 39 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src') 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 == "") { + 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 duplicate(List 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 terms, VLSConstant t2) { - + // OLD // val List eqs = newArrayList // for (t1 : terms.subList(1, terms.length)) { @@ -133,7 +140,6 @@ class Logic2VampireLanguageMapper_Support { // } // return unfoldAnd(eqs) // END OLD - val List 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) { -- cgit v1.2.3-54-g00ecf