From f87b4233437f0900c19f462b5e443a3c81b27b6e Mon Sep 17 00:00:00 2001
From: ArenBabikian <aren.babikian@mail.mcgill.ca>
Date: Tue, 15 Jan 2019 12:44:33 -0500
Subject: Initial workspace setup

---
 .../vampire/reasoner/VampireSolver.xtend           | 102 +++++++++++++++++++++
 1 file changed, 102 insertions(+)
 create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend

(limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend')

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
new file mode 100644
index 00000000..64484b88
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
@@ -0,0 +1,102 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner
+
+import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage
+import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
+import java.io.PrintWriter
+import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes
+
+class VampireSolver extends LogicReasoner{
+	
+	new() {
+		VampireLanguagePackage.eINSTANCE.eClass
+		val x = new VampireLanguageStandaloneSetupGenerated
+		VampireLanguageStandaloneSetup::doSetup()
+	}
+	
+	 val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes)
+//	 //not for now
+//	 val VampireHandler handler = new VampireHandler
+//	 val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
+	 
+	 val fileName = "problem.tptp"
+	 
+	 override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException {
+		val vampireConfig = configuration.asConfig
+		
+		// Start: Logic -> Vampire mapping
+		val transformationStart = System.currentTimeMillis
+		//TODO
+		val result = forwardMapper.transformProblem(problem,vampireConfig)
+		val vampireProblem = result.output
+		val forwardTrace = result.trace
+		
+		var String fileURI = null;
+		var String vampireCode = null;
+		if(vampireConfig.writeToFile) {
+			fileURI = workspace.writeModel(vampireProblem,fileName).toFileString
+		} else {
+			vampireCode = workspace.writeModelToString(vampireProblem,fileName)
+		} 
+		val transformationTime = System.currentTimeMillis - transformationStart
+		// Finish: Logic -> Vampire mapping
+		
+		//Creates a file containing the tptp code after transformation
+		val out = new PrintWriter("output/files/vampireCode.tptp")
+		out.println(vampireCode)
+		out.close()
+		
+		
+		/* 	
+		 * not for now -> Start: Solving Alloy problem
+		 *  
+		// Start: Solving Alloy problem
+		val solverStart = System.currentTimeMillis
+		val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,fileURI,alloyCode)
+		val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime)
+		val solverFinish = System.currentTimeMillis-solverStart
+		// Finish: Solving Alloy problem
+				
+		if(vampireConfig.writeToFile) workspace.deactivateModel(fileName)
+		
+		return logicResult
+		*/
+		
+		return null // for now
+	}
+	
+	def asConfig(LogicSolverConfiguration configuration){
+		if(configuration instanceof VampireSolverConfiguration) {
+			return configuration
+		} else {
+			throw new IllegalArgumentException('''The configuration have to be an «VampireSolverConfiguration.simpleName»!''')	
+		}
+	}
+	
+//	/*
+//	 * not for now
+//	 * 
+	override getInterpretations(ModelResult modelResult) {
+		//val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key]
+//		val sols = modelResult.representation// as List<A4Solution>
+//		//val res = answers.map 
+//		sols.map[
+//			new VampireModelInterpretation(
+//				forwardMapper.typeMapper.typeInterpreter,
+//				it as A4Solution,
+//				forwardMapper,
+//				modelResult.trace as Logic2AlloyLanguageMapperTrace
+//			)
+//		]
+	}	
+//	*/
+	
+}
\ No newline at end of file
-- 
cgit v1.2.3-54-g00ecf