provers-detection-data.conf.in 3.34 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
2
[ATP alt-ergo]
name = "Alt-Ergo"
3
exec = "ergo"
4
exec = "alt-ergo"
MARCHE Claude's avatar
MARCHE Claude committed
5
exec = "alt-ergo-0.91"
MARCHE Claude's avatar
MARCHE Claude committed
6
version_switch = "-version"
7
version_regexp = ".*Ergo \\([^ \n]*\\)"
8
version_ok = "0.92.2"
MARCHE Claude's avatar
MARCHE Claude committed
9
version_ok = "0.92.1"
10
11
version_ok = "0.92"
version_ok = "0.91"
MARCHE Claude's avatar
MARCHE Claude committed
12
version_old = "0.9"
13
version_old = "0.8"
Andrei Paskevich's avatar
Andrei Paskevich committed
14
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
15
driver = "drivers/alt_ergo.drv"
MARCHE Claude's avatar
MARCHE Claude committed
16

17
18
19
20
21
22
23
24
25
26
27
28
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "ergo"
exec = "alt-ergo"
exec = "alt-ergo-0.91"
version_switch = "-version"
version_regexp = ".*Ergo \\([^ \n]*\\)"
version_ok = "0.92.3"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
driver = "drivers/alt_ergo_trunk.drv"


29
[ATP cvc3]
MARCHE Claude's avatar
MARCHE Claude committed
30
name = "CVC3"
31
exec = "cvc3"
MARCHE Claude's avatar
MARCHE Claude committed
32
version_switch = "-version"
33
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
34
35
version_ok = "2.2"
version_old = "2.1"
Andrei Paskevich's avatar
Andrei Paskevich committed
36
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -timeout %t -lang smt %f"
37
38
driver = "drivers/cvc3.drv"

39
40
41
42
43
44
45
46
[ATP yices]
name = "Yices"
exec = "yices"
version_switch = "--version"
version_regexp = "[Yices ]*\\([^ \n]+\\)"
version_ok = "1.0.27"
version_old = "1.0.17"
version_old = "1.0.24"
Andrei Paskevich's avatar
Andrei Paskevich committed
47
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt"
48
49
driver = "drivers/yices.drv"

50
51
52
[ATP eprover]
name = "Eprover"
exec = "eprover"
53
54
version_switch = "--version"
version_regexp = "E \\([^\n]+\\)"
Andrei Paskevich's avatar
Andrei Paskevich committed
55
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
56
driver = "drivers/tptp.drv"
MARCHE Claude's avatar
MARCHE Claude committed
57
58
59

[ATP gappa]
name = "Gappa"
60
exec = "gappa"
MARCHE Claude's avatar
MARCHE Claude committed
61
version_switch = "--version"
62
version_regexp = "Gappa \\([^ \n]*\\)"
63
version_ok = "0.14.0"
MARCHE Claude's avatar
MARCHE Claude committed
64
65
version_ok = "0.13.0"
version_old = "0.12.3"
66
67
68
69
version_old = "0.12.2"
version_old = "0.12.1"
version_old = "0.12.0"
version_old = "0.11.2"
70
command = "@LOCALBIN@why3-cpulimit %t %m -s %e"
71
driver = "drivers/gappa.drv"
MARCHE Claude's avatar
MARCHE Claude committed
72
73
74

[ATP simplify]
name = "Simplify"
75
76
77
78
exec = "Simplify"
exec = "simplify"
exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
MARCHE Claude's avatar
MARCHE Claude committed
79
version_switch = "-version"
80
version_regexp = "Simplify version \\([^ \n,]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
81
version_ok = "1.5.5"
82
version_ok = "1.5.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
83
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
84
85
86
87
88
driver = "drivers/simplify.drv"

[ATP spass]
name = "Spass"
exec = "SPASS"
89
version_switch = "-TPTP || true"
90
version_regexp = "SPASS V \\([^ \n\t]+\\)"
Andrei Paskevich's avatar
Andrei Paskevich committed
91
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
92
driver = "drivers/tptp.drv"
MARCHE Claude's avatar
MARCHE Claude committed
93

94
95
[ATP verit]
name = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
96
exec = "veriT"
97
exec = "verit"
MARCHE Claude's avatar
MARCHE Claude committed
98
99
version_switch = "--help"
version_regexp = "Version: \\([^ \n\r]+\\)"
Andrei Paskevich's avatar
Andrei Paskevich committed
100
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
101
102
driver = "drivers/verit.drv"

François Bobot's avatar
François Bobot committed
103
[ATP z3_smtv1]
104
name = "Z3_smtv1"
105
106
exec = "z3"
exec = "z3-2.2"
MARCHE Claude's avatar
MARCHE Claude committed
107
version_switch = "-version"
108
version_regexp = "Z3 version \\([^ \n\r]+\\)"
François Bobot's avatar
François Bobot committed
109
version_old = "2.2"
MARCHE Claude's avatar
MARCHE Claude committed
110
111
version_old = "2.1"
version_old = "1.3"
Andrei Paskevich's avatar
Andrei Paskevich committed
112
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt %f"
113
driver = "drivers/z3.drv"
MARCHE Claude's avatar
MARCHE Claude committed
114

François Bobot's avatar
François Bobot committed
115
116
117
118
119
120
121
122
123
124
125
126
[ATP z3]
name = "Z3"
exec = "z3"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "2.19"
version_old = "2.18"
version_old = "2.17"
version_old = "2.16"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt2 %f"
driver = "drivers/z3_smtv2_array.drv"

MARCHE Claude's avatar
MARCHE Claude committed
127
128
[ITP coq]
name = "Coq"
129
exec = "coqc"
MARCHE Claude's avatar
MARCHE Claude committed
130
version_switch = "-v"
131
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
132
version_ok = "8.3"
133
version_ok = "8.2pl2"
MARCHE Claude's avatar
MARCHE Claude committed
134
version_ok = "8.2pl1"
135
136
137
version_ok = "8.2"
version_old = "8.1"
version_old = "8.0"
138
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e %f"
139
driver = "drivers/coq.drv"
MARCHE Claude's avatar
MARCHE Claude committed
140
editor = "coqide"
MARCHE Claude's avatar
MARCHE Claude committed
141
142