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:
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.xtend16
1 files changed, 8 insertions, 8 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 44efd84e..fa334322 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
@@ -299,23 +299,23 @@ class Logic2VampireLanguageMapper_Support {
299 def getSolverSpecs(BackendSolver solver) { 299 def getSolverSpecs(BackendSolver solver) {
300 switch (solver) { 300 switch (solver) {
301 case BackendSolver::CVC4: 301 case BackendSolver::CVC4:
302 return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT") 302 return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT")//TODO Update
303 case BackendSolver::DARWINFM: 303 case BackendSolver::DARWINFM:
304 return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s") 304 return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s")//TODO Update
305 case BackendSolver::EDARWIN: 305 case BackendSolver::EDARWIN:
306 return newArrayList("E-Darwin---1.5", 306 return newArrayList("E-Darwin---1.5",
307 "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s") 307 "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s")//TODO Update
308 case BackendSolver::GEOIII: 308 case BackendSolver::GEOIII:
309 return newArrayList("Geo-III---2018C", 309 return newArrayList("Geo-III---2018C",
310 "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s") 310 "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s")//TODO Update
311 case BackendSolver::IPROVER: 311 case BackendSolver::IPROVER:
312 return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s") 312 return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s")//TODO Update
313 case BackendSolver::PARADOX: 313 case BackendSolver::PARADOX:
314 return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s") 314 return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s")//TODO Update
315 case BackendSolver::VAMPIRE: 315 case BackendSolver::VAMPIRE:
316 return newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s") 316 return newArrayList("Vampire---SAT-4.5", "vampire --mode casc_sat -t %d %s")
317 case BackendSolver::Z3: 317 case BackendSolver::Z3:
318 return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:%d -file:%s") 318 return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:%d -file:%s")//TODO Update
319 } 319 }
320 } 320 }
321 321