provers-detection-data.conf 11.9 KB
Newer Older
1 2 3
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
Andrei Paskevich's avatar
Andrei Paskevich committed
4
exec = "alt-ergo-0.95.2"
5 6
version_switch = "-version"
version_regexp = "\\([0-9.]+\\(-dev\\)?\\)"
MARCHE Claude's avatar
MARCHE Claude committed
7 8
version_ok  = "0.95.2"
command = "%l/why3-cpulimit %t %m -s %e -timelimit %t %f"
9 10 11
driver = "drivers/alt_ergo.drv"
editor = "altgr-ergo"

MARCHE Claude's avatar
MARCHE Claude committed
12
[ATP alt-ergo]
13
name = "Alt-Ergo"
14
exec = "alt-ergo"
Andrei Paskevich's avatar
Andrei Paskevich committed
15
exec = "alt-ergo-0.95.1"
16
exec = "alt-ergo-0.95"
17
version_switch = "-version"
18
version_regexp = "\\([0-9.]+\\(-dev\\)?\\)"
19 20
version_ok  = "0.95.1"
version_old = "0.95"
MARCHE Claude's avatar
MARCHE Claude committed
21 22
command = "%l/why3-cpulimit %T %m -s %e -timelimit %t %f"
driver = "drivers/alt_ergo.drv"
23
editor = "altgr-ergo"
24

MARCHE Claude's avatar
MARCHE Claude committed
25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42
# [ATP alt-ergo-model]
# name = "Alt-Ergo"
# alternative = "models"
# exec = "alt-ergo"
# exec = "alt-ergo-0.95.3"
# exec = "alt-ergo-0.95.2"
# exec = "alt-ergo-0.95.1"
# exec = "alt-ergo-0.95"
# exec = "alt-ergo-0.95-dev"
# version_switch = "-version"
# version_regexp = "\\([0-9.]+\\(-dev\\)?\\)"
# version_ok  = "0.95.1"
# version_old = "0.95"
# version_old = "0.95-dev"
# command = "%l/why3-cpulimit %T %m -s %e -timelimit %t -model %f"
# driver = "drivers/alt_ergo_model.drv"
# editor = "altgr-ergo"

43 44 45 46 47 48
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-0.94"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\)"
49
version_old = "0.94"
50
command = "%l/why3-cpulimit %t %m -s %e %f"
51 52 53
driver = "drivers/alt_ergo_0.94.drv"
editor = "altgr-ergo"

54 55 56
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
57 58
exec = "alt-ergo-0.93.1"
exec = "alt-ergo-0.93"
MARCHE Claude's avatar
MARCHE Claude committed
59
version_switch = "-version"
60
version_regexp = "\\([0-9.]+\\)"
61 62
version_old = "^0\.93\..+$"
version_old = "0.93"
63
command = "%l/why3-cpulimit %t %m -s %e %f"
64
driver = "drivers/alt_ergo_0.93.drv"
MARCHE Claude's avatar
MARCHE Claude committed
65

66
[ATP alt-ergo]
67
name = "Alt-Ergo"
68
exec = "alt-ergo"
69 70 71 72
exec = "alt-ergo-0.92.3"
exec = "alt-ergo-0.92.2"
exec = "alt-ergo-0.92.1"
exec = "alt-ergo-0.92"
73
exec = "alt-ergo-0.91"
74 75 76
exec = "alt-ergo-0.9"
exec = "alt-ergo-0.8"
exec = "ergo"
77
version_switch = "-version"
78
version_regexp = "\\([0-9.]+\\)"
79
version_old = "^0\.92\..+$"
80 81
version_old = "0.92"
version_old = "0.91"
82 83
version_old = "0.9"
version_old = "0.8"
84
command = "%l/why3-cpulimit %t %m -s %e %f"
85
driver = "drivers/alt_ergo_0.92.drv"
86

