diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend | 50 |
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 | |||
6 | class Alloy2LogicMapper { | 6 | class Alloy2LogicMapper { |
7 | val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE | 7 | val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE |
8 | 8 | ||
9 | public def transformOutput(LogicProblem problem, MonitoredAlloySolution solution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { | 9 | public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { |
10 | if(solution == null) { | 10 | val models = monitoredAlloySolution.aswers.map[it.key].toList |
11 | |||
12 | if(monitoredAlloySolution.finishedBeforeTimeout) { | ||
11 | return createInsuficientResourcesResult => [ | 13 | return createInsuficientResourcesResult => [ |
12 | it.problem = problem | 14 | it.problem = problem |
13 | it.statistics = transformStatistics(solution,transformationTime) | 15 | it.representation += models |
16 | it.trace = trace | ||
17 | it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
14 | ] | 18 | ] |
15 | } else { | 19 | } else { |
16 | val logicResult = solution.solution | 20 | if(models.last.satisfiable || requiredNumberOfSolution == -1) { |
17 | if(logicResult.satisfiable) { | ||
18 | return createModelResult => [ | 21 | return createModelResult => [ |
19 | it.problem = problem | 22 | it.problem = problem |
20 | it.representation += solution | 23 | it.representation += models |
21 | it.maxInteger = logicResult.max | ||
22 | it.minInteger = logicResult.min | ||
23 | it.trace = trace | 24 | it.trace = trace |
24 | it.statistics = transformStatistics(solution,transformationTime) | 25 | it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) |
25 | ] | 26 | ] |
26 | } else { | 27 | } else { |
27 | return createInconsistencyResult => [ | 28 | return createInconsistencyResult => [ |
28 | it.problem = problem | 29 | it.problem = problem |
29 | //trace? | 30 | it.representation += models |
30 | it.statistics = transformStatistics(solution,transformationTime) | 31 | it.trace = trace |
32 | it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
31 | ] | 33 | ] |
32 | } | 34 | } |
33 | } | 35 | } |
@@ -36,13 +38,29 @@ class Alloy2LogicMapper { | |||
36 | def transformStatistics(MonitoredAlloySolution solution, long transformationTime) { | 38 | def transformStatistics(MonitoredAlloySolution solution, long transformationTime) { |
37 | createStatistics => [ | 39 | createStatistics => [ |
38 | it.transformationTime = transformationTime as int | 40 | it.transformationTime = transformationTime as int |
39 | if(solution != null) { | 41 | for(solutionIndex : 0..<solution.aswers.size) { |
40 | it.solverTime = solution.runtimeTime as int | 42 | val solutionTime = solution.aswers.get(solutionIndex).value |
41 | it.entries += LogicresultFactory.eINSTANCE.createIntStatisticEntry => [ | 43 | it.entries+= createIntStatisticEntry => [ |
42 | it.name = "KoodkodToCNFTransformationTime" | 44 | it.name = '''Answer«solutionIndex»Time''' |
43 | it.value = solution.getKodkodTime as int | 45 | it.value = solutionTime.intValue |
44 | ] | 46 | ] |
45 | } | 47 | } |
48 | it.entries+= createIntStatisticEntry => [ | ||
49 | it.name = "Alloy2KodKodTransformationTime" | ||
50 | it.value = solution.kodkodTime as int | ||
51 | ] | ||
52 | it.entries+= createIntStatisticEntry => [ | ||
53 | it.name = "Alloy2KodKodTransformationTime" | ||
54 | it.value = solution.kodkodTime as int | ||
55 | ] | ||
56 | it.entries+= createStringStatisticEntry => [ | ||
57 | it.name = "warnings" | ||
58 | it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]''' | ||
59 | ] | ||
46 | ] | 60 | ] |
47 | } | 61 | } |
62 | |||
63 | def sum(Iterable<Long> ints) { | ||
64 | ints.reduce[p1, p2|p1+p2] | ||
65 | } | ||
48 | } \ No newline at end of file | 66 | } \ No newline at end of file |