1 files changed, 51 insertions, 50 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 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<A4Solution>
 //              //val res = answers.map 
 //              sols.map[
@@ -98,7 +100,6 @@ class VampireSolver extends LogicReasoner{
 //                              modelResult.trace as Logic2AlloyLanguageMapperTrace
 //                      )
 //              ]
-        }       
+        }
 //      */
-        
-}
\ No newline at end of file
+}