diff options
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 | 16 |
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 | ||