blob: a0084204771559fcd790d2799b957ac0843d67d9 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
|
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,
MonitoredVampireSolution monitoredVampireSolution, Logic2VampireLanguageMapperTrace trace,
long transformationTime) {
// ModelRsult implements LogicResult
return createModelResult => [
it.problem = problem
it.representation += monitoredVampireSolution.generatedModel
it.trace = trace
it.statistics = transformStatistics(monitoredVampireSolution, transformationTime)
]
}
def transformStatistics(MonitoredVampireSolution solution, long transformationTime) {
return createStatistics
// 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»]'''
// ]
// ]
}
}
|
