diff options
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Smt2LogicMapper.xtend')
-rw-r--r-- | Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Smt2LogicMapper.xtend | 71 |
1 files changed, 71 insertions, 0 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Smt2LogicMapper.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Smt2LogicMapper.xtend new file mode 100644 index 00000000..cbabc7b0 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Smt2LogicMapper.xtend | |||
@@ -0,0 +1,71 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOutput | ||
4 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticsSection | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | ||
6 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticIntValue | ||
7 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticDoubleValue | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
9 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTErrorResult | ||
10 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSatResult | ||
11 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTUnsupportedResult | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | ||
14 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticValue | ||
15 | import java.math.BigDecimal | ||
16 | |||
17 | class Smt2LogicMapper { | ||
18 | val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE | ||
19 | |||
20 | public def transformOutput(LogicProblem problem, SMTOutput output, Logic2SmtMapperTrace trace, long transformationTime, long solverTime) { | ||
21 | val satResult = output.satResult | ||
22 | if(satResult === null) { // Timeout | ||
23 | return createInsuficientResourcesResult => [ init(problem,output,transformationTime,solverTime) it.resourceName = "time"] | ||
24 | } else { | ||
25 | if(satResult instanceof SMTErrorResult) { | ||
26 | return createErrorResult => [init(problem,output,transformationTime,solverTime) message = satResult.message] | ||
27 | } else if(satResult instanceof SMTUnsupportedResult) { | ||
28 | return createUndecidableResult => [init(problem,output,transformationTime,solverTime)] | ||
29 | } else if(satResult instanceof SMTSatResult) { | ||
30 | if(satResult.sat) { | ||
31 | return createModelResult => [ | ||
32 | init(problem,output,transformationTime,solverTime) | ||
33 | representation += output.eContainer | ||
34 | it.trace = trace | ||
35 | ] | ||
36 | } else if(satResult.unsat) { | ||
37 | return createInconsistencyResult => [init(problem,output,transformationTime,solverTime)] | ||
38 | } else if(satResult.unknown) { | ||
39 | return createUndecidableResult => [init(problem,output,transformationTime,solverTime)] | ||
40 | } | ||
41 | } else throw new LogicReasonerException("The solver resulted with unknown result.") | ||
42 | } | ||
43 | } | ||
44 | |||
45 | private def init(LogicResult result,LogicProblem problem, SMTOutput output, long transformationTime, long solverTime) { | ||
46 | result.problem = problem | ||
47 | result.statistics = output.statistics.transformStatistics(transformationTime,solverTime) | ||
48 | } | ||
49 | |||
50 | protected def transformStatistics(SMTStatisticsSection section, long transformationTime, long solverTime) { | ||
51 | createStatistics => [ | ||
52 | it.transformationTime = transformationTime.intValue | ||
53 | it.solverTime = solverTime.intValue | ||
54 | |||
55 | val memorySection = section.values.filter[it.name==":memory"].head | ||
56 | if(memorySection != null) { | ||
57 | it.solverMemory = ((memorySection as SMTStatisticDoubleValue).value.add(BigDecimal.valueOf(0.5))).intValue | ||
58 | } | ||
59 | entries += section.values.map[transformEntry] | ||
60 | ] | ||
61 | } | ||
62 | |||
63 | protected def dispatch transformEntry(SMTStatisticIntValue entry) { | ||
64 | createIntStatisticEntry => [name = entry.exportName value = entry.value] } | ||
65 | protected def dispatch transformEntry(SMTStatisticDoubleValue entry) { | ||
66 | createRealStatisticEntry => [name = entry.exportName value = entry.value.doubleValue] } | ||
67 | |||
68 | private def exportName(SMTStatisticValue value) { | ||
69 | return value.name.replaceFirst(":","") | ||
70 | } | ||
71 | } \ No newline at end of file | ||