provers-detection-data.conf.in 7.66 KB
Newer Older
1
[ATP alt-ergo]
2 3 4 5
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-0.95-dev"
version_switch = "-version"
6
version_regexp = "\\([0-9.]+\\(-dev\\)?\\)"
7
version_ok = "0.95-dev"
8
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -timelimit %t -model %f"
9
driver = "drivers/alt_ergo_model.drv"
10 11
editor = "altgr-ergo"

12 13
[ATP alt-ergo]
name = "Alt-Ergo"
14
exec = "alt-ergo"
15
exec = "alt-ergo-0.94"
16 17 18
version_switch = "-version"
version_regexp = "\\([0-9.]+\\)"
version_ok = "0.94"
19
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
20
driver = "drivers/alt_ergo.drv"
21
editor = "altgr-ergo"
22 23 24 25

[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
26 27
exec = "alt-ergo-0.93.1"
exec = "alt-ergo-0.93"
MARCHE Claude's avatar
MARCHE Claude committed
28
version_switch = "-version"
29
version_regexp = "\\([0-9.]+\\)"
30
version_ok = "^0\.93\.[1-3]"
31
version_ok = "0.93"
32
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
33
driver = "drivers/alt_ergo_0.93.drv"
MARCHE Claude's avatar
MARCHE Claude committed
34

35
[ATP alt-ergo]
36
name = "Alt-Ergo"
37
exec = "alt-ergo"
38 39 40 41
exec = "alt-ergo-0.92.3"
exec = "alt-ergo-0.92.2"
exec = "alt-ergo-0.92.1"
exec = "alt-ergo-0.92"
42
exec = "alt-ergo-0.91"
43 44 45
exec = "alt-ergo-0.9"
exec = "alt-ergo-0.8"
exec = "ergo"
46
version_switch = "-version"
47
version_regexp = "\\([0-9.]+\\)"
48
version_old = "^0\.92\..+"
49 50
version_old = "0.92"
version_old = "0.91"
51 52
version_old = "0.9"
version_old = "0.8"
53
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
54
driver = "drivers/alt_ergo_bare.drv"
55

56
[ATP cvc3]
Andrei Paskevich's avatar
Andrei Paskevich committed
57
name = "CVC3"
58
exec = "cvc3"
59
exec = "cvc3-2.4.1"
60
exec = "cvc3-2.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
61 62
version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
63 64
version_ok  = "2.4.1"
version_old = "2.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
65
# the -timeout option is unreliable in CVC3 2.4.1
66
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
67 68
driver = "drivers/cvc3.drv"

69
[ATP cvc3]
MARCHE Claude's avatar
MARCHE Claude committed
70
name = "CVC3"
71
exec = "cvc3"
72 73
exec = "cvc3-2.2"
exec = "cvc3-2.1"
MARCHE Claude's avatar
MARCHE Claude committed
74
version_switch = "-version"
75
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
76
version_ok  = "2.2"
MARCHE Claude's avatar
MARCHE Claude committed
77
version_old = "2.1"
78
# we pass time 0 to why3-cpulimit to avoid race
79
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -timeout %t %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
80
driver = "drivers/cvc3.drv"
81

82 83 84 85 86
[ATP yices]
name = "Yices"
exec = "yices"
version_switch = "--version"
version_regexp = "[Yices ]*\\([^ \n]+\\)"
87 88 89 90
version_ok = "^1\.0\.3[0-5]"
version_ok = "^1\.0\.2[5-9]"
version_old = "^1\.0\.2[0-4]"
version_old = "^1\.0\.1."
91
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e"
92 93
driver = "drivers/yices.drv"

94 95 96
[ATP eprover]
name = "Eprover"
exec = "eprover"
97
version_switch = "--version"
Andrei Paskevich's avatar
Andrei Paskevich committed
98 99
version_regexp = "E \\([-0-9.]+\\) [^\n]+"
version_ok = "1.4"
100
# we pass time 0 to why3-cpulimit to avoid race
101
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
102
driver = "drivers/tptp.drv"
MARCHE Claude's avatar
MARCHE Claude committed
103 104 105

[ATP gappa]
name = "Gappa"
106
exec = "gappa"
MARCHE Claude's avatar
MARCHE Claude committed
107
version_switch = "--version"
108
version_regexp = "Gappa \\([^ \n]*\\)"
109 110 111
version_ok = "^0.16.[0-1]"
version_ok = "^0\.1[4-5]\..+"
version_old = "^0\.1[1-2]\..+"
112 113 114
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
driver = "drivers/gappa.drv"

115
[ATP gappa]
MARCHE Claude's avatar
MARCHE Claude committed
116 117 118 119 120 121 122 123
name = "Gappa+dev"
exec = "gappa-0.16.0+dev"
version_switch = "--version"
version_regexp = "Gappa \\([^ \n]*\\)"
version_ok = "0.16.0"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
driver = "drivers/gappa.drv"

124
[ATP gappa]
125 126 127 128 129 130 131 132
name = "Gappa"
exec = "gappa-0.15.1"
version_switch = "--version"
version_regexp = "Gappa \\([^ \n]*\\)"
version_ok = "0.15.1"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
driver = "drivers/gappa.drv"

133
[ATP gappa]
134 135 136 137 138 139
name = "Gappa"
exec = "gappa-0.14.1"
version_switch = "--version"
version_regexp = "Gappa \\([^ \n]*\\)"
version_ok = "0.14.1"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
140
driver = "drivers/gappa.drv"
MARCHE Claude's avatar
MARCHE Claude committed
141 142 143

[ATP simplify]
name = "Simplify"
144 145 146 147
exec = "Simplify"
exec = "simplify"
exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
MARCHE Claude's avatar
MARCHE Claude committed
148
version_switch = "-version"
149
version_regexp = "Simplify version \\([^ \n,]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
150
version_ok = "1.5.5"
151
version_ok = "1.5.4"
152
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
153 154 155 156 157
driver = "drivers/simplify.drv"

[ATP spass]
name = "Spass"
exec = "SPASS"
158
version_switch = "-TPTP || true"
159
version_regexp = "SPASS V \\([^ \n\t]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
160
version_ok = "3.7"
161
# we pass time 0 to why3-cpulimit to avoid race
162
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
163
driver = "drivers/tptp.drv"
MARCHE Claude's avatar
MARCHE Claude committed
164

MARCHE Claude's avatar
MARCHE Claude committed
165 166 167 168 169
[ATP vampire]
name = "Vampire"
exec = "vampire"
version_switch = "--version"
version_regexp = "Vampire \\([0-9.]+\\)"
170
# we pass time 0 to why3-cpulimit to avoid race
171
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -t %t"
MARCHE Claude's avatar
MARCHE Claude committed
172
driver = "drivers/vampire.drv"
173
version_ok = "0.6"
MARCHE Claude's avatar
MARCHE Claude committed
174

175 176
[ATP verit]
name = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
177
exec = "veriT"
178
exec = "verit"
MARCHE Claude's avatar
MARCHE Claude committed
179 180
version_switch = "--help"
version_regexp = "Version: \\([^ \n\r]+\\)"
181
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
182 183
driver = "drivers/verit.drv"

184
[ATP z3]
185 186 187 188 189 190 191 192 193
name = "Z3"
exec = "z3"
exec = "z3-4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok  = "4.0"
driver = "drivers/z3.drv"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt2 -rs:42 %f"

194
[ATP z3]
195
name = "Z3"
196
exec = "z3"
197
exec = "z3-3.2"
198 199
exec = "z3-3.1"
exec = "z3-3.0"
200 201
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
202
version_ok  = "^3\..+"
203 204 205
version_old = "3.1"
version_old = "3.0"
driver = "drivers/z3.drv"
Andrei Paskevich's avatar
Andrei Paskevich committed
206
# the -T is unreliable in Z3 3.2
207
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt2 -rs:42 %f"
208

209
[ATP z3]
François Bobot's avatar
François Bobot committed
210 211
name = "Z3"
exec = "z3"
212 213 214 215
exec = "z3-2.19"
exec = "z3-2.18"
exec = "z3-2.17"
exec = "z3-2.16"
François Bobot's avatar
François Bobot committed
216 217
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
218 219
version_old = "^2\.2.+"
version_old = "^2\.1[6-9]"
Andrei Paskevich's avatar
Andrei Paskevich committed
220
driver = "drivers/z3.drv"
221
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt2 -rs:42 \
222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240
PHASE_SELECTION=0 \
RESTART_STRATEGY=0 \
RESTART_FACTOR=1.5 \
QI_EAGER_THRESHOLD=100 \
ARITH_RANDOM_INITIAL_VALUE=true \
SORT_AND_OR=false \
CASE_SPLIT=3 \
DELAY_UNITS=true \
DELAY_UNITS_THRESHOLD=16 \
%f"
#Other Parameters given by Nikolaj Bjorner
#BV_REFLECT=true #arith?
#MODEL_PARTIAL=true
#MODEL_VALUE_COMPLETION=false
#MODEL_HIDE_UNUSED_PARTITIONS=false
#MODEL_V1=true
#ASYNC_COMMANDS=false
#NNF_SK_HACK=true

241
[ATP z3]
242
name = "Z3"
243 244
exec = "z3"
exec = "z3-2.2"
245 246
exec = "z3-2.1"
exec = "z3-1.3"
247 248
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
249 250
version_old = "^2\.1[0-5]"
version_old = "^2\.[0-9]"
251
version_old = "1.3"
252
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
253
driver = "drivers/z3_smtv1.drv"
254

MARCHE Claude's avatar
MARCHE Claude committed
255 256
[ITP coq]
name = "Coq"
257
exec = "coqtop -batch"
MARCHE Claude's avatar
MARCHE Claude committed
258
version_switch = "-v"
259
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
260
version_ok = "8.3pl4"
261
version_ok = "8.3pl3"
262 263
version_ok = "8.3pl2"
version_ok = "8.3pl1"
MARCHE Claude's avatar
MARCHE Claude committed
264
version_ok = "8.3"
265 266 267 268 269 270 271 272 273
command = "'@LOCALBIN@why3-cpulimit' 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
driver = "drivers/coq.drv"
editor = "coqide"

[ITP coq]
name = "Coq"
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
274 275 276
version_old = "8.2pl2"
version_old = "8.2pl1"
version_old = "8.2"
277 278
version_old = "8.1"
version_old = "8.0"
279
command = "'@LOCALBIN@why3-cpulimit' 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
280
driver = "drivers/coq.drv"
281
editor = "coqide"
MARCHE Claude's avatar
MARCHE Claude committed
282

283 284 285 286 287 288 289 290
[ITP pvs]
name = "PVS"
exec = "pvs"
version_switch = "-version"
version_regexp = "PVS Version \\([^ \n]+\\)"
version_ok = "5.0"
command = "'@LOCALBIN@why3-cpulimit' 0 %m -s @LOCALBIN@why3-check-pvs %l %f"
driver = "drivers/pvs.drv"
291
in_place = true
292
editor = "pvs"
293

294 295 296
[editor pvs]
name = "PVS"
command = "@LOCALBIN@why3-call-pvs %l %f"
297 298

[editor coqide]
MARCHE Claude's avatar
MARCHE Claude committed
299
name = "CoqIDE"
300 301 302
command = "coqide -I %l/coq-tactic -R %l/coq Why3 %f"

[editor proofgeneral-coq]
MARCHE Claude's avatar
MARCHE Claude committed
303
name = "Emacs/ProofGeneral/Coq"
304
command = "emacs23 --eval \"(setq coq-load-path '((\\\"%l/coq\\\" \\\"Why3\\\")))\" %f"
305 306

[editor altgr-ergo]
MARCHE Claude's avatar
MARCHE Claude committed
307
name = "AltGr-Ergo"
308
command = "altgr-ergo %f"
309 310 311 312

[shortcut shortcut1]
name="Alt-Ergo"
shortcut="altergo"