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 | //} | ||