provers-detection-data.conf.in 8.85 KB
Newer Older
1
[ATP alt-ergo-model]
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 8 9 10 11 12 13 14 15 16 17
version_ok = "0.95-dev"
version_bad = "0.94"
version_bad = "0.93.1"
version_bad = "0.93"
version_bad = "0.92.3"
version_bad = "0.92.2"
version_bad = "0.92.1"
version_bad = "0.92"
version_bad = "0.91"
version_bad = "0.9"
version_bad = "0.8"
18
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -timelimit %t -model %f"
19
driver = "drivers/alt_ergo_model.drv"
20 21
editor = "altgr-ergo"

22 23
[ATP alt-ergo]
name = "Alt-Ergo"
24
exec = "alt-ergo"
25
exec = "alt-ergo-0.94"
26 27 28 29 30 31 32 33 34 35 36 37
version_switch = "-version"
version_regexp = "\\([0-9.]+\\)"
version_ok = "0.94"
version_bad = "0.93.1"
version_bad = "0.93"
version_bad = "0.92.3"
version_bad = "0.92.2"
version_bad = "0.92.1"
version_bad = "0.92"
version_bad = "0.91"
version_bad = "0.9"
version_bad = "0.8"
38
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
39
driver = "drivers/alt_ergo.drv"
40
editor = "altgr-ergo"
41 42 43 44

