diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend')
| -rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend | 67 |
1 files changed, 67 insertions, 0 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend new file mode 100644 index 00000000..9c9e65b4 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend | |||
| @@ -0,0 +1,67 @@ | |||
| 1 | package ca.mcgill.ecse.dslreasoner.vampire.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 Vampire2LogicMapper { | ||
| 7 | } | ||
| 8 | // val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE | ||
| 9 | // | ||
| 10 | // public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, VampireSolutionModel vampireSolution, Logic2VampireLanguageMapperTrace trace, long transformationTime) { | ||
| 11 | // val models = vampireSolution.aswers.map[it.key].toList | ||
| 12 | // | ||
| 13 | // if(!monitoredAlloySolution.finishedBeforeTimeout) { | ||
| 14 | // return createInsuficientResourcesResult => [ | ||
| 15 | // it.problem = problem | ||
| 16 | // it.representation += models | ||
| 17 | // it.trace = trace | ||
| 18 | // it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
| 19 | // ] | ||
| 20 | // } else { | ||
| 21 | // if(models.last.satisfiable || requiredNumberOfSolution == -1) { | ||
| 22 | // return createModelResult => [ | ||
| 23 | // it.problem = problem | ||
| 24 | // it.representation += models | ||
| 25 | // it.trace = trace | ||
| 26 | // it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
| 27 | // ] | ||
| 28 | // } else { | ||
| 29 | // return createInconsistencyResult => [ | ||
| 30 | // it.problem = problem | ||
| 31 | // it.representation += models | ||
| 32 | // it.trace = trace | ||
| 33 | // it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
| 34 | // ] | ||
| 35 | // } | ||
| 36 | // } | ||
| 37 | // } | ||
| 38 | // | ||
| 39 | // def transformStatistics(MonitoredAlloySolution solution, long transformationTime) { | ||
| 40 | // createStatistics => [ | ||
| 41 | // it.transformationTime = transformationTime as int | ||
| 42 | // for(solutionIndex : 0..<solution.aswers.size) { | ||
| 43 | // val solutionTime = solution.aswers.get(solutionIndex).value | ||
| 44 | // it.entries+= createIntStatisticEntry => [ | ||
| 45 | // it.name = '''Answer«solutionIndex»Time''' | ||
| 46 | // it.value = solutionTime.intValue | ||
| 47 | // ] | ||
| 48 | // } | ||
| 49 | // it.entries+= createIntStatisticEntry => [ | ||
| 50 | // it.name = "Alloy2KodKodTransformationTime" | ||
| 51 | // it.value = solution.kodkodTime as int | ||
| 52 | // ] | ||
| 53 | // it.entries+= createIntStatisticEntry => [ | ||
| 54 | // it.name = "Alloy2KodKodTransformationTime" | ||
| 55 | // it.value = solution.kodkodTime as int | ||
| 56 | // ] | ||
| 57 | // it.entries+= createStringStatisticEntry => [ | ||
| 58 | // it.name = "warnings" | ||
| 59 | // it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]''' | ||
| 60 | // ] | ||
| 61 | // ] | ||
| 62 | // } | ||
| 63 | // | ||
| 64 | // def sum(Iterable<Long> ints) { | ||
| 65 | // ints.reduce[p1, p2|p1+p2] | ||
| 66 | // } | ||
| 67 | //} | ||