provers-detection-data.conf.in 4.11 KB
Newer Older
1
2
[ATP alt-ergo]
name = "Alt-Ergo"
3
exec = "alt-ergo"
MARCHE Claude's avatar
MARCHE Claude committed
4
version_switch = "-version"
5
version_regexp = ".*Ergo \\([^ \n]*\\)"
6
7
8
9
10
11
12
13
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"
MARCHE Claude's avatar
MARCHE Claude committed
14
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -proof %f"
15
driver = "drivers/alt_ergo_trunk.drv"
MARCHE Claude's avatar
MARCHE Claude committed
16

17
[ATP alt-ergo]
Andrei Paskevich's avatar
Andrei Paskevich committed
18
name = "Alt-Ergo (w/o arrays)"
19
exec = "ergo"
20
exec = "alt-ergo"
21
exec = "alt-ergo-0.91"
22
23
version_switch = "-version"
version_regexp = ".*Ergo \\([^ \n]*\\)"
24
25
26
27
version_old = "0.92.2"
version_old = "0.92.1"
version_old = "0.92"
version_old = "0.91"
28
29
version_old = "0.9"
version_old = "0.8"
30
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
31
driver = "drivers/alt_ergo.drv"
32

33
[ATP cvc3]
MARCHE Claude's avatar
MARCHE Claude committed
34
name = "CVC3"
35
exec = "cvc3"
MARCHE Claude's avatar
MARCHE Claude committed
36
version_switch = "-version"
37
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
38
39
version_ok = "2.2"
version_old = "2.1"
40
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -timeout %t %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
41
driver = "drivers/cvc3.drv"
42

43
44
45
46
47
48
49
50
[ATP yices]
name = "Yices"
exec = "yices"
version_switch = "--version"
version_regexp = "[Yices ]*\\([^ \n]+\\)"
version_ok = "1.0.27"
version_old = "1.0.17"
version_old = "1.0.24"
François Bobot's avatar
François Bobot committed
51
command = "@LOCALBIN@why3-cpulimit %t %m -s %e"
52
53
driver = "drivers/yices.drv"

54
55
56
[ATP eprover]
name = "Eprover"
exec = "eprover"
57
58
version_switch = "--version"
version_regexp = "E \\([^\n]+\\)"
Andrei Paskevich's avatar
Andrei Paskevich committed
59
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
60
driver = "drivers/tptp.drv"
MARCHE Claude's avatar
MARCHE Claude committed
61
62
63

[ATP gappa]
name = "Gappa"
64
exec = "gappa"
MARCHE Claude's avatar
MARCHE Claude committed
65
version_switch = "--version"
66
version_regexp = "Gappa \\([^ \n]*\\)"
67
version_ok = "0.14.0"
MARCHE Claude's avatar
MARCHE Claude committed
68
69
version_ok = "0.13.0"
version_old = "0.12.3"
70
71
72
73
version_old = "0.12.2"
version_old = "0.12.1"
version_old = "0.12.0"
version_old = "0.11.2"
74
command = "@LOCALBIN@why3-cpulimit %t %m -s %e"
75
driver = "drivers/gappa.drv"
MARCHE Claude's avatar
MARCHE Claude committed
76
77
78

[ATP simplify]
name = "Simplify"
79
80
81
82
exec = "Simplify"
exec = "simplify"
exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
MARCHE Claude's avatar
MARCHE Claude committed
83
version_switch = "-version"
84
version_regexp = "Simplify version \\([^ \n,]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
85
version_ok = "1.5.5"
86
version_ok = "1.5.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
87
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
88
89
90
91
92
driver = "drivers/simplify.drv"

[ATP spass]
name = "Spass"
exec = "SPASS"
93
version_switch = "-TPTP || true"
94
version_regexp = "SPASS V \\([^ \n\t]+\\)"
Andrei Paskevich's avatar
Andrei Paskevich committed
95
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
96
driver = "drivers/tptp.drv"
MARCHE Claude's avatar
MARCHE Claude committed
97

MARCHE Claude's avatar
MARCHE Claude committed
98
99
100
101
102
103
104
105
[ATP vampire]
name = "Vampire"
exec = "vampire"
version_switch = "--version"
version_regexp = "Vampire \\([0-9.]+\\)"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e"
driver = "drivers/vampire.drv"

106
107
[ATP verit]
name = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
108
exec = "veriT"
109
exec = "verit"
MARCHE Claude's avatar
MARCHE Claude committed
110
111
version_switch = "--help"
version_regexp = "Version: \\([^ \n\r]+\\)"
Andrei Paskevich's avatar
Andrei Paskevich committed
112
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
113
114
driver = "drivers/verit.drv"

François Bobot's avatar
François Bobot committed
115
116
117
118
119
120
121
122
123
[ATP z3]
name = "Z3"
exec = "z3"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "2.19"
version_old = "2.18"
version_old = "2.17"
version_old = "2.16"
124
125
126
version_bad = "2.2"
version_bad = "2.1"
version_bad = "1.3"
Andrei Paskevich's avatar
Andrei Paskevich committed
127
driver = "drivers/z3.drv"
128
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt2 \
129
-rs:42 \
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
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

149
[ATP z3]
Andrei Paskevich's avatar
Andrei Paskevich committed
150
name = "Z3 smtv1"
151
152
153
154
155
156
157
158
exec = "z3"
exec = "z3-2.2"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_old = "2.2"
version_old = "2.1"
version_old = "1.3"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
159
driver = "drivers/z3_smtv1.drv"
160

MARCHE Claude's avatar
MARCHE Claude committed
161
162
[ITP coq]
name = "Coq"
163
exec = "coqc"
MARCHE Claude's avatar
MARCHE Claude committed
164
version_switch = "-v"
165
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
166
version_ok = "8.3"
167
version_ok = "8.2pl2"
MARCHE Claude's avatar
MARCHE Claude committed
168
version_ok = "8.2pl1"
169
170
171
version_ok = "8.2"
version_old = "8.1"
version_old = "8.0"
172
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e %f"
173
driver = "drivers/coq.drv"
MARCHE Claude's avatar
MARCHE Claude committed
174
editor = "coqide"
MARCHE Claude's avatar
MARCHE Claude committed
175