diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java | 88 |
1 files changed, 88 insertions, 0 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java index dae0df6e..1255b25c 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java | |||
@@ -1,5 +1,6 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver; | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; |
@@ -29,6 +30,12 @@ import java.util.Collection; | |||
29 | import java.util.HashMap; | 30 | import java.util.HashMap; |
30 | import java.util.List; | 31 | import java.util.List; |
31 | import java.util.Map; | 32 | import java.util.Map; |
33 | import java.util.concurrent.TimeUnit; | ||
34 | import okhttp3.MediaType; | ||
35 | import okhttp3.OkHttpClient; | ||
36 | import okhttp3.Request; | ||
37 | import okhttp3.RequestBody; | ||
38 | import okhttp3.Response; | ||
32 | import org.eclipse.emf.common.util.EList; | 39 | import org.eclipse.emf.common.util.EList; |
33 | import org.eclipse.xtend2.lib.StringConcatenation; | 40 | import org.eclipse.xtend2.lib.StringConcatenation; |
34 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 41 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
@@ -421,4 +428,85 @@ public class Logic2VampireLanguageMapper_Support { | |||
421 | }; | 428 | }; |
422 | return ObjectExtensions.<HashMap<Variable, VLSVariable>>operator_doubleArrow(_hashMap, _function); | 429 | return ObjectExtensions.<HashMap<Variable, VLSVariable>>operator_doubleArrow(_hashMap, _function); |
423 | } | 430 | } |
431 | |||
432 | public String makeForm(final String formula, final BackendSolver solver, final int time) { | ||
433 | String _header = this.getHeader(); | ||
434 | String _plus = (_header + formula); | ||
435 | String _addOptions = this.addOptions(); | ||
436 | String _plus_1 = (_plus + _addOptions); | ||
437 | String _addSolver = this.addSolver(solver, time); | ||
438 | String _plus_2 = (_plus_1 + _addSolver); | ||
439 | String _addEnd = this.addEnd(); | ||
440 | return (_plus_2 + _addEnd); | ||
441 | } | ||
442 | |||
443 | public ArrayList<String> getSolverSpecs(final BackendSolver solver) { | ||
444 | if (solver != null) { | ||
445 | switch (solver) { | ||
446 | case CVC4: | ||
447 | return CollectionLiterals.<String>newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT"); | ||
448 | case DARWINFM: | ||
449 | return CollectionLiterals.<String>newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s"); | ||
450 | case EDARWIN: | ||
451 | return CollectionLiterals.<String>newArrayList("E-Darwin---1.5", "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s"); | ||
452 | case GEOIII: | ||
453 | return CollectionLiterals.<String>newArrayList("Geo-III---2018C", "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s"); | ||
454 | case IPROVER: | ||
455 | return CollectionLiterals.<String>newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s"); | ||
456 | case PARADOX: | ||
457 | return CollectionLiterals.<String>newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s"); | ||
458 | case VAMPIRE: | ||
459 | return CollectionLiterals.<String>newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s"); | ||
460 | case Z3: | ||
461 | return CollectionLiterals.<String>newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s"); | ||
462 | default: | ||
463 | break; | ||
464 | } | ||
465 | } | ||
466 | return null; | ||
467 | } | ||
468 | |||
469 | public String getHeader() { | ||
470 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"ProblemSource\"\r\n\r\nFORMULAE\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"FORMULAEProblem\"\r\n\r\n\r\n"; | ||
471 | } | ||
472 | |||
473 | public String addSpec(final String spec) { | ||
474 | return spec.replace("\n", "\\r\\n"); | ||
475 | } | ||
476 | |||
477 | public String addOptions() { | ||
478 | return "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"QuietFlag\"\r\n\r\n-q3\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"SubmitButton\"\r\n\r\nRunSelectedSystems\r\n"; | ||
479 | } | ||
480 | |||
481 | public String addSolver(final BackendSolver solver, final int time) { | ||
482 | final ArrayList<String> solverSpecs = this.getSolverSpecs(solver); | ||
483 | final String ID = solverSpecs.get(0); | ||
484 | final String cmd = solverSpecs.get(1); | ||
485 | String _replace = cmd.replace("%d", Integer.valueOf(time).toString()); | ||
486 | String _plus = ((((((("------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID) + | ||
487 | "\"\r\n\r\n") + ID) + | ||
488 | "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___") + ID) + | ||
489 | "\"\r\n\r\n") + _replace); | ||
490 | return (_plus + "\r\n"); | ||
491 | } | ||
492 | |||
493 | public String addEnd() { | ||
494 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--"; | ||
495 | } | ||
496 | |||
497 | public ArrayList<String> sendPost(final String formData) throws Exception { | ||
498 | final OkHttpClient client = new OkHttpClient.Builder().connectTimeout(350, TimeUnit.SECONDS).readTimeout(350, TimeUnit.SECONDS).build(); | ||
499 | final MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA"); | ||
500 | final RequestBody body = RequestBody.create(mediaType, formData); | ||
501 | final Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body).addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin", | ||
502 | "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", | ||
503 | "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent", | ||
504 | "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36").addHeader("Accept", | ||
505 | "text/html,application/xhtml+xml,application/xmlq=0.9,image/webp,image/apng,*/*q=0.8,application/signed-exchangev=b3").addHeader("Referer", "http://tptp.cs.miami.edu/cgi-bin/SystemOnTPTP").addHeader("Accept-Encoding", | ||
506 | "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", | ||
507 | "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", | ||
508 | "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build(); | ||
509 | final Response response = client.newCall(request).execute(); | ||
510 | return CollectionLiterals.<String>newArrayList(response.body().string().split("\n")); | ||
511 | } | ||
424 | } | 512 | } |