Commit e5cbf29e authored by Andrei Paskevich's avatar Andrei Paskevich

menage in provers-detection-data.conf

- recognize versioned executables
- mark old versions as old
- mark all Simplify versions old
    and I'd like to get rid of it completely
parent f960d2a8
......@@ -8,11 +8,9 @@ exec = "alt-ergo-0.95"
exec = "alt-ergo-0.95-dev"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\(-dev\\)?\\)"
version_ok = "0.95.3"
version_ok = "0.95.2"
version_ok = "0.95.1"
version_ok = "0.95"
version_ok = "0.95-dev"
version_ok = "0.95.1"
version_old = "0.95"
version_old = "0.95-dev"
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -timelimit %t %f"
driver = "drivers/alt_ergo.drv"
editor = "altgr-ergo"
......@@ -28,11 +26,9 @@ exec = "alt-ergo-0.95"
exec = "alt-ergo-0.95-dev"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\(-dev\\)?\\)"
version_ok = "0.95.3"
version_ok = "0.95.2"
version_ok = "0.95.1"
version_ok = "0.95"
version_ok = "0.95-dev"
version_ok = "0.95.1"
version_old = "0.95"
version_old = "0.95-dev"
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -timelimit %t -model %f"
driver = "drivers/alt_ergo_model.drv"
editor = "altgr-ergo"
......@@ -43,7 +39,7 @@ exec = "alt-ergo"
exec = "alt-ergo-0.94"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\)"
version_ok = "0.94"
version_old = "0.94"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
driver = "drivers/alt_ergo_0.94.drv"
editor = "altgr-ergo"
......@@ -55,8 +51,8 @@ exec = "alt-ergo-0.93.1"
exec = "alt-ergo-0.93"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\)"
version_ok = "^0\.93\..+$"
version_ok = "0.93"
version_old = "^0\.93\..+$"
version_old = "0.93"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
driver = "drivers/alt_ergo_0.93.drv"
......@@ -81,6 +77,17 @@ version_old = "0.8"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
driver = "drivers/alt_ergo_0.92.drv"
# CVC4 version 1.0
[ATP cvc4]
name = "CVC4"
exec = "cvc4"
exec = "cvc4-1.0"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok = "1.0"
driver = "drivers/cvc4.drv"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e --lang=smt2 %f"
# CVC3 versions 2.4.x
[ATP cvc3]
name = "CVC3"
......@@ -103,31 +110,21 @@ exec = "cvc3-2.2"
exec = "cvc3-2.1"
version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
version_ok = "2.2"
version_old = "2.2"
version_old = "2.1"
# we pass time 0 to why3-cpulimit to avoid race
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -timeout %t %f"
driver = "drivers/cvc3.drv"
# CVC4 version 1.0
[ATP cvc4]
name = "CVC4"
exec = "cvc4"
exec = "cvc4-1.0"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok = "1.0"
driver = "drivers/cvc4.drv"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e --lang=smt2 %f"
[ATP yices]
name = "Yices"
exec = "yices"
exec = "yices-1.0.38"
version_switch = "--version"
version_regexp = "[Yices ]*\\([^ \n]+\\)"
version_ok = "^1\.0\.3[0-8]$"
version_ok = "^1\.0\.2[5-9]$"
version_ok = "1.0.38"
version_old = "^1\.0\.3[0-7]$"
version_old = "^1\.0\.2[5-9]$"
version_old = "^1\.0\.2[0-4]$"
version_old = "^1\.0\.1\.*$"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e"
......@@ -146,11 +143,14 @@ driver = "drivers/yices.drv"
[ATP eprover]
name = "Eprover"
exec = "eprover"
exec = "eprover-1.6"
exec = "eprover-1.5"
exec = "eprover-1.4"
version_switch = "--version"
version_regexp = "E \\([-0-9.]+\\) [^\n]+"
version_ok = "1.6"
version_ok = "1.5"
version_ok = "1.4"
version_ok = "1.6"
version_old = "1.5"
version_old = "1.4"
# we pass time 0 to why3-cpulimit to avoid race
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
driver = "drivers/eprover.drv"
......@@ -173,13 +173,13 @@ driver = "drivers/gappa.drv"
[ATP mathsat]
name = "MathSAT5"
exec = "mathsat"
exec = "mathsat-5.2.2"
version_switch = "-version"
version_regexp = "MathSAT5 version \\([^ \n]+\\)"
version_ok = "5.2.2"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -input=smt2 -model -random_seed=80 %f"
driver = "drivers/mathsat.drv"
[ATP simplify]
name = "Simplify"
exec = "Simplify"
......@@ -188,14 +188,15 @@ exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
version_switch = "-version"
version_regexp = "Simplify version \\([^ \n,]+\\)"
version_ok = "1.5.5"
version_ok = "1.5.4"
version_old = "1.5.5"
version_old = "1.5.4"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
driver = "drivers/simplify.drv"
[ATP spass]
name = "Spass"
exec = "SPASS"
exec = "SPASS-3.7"
version_switch = " | grep 'SPASS V'"
version_regexp = "SPASS V \\([^ \n\t]+\\)"
version_ok = "3.7"
......@@ -215,6 +216,7 @@ driver = "drivers/spass_types.drv"
[ATP vampire]
name = "Vampire"
exec = "vampire"
exec = "vampire-0.6"
version_switch = "--version"
version_regexp = "Vampire \\([0-9.]+\\)"
# we pass time 0 to why3-cpulimit to avoid race
......@@ -243,11 +245,11 @@ exec = "z3-4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.3.1"
version_ok = "4.3.0"
version_ok = "4.2"
version_ok = "4.1.2"
version_ok = "4.1.1"
version_ok = "4.0"
version_old = "4.3.0"
version_old = "4.2"
version_old = "4.1.2"
version_old = "4.1.1"
version_old = "4.0"
driver = "drivers/z3.drv"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt2 -rs:42 %f"
......@@ -259,7 +261,7 @@ exec = "z3-3.1"
exec = "z3-3.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "^3\..+$"
version_old = "3.2"
version_old = "3.1"
version_old = "3.0"
driver = "drivers/z3.drv"
......@@ -325,6 +327,7 @@ driver = "drivers/zenon.drv"
[ATP iprover]
name = "iProver"
exec = "iprover"
exec = "iprover-0.8.1"
version_switch = " | grep iProver"
version_regexp = "iProver v\\([^ \n\t]+\\)"
version_ok = "0.8.1"
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment