From 5d1165ceef23e20c4bbe46fe6f88e95f317234b5 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Mon, 7 Oct 2019 00:35:42 -0400 Subject: VAMPIRE: Implement Vampire measurement code --- .../dslreasoner/vampire/reasoner/builder/VampireHandler.xtend | 10 ++++++---- 1 file changed, 6 insertions(+), 4 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 ce672211..74532ee5 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 @@ -28,7 +28,7 @@ class VampireSolverException extends Exception { @Data class MonitoredVampireSolution { // List warnings // List debugs -// long kodkodTime + long solverTime // val List> aswers val VampireModel generatedModel // val boolean finishedBeforeTimeout @@ -43,8 +43,8 @@ class VampireHandler { val VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\" val VAMPNAME = "vampire.exe" val TEMPNAME = "TEMP.tptp" - val OPTION = " --mode casc_sat " - val SOLNNAME = "solution.tptp" + val OPTION = " --mode casc_sat -t 300 " + val SOLNNAME = "_solution" + configuration.typeScopes.maxNewElements + ".tptp" val PATH = "C:/cygwin64/bin" val wsURI = workspace.workspaceURI @@ -57,9 +57,11 @@ class VampireHandler { // 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 // 2.2 store output into local variable val BufferedReader reader = new BufferedReader(new InputStreamReader(p.getInputStream())); @@ -80,7 +82,7 @@ class VampireHandler { // println((root.get(0) as VampireModel ).comments) - return new MonitoredVampireSolution(root.get(0) as VampireModel) + return new MonitoredVampireSolution(solverTime, root.get(0) as VampireModel) /* * //Prepare -- cgit v1.2.3-54-g00ecf