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

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

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

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

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

[ATP gappa]
name = "Gappa"
70
exec = "gappa"
71
version_switch = "--version"
72
version_regexp = "Gappa \\([^ \n]*\\)"
MARCHE Claude's avatar
MARCHE Claude committed
73
version_ok = "0.15.1"
74 75
version_ok = "0.15.0"
version_ok = "0.14.1"
76
version_ok = "0.14.0"
77 78
version_ok = "0.13.0"
version_old = "0.12.3"
79 80 81 82
version_old = "0.12.2"
version_old = "0.12.1"
version_old = "0.12.0"
version_old = "0.11.2"
83
command = "@LOCALBIN@why3-cpulimit %t %m -s %e"
84
driver = "drivers/gappa.drv"
85 86 87

[ATP simplify]
name = "Simplify"
88 89 90 91
exec = "Simplify"
exec = "simplify"
exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
92
version_switch = "-version"
93
version_regexp = "Simplify version \\([^ \n,]+\\)"
94
version_ok = "1.5.5"
95
version_ok = "1.5.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
96
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
97 98 99 100 101
driver = "drivers/simplify.drv"

[ATP spass]
name = "Spass"
exec = "SPASS"
102
version_switch = "-TPTP || true"
103
version_regexp = "SPASS V \\([^ \n\t]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
104
version_ok = "3.7"
Andrei Paskevich's avatar
Andrei Paskevich committed
105
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
106
driver = "drivers/tptp.drv"
107

MARCHE Claude's avatar
MARCHE Claude committed
108 109 110 111 112
[ATP vampire]
name = "Vampire"
exec = "vampire"
version_switch = "--version"
version_regexp = "Vampire \\([0-9.]+\\)"
113
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -t %t"
MARCHE Claude's avatar
MARCHE Claude committed
114
driver = "drivers/vampire.drv"
115
version_ok = "0.6"
MARCHE Claude's avatar
MARCHE Claude committed
116

117 118
[ATP verit]
name = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
119
exec = "veriT"
120
exec = "verit"
MARCHE Claude's avatar
MARCHE Claude committed
121 122
version_switch = "--help"
version_regexp = "Version: \\([^ \n\r]+\\)"
Andrei Paskevich's avatar
Andrei Paskevich committed
123
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
124 125
driver = "drivers/verit.drv"

126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154

[ATP z3]
name = "Z3"
exec = "z3"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "3.2"
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"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smtc \
-rs:42 \
PHASE_SELECTION=0 \
RESTART_STRATEGY=0 \
RESTART_FACTOR=1.5 \
QI_EAGER_THRESHOLD=100 \
ARITH_RANDOM_INITIAL_VALUE=true \
CASE_SPLIT=3 \
DELAY_UNITS=true \
DELAY_UNITS_THRESHOLD=16 \
%f"

François Bobot's avatar
François Bobot committed
155 156 157 158 159
[ATP z3]
name = "Z3"
exec = "z3"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
160
version_old = "2.19"
François Bobot's avatar
François Bobot committed
161 162 163
version_old = "2.18"
version_old = "2.17"
version_old = "2.16"
164 165 166
version_bad = "2.2"
version_bad = "2.1"
version_bad = "1.3"
Andrei Paskevich's avatar
Andrei Paskevich committed
167
driver = "drivers/z3.drv"
168
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt2 \
169
-rs:42 \
170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188
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

189
[ATP z3]
Andrei Paskevich's avatar
Andrei Paskevich committed
190
name = "Z3 smtv1"
191 192 193 194 195 196 197 198
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
199
driver = "drivers/z3_smtv1.drv"
200

201 202
[ITP coq]
name = "Coq"
203
exec = "coqc"
MARCHE Claude's avatar
MARCHE Claude committed
204
version_switch = "-v"
205
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
206 207
version_ok = "8.3pl2"
version_ok = "8.3pl1"
208
version_ok = "8.3"
209
version_ok = "8.2pl2"
210
version_ok = "8.2pl1"
211 212 213
version_ok = "8.2"
version_old = "8.1"
version_old = "8.0"
214
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e %f"
215
driver = "drivers/coq.drv"
MARCHE Claude's avatar
MARCHE Claude committed
216
editor = "coqide"
217