provers-detection-data.conf 16.3 KB
Newer Older
1 2 3
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
4
exec = "alt-ergo-2.3.0"
5
exec = "alt-ergo-2.2.0"
6
exec = "alt-ergo-2.1.0"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
7
exec = "alt-ergo-2.0.0"
8 9
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\)$"
10
version_ok  = "2.3.0"
11
version_ok  = "2.2.0"
12
version_ok  = "2.1.0"
13
version_ok  = "2.0.0"
14 15 16 17
version_bad = "1.30"
version_bad = "1.01"
version_bad = "0.99.1"
version_bad = "0.95.2"
18 19
command = "%e -timelimit %t %f"
command_steps = "%e -steps-bound %S %f"
20
driver = "alt_ergo"
21
editor = "altgr-ergo"
22
use_at_auto_level = 1
23

24
# CVC4 version >= 1.6, with counterexamples
25 26 27 28
[ATP cvc4-ce]
name = "CVC4"
alternative = "counterexamples"
exec = "cvc4"
29
exec = "cvc4-1.6"
MARCHE Claude's avatar
MARCHE Claude committed
30
exec = "cvc4-1.7"
31 32
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
33
version_ok  = "1.6"
MARCHE Claude's avatar
MARCHE Claude committed
34
version_ok  = "1.7"
35 36 37 38 39 40 41 42 43 44 45
driver = "cvc4_16_counterexample"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
command = "%e --tlimit-per=%t000 --lang=smt2 %f"
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"

# CVC4 version >= 1.6
[ATP cvc4]
name = "CVC4"
exec = "cvc4"
exec = "cvc4-1.6"
MARCHE Claude's avatar
MARCHE Claude committed
46
exec = "cvc4-1.7"
47 48 49
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok  = "1.6"
MARCHE Claude's avatar
MARCHE Claude committed
50
version_ok  = "1.7"
51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
driver = "cvc4_16"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
command = "%e --tlimit=%t000 --lang=smt2 %f"
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
use_at_auto_level = 1

# CVC4 version = 1.5, with counterexamples
[ATP cvc4-ce]
name = "CVC4"
alternative = "counterexamples"
exec = "cvc4"
exec = "cvc4-1.5"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
66
version_ok  = "1.5"
67
driver = "cvc4_15_counterexample"
68 69 70 71 72
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
command = "%e --tlimit-per=%t000 --lang=smt2 %f"
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"

73
# CVC4 version 1.5
74
[ATP cvc4]
75
name = "CVC4"
76
exec = "cvc4"
77
exec = "cvc4-1.5"
78 79
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
80
version_ok  = "1.5"
81
driver = "cvc4_15"
82 83
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
84
command = "%e --tlimit=%t000 --lang=smt2 %f"
85
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
MARCHE Claude's avatar
MARCHE Claude committed
86
use_at_auto_level = 1
87

88 89
# CVC4 version 1.4, using SMTLIB fixed-size bitvectors
[ATP cvc4]
90
name = "CVC4"
91 92 93 94
exec = "cvc4"
exec = "cvc4-1.4"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
95
version_old  = "1.4"
96
driver = "cvc4_14"
97 98 99 100
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
# --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument
# cvc4 1.4 does not print steps used in --stats anyway
101
command = "%e --tlimit=%t000 --lang=smt2 %f"
102
use_at_auto_level = 1
103

104
# CVC4 version 1.4, not using SMTLIB bitvectors
105 106
[ATP cvc4]
name = "CVC4"
107
alternative = "noBV"
108 109 110 111
exec = "cvc4"
exec = "cvc4-1.4"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
112
version_old  = "1.4"
113
driver = "cvc4"
114
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
115 116
# to try: --inst-when=full-last-call
# --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument
117
# cvc4 1.4 does not print steps used in --stats anyway
118
command = "%e --tlimit=%t000 --lang=smt2 %f"
119

120

