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 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
+class Alloy2LogicMapper {
+        val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
+        
+        public def transformOutput(LogicProblem problem, MonitoredAlloySolution solution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {
+                if(solution == null) {
+                        return createInsuficientResourcesResult => [
+                                it.problem = problem
+                                it.statistics = transformStatistics(solution,transformationTime)
+                        ]
+                } else {
+                        val logicResult = solution.solution
+                        if(logicResult.satisfiable) {
+                                return createModelResult => [
+                                        it.problem = problem
+                                        it.representation += solution
+                                        it.maxInteger = logicResult.max
+                                        it.minInteger = logicResult.min
+                                        it.trace = trace
+                                        it.statistics = transformStatistics(solution,transformationTime)
+                                ]
+                        } else {
+                                return createInconsistencyResult => [
+                                        it.problem = problem
+                                        //trace?
+                                        it.statistics = transformStatistics(solution,transformationTime)
+                                ]
+                        }
+                }
+        }
+        
+        def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {
+                createStatistics => [
+                        it.transformationTime = transformationTime as int
+                        if(solution != null) {
+                                it.solverTime = solution.runtimeTime as int
+                                it.entries += LogicresultFactory.eINSTANCE.createIntStatisticEntry => [
+                                        it.name = "KoodkodToCNFTransformationTime"
+                                        it.value = solution.getKodkodTime as int
+                                ]
+                        }
+                ]
+        }
+}
+\ No newline at end of file

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