diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src')
2 files changed, 25 insertions, 11 deletions
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 index 31aa091c..9ec08163 100644 --- 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 | |||
@@ -90,6 +90,7 @@ class VampireSolver extends LogicReasoner { | |||
90 | ind = 0 | 90 | ind = 0 |
91 | while (!responseFound) { | 91 | while (!responseFound) { |
92 | var line = response.get(ind) | 92 | var line = response.get(ind) |
93 | // println(line) | ||
93 | if (line.length >= 5 && line.substring(0, 5) == "ERROR") { | 94 | if (line.length >= 5 && line.substring(0, 5) == "ERROR") { |
94 | done = false | 95 | done = false |
95 | responseFound = true | 96 | responseFound = true |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend index 7b1c7d9a..44efd84e 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend | |||
@@ -298,14 +298,24 @@ class Logic2VampireLanguageMapper_Support { | |||
298 | 298 | ||
299 | def getSolverSpecs(BackendSolver solver) { | 299 | def getSolverSpecs(BackendSolver solver) { |
300 | switch (solver) { | 300 | switch (solver) { |
301 | case BackendSolver::CVC4: return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT") | 301 | case BackendSolver::CVC4: |
302 | case BackendSolver::DARWINFM: return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s") | 302 | return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT") |
303 | case BackendSolver::EDARWIN: return newArrayList("E-Darwin---1.5", "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s") | 303 | case BackendSolver::DARWINFM: |
304 | case BackendSolver::GEOIII: return newArrayList("Geo-III---2018C", "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s") | 304 | return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s") |
305 | case BackendSolver::IPROVER: return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s") | 305 | case BackendSolver::EDARWIN: |
306 | case BackendSolver::PARADOX: return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s") | 306 | return newArrayList("E-Darwin---1.5", |
307 | case BackendSolver::VAMPIRE: return newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s") | 307 | "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s") |
308 | case BackendSolver::Z3: return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s") | 308 | case BackendSolver::GEOIII: |
309 | return newArrayList("Geo-III---2018C", | ||
310 | "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s") | ||
311 | case BackendSolver::IPROVER: | ||
312 | return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s") | ||
313 | case BackendSolver::PARADOX: | ||
314 | return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s") | ||
315 | case BackendSolver::VAMPIRE: | ||
316 | return newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s") | ||
317 | case BackendSolver::Z3: | ||
318 | return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:%d -file:%s") | ||
309 | } | 319 | } |
310 | } | 320 | } |
311 | 321 | ||
@@ -326,10 +336,12 @@ class Logic2VampireLanguageMapper_Support { | |||
326 | val ID = solverSpecs.get(0) | 336 | val ID = solverSpecs.get(0) |
327 | val cmd = solverSpecs.get(1) | 337 | val cmd = solverSpecs.get(1) |
328 | 338 | ||
329 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID + | 339 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"TimeLimit___" + ID + |
340 | "\"\r\n\r\n" + time + | ||
341 | "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID + | ||
330 | "\"\r\n\r\n" + ID + | 342 | "\"\r\n\r\n" + ID + |
331 | "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___" + ID + | 343 | "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___" + ID + |
332 | "\"\r\n\r\n" + cmd.replace("%d", time.toString) + "\r\n" | 344 | "\"\r\n\r\n" + cmd + "\r\n" |
333 | } | 345 | } |
334 | 346 | ||
335 | def addEnd() { | 347 | def addEnd() { |
@@ -338,7 +350,8 @@ class Logic2VampireLanguageMapper_Support { | |||
338 | 350 | ||
339 | def sendPost(String formData) throws Exception { | 351 | def sendPost(String formData) throws Exception { |
340 | 352 | ||
341 | val OkHttpClient client = new OkHttpClient.Builder().connectTimeout(350, TimeUnit.SECONDS).readTimeout(350, TimeUnit.SECONDS).build() | 353 | val OkHttpClient client = new OkHttpClient.Builder().connectTimeout(600, TimeUnit.SECONDS).readTimeout(350, |
354 | TimeUnit.SECONDS).build() | ||
342 | 355 | ||
343 | val MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA") | 356 | val MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA") |
344 | val RequestBody body = RequestBody.create(mediaType, formData) | 357 | val RequestBody body = RequestBody.create(mediaType, formData) |