121 122 123 124
# CVC4 version 1.0 to 1.3
[ATP cvc4]
name = "CVC4"
exec = "cvc4"
125 126 127 128
exec = "cvc4-1.3"
exec = "cvc4-1.2"
exec = "cvc4-1.1"
exec = "cvc4-1.0"
129 130
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
131 132 133 134
version_old = "1.3"
version_old = "1.2"
version_old = "1.1"
version_old = "1.0"
135
driver = "cvc4"
136
command = "%e --lang=smt2 %f"
137

138 139 140 141 142 143 144 145
# Psyche version 2.x
[ATP psyche]
name = "Psyche"
exec = "psyche"
exec = "psyche-2.02"
version_switch = "-version"
version_regexp = "\\([^ \n\r]+\\)"
version_ok  = "2.0"
146
driver = "psyche"
147
command = "%e -gplugin dpll_wl %f"
148

149
# CVC3 versions 2.4.x
150
[ATP cvc3]
Andrei Paskevich's avatar
Andrei Paskevich committed
151
name = "CVC3"
152
exec = "cvc3"
153
exec = "cvc3-2.4.1"
154
exec = "cvc3-2.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
155 156
version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
157 158
version_ok  = "2.4.1"
version_old = "2.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
159
# the -timeout option is unreliable in CVC3 2.4.1
160
command = "%e -seed 42 %f"
161
driver = "cvc3"
Andrei Paskevich's avatar
Andrei Paskevich committed
162

163
# CVC3 versions 2.x
164
[ATP cvc3]
165
name = "CVC3"
166
exec = "cvc3"
167 168
exec = "cvc3-2.2"
exec = "cvc3-2.1"
169
version_switch = "-version"
170
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
171
version_old = "2.2"
172
version_old = "2.1"
173
command = "%e  -seed 42 -timeout %t %f"
174
driver = "cvc3"
175

176 177 178
[ATP yices]
name = "Yices"
exec = "yices"
179
exec = "yices-1.0.38"
180
version_switch = "--version"
181
version_regexp = "\\([^ \n]+\\)"
182 183 184
version_ok = "1.0.38"
version_old = "^1\.0\.3[0-7]$"
version_old = "^1\.0\.2[5-9]$"
185 186
version_old = "^1\.0\.2[0-4]$"
version_old = "^1\.0\.1\.*$"
187
command = "%e"
188
driver = "yices"
189

190 191 192 193
[ATP yices-smt2]
name = "Yices"
exec = "yices-smt2"
exec = "yices-smt2-2.3.0"
Jean-Christophe's avatar
Jean-Christophe committed
194
version_switch = "--version"
195 196
version_regexp = "^Yices \\([^ \n]+\\)$"
version_ok = "2.3.0"
197
command = "%e"
198
driver = "yices-smt2"
Jean-Christophe's avatar
Jean-Christophe committed
199

200 201 202
[ATP eprover]
name = "Eprover"
exec = "eprover"
203 204 205
exec = "eprover-2.0"
exec = "eprover-1.9.1"
exec = "eprover-1.9"
MARCHE Claude's avatar
MARCHE Claude committed
206 207
exec = "eprover-1.8"
exec = "eprover-1.7"
208 209 210
exec = "eprover-1.6"
exec = "eprover-1.5"
exec = "eprover-1.4"
211
version_switch = "--version"
Andrei Paskevich's avatar
Andrei Paskevich committed
212
version_regexp = "E \\([-0-9.]+\\) [^\n]+"
213 214 215 216
version_ok  = "2.0"
version_old = "1.9.1-001"
version_old = "1.9"
version_old = "1.8-001"
217 218
version_old = "1.7"
version_old = "1.6"
219 220
version_old = "1.5"
version_old = "1.4"
221
command = "%e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
222
driver = "eprover"
223
use_at_auto_level = 2
224 225 226

