From 2c05097ccbeeadd70b20f5001ebeb22ffdc465de Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Mon, 4 Mar 2019 17:31:16 -0500 Subject: Begin handing of scope and fix type definitions. --- .../vampire/reasoner/VampireSolver.xtend | 101 +++++++++++---------- 1 file changed, 51 insertions(+), 50 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 cbe53bff..ee802a99 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 @@ -7,6 +7,7 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage +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 @@ -14,80 +15,81 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace -class VampireSolver extends LogicReasoner{ - +class VampireSolver extends LogicReasoner { + new() { VampireLanguagePackage.eINSTANCE.eClass val x = new VampireLanguageStandaloneSetupGenerated VampireLanguageStandaloneSetup::doSetup() } - - val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes) - val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper - val VampireHandler handler = new VampireHandler - - - val fileName = "vampireProblem.tptp" - - override solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace) throws LogicReasonerException { + + val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper( + new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes) + val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper + val VampireHandler handler = new VampireHandler + + val fileName = "vampireProblem.tptp" + + override solve(LogicProblem problem, LogicSolverConfiguration config, + ReasonerWorkspace workspace) throws LogicReasonerException { val vampireConfig = config.asConfig - + // Start: Logic -> Vampire mapping val transformationStart = System.currentTimeMillis - //TODO - val result = forwardMapper.transformProblem(problem,vampireConfig) + // TODO + val result = forwardMapper.transformProblem(problem, vampireConfig) val vampireProblem = result.output val forwardTrace = result.trace - + var String fileURI = null; var String vampireCode = null; - vampireCode = workspace.writeModelToString(vampireProblem,fileName) - if(vampireConfig.writeToFile) { - fileURI = workspace.writeModel(vampireProblem,fileName).toFileString + vampireCode = workspace.writeModelToString(vampireProblem, fileName) + + val writeFile = ( + vampireConfig.documentationLevel === DocumentationLevel::NORMAL || + vampireConfig.documentationLevel === DocumentationLevel::FULL) + if (writeFile) { + fileURI = workspace.writeModel(vampireProblem, fileName).toFileString } - - //Result as String - + // Result as String val transformationTime = System.currentTimeMillis - transformationStart // Finish: Logic -> Vampire mapping - - /* - // Start: Solving Alloy problem - val solverStart = System.currentTimeMillis - //Calling Solver (Currently Manually) - val result2 = handler.callSolver(vampireProblem,workspace,vampireConfig,vampireCode) -// val result2 = null - //TODO - //Backwards Mapper - val logicResult = backwardMapper.transformOutput(problem,config.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) - - val solverFinish = System.currentTimeMillis-solverStart - // Finish: Solving Alloy problem - - if(vampireConfig.writeToFile) workspace.deactivateModel(fileName) - - return logicResult - - /*/ + * // Start: Solving Alloy problem + * val solverStart = System.currentTimeMillis + * //Calling Solver (Currently Manually) + * val result2 = handler.callSolver(vampireProblem,workspace,vampireConfig,vampireCode) + * // val result2 = null + * //TODO + * //Backwards Mapper + * val logicResult = backwardMapper.transformOutput(problem,config.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) + * + * val solverFinish = System.currentTimeMillis-solverStart + * // Finish: Solving Alloy problem + * + * if(vampireConfig.writeToFile) workspace.deactivateModel(fileName) + * + * return logicResult + * + /*/ return null // for now - //*/ + // */ } - - def asConfig(LogicSolverConfiguration configuration){ - if(configuration instanceof VampireSolverConfiguration) { + + def asConfig(LogicSolverConfiguration configuration) { + if (configuration instanceof VampireSolverConfiguration) { return configuration } else { - throw new IllegalArgumentException('''The configuration have to be an «VampireSolverConfiguration.simpleName»!''') + throw new IllegalArgumentException('''The configuration have to be an «VampireSolverConfiguration.simpleName»!''') } } - + // /* // * not for now // * override getInterpretations(ModelResult modelResult) { - //val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] + // val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] // val sols = modelResult.representation// as List // //val res = answers.map // sols.map[ @@ -98,7 +100,6 @@ class VampireSolver extends LogicReasoner{ // modelResult.trace as Logic2AlloyLanguageMapperTrace // ) // ] - } + } // */ - -} \ No newline at end of file +} -- cgit v1.2.3-54-g00ecf