Fix FAM Test. Begin Grammar Fix.

1 files changed, 66 insertions, 0 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
new file mode 100644
index 00000000..5cb0198e
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
@@ -0,0 +1,66 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder

+

+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]

+        }

+}