[ATP gappa]
name = "Gappa"
227
exec = "gappa"
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
228
exec = "gappa-1.3.3"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
229
exec = "gappa-1.3.2"
230 231
exec = "gappa-1.3.0"
exec = "gappa-1.2.2"
MARCHE Claude's avatar
MARCHE Claude committed
232
exec = "gappa-1.2.0"
233
exec = "gappa-1.1.1"
234
exec = "gappa-1.1.0"
235
exec = "gappa-1.0.0"
MARCHE Claude's avatar
MARCHE Claude committed
236
exec = "gappa-0.16.1"
237
exec = "gappa-0.14.1"
238
version_switch = "--version"
239
version_regexp = "Gappa \\([^ \n]*\\)"
240
version_ok = "^1\.[0-3]\..+$"
241
version_old = "^0\.1[1-8]\..+$"
242
command = "%e -Eprecision=70"
243
driver = "gappa"
244

245 246 247
[ATP mathsat]
name = "MathSAT5"
exec = "mathsat"
248
exec = "mathsat-5.2.2"
249 250 251
version_switch = "-version"
version_regexp = "MathSAT5 version \\([^ \n]+\\)"
version_ok  = "5.2.2"
252
command = "%e -input=smt2 -model -random_seed=80"
253
driver = "mathsat"
254

255 256
[ATP simplify]
name = "Simplify"
257 258 259 260
exec = "Simplify"
exec = "simplify"
exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
261
version_switch = "-version"
262
version_regexp = "Simplify version \\([^ \n,]+\\)"
263 264
version_old = "1.5.5"
version_old = "1.5.4"
265
command = "%e %f"
266
driver = "simplify"
267

268 269 270 271 272 273
[ATP metis]
name = "Metis"
exec = "metis"
version_switch = "-v"
version_regexp = "metis \\([^ \n,]+\\)"
version_ok = "2.3"
274
command = "%e --time-limit %t %f"
275
driver = "metis"
276 277 278 279

[ATP metitarski]
name = "MetiTarski"
exec = "metit"
280 281
exec = "metit-2.4"
exec = "metit-2.2"
282 283
version_switch = "-v"
version_regexp = "MetiTarski \\([^ \n,]+\\)"
284 285
version_ok = "2.4"
version_old = "2.2"
286
command = "%e --time %t %f"
287
driver = "metitarski"
288

289 290 291 292 293 294 295
[ATP polypaver]
name = "PolyPaver"
exec = "polypaver"
exec = "polypaver-0.3"
version_switch = "--version"
version_regexp = "PolyPaver \\([0-9.]+\\) (c)"
version_ok = "0.3"
296
command = "%e -d 2 -m 10 --time=%t %f"
297
driver = "polypaver"
298

299 300 301
[ATP spass]
name = "Spass"
exec = "SPASS"
302
exec = "SPASS-3.7"
303
version_switch = " | grep 'SPASS V'"
304
version_regexp = "SPASS V \\([^ \n\t]+\\)"
305
version_ok = "3.7"
306
command = "%e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
307
driver = "spass"
308
use_at_auto_level = 2
309