87
# CVC4 version 1.x
88 89 90 91
[ATP cvc4]
name = "CVC4"
exec = "cvc4"
exec = "cvc4-1.0"
92 93
exec = "cvc4-1.1"
exec = "cvc4-1.2"
MARCHE Claude's avatar
MARCHE Claude committed
94
exec = "cvc4-1.3"
95 96 97
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok  = "1.0"
98 99
version_ok  = "1.1"
version_ok  = "1.2"
MARCHE Claude's avatar
MARCHE Claude committed
100
version_ok  = "1.3"
101
driver = "drivers/cvc4.drv"
102
command = "%l/why3-cpulimit %t %m -s %e --lang=smt2 %f"
103

104
# CVC3 versions 2.4.x
105
[ATP cvc3]
Andrei Paskevich's avatar
Andrei Paskevich committed
106
name = "CVC3"
107
exec = "cvc3"
108
exec = "cvc3-2.4.1"
109
exec = "cvc3-2.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
110 111
version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
112 113
version_ok  = "2.4.1"
version_old = "2.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
114
# the -timeout option is unreliable in CVC3 2.4.1
115
command = "%l/why3-cpulimit %t %m -s %e -seed 42 %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
116 117
driver = "drivers/cvc3.drv"

118
# CVC3 versions 2.x
119
[ATP cvc3]
MARCHE Claude's avatar
MARCHE Claude committed
120
name = "CVC3"
121
exec = "cvc3"
122 123
exec = "cvc3-2.2"
exec = "cvc3-2.1"
MARCHE Claude's avatar
MARCHE Claude committed
124
version_switch = "-version"
125
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
126
version_old = "2.2"
MARCHE Claude's avatar
MARCHE Claude committed
127
version_old = "2.1"
128
# we pass time 0 to why3-cpulimit to avoid race
129
command = "%l/why3-cpulimit %T %m -s %e  -seed 42 -timeout %t %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
130
driver = "drivers/cvc3.drv"
131

132 133 134
[ATP yices]
name = "Yices"
exec = "yices"
135
exec = "yices-1.0.38"
136 137
version_switch = "--version"
version_regexp = "[Yices ]*\\([^ \n]+\\)"
138 139 140
version_ok = "1.0.38"
version_old = "^1\.0\.3[0-7]$"
version_old = "^1\.0\.2[5-9]$"
141 142
version_old = "^1\.0\.2[0-4]$"
version_old = "^1\.0\.1\.*$"
143
command = "%l/why3-cpulimit %t %m -s %e"
144 145
driver = "drivers/yices.drv"

146 147 148 149 150 151 152
[ATP yices2]
name = "Yices2"
exec = "yices"
exec = "yices-2.0.4"
version_switch = "--version"
version_regexp = "[Yices ]*\\([^ \n]+\\)\."
version_ok = "^2\.0\.4"
153
command = "%l/why3-cpulimit %t %m -s %e"
154 155
driver = "drivers/yices.drv"

156 157 158
[ATP eprover]
name = "Eprover"
exec = "eprover"
159 160 161
exec = "eprover-1.6"
exec = "eprover-1.5"
exec = "eprover-1.4"
162
version_switch = "--version"
Andrei Paskevich's avatar
Andrei Paskevich committed
163
version_regexp = "E \\([-0-9.]+\\) [^\n]+"
164 165 166
version_ok  = "1.6"
version_old = "1.5"
version_old = "1.4"
167
# we pass time 0 to why3-cpulimit to avoid race
168
command = "%l/why3-cpulimit %T %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
MARCHE Claude's avatar
MARCHE Claude committed
169
driver = "drivers/eprover.drv"
MARCHE Claude's avatar
MARCHE Claude committed
170 171 172

[ATP gappa]
name = "Gappa"
173
exec = "gappa"
MARCHE Claude's avatar
MARCHE Claude committed
174 175
exec = "gappa-0.15.1"
exec = "gappa-0.14.1"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
176 177
exec = "gappa-0.13.0"
exec = "gappa-0.12.3"
MARCHE Claude's avatar
MARCHE Claude committed
178
version_switch = "--version"
179
version_regexp = "Gappa \\([^ \n]*\\)"
180 181
version_ok = "^1\.0\..+$"
version_ok = "^0\.1[4-8]\..+$"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
182
version_old = "^0\.1[1-3]\..+$"
183
command = "%l/why3-cpulimit %t %m -s %e -Eprecision=70"
184 185
driver = "drivers/gappa.drv"

