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 --- .../vampire/reasoner/VampireSolver.xtend | 116 +++++++++++++++++---- 1 file changed, 94 insertions(+), 22 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend') 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) { -- cgit v1.2.3-54-g00ecf