1 files changed, 60 insertions, 59 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
index 5cb0198e..9c9e65b4 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
@@ -4,63 +4,64 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
 class Vampire2LogicMapper {
-        val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
-        
-        public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, VampireSolutionModel vampireSolution, Logic2VampireLanguageMapperTrace trace, long transformationTime) {
-                val models = vampireSolution.aswers.map[it.key].toList
-                
-                if(!monitoredAlloySolution.finishedBeforeTimeout) {
-                        return createInsuficientResourcesResult => [
-                                it.problem = problem
-                                it.representation += models
-                                it.trace = trace
-                                it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
-                        ]
-                } else {
-                        if(models.last.satisfiable || requiredNumberOfSolution == -1) {
-                                return createModelResult => [
-                                        it.problem = problem
-                                        it.representation += models
-                                        it.trace = trace
-                                        it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
-                                ]
-                        } else {
-                                return createInconsistencyResult => [
-                                        it.problem = problem
-                                        it.representation += models
-                                        it.trace = trace
-                                        it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
-                                ]
-                        }
-                }
-        }
-        
-        def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {
-                createStatistics => [
-                        it.transformationTime = transformationTime as int
-                        for(solutionIndex : 0..<solution.aswers.size) {
-                                val solutionTime = solution.aswers.get(solutionIndex).value
-                                 it.entries+= createIntStatisticEntry => [
-                                        it.name = '''Answer«solutionIndex»Time'''
-                                        it.value = solutionTime.intValue
-                                ]
-                        }
-                        it.entries+= createIntStatisticEntry => [
-                                it.name = "Alloy2KodKodTransformationTime"
-                                it.value = solution.kodkodTime as int
-                        ]
-                        it.entries+= createIntStatisticEntry => [
-                                it.name = "Alloy2KodKodTransformationTime"
-                                it.value = solution.kodkodTime as int
-                        ]
-                        it.entries+= createStringStatisticEntry => [
-                                it.name = "warnings"
-                                it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]'''
-                        ]
-                ]
-        }
-        
-        def sum(Iterable<Long> ints) {
-                ints.reduce[p1, p2|p1+p2]
-        }
 }
+//      val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
+//      
+//      public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, VampireSolutionModel vampireSolution, Logic2VampireLanguageMapperTrace trace, long transformationTime) {
+//              val models = vampireSolution.aswers.map[it.key].toList
+//              
+//              if(!monitoredAlloySolution.finishedBeforeTimeout) {
+//                      return createInsuficientResourcesResult => [
+//                              it.problem = problem
+//                              it.representation += models
+//                              it.trace = trace
+//                              it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
+//                      ]
+//              } else {
+//                      if(models.last.satisfiable || requiredNumberOfSolution == -1) {
+//                              return createModelResult => [
+//                                      it.problem = problem
+//                                      it.representation += models
+//                                      it.trace = trace
+//                                      it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
+//                              ]
+//                      } else {
+//                              return createInconsistencyResult => [
+//                                      it.problem = problem
+//                                      it.representation += models
+//                                      it.trace = trace
+//                                      it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
+//                              ]
+//                      }
+//              }
+//      }
+//      
+//      def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {
+//              createStatistics => [
+//                      it.transformationTime = transformationTime as int
+//                      for(solutionIndex : 0..<solution.aswers.size) {
+//                              val solutionTime = solution.aswers.get(solutionIndex).value
+//                               it.entries+= createIntStatisticEntry => [
+//                                      it.name = '''Answer«solutionIndex»Time'''
+//                                      it.value = solutionTime.intValue
+//                              ]
+//                      }
+//                      it.entries+= createIntStatisticEntry => [
+//                              it.name = "Alloy2KodKodTransformationTime"
+//                              it.value = solution.kodkodTime as int
+//                      ]
+//                      it.entries+= createIntStatisticEntry => [
+//                              it.name = "Alloy2KodKodTransformationTime"
+//                              it.value = solution.kodkodTime as int
+//                      ]
+//                      it.entries+= createStringStatisticEntry => [
+//                              it.name = "warnings"
+//                              it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]'''
+//                      ]
+//              ]
+//      }
+//      
+//      def sum(Iterable<Long> ints) {
+//              ints.reduce[p1, p2|p1+p2]
+//      }
+//}