blob: 637752b05886660c0c253d8ce37e61cd2204925b (
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
|
package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
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) {
if(solution == null) {
return createInsuficientResourcesResult => [
it.problem = problem
it.statistics = transformStatistics(solution,transformationTime)
]
} else {
val logicResult = solution.solution
if(logicResult.satisfiable) {
return createModelResult => [
it.problem = problem
it.representation += solution
it.maxInteger = logicResult.max
it.minInteger = logicResult.min
it.trace = trace
it.statistics = transformStatistics(solution,transformationTime)
]
} else {
return createInconsistencyResult => [
it.problem = problem
//trace?
it.statistics = transformStatistics(solution,transformationTime)
]
}
}
}
def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {
createStatistics => [
it.transformationTime = transformationTime as int
if(solution != null) {
it.solverTime = solution.runtimeTime as int
it.entries += LogicresultFactory.eINSTANCE.createIntStatisticEntry => [
it.name = "KoodkodToCNFTransformationTime"
it.value = solution.getKodkodTime as int
]
}
]
}
}
|
