aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2020-06-13 19:24:25 -0400
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2020-06-13 19:24:25 -0400
commit022a1e52e0cf20f64d9cd6685c65d945c04eaecc (patch)
treec281cd871d008ae63640fbdd9ff5739e273cb224 /Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
parentMerge branch 'Vampire-New' into Vampire-New (diff)
downloadVIATRA-Generator-022a1e52e0cf20f64d9cd6685c65d945c04eaecc.tar.gz
VIATRA-Generator-022a1e52e0cf20f64d9cd6685c65d945c04eaecc.tar.zst
VIATRA-Generator-022a1e52e0cf20f64d9cd6685c65d945c04eaecc.zip
remove Alloy solver copy
Diffstat (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend')
-rw-r--r--Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend66
1 files changed, 0 insertions, 66 deletions
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
deleted file mode 100644
index 09b67599..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
+++ /dev/null
@@ -1,66 +0,0 @@
1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
2
3import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
4import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
5
6class Alloy2LogicMapper {
7 val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
8
9 public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {
10 val models = monitoredAlloySolution.aswers.map[it.key].toList
11
12 if(!monitoredAlloySolution.finishedBeforeTimeout) {
13 return createInsuficientResourcesResult => [
14 it.problem = problem
15 it.representation += models
16 it.trace = trace
17 it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
18 ]
19 } else {
20 if(models.last.satisfiable || requiredNumberOfSolution == -1) {
21 return createModelResult => [
22 it.problem = problem
23 it.representation += models
24 it.trace = trace
25 it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
26 ]
27 } else {
28 return createInconsistencyResult => [
29 it.problem = problem
30 it.representation += models
31 it.trace = trace
32 it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
33 ]
34 }
35 }
36 }
37
38 def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {
39 createStatistics => [
40 it.transformationTime = transformationTime as int
41 for(solutionIndex : 0..<solution.aswers.size) {
42 val solutionTime = solution.aswers.get(solutionIndex).value
43 it.entries+= createIntStatisticEntry => [
44 it.name = '''Answer«solutionIndex»Time'''
45 it.value = solutionTime.intValue
46 ]
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 ]
60 ]
61 }
62
63 def sum(Iterable<Long> ints) {
64 ints.reduce[p1, p2|p1+p2]
65 }
66} \ No newline at end of file