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 | 48 |
1 files changed, 48 insertions, 0 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 new file mode 100644 index 00000000..637752b0 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend | |||
@@ -0,0 +1,48 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | ||
5 | |||
6 | class Alloy2LogicMapper { | ||
7 | val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE | ||
8 | |||
9 | public def transformOutput(LogicProblem problem, MonitoredAlloySolution solution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { | ||
10 | if(solution == null) { | ||
11 | return createInsuficientResourcesResult => [ | ||
12 | it.problem = problem | ||
13 | it.statistics = transformStatistics(solution,transformationTime) | ||
14 | ] | ||
15 | } else { | ||
16 | val logicResult = solution.solution | ||
17 | if(logicResult.satisfiable) { | ||
18 | return createModelResult => [ | ||
19 | it.problem = problem | ||
20 | it.representation += solution | ||
21 | it.maxInteger = logicResult.max | ||
22 | it.minInteger = logicResult.min | ||
23 | it.trace = trace | ||
24 | it.statistics = transformStatistics(solution,transformationTime) | ||
25 | ] | ||
26 | } else { | ||
27 | return createInconsistencyResult => [ | ||
28 | it.problem = problem | ||
29 | //trace? | ||
30 | it.statistics = transformStatistics(solution,transformationTime) | ||
31 | ] | ||
32 | } | ||
33 | } | ||
34 | } | ||
35 | |||
36 | def transformStatistics(MonitoredAlloySolution solution, long transformationTime) { | ||
37 | createStatistics => [ | ||
38 | it.transformationTime = transformationTime as int | ||
39 | if(solution != null) { | ||
40 | it.solverTime = solution.runtimeTime as int | ||
41 | it.entries += LogicresultFactory.eINSTANCE.createIntStatisticEntry => [ | ||
42 | it.name = "KoodkodToCNFTransformationTime" | ||
43 | it.value = solution.getKodkodTime as int | ||
44 | ] | ||
45 | } | ||
46 | ] | ||
47 | } | ||
48 | } \ No newline at end of file | ||