1 files changed, 34 insertions, 16 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
index 637752b0..7db9e0ea 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
@@ -6,28 +6,30 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
 class Alloy2LogicMapper {
        val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
        
-        public def transformOutput(LogicProblem problem, MonitoredAlloySolution solution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {
+        public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {
-                if(solution == null) {
+                val models = monitoredAlloySolution.aswers.map[it.key].toList
+                
+                if(monitoredAlloySolution.finishedBeforeTimeout) {
                        return createInsuficientResourcesResult => [
                                it.problem = problem
-                                it.statistics = transformStatistics(solution,transformationTime)
+                                it.representation += models
+                                it.trace = trace
+                                it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
                        ]
                } else {
-                        val logicResult = solution.solution
+                        if(models.last.satisfiable || requiredNumberOfSolution == -1) {
-                        if(logicResult.satisfiable) {
                                return createModelResult => [
                                        it.problem = problem
-                                        it.representation += solution
+                                        it.representation += models
-                                        it.maxInteger = logicResult.max
-                                        it.minInteger = logicResult.min
                                        it.trace = trace
-                                        it.statistics = transformStatistics(solution,transformationTime)
+                                        it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
                                ]
                        } else {
                                return createInconsistencyResult => [
                                        it.problem = problem
-                                        //trace?
+                                        it.representation += models
-                                        it.statistics = transformStatistics(solution,transformationTime)
+                                        it.trace = trace
+                                        it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
                                ]
                        }
                }
@@ -36,13 +38,29 @@ class Alloy2LogicMapper {
        def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {
                createStatistics => [
                        it.transformationTime = transformationTime as int
-                        if(solution != null) {
+                        for(solutionIndex : 0..<solution.aswers.size) {
-                                it.solverTime = solution.runtimeTime as int
+                                val solutionTime = solution.aswers.get(solutionIndex).value
-                                it.entries += LogicresultFactory.eINSTANCE.createIntStatisticEntry => [
+                                 it.entries+= createIntStatisticEntry => [
-                                        it.name = "KoodkodToCNFTransformationTime"
+                                        it.name = '''Answer«solutionIndex»Time'''
-                                        it.value = solution.getKodkodTime as int
+                                        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]
+        }
 }
 \ No newline at end of file