From 60f01f46ba232ed6416054f0a6115cb2a9b70b4e Mon Sep 17 00:00:00 2001
From: OszkarSemerath <oszka@152.66.252.189>
Date: Sat, 10 Jun 2017 19:05:05 +0200
Subject: Migrating Additional projects

---
 .../dslreasoner/smt/reasoner/Smt2LogicMapper.xtend | 71 ++++++++++++++++++++++
 1 file changed, 71 insertions(+)
 create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Smt2LogicMapper.xtend

(limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Smt2LogicMapper.xtend')

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 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner
+
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOutput
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticsSection
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticIntValue
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticDoubleValue
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTErrorResult
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSatResult
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTUnsupportedResult
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticValue
+import java.math.BigDecimal
+
+class Smt2LogicMapper {
+	val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
+	
+	public def transformOutput(LogicProblem problem, SMTOutput output, Logic2SmtMapperTrace trace, long transformationTime, long solverTime) {
+		val satResult = output.satResult
+		if(satResult === null) { // Timeout
+			return createInsuficientResourcesResult => [ init(problem,output,transformationTime,solverTime) it.resourceName = "time"]
+		} else {
+			if(satResult instanceof SMTErrorResult) {
+				return createErrorResult => [init(problem,output,transformationTime,solverTime) message = satResult.message]
+			} else if(satResult instanceof SMTUnsupportedResult) {
+				return createUndecidableResult => [init(problem,output,transformationTime,solverTime)]
+			} else if(satResult instanceof SMTSatResult) {
+				if(satResult.sat) {
+					return createModelResult => [
+						init(problem,output,transformationTime,solverTime)
+						representation += output.eContainer
+						it.trace = trace
+					]
+				} else if(satResult.unsat) {
+					return createInconsistencyResult => [init(problem,output,transformationTime,solverTime)]
+				} else if(satResult.unknown) {
+					return createUndecidableResult => [init(problem,output,transformationTime,solverTime)]	
+				}
+			} else throw new LogicReasonerException("The solver resulted with unknown result.")
+		}
+	}
+	
+	private def init(LogicResult result,LogicProblem problem, SMTOutput output, long transformationTime, long solverTime) {
+		result.problem = problem
+		result.statistics = output.statistics.transformStatistics(transformationTime,solverTime)
+	}
+	
+	protected def transformStatistics(SMTStatisticsSection section, long transformationTime, long solverTime) {
+		createStatistics => [
+			it.transformationTime = transformationTime.intValue
+			it.solverTime = solverTime.intValue
+			
+			val memorySection = section.values.filter[it.name==":memory"].head
+			if(memorySection != null) {
+				it.solverMemory = ((memorySection as SMTStatisticDoubleValue).value.add(BigDecimal.valueOf(0.5))).intValue
+			}
+			entries += section.values.map[transformEntry]
+		]
+	}
+	
+	protected def dispatch transformEntry(SMTStatisticIntValue entry) {
+		createIntStatisticEntry => [name = entry.exportName value = entry.value] }
+	protected def dispatch transformEntry(SMTStatisticDoubleValue entry) {
+		createRealStatisticEntry => [name = entry.exportName value = entry.value.doubleValue] }
+	
+	private def exportName(SMTStatisticValue value) {
+		return value.name.replaceFirst(":","")
+	}
+}
\ No newline at end of file
-- 
cgit v1.2.3-54-g00ecf