diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-07 00:35:42 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:42:47 -0400 |
commit | b503c81bee920c18806af25393d0a90b8f77dba6 (patch) | |
tree | 9b70f606bfa7fa450457c04714e045e5ac5f6199 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend | |
parent | VAMPIRE: fix model generation (diff) | |
download | VIATRA-Generator-b503c81bee920c18806af25393d0a90b8f77dba6.tar.gz VIATRA-Generator-b503c81bee920c18806af25393d0a90b8f77dba6.tar.zst VIATRA-Generator-b503c81bee920c18806af25393d0a90b8f77dba6.zip |
VAMPIRE: Implement Vampire measurement code
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend | 10 |
1 files changed, 6 insertions, 4 deletions
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 { | |||
28 | @Data class MonitoredVampireSolution { | 28 | @Data class MonitoredVampireSolution { |
29 | // List<String> warnings | 29 | // List<String> warnings |
30 | // List<String> debugs | 30 | // List<String> debugs |
31 | // long kodkodTime | 31 | long solverTime |
32 | // val List<Pair<A4Solution, Long>> aswers | 32 | // val List<Pair<A4Solution, Long>> aswers |
33 | val VampireModel generatedModel | 33 | val VampireModel generatedModel |
34 | // val boolean finishedBeforeTimeout | 34 | // val boolean finishedBeforeTimeout |
@@ -43,8 +43,8 @@ class VampireHandler { | |||
43 | val VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\" | 43 | val VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\" |
44 | val VAMPNAME = "vampire.exe" | 44 | val VAMPNAME = "vampire.exe" |
45 | val TEMPNAME = "TEMP.tptp" | 45 | val TEMPNAME = "TEMP.tptp" |
46 | val OPTION = " --mode casc_sat " | 46 | val OPTION = " --mode casc_sat -t 300 " |
47 | val SOLNNAME = "solution.tptp" | 47 | val SOLNNAME = "_solution" + configuration.typeScopes.maxNewElements + ".tptp" |
48 | val PATH = "C:/cygwin64/bin" | 48 | val PATH = "C:/cygwin64/bin" |
49 | 49 | ||
50 | val wsURI = workspace.workspaceURI | 50 | val wsURI = workspace.workspaceURI |
@@ -57,9 +57,11 @@ class VampireHandler { | |||
57 | 57 | ||
58 | // 2. run command and save to | 58 | // 2. run command and save to |
59 | // need to have cygwin downloaded | 59 | // need to have cygwin downloaded |
60 | var startTime = System.currentTimeMillis | ||
60 | val p = Runtime.runtime.exec(CMD + vampLoc + OPTION + tempLoc + " > " + solnLoc, newArrayList("Path=" + PATH)) | 61 | val p = Runtime.runtime.exec(CMD + vampLoc + OPTION + tempLoc + " > " + solnLoc, newArrayList("Path=" + PATH)) |
61 | // 2.1 determine time left | 62 | // 2.1 determine time left |
62 | p.waitFor | 63 | p.waitFor |
64 | val solverTime = System.currentTimeMillis - startTime | ||
63 | 65 | ||
64 | // 2.2 store output into local variable | 66 | // 2.2 store output into local variable |
65 | val BufferedReader reader = new BufferedReader(new InputStreamReader(p.getInputStream())); | 67 | val BufferedReader reader = new BufferedReader(new InputStreamReader(p.getInputStream())); |
@@ -80,7 +82,7 @@ class VampireHandler { | |||
80 | 82 | ||
81 | // println((root.get(0) as VampireModel ).comments) | 83 | // println((root.get(0) as VampireModel ).comments) |
82 | 84 | ||
83 | return new MonitoredVampireSolution(root.get(0) as VampireModel) | 85 | return new MonitoredVampireSolution(solverTime, root.get(0) as VampireModel) |
84 | 86 | ||
85 | /* | 87 | /* |
86 | * //Prepare | 88 | * //Prepare |