[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
45 46
exec = "alt-ergo-0.93.1"
exec = "alt-ergo-0.93"
MARCHE Claude's avatar
MARCHE Claude committed
47
version_switch = "-version"
48
version_regexp = "\\([0-9.]+\\)"
49
version_ok = "0.93.1"
50 51 52 53 54 55 56 57
version_ok = "0.93"
version_bad = "0.92.3"
version_bad = "0.92.2"
version_bad = "0.92.1"
version_bad = "0.92"
version_bad = "0.91"
version_bad = "0.9"
version_bad = "0.8"
58
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
59
driver = "drivers/alt_ergo_0.93.drv"
MARCHE Claude's avatar
MARCHE Claude committed
60

61
[ATP alt-ergo]
62
name = "Alt-Ergo"
63
exec = "alt-ergo"
64 65 66 67
exec = "alt-ergo-0.92.3"
exec = "alt-ergo-0.92.2"
exec = "alt-ergo-0.92.1"
exec = "alt-ergo-0.92"
68
exec = "alt-ergo-0.91"
69 70 71
exec = "alt-ergo-0.9"
exec = "alt-ergo-0.8"
exec = "ergo"
72
version_switch = "-version"
73 74
version_regexp = "\\([0-9.]+\\)"
version_old = "0.92.3"
75 76 77 78
version_old = "0.92.2"
version_old = "0.92.1"
version_old = "0.92"
version_old = "0.91"
79 80
version_old = "0.9"
version_old = "0.8"
81
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
82
driver = "drivers/alt_ergo_bare.drv"
83

84
[ATP cvc3-2.4]
Andrei Paskevich's avatar
Andrei Paskevich committed
85
name = "CVC3"
86
exec = "cvc3"
87
exec = "cvc3-2.4.1"
88
exec = "cvc3-2.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
89 90
version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
91 92
version_ok  = "2.4.1"
version_old = "2.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
93 94 95
version_bad = "2.2"
version_bad = "2.1"
# the -timeout option is unreliable in CVC3 2.4.1
96
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
97 98
driver = "drivers/cvc3.drv"

99
[ATP cvc3-2.2]
MARCHE Claude's avatar
MARCHE Claude committed
100
name = "CVC3"
101
exec = "cvc3"
102 103
exec = "cvc3-2.2"
exec = "cvc3-2.1"
MARCHE Claude's avatar
MARCHE Claude committed
104
version_switch = "-version"
105
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
106 107 108
version_bad = "2.4.1"
version_bad = "2.4"
version_ok  = "2.2"
MARCHE Claude's avatar
MARCHE Claude committed
109
version_old = "2.1"
110
# we pass time 0 to why3-cpulimit to avoid race
111
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -timeout %t %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
112
driver = "drivers/cvc3.drv"
113

114 115 116 117 118
[ATP yices]
name = "Yices"
exec = "yices"
version_switch = "--version"
version_regexp = "[Yices ]*\\([^ \n]+\\)"
119
version_ok = "1.0.35"
120 121
version_ok = "1.0.29"
version_ok = "1.0.28"
122
version_ok = "1.0.27"
123 124
version_ok = "1.0.26"
version_ok = "1.0.25"
125 126
version_old = "1.0.17"
version_old = "1.0.24"
127
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e"
128 129
driver = "drivers/yices.drv"

130 131 132
[ATP eprover]
name = "Eprover"
exec = "eprover"
133
version_switch = "--version"
Andrei Paskevich's avatar
Andrei Paskevich committed
134 135
version_regexp = "E \\([-0-9.]+\\) [^\n]+"
version_ok = "1.4"
136
# we pass time 0 to why3-cpulimit to avoid race
137
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
138
driver = "drivers/tptp.drv"
MARCHE Claude's avatar
MARCHE Claude committed
139 140 141

[ATP gappa]
name = "Gappa"
142
exec = "gappa"
MARCHE Claude's avatar
MARCHE Claude committed
143
version_switch = "--version"
144
version_regexp = "Gappa \\([^ \n]*\\)"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
145
version_ok = "0.16.1"
146
version_ok = "0.16.0"
MARCHE Claude's avatar
MARCHE Claude committed
147
version_ok = "0.15.1"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
148 149
version_ok = "0.15.0"
version_ok = "0.14.1"
150
version_ok = "0.14.0"
MARCHE Claude's avatar
MARCHE Claude committed
151 152
version_ok = "0.13.0"
version_old = "0.12.3"
153 154 155 156
version_old = "0.12.2"
version_old = "0.12.1"
version_old = "0.12.0"
version_old = "0.11.2"
157 158 159
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
driver = "drivers/gappa.drv"

MARCHE Claude's avatar
MARCHE Claude committed
160 161 162 163 164 165 166 167 168
[ATP gappa016dev]
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"

169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184
[ATP gappa015]
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"

[ATP gappa014]
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"
185
driver = "drivers/gappa.drv"
MARCHE Claude's avatar
MARCHE Claude committed
186 187 188

[ATP simplify]
name = "Simplify"
189 190 191 192
exec = "Simplify"
exec = "simplify"
exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
MARCHE Claude's avatar
MARCHE Claude committed
193
version_switch = "-version"
194
version_regexp = "Simplify version \\([^ \n,]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
195
version_ok = "1.5.5"
196
version_ok = "1.5.4"
197
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
198 199 200 201 202
driver = "drivers/simplify.drv"

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

MARCHE Claude's avatar
MARCHE Claude committed
210 211 212 213 214
[ATP vampire]
name = "Vampire"
exec = "vampire"
version_switch = "--version"
version_regexp = "Vampire \\([0-9.]+\\)"
215
# we pass time 0 to why3-cpulimit to avoid race
216
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -t %t"
MARCHE Claude's avatar
MARCHE Claude committed
217
driver = "drivers/vampire.drv"
218
version_ok = "0.6"
MARCHE Claude's avatar
MARCHE Claude committed
219

220 221
[ATP verit]
name = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
222
exec = "veriT"
223
exec = "verit"
MARCHE Claude's avatar
MARCHE Claude committed
224 225
version_switch = "--help"
version_regexp = "Version: \\([^ \n\r]+\\)"
226
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
227 228
driver = "drivers/verit.drv"

229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248
[ATP z3-4]
name = "Z3"
exec = "z3"
exec = "z3-4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok  = "4.0"
version_bad = "3.2"
version_bad = "3.1"
version_bad = "3.0"
version_bad = "2.19"
version_bad = "2.18"
version_bad = "2.17"
version_bad = "2.16"
version_bad = "2.2"
version_bad = "2.1"
version_bad = "1.3"
driver = "drivers/z3.drv"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt2 -rs:42 %f"

249
[ATP z3-3]
250
name = "Z3"
251
exec = "z3"
252
exec = "z3-3.2"
253 254
exec = "z3-3.1"
exec = "z3-3.0"
255 256
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
257
version_bad = "4.0"
258
version_ok  = "3.2"
259 260 261 262 263 264 265 266 267 268
version_old = "3.1"
version_old = "3.0"
version_bad = "2.19"
version_bad = "2.18"
version_bad = "2.17"
version_bad = "2.16"
version_bad = "2.2"
version_bad = "2.1"
version_bad = "1.3"
driver = "drivers/z3.drv"
Andrei Paskevich's avatar
Andrei Paskevich committed
269
# the -T is unreliable in Z3 3.2
270
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt2 -rs:42 %f"
271

272
[ATP z3-2]
François Bobot's avatar
François Bobot committed
273 274
name = "Z3"
exec = "z3"
275 276 277 278
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
279 280
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
281
version_bad = "4.0"
282 283 284 285
version_bad = "3.2"
version_bad = "3.1"
version_bad = "3.0"
version_ok  = "2.19"
François Bobot's avatar
François Bobot committed
286 287 288
version_old = "2.18"
version_old = "2.17"
version_old = "2.16"
289 290 291
version_bad = "2.2"
version_bad = "2.1"
version_bad = "1.3"
Andrei Paskevich's avatar
Andrei Paskevich committed
292
driver = "drivers/z3.drv"
293
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt2 -rs:42 \
294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312
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

313 314
[ATP z3-2]
name = "Z3"
315 316
exec = "z3"
exec = "z3-2.2"
317 318
exec = "z3-2.1"
exec = "z3-1.3"
319 320
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
321 322 323
version_bad = "3.2"
version_bad = "3.1"
version_bad = "3.0"
324 325 326
version_old = "2.2"
version_old = "2.1"
version_old = "1.3"
327
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
328
driver = "drivers/z3_smtv1.drv"
329

MARCHE Claude's avatar
MARCHE Claude committed
330 331
[ITP coq]
name = "Coq"
332
exec = "coqtop -batch"
MARCHE Claude's avatar
MARCHE Claude committed
333
version_switch = "-v"
334
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
335
version_ok = "8.3pl4"
336
version_ok = "8.3pl3"
337 338
version_ok = "8.3pl2"
version_ok = "8.3pl1"
MARCHE Claude's avatar
MARCHE Claude committed
339
version_ok = "8.3"
340 341 342
version_old = "8.2pl2"
version_old = "8.2pl1"
version_old = "8.2"
343 344
version_old = "8.1"
version_old = "8.0"
345
command = "'@LOCALBIN@why3-cpulimit' 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
346
driver = "drivers/coq.drv"
347
editor = "coqide"
MARCHE Claude's avatar
MARCHE Claude committed
348

349 350 351 352 353 354 355 356
[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"
357
in_place = true
358
editor = "pvs"
359

360 361 362
[editor pvs]
name = "PVS"
command = "@LOCALBIN@why3-call-pvs %l %f"
363 364

[editor coqide]
MARCHE Claude's avatar
MARCHE Claude committed
365
name = "CoqIDE"
366 367 368
command = "coqide -I %l/coq-tactic -R %l/coq Why3 %f"

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

[editor altgr-ergo]
MARCHE Claude's avatar
MARCHE Claude committed
373
name = "AltGr-Ergo"
374
command = "altgr-ergo %f"