186 187 188
[ATP mathsat]
name = "MathSAT5"
exec = "mathsat"
189
exec = "mathsat-5.2.2"
190 191 192
version_switch = "-version"
version_regexp = "MathSAT5 version \\([^ \n]+\\)"
version_ok  = "5.2.2"
193
command = "%l/why3-cpulimit %t %m -s %e -input=smt2 -model -random_seed=80 %f"
194 195
driver = "drivers/mathsat.drv"

MARCHE Claude's avatar
MARCHE Claude committed
196 197
[ATP simplify]
name = "Simplify"
198 199 200 201
exec = "Simplify"
exec = "simplify"
exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
MARCHE Claude's avatar
MARCHE Claude committed
202
version_switch = "-version"
203
version_regexp = "Simplify version \\([^ \n,]+\\)"
204 205
version_old = "1.5.5"
version_old = "1.5.4"
206
command = "%l/why3-cpulimit %t %m -s %e %f"
207 208
driver = "drivers/simplify.drv"

209 210 211 212 213 214
[ATP metis]
name = "Metis"
exec = "metis"
version_switch = "-v"
version_regexp = "metis \\([^ \n,]+\\)"
version_ok = "2.3"
215
command = "%l/why3-cpulimit %T %m -s %e --time-limit %t %f"
216 217 218 219 220 221 222 223
driver = "drivers/metis.drv"

[ATP metitarski]
name = "MetiTarski"
exec = "metit"
version_switch = "-v"
version_regexp = "MetiTarski \\([^ \n,]+\\)"
version_ok = "2.2"
224
command = "%l/why3-cpulimit %T %m -s %e --time %t %f"
225 226
driver = "drivers/metitarski.drv"

227 228 229
[ATP spass]
name = "Spass"
exec = "SPASS"
230
exec = "SPASS-3.7"
231
version_switch = " | grep 'SPASS V'"
232
version_regexp = "SPASS V \\([^ \n\t]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
233
version_ok = "3.7"
234
command = "%l/why3-cpulimit %T %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
MARCHE Claude's avatar
MARCHE Claude committed
235
driver = "drivers/spass.drv"
MARCHE Claude's avatar
MARCHE Claude committed
236

237 238 239 240 241 242 243
[ATP spass]
name = "Spass"
exec = "SPASS"
exec = "SPASS-3.8ds"
version_switch = " | grep 'SPASS[^ \\n\\t]* V'"
version_regexp = "SPASS[^ \n\t]* V \\([^ \n\t]+\\)"
version_ok = "3.8ds"
244
command = "%l/why3-cpulimit %T %m -s %e -Isabelle=1 -PGiven=0 -TimeLimit=%t %f"
245 246
driver = "drivers/spass_types.drv"

MARCHE Claude's avatar
MARCHE Claude committed
247 248 249
[ATP vampire]
name = "Vampire"
exec = "vampire"
250
exec = "vampire-0.6"
MARCHE Claude's avatar
MARCHE Claude committed
251 252
version_switch = "--version"
version_regexp = "Vampire \\([0-9.]+\\)"
253
# we pass time 0 to why3-cpulimit to avoid race
254
command = "%l/why3-cpulimit %T %m -s %e -t %t"
MARCHE Claude's avatar
MARCHE Claude committed
255
driver = "drivers/vampire.drv"
256
version_ok = "0.6"
MARCHE Claude's avatar
MARCHE Claude committed
257

258 259 260 261
[ATP princess]
name = "Princess"
exec = "princess"
# version_switch = "-h"
262
version_regexp = "(CASC version \\([0-9-]+\\))"
263
command = "%l/why3-cpulimit %T 0 -s %e -timeout=%t %f"
264
driver = "drivers/princess.drv"
265 266 267 268 269 270 271 272
version_ok = "2013-05-13"

