aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-10-11 15:51:49 -0400
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-10-11 15:51:49 -0400
commit17d6aa5028bff14c80f0be6a042c6a68fe8b61b0 (patch)
tree0c156ad34304a1ac296690fd4c3bf1c438245456 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
parentimplement http requests for the TPTP server (diff)
downloadVIATRA-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.xtend95
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 @@
1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder 1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
2 2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver
3import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant 4import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant
4import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction 5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm 6import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm
@@ -16,6 +17,12 @@ import java.util.ArrayList
16import java.util.HashMap 17import java.util.HashMap
17import java.util.List 18import java.util.List
18import java.util.Map 19import java.util.Map
20import java.util.concurrent.TimeUnit
21import okhttp3.MediaType
22import okhttp3.OkHttpClient
23import okhttp3.Request
24import okhttp3.RequestBody
25import okhttp3.Response
19import org.eclipse.emf.common.util.EList 26import org.eclipse.emf.common.util.EList
20 27
21import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 28import 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}