diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-09 01:03:49 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:43:12 -0400 |
commit | 8ec0122cbcb257c394156e899184e7b26ef7a860 (patch) | |
tree | dbd818d80ff10c8761e369c5a3c85368408b3e9e /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill | |
parent | VAMPIRE: fix bug in transformation, further implement measurement code (diff) | |
download | VIATRA-Generator-8ec0122cbcb257c394156e899184e7b26ef7a860.tar.gz VIATRA-Generator-8ec0122cbcb257c394156e899184e7b26ef7a860.tar.zst VIATRA-Generator-8ec0122cbcb257c394156e899184e7b26ef7a860.zip |
VAMPIRE: Further develop testing fo r Vampire solver
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill')
2 files changed, 43 insertions, 12 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend index fc8d3e99..b223dbe5 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend | |||
@@ -7,12 +7,15 @@ class VampireSolverConfiguration extends LogicSolverConfiguration { | |||
7 | public var int contCycleLevel = 0 | 7 | public var int contCycleLevel = 0 |
8 | public var boolean uniquenessDuplicates = false | 8 | public var boolean uniquenessDuplicates = false |
9 | public var int iteration = -1 | 9 | public var int iteration = -1 |
10 | public var BackendSolver solver = BackendSolver::VAMP | ||
10 | //choose needed backend solver | 11 | //choose needed backend solver |
11 | // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J | 12 | // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J |
12 | } | 13 | } |
13 | 14 | ||
14 | 15 | ||
15 | enum VampireBackendSolver { | 16 | enum BackendSolver { |
17 | VAMP, | ||
18 | CVC4 | ||
16 | //add needed things | 19 | //add needed things |
17 | } | 20 | } |
18 | 21 | ||
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 | |||
10 | import org.eclipse.xtend.lib.annotations.Data | 10 | import org.eclipse.xtend.lib.annotations.Data |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl |
13 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver | ||
13 | 14 | ||
14 | class VampireSolverException extends Exception { | 15 | class VampireSolverException extends Exception { |
15 | new(String s) { | 16 | new(String s) { |
@@ -39,30 +40,58 @@ class VampireHandler { | |||
39 | // val fileName = "problem.als" | 40 | // val fileName = "problem.als" |
40 | public def callSolver(VampireModel problem, ReasonerWorkspace workspace, VampireSolverConfiguration configuration) { | 41 | public def callSolver(VampireModel problem, ReasonerWorkspace workspace, VampireSolverConfiguration configuration) { |
41 | 42 | ||
42 | val CMD = "cmd /c " | 43 | // Vampire |
43 | val VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\" | 44 | val VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\" |
44 | val VAMPNAME = "vampire.exe" | 45 | val VAMPNAME = "vampire.exe" |
46 | val VAMPLOC = VAMPDIR + VAMPNAME | ||
47 | |||
48 | // CVC4 | ||
49 | val CVC4DIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\" | ||
50 | val CVC4NAME = "vampire.exe" | ||
51 | val CVC4LOC = CVC4DIR + CVC4NAME | ||
52 | |||
53 | val CMD = "cmd /c " | ||
45 | val TEMPNAME = "TEMP.tptp" | 54 | val TEMPNAME = "TEMP.tptp" |
46 | val OPTION = " --mode casc_sat -t 300 " | 55 | val SOLNNAME = "solution" + configuration.solver.toString + "_" + configuration.typeScopes.maxNewElements + |
47 | val SOLNNAME = "solution" + configuration.typeScopes.maxNewElements +"_" + configuration.iteration + ".tptp" | 56 | "_" + configuration.iteration + ".tptp" |
48 | val PATH = "C:/cygwin64/bin" | 57 | val PATH = "C:/cygwin64/bin" |
49 | 58 | ||
50 | val wsURI = workspace.workspaceURI | 59 | val wsURI = workspace.workspaceURI |
51 | val tempLoc = wsURI + TEMPNAME | 60 | val tempLoc = wsURI + TEMPNAME |
52 | val solnLoc = wsURI + SOLNNAME + " " | 61 | val solnLoc = wsURI + SOLNNAME + " " |
53 | val vampLoc = VAMPDIR + VAMPNAME | ||
54 | 62 | ||
55 | // 1. create temp file for vampire problem | 63 | // 1. create temp file for vampire problem |
56 | var tempURI = workspace.writeModel(problem, TEMPNAME).toFileString | 64 | var tempURI = workspace.writeModel(problem, TEMPNAME).toFileString |
57 | 65 | ||
58 | // 2. run command and save to | 66 | // 2. run command and save to |
59 | // need to have cygwin downloaded | 67 | // need to have cygwin downloaded |
60 | var startTime = System.currentTimeMillis | 68 | var long startTime = -1 as long |
61 | val p = Runtime.runtime.exec(CMD + vampLoc + OPTION + tempLoc + " > " + solnLoc, newArrayList("Path=" + PATH)) | 69 | var long solverTime = -1 as long |
62 | // 2.1 determine time left | 70 | var Process p = null |
63 | p.waitFor | 71 | if (configuration.solver == BackendSolver::VAMP) { |
64 | val solverTime = System.currentTimeMillis - startTime | ||
65 | 72 | ||
73 | var OPTION = " --mode casc_sat " | ||
74 | if (configuration.runtimeLimit != -1) { | ||
75 | OPTION = OPTION + "-t " + configuration.runtimeLimit + " " | ||
76 | } | ||
77 | |||
78 | startTime = System.currentTimeMillis | ||
79 | p = Runtime.runtime.exec(CMD + VAMPLOC + OPTION + tempLoc + " > " + solnLoc, newArrayList("Path=" + PATH)) | ||
80 | p.waitFor | ||
81 | solverTime = System.currentTimeMillis - startTime | ||
82 | } | ||
83 | if (configuration.solver == BackendSolver::CVC4) { | ||
84 | var OPTION = " SAT " | ||
85 | if (configuration.runtimeLimit != -1) { | ||
86 | OPTION = " " + configuration.runtimeLimit + OPTION | ||
87 | } | ||
88 | println(CMD + CVC4LOC + tempLoc + OPTION + " > " + solnLoc) | ||
89 | p = Runtime.runtime.exec(CMD + CVC4LOC + tempLoc + OPTION + " > " + solnLoc, newArrayList("Path=" + PATH)) | ||
90 | p.waitFor | ||
91 | solverTime = System.currentTimeMillis - startTime | ||
92 | } | ||
93 | |||
94 | // 2.1 determine time left | ||
66 | // 2.2 store output into local variable | 95 | // 2.2 store output into local variable |
67 | val BufferedReader reader = new BufferedReader(new InputStreamReader(p.getInputStream())); | 96 | val BufferedReader reader = new BufferedReader(new InputStreamReader(p.getInputStream())); |
68 | val List<String> output = newArrayList | 97 | val List<String> output = newArrayList |
@@ -74,14 +103,13 @@ class VampireHandler { | |||
74 | 103 | ||
75 | // println(output.toString()) | 104 | // println(output.toString()) |
76 | // 4. delete temp file | 105 | // 4. delete temp file |
77 | workspace.getFile(TEMPNAME).delete | 106 | workspace.getFile(TEMPNAME).delete |
78 | 107 | ||
79 | // 5. determine and return whether or not finite model was found | 108 | // 5. determine and return whether or not finite model was found |
80 | // 6. save solution as a .tptp model | 109 | // 6. save solution as a .tptp model |
81 | val root = workspace.readModel(VampireModel, SOLNNAME).eResource.contents | 110 | val root = workspace.readModel(VampireModel, SOLNNAME).eResource.contents |
82 | 111 | ||
83 | // println((root.get(0) as VampireModel ).comments) | 112 | // println((root.get(0) as VampireModel ).comments) |
84 | |||
85 | return new MonitoredVampireSolution(solverTime, root.get(0) as VampireModel) | 113 | return new MonitoredVampireSolution(solverTime, root.get(0) as VampireModel) |
86 | 114 | ||
87 | /* | 115 | /* |