diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-11 15:51:49 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-11 15:51:49 -0400 |
commit | 17d6aa5028bff14c80f0be6a042c6a68fe8b61b0 (patch) | |
tree | 0c156ad34304a1ac296690fd4c3bf1c438245456 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend | |
parent | implement http requests for the TPTP server (diff) | |
download | VIATRA-Generator-17d6aa5028bff14c80f0be6a042c6a68fe8b61b0.tar.gz VIATRA-Generator-17d6aa5028bff14c80f0be6a042c6a68fe8b61b0.tar.zst VIATRA-Generator-17d6aa5028bff14c80f0be6a042c6a68fe8b61b0.zip |
VAMPIRE: complete testing setup
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend | 95 |
1 files changed, 86 insertions, 9 deletions
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 680213ab..7b1c7d9a 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 | |||
@@ -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.vampireLanguage.VLSConstant | 4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant |
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm |
@@ -16,6 +17,12 @@ import java.util.ArrayList | |||
16 | import java.util.HashMap | 17 | import java.util.HashMap |
17 | import java.util.List | 18 | import java.util.List |
18 | import java.util.Map | 19 | import java.util.Map |
20 | import java.util.concurrent.TimeUnit | ||
21 | import okhttp3.MediaType | ||
22 | import okhttp3.OkHttpClient | ||
23 | import okhttp3.Request | ||
24 | import okhttp3.RequestBody | ||
25 | import okhttp3.Response | ||
19 | import org.eclipse.emf.common.util.EList | 26 | import org.eclipse.emf.common.util.EList |
20 | 27 | ||
21 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 28 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
@@ -77,13 +84,13 @@ class Logic2VampireLanguageMapper_Support { | |||
77 | it.terms += duplicate(v) | 84 | it.terms += duplicate(v) |
78 | ] | 85 | ] |
79 | } | 86 | } |
80 | 87 | ||
81 | def protected List<VLSVariable> duplicate(List<VLSVariable> vars) { | 88 | def protected List<VLSVariable> duplicate(List<VLSVariable> vars) { |
82 | var newList = newArrayList | 89 | var newList = newArrayList |
83 | for (v : vars) { | 90 | for (v : vars) { |
84 | newList.add(duplicate(v)) | 91 | newList.add(duplicate(v)) |
85 | } | 92 | } |
86 | return newList | 93 | return newList |
87 | } | 94 | } |
88 | 95 | ||
89 | def protected VLSConstant toConstant(VLSFunctionAsTerm term) { | 96 | def protected VLSConstant toConstant(VLSFunctionAsTerm term) { |
@@ -117,7 +124,7 @@ class Logic2VampireLanguageMapper_Support { | |||
117 | 124 | ||
118 | // TODO Make more general | 125 | // TODO Make more general |
119 | def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) { | 126 | def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) { |
120 | 127 | ||
121 | // OLD | 128 | // OLD |
122 | // val List<VLSInequality> eqs = newArrayList | 129 | // val List<VLSInequality> eqs = newArrayList |
123 | // for (t1 : terms.subList(1, terms.length)) { | 130 | // for (t1 : terms.subList(1, terms.length)) { |
@@ -133,7 +140,6 @@ class Logic2VampireLanguageMapper_Support { | |||
133 | // } | 140 | // } |
134 | // return unfoldAnd(eqs) | 141 | // return unfoldAnd(eqs) |
135 | // END OLD | 142 | // END OLD |
136 | |||
137 | val List<VLSInequality> eqs = newArrayList | 143 | val List<VLSInequality> eqs = newArrayList |
138 | for (t1 : terms) { | 144 | for (t1 : terms) { |
139 | if (t1 != t2) { | 145 | if (t1 != t2) { |
@@ -257,7 +263,8 @@ class Logic2VampireLanguageMapper_Support { | |||
257 | } | 263 | } |
258 | } | 264 | } |
259 | } | 265 | } |
260 | //TODO rewrite such that it uses "listSubTypes" | 266 | |
267 | // TODO rewrite such that it uses "listSubTypes" | ||
261 | def protected boolean dfsSubtypeCheck(Type type, Type type2) { | 268 | def protected boolean dfsSubtypeCheck(Type type, Type type2) { |
262 | // There is surely a better way to do this | 269 | // There is surely a better way to do this |
263 | if (type.subtypes.isEmpty) | 270 | if (type.subtypes.isEmpty) |
@@ -284,4 +291,74 @@ class Logic2VampireLanguageMapper_Support { | |||
284 | new HashMap(map1) => [putAll(map2)] | 291 | new HashMap(map1) => [putAll(map2)] |
285 | } | 292 | } |
286 | 293 | ||
294 | // SERVERS | ||
295 | def makeForm(String formula, BackendSolver solver, int time) { | ||
296 | return header + formula + addOptions + addSolver(solver, time) + addEnd | ||
297 | } | ||
298 | |||
299 | def getSolverSpecs(BackendSolver solver) { | ||
300 | switch (solver) { | ||
301 | case BackendSolver::CVC4: return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT") | ||
302 | case BackendSolver::DARWINFM: return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s") | ||
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") | ||
304 | case BackendSolver::GEOIII: return newArrayList("Geo-III---2018C", "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s") | ||
305 | case BackendSolver::IPROVER: return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s") | ||
306 | case BackendSolver::PARADOX: return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s") | ||
307 | case BackendSolver::VAMPIRE: return newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s") | ||
308 | case BackendSolver::Z3: return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s") | ||
309 | } | ||
310 | } | ||
311 | |||
312 | def getHeader() { | ||
313 | 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" | ||
314 | } | ||
315 | |||
316 | def addSpec(String spec) { | ||
317 | return spec.replace("\n", "\\r\\n") | ||
318 | } | ||
319 | |||
320 | def addOptions() { | ||
321 | 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" | ||
322 | } | ||
323 | |||
324 | def addSolver(BackendSolver solver, int time) { | ||
325 | val solverSpecs = getSolverSpecs(solver) | ||
326 | val ID = solverSpecs.get(0) | ||
327 | val cmd = solverSpecs.get(1) | ||
328 | |||
329 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID + | ||
330 | "\"\r\n\r\n" + ID + | ||
331 | "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___" + ID + | ||
332 | "\"\r\n\r\n" + cmd.replace("%d", time.toString) + "\r\n" | ||
333 | } | ||
334 | |||
335 | def addEnd() { | ||
336 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--" | ||
337 | } | ||
338 | |||
339 | def sendPost(String formData) throws Exception { | ||
340 | |||
341 | val OkHttpClient client = new OkHttpClient.Builder().connectTimeout(350, TimeUnit.SECONDS).readTimeout(350, TimeUnit.SECONDS).build() | ||
342 | |||
343 | val MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA") | ||
344 | val RequestBody body = RequestBody.create(mediaType, formData) | ||
345 | val Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body). | ||
346 | addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin", | ||
347 | "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", | ||
348 | "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent", | ||
349 | "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36"). | ||
350 | addHeader("Accept", | ||
351 | "text/html,application/xhtml+xml,application/xmlq=0.9,image/webp,image/apng,*/*q=0.8,application/signed-exchangev=b3"). | ||
352 | addHeader("Referer", "http://tptp.cs.miami.edu/cgi-bin/SystemOnTPTP").addHeader("Accept-Encoding", | ||
353 | "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", | ||
354 | "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", | ||
355 | "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build() | ||
356 | |||
357 | val Response response = client.newCall(request).execute() | ||
358 | // TimeUnit.SECONDS.sleep(5) | ||
359 | return newArrayList(response.body.string.split("\n")) | ||
360 | // return response.body.string | ||
361 | // case 1: | ||
362 | } | ||
363 | |||
287 | } | 364 | } |