310 311 312 313 314 315 316
[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"
317
command = "%e -Isabelle=1 -PGiven=0 -TimeLimit=%t %f"
318
driver = "spass_types"
319
use_at_auto_level = 2
320

MARCHE Claude's avatar
MARCHE Claude committed
321 322 323
[ATP vampire]
name = "Vampire"
exec = "vampire"
324
exec = "vampire-0.6"
MARCHE Claude's avatar
MARCHE Claude committed
325 326
version_switch = "--version"
version_regexp = "Vampire \\([0-9.]+\\)"
327
command = "%e -t %t"
328
driver = "vampire"
329
version_ok = "0.6"
MARCHE Claude's avatar
MARCHE Claude committed
330

331 332 333
[ATP princess]
name = "Princess"
exec = "princess"
334
exec = "princess-2015-12-07"
335
# version_switch = "-h"
336 337
# version_regexp = "(CASC version \\([0-9-]+\\))"
version_regexp = "(release \\([0-9-]+\\))"
338
command = "%e -timeout=%t %f"
339
driver = "princess"
340 341
# version_ok = "2013-05-13"
version_ok = "2015-12-07"
342 343 344 345 346 347 348

[ATP beagle]
name = "Beagle"
exec = "beagle"
exec = "beagle-0.4.1"
# version_switch = "-h"
version_regexp = "version \\([0-9.]+\\)"
349
command = "%e %f"
350
driver = "beagle"
351
version_ok = "0.4.1"
352

MARCHE Claude's avatar
MARCHE Claude committed
353 354 355 356 357 358
[ATP verit]
name = "veriT"
exec = "veriT"
exec = "veriT-201410"
version_switch = "--version"
version_regexp = "version \\([^ \n\r]+\\)"
359
command = "%e --disable-print-success %f"
360
driver = "verit"
MARCHE Claude's avatar
MARCHE Claude committed
361 362
version_ok = "201410"

363 364
[ATP verit]
name = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
365
exec = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
366 367
exec = "veriT-201310"
version_switch = "--version"
MARCHE Claude's avatar
MARCHE Claude committed
368
version_regexp = "version \\([^ \n\r]+\\)"
369
command = "%e --disable-print-success --enable-simp \
370
--enable-unit-simp --enable-simp-sym --enable-unit-subst-simp --enable-bclause %f"
371
driver = "verit"
MARCHE Claude's avatar
MARCHE Claude committed
372
version_old = "201310"
373

374
# Z3 >= 4.6.0, with counterexamples and incremental usage
375 376 377 378
[ATP z3-ce]
name = "Z3"
alternative = "counterexamples"
exec = "z3"
379 380 381
exec = "z3-4.8.4"
exec = "z3-4.8.3"
exec = "z3-4.8.1"
MARCHE Claude's avatar
MARCHE Claude committed
382
exec = "z3-4.7.1"
383 384 385 386 387 388
exec = "z3-4.6.0"
exec = "z3-4.5.0"
exec = "z3-4.4.1"
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
389 390 391
version_ok  = "4.8.4"
version_ok  = "4.8.3"
version_ok  = "4.8.1"
MARCHE Claude's avatar
MARCHE Claude committed
392
version_ok  = "4.7.1"
393 394 395 396
version_ok  = "4.6.0"
version_ok  = "4.5.0"
version_old  = "4.4.1"
version_old  = "4.4.0"
397
driver = "z3_440_counterexample"
398
# -t sets the time limit per query
399 400 401
command = "%e -smt2 -t:%t000 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"

Sylvain Dailler's avatar
Sylvain Dailler committed
402
# Z3 >= 4.5.0, with BV support
403
[ATP z3]
404
name = "Z3"
405
exec = "z3"
406 407 408
exec = "z3-4.8.4"
exec = "z3-4.8.3"
exec = "z3-4.8.1"
MARCHE Claude's avatar
MARCHE Claude committed
409
exec = "z3-4.7.1"
MARCHE Claude's avatar
MARCHE Claude committed
410
exec = "z3-4.6.0"
411
exec = "z3-4.5.0"
412 413
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
414 415 416
version_ok  = "4.8.4"
version_ok  = "4.8.3"
version_ok  = "4.8.1"
MARCHE Claude's avatar
MARCHE Claude committed
417
version_ok  = "4.7.1"
MARCHE Claude's avatar
MARCHE Claude committed
418
version_ok  = "4.6.0"
419
version_ok  = "4.5.0"
Sylvain Dailler's avatar
Sylvain Dailler committed
420 421 422 423 424 425 426 427 428 429 430 431 432
driver = "z3_440"
command = "%e -smt2 -T:%t sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 -st %f"
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 -st rlimit=%S %f"
use_at_auto_level = 1

# Z3 = 4.4.0, with BV support
[ATP z3]
name = "Z3"
exec = "z3"
exec = "z3-4.4.1"
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
433 434
version_old  = "4.4.1"
version_old  = "4.4.0"
435
driver = "z3_440"
436
command = "%e -smt2 -T:%t sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
437
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
438
use_at_auto_level = 1
439

440
# Z3 >= 4.4.0, without BV support
441
[ATP z3-nobv]
442 443 444
name = "Z3"
alternative = "noBV"
exec = "z3"
445 446 447
exec = "z3-4.8.4"
exec = "z3-4.8.3"
exec = "z3-4.8.1"
MARCHE Claude's avatar
MARCHE Claude committed
448
exec = "z3-4.7.1"
MARCHE Claude's avatar
MARCHE Claude committed
449
exec = "z3-4.6.0"
450
exec = "z3-4.5.0"
451
exec = "z3-4.4.1"
452 453 454
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
455 456 457
version_ok  = "4.8.4"
version_ok  = "4.8.3"
version_ok  = "4.8.1"
MARCHE Claude's avatar
MARCHE Claude committed
458
version_ok  = "4.7.1"
MARCHE Claude's avatar
MARCHE Claude committed
459
version_ok  = "4.6.0"
460
version_ok  = "4.5.0"
MARCHE Claude's avatar
MARCHE Claude committed
461 462
version_old  = "4.4.1"
version_old  = "4.4.0"
463
driver = "z3_432"
464
command = "%e -smt2 -T:%t sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
465
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
466

MARCHE Claude's avatar
MARCHE Claude committed
467 468
# Z3 4.3.2 does not support option global option -rs anymore.
# use settings given by "z3 -p" instead
469
# Z3 4.3.2 supports Datatypes
MARCHE Claude's avatar
MARCHE Claude committed
470 471 472 473 474
[ATP z3]
name = "Z3"
exec = "z3-4.3.2"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
475
version_old  = "4.3.2"
476
driver = "z3_432"
477 478
command = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
MARCHE Claude's avatar
MARCHE Claude committed
479

480
[ATP z3]
Jean-Christophe's avatar
Jean-Christophe committed
481 482
name = "Z3"
exec = "z3"
483 484
exec = "z3-4.3.1"
exec = "z3-4.3.0"
MARCHE Claude's avatar
MARCHE Claude committed
485
exec = "z3-4.2"
486 487
exec = "z3-4.1.2"
exec = "z3-4.1.1"
Jean-Christophe's avatar
Jean-Christophe committed
488 489 490
exec = "z3-4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
491
version_old = "4.3.1"
492 493 494 495 496
version_old = "4.3.0"
version_old = "4.2"
version_old = "4.1.2"
version_old = "4.1.1"
version_old = "4.0"
497
driver = "z3"
498
command = "%e -smt2 -rs:42 %f"
Jean-Christophe's avatar
Jean-Christophe committed
499

500
[ATP z3]
501
name = "Z3"
502
exec = "z3"
503
exec = "z3-3.2"
504 505
exec = "z3-3.1"
exec = "z3-3.0"
506 507
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
508
version_old = "3.2"
509 510
version_old = "3.1"
version_old = "3.0"
511
driver = "z3"
Andrei Paskevich's avatar
Andrei Paskevich committed
512
# the -T is unreliable in Z3 3.2
513
command = "%e -smt2 -rs:42 %f"
514

515
[ATP z3]
François Bobot's avatar
François Bobot committed
516 517
name = "Z3"
exec = "z3"
518 519 520 521
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
522 523
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
524 525
version_old = "^2\.2.+$"
version_old = "^2\.1[6-9]$"
526
driver = "z3"
527
command = "%e -smt2 -rs:42 \
528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546
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

547
[ATP z3]
548
name = "Z3"
549 550
exec = "z3"
exec = "z3-2.2"
551 552
exec = "z3-2.1"
exec = "z3-1.3"
553 554
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
555 556
version_old = "^2\.1[0-5]$"
version_old = "^2\.[0-9]$"
557
version_old = "1.3"
558
command = "%e -smt %f"
559
driver = "z3_smtv1"
560

561 562 563
[ATP zenon]
name = "Zenon"
exec = "zenon"
564
exec = "zenon-0.8.0"
565 566 567
exec = "zenon-0.7.1"
version_switch = "-v"
version_regexp = "zenon version \\([^ \n\t]+\\)"
568
version_ok = "0.8.0"
569
version_ok = "0.7.1"
570
command = "%e -p0 -itptp -max-size %mM -max-time %ts %f"
571
driver = "zenon"
572

573 574 575 576 577
[ATP zenon_modulo]
name = "Zenon Modulo"
exec = "zenon_modulo"
version_switch = "-v"
version_regexp = "zenon_modulo version \\([0-9.]+\\)"
578
version_ok = "0.4.1"
579
command = "%e -p0 -itptp -max-size %mM -max-time %ts %f"
580
driver = "zenon_modulo"
581

582 583 584
[ATP iprover]
name = "iProver"
exec = "iprover"
585
exec = "iprover-0.8.1"
586 587 588
version_switch = " | grep iProver"
version_regexp = "iProver v\\([^ \n\t]+\\)"
version_ok = "0.8.1"
589
command = "%e --fof true --out_options none \
590 591
--time_out_virtual %t --clausifier /usr/bin/env --clausifier_options \
\"eprover --cnf --tstp-format \" %f"
592
driver = "iprover"
593

594 595 596 597 598
[ATP mathematica]
name = "Mathematica"
exec = "math"
version_switch = "-run \"Exit[]\""
version_regexp = "Mathematica \\([0-9.]+\\)"
599
version_ok = "9.0"
600 601
version_ok = "8.0"
version_ok = "7.0"
602
command = "%e -noprompt"
603
driver = "mathematica"
604

605 606
[ITP coq]
name = "Coq"
607
support_library = "%l/coq/version"
608
exec = "coqtop"
609 610
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
611
version_ok = "^8\.9\.[0]$"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
612
version_ok = "^8\.8\.[0-2]$"
613
version_ok = "^8\.7\.[0-2]$"
MARCHE Claude's avatar
MARCHE Claude committed
614
version_ok = "8.6.1"
615
version_ok = "8.6"
MARCHE Claude's avatar
MARCHE Claude committed
616 617
version_old = "^8\.5pl[1-3]$"
version_old = "8.5"
618
command = "%e -batch -R %l/coq Why3 -l %f"
619
driver = "coq"
620 621
editor = "coqide"

622 623
[ITP pvs]
name = "PVS"
624
support_library = "%l/pvs/version"
625 626 627
exec = "pvs"
version_switch = "-version"
version_regexp = "PVS Version \\([^ \n]+\\)"
628
version_ok = "6.0"
629
version_bad = "^[0-5]\..+$"
630
command = "%l/why3-call-pvs %l/pvs proveit -f %f"
631
driver = "pvs"
632
in_place = true
633
editor = "pvs"
634

635 636 637 638
[ITP isabelle]
name = "Isabelle"
exec = "isabelle"
version_switch = "version"
639
version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)"
640
version_ok = "2018"
641
version_bad = "2017"
642
version_bad = "2016-1"
643
command = "%e why3 -b %f"
644
driver = "isabelle2018"
645
in_place = true
646
editor = "isabelle-jedit"
647 648 649 650 651 652

[ITP isabelle]
name = "Isabelle"
exec = "isabelle"
version_switch = "version"
version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)"
653
version_ok = "2017"
654
version_bad = "2018"
655
version_bad = "2016-1"
656
command = "%e why3 -b %f"
657
driver = "isabelle2017"
658
in_place = true
659
editor = "isabelle-jedit"
660

661 662
[editor pvs]
name = "PVS"
663
command = "%l/why3-call-pvs %l pvs %f"
664 665

[editor coqide]
MARCHE Claude's avatar
MARCHE Claude committed
666
name = "CoqIDE"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
667
command = "coqide -R %l/coq Why3 %f"
668 669

[editor proofgeneral-coq]
MARCHE Claude's avatar
MARCHE Claude committed
670
name = "Emacs/ProofGeneral/Coq"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
671
command = "emacs --eval \"(setq coq-load-path '((\\\"%l/coq\\\" \\\"Why3\\\")))\" %f"
672

673 674
[editor isabelle-jedit]
name = "Isabelle/jEdit"
675
command = "isabelle why3 -i %f"
676

677
[editor altgr-ergo]
MARCHE Claude's avatar
MARCHE Claude committed
678
name = "AltGr-Ergo"
679
command = "altgr-ergo %f"
680 681 682 683

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