From abf9662662c7f4c9fc410ea416a42fea9e0f43d4 Mon Sep 17 00:00:00 2001
From: ArenBabikian <aren.babikian@mail.mcgill.ca>
Date: Wed, 9 Oct 2019 01:03:49 -0400
Subject: VAMPIRE: Further develop testing fo r Vampire solver

---
 .../vampire/reasoner/builder/VampireHandler.xtend  | 50 +++++++++++++++++-----
 1 file changed, 39 insertions(+), 11 deletions(-)

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

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
index c5cfb1c7..c1eb3382 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
@@ -10,6 +10,7 @@ import org.eclipse.emf.ecore.resource.Resource
 import org.eclipse.xtend.lib.annotations.Data
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver
 
 class VampireSolverException extends Exception {
 	new(String s) {
@@ -39,30 +40,58 @@ class VampireHandler {
 	// val fileName = "problem.als"
 	public def callSolver(VampireModel problem, ReasonerWorkspace workspace, VampireSolverConfiguration configuration) {
 
-		val CMD = "cmd /c "
+		// Vampire
 		val VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\"
 		val VAMPNAME = "vampire.exe"
+		val VAMPLOC = VAMPDIR + VAMPNAME
+
+		// CVC4
+		val CVC4DIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\"
+		val CVC4NAME = "vampire.exe"
+		val CVC4LOC = CVC4DIR + CVC4NAME
+
+		val CMD = "cmd /c "
 		val TEMPNAME = "TEMP.tptp"
-		val OPTION = " --mode casc_sat -t 300 "
-		val SOLNNAME = "solution" + configuration.typeScopes.maxNewElements +"_" + configuration.iteration + ".tptp"
+		val SOLNNAME = "solution" + configuration.solver.toString + "_" + configuration.typeScopes.maxNewElements +
+			"_" + configuration.iteration + ".tptp"
 		val PATH = "C:/cygwin64/bin"
 
 		val wsURI = workspace.workspaceURI
 		val tempLoc = wsURI + TEMPNAME
 		val solnLoc = wsURI + SOLNNAME + " "
-		val vampLoc = VAMPDIR + VAMPNAME
 
 		// 1. create temp file for vampire problem
 		var tempURI = workspace.writeModel(problem, TEMPNAME).toFileString
 
 		// 2. run command and save to 
 		// need to have cygwin downloaded
-		var startTime = System.currentTimeMillis
-		val p = Runtime.runtime.exec(CMD + vampLoc + OPTION + tempLoc + " > " + solnLoc, newArrayList("Path=" + PATH))
-		// 2.1 determine time left
-		p.waitFor
-		val solverTime = System.currentTimeMillis - startTime
+		var long startTime = -1 as long
+		var long solverTime = -1 as long
+		var Process p = null
+		if (configuration.solver == BackendSolver::VAMP) {
 
+			var OPTION = " --mode casc_sat "
+			if (configuration.runtimeLimit != -1) {
+				OPTION = OPTION + "-t " + configuration.runtimeLimit + " "
+			}
+
+			startTime = System.currentTimeMillis
+			p = Runtime.runtime.exec(CMD + VAMPLOC + OPTION + tempLoc + " > " + solnLoc, newArrayList("Path=" + PATH))
+			p.waitFor
+			solverTime = System.currentTimeMillis - startTime
+		}
+		if (configuration.solver == BackendSolver::CVC4) {
+			var OPTION = " SAT "
+			if (configuration.runtimeLimit != -1) {
+				OPTION = " " + configuration.runtimeLimit + OPTION
+			}
+			println(CMD + CVC4LOC + tempLoc + OPTION + " > " + solnLoc)
+			p = Runtime.runtime.exec(CMD + CVC4LOC + tempLoc + OPTION + " > " + solnLoc, newArrayList("Path=" + PATH))
+			p.waitFor
+			solverTime = System.currentTimeMillis - startTime
+		}
+
+		// 2.1 determine time left
 		// 2.2 store output into local variable
 		val BufferedReader reader = new BufferedReader(new InputStreamReader(p.getInputStream()));
 		val List<String> output = newArrayList
@@ -74,14 +103,13 @@ class VampireHandler {
 
 //    	println(output.toString())
 		// 4. delete temp file
-		workspace.getFile(TEMPNAME).delete		
+		workspace.getFile(TEMPNAME).delete
 
 		// 5. determine and return whether or not finite model was found
 		// 6. save solution as a .tptp model
 		val root = workspace.readModel(VampireModel, SOLNNAME).eResource.contents
 
 //		println((root.get(0) as VampireModel ).comments)
-		
 		return new MonitoredVampireSolution(solverTime, root.get(0) as VampireModel)
 
 	/*
-- 
cgit v1.2.3-54-g00ecf