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

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

MARCHE Claude's avatar
MARCHE Claude committed
27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
# [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"

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

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

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

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

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

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

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

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

160 161 162
[ATP eprover]
name = "Eprover"
exec = "eprover"
MARCHE Claude's avatar
MARCHE Claude committed
163 164
exec = "eprover-1.8"
exec = "eprover-1.7"
165 166 167
exec = "eprover-1.6"
exec = "eprover-1.5"
exec = "eprover-1.4"
168
version_switch = "--version"
Andrei Paskevich's avatar
Andrei Paskevich committed
169
version_regexp = "E \\([-0-9.]+\\) [^\n]+"
MARCHE Claude's avatar
MARCHE Claude committed
170
version_ok  = "1.8-001"
171 172
version_old = "1.7"
version_old = "1.6"
173 174
version_old = "1.5"
version_old = "1.4"
175
# we pass time 0 to why3-cpulimit to avoid race
176
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
177
driver = "drivers/eprover.drv"
MARCHE Claude's avatar
MARCHE Claude committed
178 179 180

[ATP gappa]
name = "Gappa"
181
exec = "gappa"
182
exec = "gappa-1.1.1"
183
exec = "gappa-1.1.0"
184
exec = "gappa-1.0.0"
MARCHE Claude's avatar
MARCHE Claude committed
185
exec = "gappa-0.16.1"
186
exec = "gappa-0.14.1"
MARCHE Claude's avatar
MARCHE Claude committed
187
version_switch = "--version"
188
version_regexp = "Gappa \\([^ \n]*\\)"
189
version_ok = "^1\.[0-1]\..+$"
190
version_old = "^0\.1[1-8]\..+$"
191
command = "%l/why3-cpulimit %t %m -s %e -Eprecision=70"
192 193
driver = "drivers/gappa.drv"

194 195 196
[ATP mathsat]
name = "MathSAT5"
exec = "mathsat"
197
exec = "mathsat-5.2.2"
198 199 200
version_switch = "-version"
version_regexp = "MathSAT5 version \\([^ \n]+\\)"
version_ok  = "5.2.2"
201
command = "%l/why3-cpulimit %t %m -s %e -input=smt2 -model -random_seed=80 %f"
202 203
driver = "drivers/mathsat.drv"

MARCHE Claude's avatar
MARCHE Claude committed
204 205
[ATP simplify]
name = "Simplify"
206 207 208 209
exec = "Simplify"
exec = "simplify"
exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
MARCHE Claude's avatar
MARCHE Claude committed
210
version_switch = "-version"
211
version_regexp = "Simplify version \\([^ \n,]+\\)"
212 213
version_old = "1.5.5"
version_old = "1.5.4"
214
command = "%l/why3-cpulimit %t %m -s %e %f"
215 216
driver = "drivers/simplify.drv"

217 218 219 220 221 222
[ATP metis]
name = "Metis"
exec = "metis"
version_switch = "-v"
version_regexp = "metis \\([^ \n,]+\\)"
version_ok = "2.3"
223 224 225 226
# %U means 2*timelimit+1. Required because Metis tends to
# react very slowly to the time limit given, hence answers
# oscillate between Timeout and Unknown
command = "%l/why3-cpulimit %U %m -s %e --time-limit %t %f"
227 228 229 230 231
driver = "drivers/metis.drv"

[ATP metitarski]
name = "MetiTarski"
exec = "metit"
MARCHE Claude's avatar
MARCHE Claude committed
232 233
exec = "metit-2.4"
exec = "metit-2.2"
234 235
version_switch = "-v"
version_regexp = "MetiTarski \\([^ \n,]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
236 237
version_ok = "2.4"
version_old = "2.2"
238
command = "%l/why3-cpulimit %T %m -s %e --time %t %f"
239 240
driver = "drivers/metitarski.drv"

241 242 243
[ATP spass]
name = "Spass"
exec = "SPASS"
244
exec = "SPASS-3.7"
245
version_switch = " | grep 'SPASS V'"
246
version_regexp = "SPASS V \\([^ \n\t]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
247
version_ok = "3.7"
248
command = "%l/why3-cpulimit %T %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
MARCHE Claude's avatar
MARCHE Claude committed
249
driver = "drivers/spass.drv"
MARCHE Claude's avatar
MARCHE Claude committed
250