[ATP beagle]
name = "Beagle"
exec = "beagle"
exec = "beagle-0.4.1"
# version_switch = "-h"
version_regexp = "version \\([0-9.]+\\)"
273
command = "%l/why3-cpulimit %t 0 -s %e %f"
274 275
driver = "drivers/beagle.drv"
version_ok = "0.4.1"
276

277 278
[ATP verit]
name = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
279
exec = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
280 281
exec = "veriT-201310"
version_switch = "--version"
MARCHE Claude's avatar
MARCHE Claude committed
282
version_regexp = "version \\([^ \n\r]+\\)"
283 284
command = "%l/why3-cpulimit %t %m -s %e --disable-print-success --enable-simp \
--enable-unit-simp --enable-simp-sym --enable-unit-subst-simp --enable-bclause %f"
285
driver = "drivers/verit.drv"
MARCHE Claude's avatar
MARCHE Claude committed
286
version_ok = "201310"
287

288
[ATP z3]
289 290
name = "Z3"
exec = "z3"
291 292
exec = "z3-4.3.1"
exec = "z3-4.3.0"
MARCHE Claude's avatar
MARCHE Claude committed
293
exec = "z3-4.2"
294 295
exec = "z3-4.1.2"
exec = "z3-4.1.1"
296 297 298
exec = "z3-4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
299
version_ok  = "4.3.1"
300 301 302 303 304
version_old = "4.3.0"
version_old = "4.2"
version_old = "4.1.2"
version_old = "4.1.1"
version_old = "4.0"
305
driver = "drivers/z3.drv"
306
command = "%l/why3-cpulimit %t %m -s %e -smt2 -rs:42 %f"
307

308
[ATP z3]
309
name = "Z3"
310
exec = "z3"
311
exec = "z3-3.2"
312 313
exec = "z3-3.1"
exec = "z3-3.0"
314 315
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
316
version_old = "3.2"
317 318 319
version_old = "3.1"
version_old = "3.0"
driver = "drivers/z3.drv"
Andrei Paskevich's avatar
Andrei Paskevich committed
320
# the -T is unreliable in Z3 3.2
321
command = "%l/why3-cpulimit %t %m -s %e -smt2 -rs:42 %f"
322

323
[ATP z3]
François Bobot's avatar
François Bobot committed
324 325
name = "Z3"
exec = "z3"
326 327 328 329
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
330 331
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
332 333
version_old = "^2\.2.+$"
version_old = "^2\.1[6-9]$"
Andrei Paskevich's avatar
Andrei Paskevich committed
334
driver = "drivers/z3.drv"
335
command = "%l/why3-cpulimit %t %m -s %e -smt2 -rs:42 \
336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354
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

355
[ATP z3]
356
name = "Z3"
357 358
exec = "z3"
exec = "z3-2.2"
359 360
exec = "z3-2.1"
exec = "z3-1.3"
361 362
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
363 364
version_old = "^2\.1[0-5]$"
version_old = "^2\.[0-9]$"
365
version_old = "1.3"
366
command = "%l/why3-cpulimit %t %m -s %e -smt %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
367
driver = "drivers/z3_smtv1.drv"
368

369 370 371 372 373 374 375
[ATP zenon]
name = "Zenon"
exec = "zenon"
exec = "zenon-0.7.1"
version_switch = "-v"
version_regexp = "zenon version \\([^ \n\t]+\\)"
version_ok = "0.7.1"
376
command = "%l/why3-cpulimit %T 0 -s %e -p0 -itptp -max-size %mM -max-time %ts %f"
377 378 379 380 381
driver = "drivers/zenon.drv"

[ATP iprover]
name = "iProver"
exec = "iprover"
382
exec = "iprover-0.8.1"
383 384 385
version_switch = " | grep iProver"
version_regexp = "iProver v\\([^ \n\t]+\\)"
version_ok = "0.8.1"
386
command = "%l/why3-cpulimit %T %m -s %e --fof true --out_options none \
387 388
--time_out_virtual %t --clausifier /usr/bin/env --clausifier_options \
\"eprover --cnf --tstp-format \" %f"
389 390
driver = "drivers/iprover.drv"

Daisuke Ishii's avatar
Daisuke Ishii committed
391 392 393 394 395
[ATP mathematica]
name = "Mathematica"
exec = "math"
version_switch = "-run \"Exit[]\""
version_regexp = "Mathematica \\([0-9.]+\\)"
396
version_ok = "9.0"
Daisuke Ishii's avatar
Daisuke Ishii committed
397 398
version_ok = "8.0"
version_ok = "7.0"
399
command = "%l/why3-cpulimit %t %m -s %e -noprompt"
Daisuke Ishii's avatar
Daisuke Ishii committed
400 401
driver = "drivers/mathematica.drv"

MARCHE Claude's avatar
MARCHE Claude committed
402 403
[ITP coq]
name = "Coq"
404
compile_time_support = true
405
exec = "coqtop -batch"
MARCHE Claude's avatar
MARCHE Claude committed
406
version_switch = "-v"
407
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
408
version_ok = "8.4pl2"
MARCHE Claude's avatar
MARCHE Claude committed
409
version_ok = "8.4pl1"
410
version_ok = "8.4"
411
command = "%l/why3-cpulimit 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
MARCHE Claude's avatar
MARCHE Claude committed
412 413 414 415 416
driver = "drivers/coq_8_4.drv"
editor = "coqide"

[ITP coq]
name = "Coq"
417
compile_time_support = true
MARCHE Claude's avatar
MARCHE Claude committed
418 419 420
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
421
version_ok = "8.3pl4"
422
version_ok = "8.3pl3"
423 424
version_ok = "8.3pl2"
version_ok = "8.3pl1"
MARCHE Claude's avatar
MARCHE Claude committed
425
version_ok = "8.3"
426
command = "%l/why3-cpulimit 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
427 428 429
driver = "drivers/coq.drv"
editor = "coqide"

430 431
[ITP pvs]
name = "PVS"
432
compile_time_support = true
433 434 435
exec = "pvs"
version_switch = "-version"
version_regexp = "PVS Version \\([^ \n]+\\)"
436
version_ok = "6.0"
437
version_bad = "^[0-5]\..+$"
438 439
# not why3-cpulimit 0 %m because 'proveit' allocates 8Gb at start-up
command = "%l/why3-cpulimit 0 0 -s %l/why3-call-pvs %l proveit -f %f"
440
driver = "drivers/pvs.drv"
441
in_place = true
442
editor = "pvs"
443

444 445 446 447 448
[ITP isabelle]
name = "Isabelle"
exec = "isabelle"
version_switch = "version"
version_regexp = "Isabelle\\([^:]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
449
version_ok = "2013-2"
450 451
# not why3-cpulimit 0 %m because isabelle needs more memory at start-up
command = "%l/why3-cpulimit 0 0 -s %e why3 -b %f"
452
driver = "drivers/isabelle.drv"
453
in_place = true
454
editor = "jedit-isabelle"
455

456 457
[editor pvs]
name = "PVS"
458
command = "%l/why3-call-pvs %l pvs %f"
459 460

[editor coqide]
MARCHE Claude's avatar
MARCHE Claude committed
461
name = "CoqIDE"
462 463 464
command = "coqide -I %l/coq-tactic -R %l/coq Why3 %f"

[editor proofgeneral-coq]
MARCHE Claude's avatar
MARCHE Claude committed
465
name = "Emacs/ProofGeneral/Coq"
466 467
command = "emacs23 --eval \"(setq coq-load-path '(\\\"%l/coq-tactic\\\" \
(\\\"%l/coq\\\" \\\"Why3\\\")))\" %f"
468

469
[editor jedit-isabelle]
MARCHE Claude's avatar
MARCHE Claude committed
470
name = "Isabelle/jEdit"
471 472 473 474 475 476
command = "isabelle why3 -i jedit %f"

[editor proofgeneral-isabelle]
name = "Emacs/ProofGeneral/Isabelle"
command = "isabelle why3 -i emacs %f"

477
[editor altgr-ergo]
MARCHE Claude's avatar
MARCHE Claude committed
478
name = "AltGr-Ergo"
479
command = "altgr-ergo %f"
480 481 482 483

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