251 252 253 254 255 256 257
[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"
258
command = "%l/why3-cpulimit %T %m -s %e -Isabelle=1 -PGiven=0 -TimeLimit=%t %f"
259 260
driver = "drivers/spass_types.drv"

MARCHE Claude's avatar
MARCHE Claude committed
261 262 263
[ATP vampire]
name = "Vampire"
exec = "vampire"
264
exec = "vampire-0.6"
MARCHE Claude's avatar
MARCHE Claude committed
265 266
version_switch = "--version"
version_regexp = "Vampire \\([0-9.]+\\)"
267
# we pass time 0 to why3-cpulimit to avoid race
268
command = "%l/why3-cpulimit %T %m -s %e -t %t"
MARCHE Claude's avatar
MARCHE Claude committed
269
driver = "drivers/vampire.drv"
270
version_ok = "0.6"
MARCHE Claude's avatar
MARCHE Claude committed
271

272 273 274 275
[ATP princess]
name = "Princess"
exec = "princess"
# version_switch = "-h"
276
version_regexp = "(CASC version \\([0-9-]+\\))"
277
command = "%l/why3-cpulimit %T 0 -s %e -timeout=%t %f"
278
driver = "drivers/princess.drv"
279 280 281 282 283 284 285 286
version_ok = "2013-05-13"

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

291 292
[ATP verit]
name = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
293
exec = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
294 295
exec = "veriT-201310"
version_switch = "--version"
MARCHE Claude's avatar
MARCHE Claude committed
296
version_regexp = "version \\([^ \n\r]+\\)"
297 298
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"
299
driver = "drivers/verit.drv"
MARCHE Claude's avatar
MARCHE Claude committed
300
version_ok = "201310"
301

MARCHE Claude's avatar
MARCHE Claude committed
302 303 304 305 306
# Z3 4.3.2 does not support option global option -rs anymore.
# use settings given by "z3 -p" instead
[ATP z3]
name = "Z3"
exec = "z3"
Andrei Paskevich's avatar
Andrei Paskevich committed
307
exec = "z3-4.3.3"
MARCHE Claude's avatar
MARCHE Claude committed
308 309 310
exec = "z3-4.3.2"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
Andrei Paskevich's avatar
Andrei Paskevich committed
311 312
version_ok  = "4.3.3"
version_old = "4.3.2"
313
driver = "drivers/z3_bare.drv"  # Do not set any logic, let z3 choose by itself
MARCHE Claude's avatar
MARCHE Claude committed
314 315
command = "%l/why3-cpulimit %t %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"

316
[ATP z3]
317 318
name = "Z3"
exec = "z3"
319 320
exec = "z3-4.3.1"
exec = "z3-4.3.0"
MARCHE Claude's avatar
MARCHE Claude committed
321
exec = "z3-4.2"
322 323
exec = "z3-4.1.2"
exec = "z3-4.1.1"
324 325 326
exec = "z3-4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
Andrei Paskevich's avatar
Andrei Paskevich committed
327
version_old = "4.3.1"
328 329 330 331 332
version_old = "4.3.0"
version_old = "4.2"
version_old = "4.1.2"
version_old = "4.1.1"
version_old = "4.0"
333
driver = "drivers/z3.drv"
334
command = "%l/why3-cpulimit %t %m -s %e -smt2 -rs:42 %f"
335

336
[ATP z3]
337
name = "Z3"
338
exec = "z3"
339
exec = "z3-3.2"
340 341
exec = "z3-3.1"
exec = "z3-3.0"
342 343
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
344
version_old = "3.2"
345 346 347
version_old = "3.1"
version_old = "3.0"
driver = "drivers/z3.drv"
Andrei Paskevich's avatar
Andrei Paskevich committed
348
# the -T is unreliable in Z3 3.2
349
command = "%l/why3-cpulimit %t %m -s %e -smt2 -rs:42 %f"
350

351
[ATP z3]
François Bobot's avatar
François Bobot committed
352 353
name = "Z3"
exec = "z3"
354 355 356 357
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
358 359
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
360 361
version_old = "^2\.2.+$"
version_old = "^2\.1[6-9]$"
Andrei Paskevich's avatar
Andrei Paskevich committed
362
driver = "drivers/z3.drv"
363
command = "%l/why3-cpulimit %t %m -s %e -smt2 -rs:42 \
364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382
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

383
[ATP z3]
384
name = "Z3"
385 386
exec = "z3"
exec = "z3-2.2"
387 388
exec = "z3-2.1"
exec = "z3-1.3"
389 390
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
391 392
version_old = "^2\.1[0-5]$"
version_old = "^2\.[0-9]$"
393
version_old = "1.3"
394
command = "%l/why3-cpulimit %t %m -s %e -smt %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
395
driver = "drivers/z3_smtv1.drv"
396

397 398 399 400 401 402 403
[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"
404
command = "%l/why3-cpulimit %T 0 -s %e -p0 -itptp -max-size %mM -max-time %ts %f"
405 406 407 408 409
driver = "drivers/zenon.drv"

[ATP iprover]
name = "iProver"
exec = "iprover"
410
exec = "iprover-0.8.1"
411 412 413
version_switch = " | grep iProver"
version_regexp = "iProver v\\([^ \n\t]+\\)"
version_ok = "0.8.1"
414
command = "%l/why3-cpulimit %T %m -s %e --fof true --out_options none \
415 416
--time_out_virtual %t --clausifier /usr/bin/env --clausifier_options \
\"eprover --cnf --tstp-format \" %f"
417 418
driver = "drivers/iprover.drv"

Daisuke Ishii's avatar
Daisuke Ishii committed
419 420 421 422 423
[ATP mathematica]
name = "Mathematica"
exec = "math"
version_switch = "-run \"Exit[]\""
version_regexp = "Mathematica \\([0-9.]+\\)"
424
version_ok = "9.0"
Daisuke Ishii's avatar
Daisuke Ishii committed
425 426
version_ok = "8.0"
version_ok = "7.0"
427
command = "%l/why3-cpulimit %t %m -s %e -noprompt"
Daisuke Ishii's avatar
Daisuke Ishii committed
428 429
driver = "drivers/mathematica.drv"

MARCHE Claude's avatar
MARCHE Claude committed
430 431
[ITP coq]
name = "Coq"
432
compile_time_support = true
433
exec = "coqtop -batch"
MARCHE Claude's avatar
MARCHE Claude committed
434
version_switch = "-v"
435
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
436
version_ok = "8.4pl5"
437
version_ok = "8.4pl4"
Andrei Paskevich's avatar
Andrei Paskevich committed
438
version_ok = "8.4pl3"
439
version_ok = "8.4pl2"
MARCHE Claude's avatar
MARCHE Claude committed
440
version_ok = "8.4pl1"
441
version_ok = "8.4"
442
command = "%l/why3-cpulimit 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
443 444 445
driver = "drivers/coq.drv"
editor = "coqide"

446 447
[ITP pvs]
name = "PVS"
448
compile_time_support = true
449 450 451
exec = "pvs"
version_switch = "-version"
version_regexp = "PVS Version \\([^ \n]+\\)"
452
version_ok = "6.0"
453
version_bad = "^[0-5]\..+$"
454 455
# 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"
456
driver = "drivers/pvs.drv"
457
in_place = true
458
editor = "pvs"
459

460 461 462 463 464
[ITP isabelle]
name = "Isabelle"
exec = "isabelle"
version_switch = "version"
version_regexp = "Isabelle\\([^:]+\\)"
465
version_ok = "2014"
466
version_bad = "2013-2"
467 468
# not why3-cpulimit 0 %m because isabelle needs more memory at start-up
command = "%l/why3-cpulimit 0 0 -s %e why3 -b %f"
469
driver = "drivers/isabelle.drv"
470
in_place = true
471
editor = "isabelle-jedit"
472

473 474
[editor pvs]
name = "PVS"
475
command = "%l/why3-call-pvs %l pvs %f"
476 477

[editor coqide]
MARCHE Claude's avatar
MARCHE Claude committed
478
name = "CoqIDE"
479 480 481
command = "coqide -I %l/coq-tactic -R %l/coq Why3 %f"

[editor proofgeneral-coq]
MARCHE Claude's avatar
MARCHE Claude committed
482
name = "Emacs/ProofGeneral/Coq"
483
command = "emacs --eval \"(setq coq-load-path '(\\\"%l/coq-tactic\\\" \
484
(\\\"%l/coq\\\" \\\"Why3\\\")))\" %f"
485

486
[editor isabelle-jedit]
MARCHE Claude's avatar
MARCHE Claude committed
487
name = "Isabelle/jEdit"
488 489 490 491 492 493
command = "isabelle why3 -i jedit %f"

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

494
[editor altgr-ergo]
MARCHE Claude's avatar
MARCHE Claude committed
495
name = "AltGr-Ergo"
496
command = "altgr-ergo %f"
497 498 499 500

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