author  boehmes 
Thu, 27 May 2010 14:55:53 +0200  
changeset 37151  3e9e8dfb3c98 
parent 37124  fe22fc54b876 
child 37153  8feed34275ce 
permissions  rwrr 
36898  1 
(* Title: HOL/SMT.thy 
2 
Author: Sascha Boehme, TU Muenchen 

3 
*) 

4 

5 
header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *} 

6 

7 
theory SMT 

8 
imports List 

9 
uses 

10 
"~~/src/Tools/cache_io.ML" 

11 
("Tools/SMT/smt_monomorph.ML") 

12 
("Tools/SMT/smt_normalize.ML") 

13 
("Tools/SMT/smt_translate.ML") 

14 
("Tools/SMT/smt_solver.ML") 

15 
("Tools/SMT/smtlib_interface.ML") 

16 
("Tools/SMT/z3_proof_parser.ML") 

17 
("Tools/SMT/z3_proof_tools.ML") 

18 
("Tools/SMT/z3_proof_literals.ML") 

19 
("Tools/SMT/z3_proof_reconstruction.ML") 

20 
("Tools/SMT/z3_model.ML") 

21 
("Tools/SMT/z3_interface.ML") 

22 
("Tools/SMT/z3_solver.ML") 

23 
("Tools/SMT/cvc3_solver.ML") 

24 
("Tools/SMT/yices_solver.ML") 

25 
begin 

26 

27 

28 

36902
c6bae4456741
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents:
36899
diff
changeset

29 
subsection {* Triggers for quantifier instantiation *} 
36898  30 

31 
text {* 

32 
Some SMT solvers support triggers for quantifier instantiation. 

33 
Each trigger consists of one ore more patterns. A pattern may either 

37124  34 
be a list of positive subterms (each being tagged by "pat"), or a 
35 
list of negative subterms (each being tagged by "nopat"). 

36 

37 
When an SMT solver finds a term matching a positive pattern (a 

38 
pattern with positive subterms only), it instantiates the 

39 
corresponding quantifier accordingly. Negative patterns inhibit 

40 
quantifier instantiations. Each pattern should mention all preceding 

41 
bound variables. 

36898  42 
*} 
43 

44 
datatype pattern = Pattern 

45 

37124  46 
definition pat :: "'a \<Rightarrow> pattern" where "pat _ = Pattern" 
47 
definition nopat :: "'a \<Rightarrow> pattern" where "nopat _ = Pattern" 

36898  48 

37124  49 
definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool" 
36898  50 
where "trigger _ P = P" 
51 

52 

53 

36902
c6bae4456741
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents:
36899
diff
changeset

54 
subsection {* Higherorder encoding *} 
36898  55 

56 
text {* 

57 
Application is made explicit for constants occurring with varying 

58 
numbers of arguments. This is achieved by the introduction of the 

59 
following constant. 

60 
*} 

61 

62 
definition "apply" where "apply f x = f x" 

63 

64 
text {* 

65 
Some solvers support a theory of arrays which can be used to encode 

66 
higherorder functions. The following set of lemmas specifies the 

67 
properties of such (extensional) arrays. 

68 
*} 

69 

70 
lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other 

71 
fun_upd_upd 

72 

73 

74 

36902
c6bae4456741
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents:
36899
diff
changeset

75 
subsection {* Firstorder logic *} 
36898  76 

77 
text {* 

78 
Some SMT solvers require a strict separation between formulas and 

79 
terms. When translating higherorder into firstorder problems, 

80 
all uninterpreted constants (those not builtin in the target solver) 

81 
are treated as function symbols in the firstorder sense. Their 

82 
occurrences as head symbols in atoms (i.e., as predicate symbols) is 

83 
turned into terms by equating such atoms with @{term True} using the 

84 
following termlevel equation symbol. 

85 
*} 

86 

37124  87 
definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "term_eq x y = (x = y)" 
36898  88 

89 

90 

37151  91 
subsection {* Integer division and modulo for Z3 *} 
92 

93 
definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where 

94 
"z3div k l = (if 0 \<le> l then k div l else (k div (l)))" 

95 

96 
definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where 

97 
"z3mod k l = (if 0 \<le> l then k mod l else k mod (l))" 

98 

99 
lemma div_by_z3div: "k div l = ( 

100 
if k = 0 \<or> l = 0 then 0 

101 
else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3div k l 

102 
else z3div (k) (l))" 

103 
by (auto simp add: z3div_def) 

104 

105 
lemma mod_by_z3mod: "k mod l = ( 

106 
if l = 0 then k 

107 
else if k = 0 then 0 

108 
else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3mod k l 

109 
else  z3mod (k) (l))" 

110 
by (auto simp add: z3mod_def) 

111 

112 

113 

36902
c6bae4456741
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents:
36899
diff
changeset

114 
subsection {* Setup *} 
36898  115 

116 
use "Tools/SMT/smt_monomorph.ML" 

117 
use "Tools/SMT/smt_normalize.ML" 

118 
use "Tools/SMT/smt_translate.ML" 

119 
use "Tools/SMT/smt_solver.ML" 

120 
use "Tools/SMT/smtlib_interface.ML" 

121 
use "Tools/SMT/z3_interface.ML" 

122 
use "Tools/SMT/z3_proof_parser.ML" 

123 
use "Tools/SMT/z3_proof_tools.ML" 

124 
use "Tools/SMT/z3_proof_literals.ML" 

125 
use "Tools/SMT/z3_proof_reconstruction.ML" 

126 
use "Tools/SMT/z3_model.ML" 

127 
use "Tools/SMT/z3_solver.ML" 

128 
use "Tools/SMT/cvc3_solver.ML" 

129 
use "Tools/SMT/yices_solver.ML" 

130 

131 
setup {* 

132 
SMT_Solver.setup #> 

133 
Z3_Proof_Reconstruction.setup #> 

134 
Z3_Solver.setup #> 

135 
CVC3_Solver.setup #> 

136 
Yices_Solver.setup 

137 
*} 

138 

139 

140 

36902
c6bae4456741
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents:
36899
diff
changeset

141 
subsection {* Configuration *} 
36898  142 

143 
text {* 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

144 
The current configuration can be printed by the command 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

145 
@{text smt_status}, which shows the values of most options. 
36898  146 
*} 
147 

148 

149 

150 
subsection {* General configuration options *} 

151 

152 
text {* 

153 
The option @{text smt_solver} can be used to change the target SMT 

154 
solver. The possible values are @{text cvc3}, @{text yices}, and 

155 
@{text z3}. It is advisable to locally install the selected solver, 

156 
although this is not necessary for @{text cvc3} and @{text z3}, which 

157 
can also be used over an Internetbased service. 

158 

159 
When using local SMT solvers, the path to their binaries should be 

160 
declared by setting the following environment variables: 

161 
@{text CVC3_SOLVER}, @{text YICES_SOLVER}, and @{text Z3_SOLVER}. 

162 
*} 

163 

164 
declare [[ smt_solver = z3 ]] 

165 

166 
text {* 

167 
Since SMT solvers are potentially nonterminating, there is a timeout 

168 
(given in seconds) to restrict their runtime. A value greater than 

169 
120 (seconds) is in most cases not advisable. 

170 
*} 

171 

172 
declare [[ smt_timeout = 20 ]] 

173 

174 

175 

176 
subsection {* Certificates *} 

177 

178 
text {* 

179 
By setting the option @{text smt_certificates} to the name of a file, 

180 
all following applications of an SMT solver a cached in that file. 

181 
Any further application of the same SMT solver (using the very same 

182 
configuration) reuses the cached certificate instead of invoking the 

183 
solver. An empty string disables caching certificates. 

184 

185 
The filename should be given as an explicit path. It is good 

186 
practice to use the name of the current theory (with ending 

187 
@{text ".certs"} instead of @{text ".thy"}) as the certificates file. 

188 
*} 

189 

190 
declare [[ smt_certificates = "" ]] 

191 

192 
text {* 

193 
The option @{text smt_fixed} controls whether only stored 

194 
certificates are should be used or invocation of an SMT solver is 

195 
allowed. When set to @{text true}, no SMT solver will ever be 

196 
invoked and only the existing certificates found in the configured 

197 
cache are used; when set to @{text false} and there is no cached 

198 
certificate for some proposition, then the configured SMT solver is 

199 
invoked. 

200 
*} 

201 

202 
declare [[ smt_fixed = false ]] 

203 

204 

205 

206 
subsection {* Tracing *} 

207 

208 
text {* 

209 
For tracing the generated problem file given to the SMT solver as 

210 
well as the returned result of the solver, the option 

211 
@{text smt_trace} should be set to @{text true}. 

212 
*} 

213 

214 
declare [[ smt_trace = false ]] 

215 

216 

217 

218 
subsection {* Z3specific options *} 

219 

220 
text {* 

221 
Z3 is the only SMT solver whose proofs are checked (or reconstructed) 

222 
in Isabelle (all other solvers are implemented as oracles). Enabling 

223 
or disabling proof reconstruction for Z3 is controlled by the option 

224 
@{text z3_proofs}. 

225 
*} 

226 

227 
declare [[ z3_proofs = true ]] 

228 

229 
text {* 

230 
From the set of assumptions given to Z3, those assumptions used in 

231 
the proof are traced when the option @{text z3_trace_assms} is set to 

232 
@{term true}. 

233 
*} 

234 

235 
declare [[ z3_trace_assms = false ]] 

236 

237 
text {* 

238 
Z3 provides several commandline options to tweak its behaviour. They 

239 
can be configured by writing them literally as value for the option 

240 
@{text z3_options}. 

241 
*} 

242 

243 
declare [[ z3_options = "" ]] 

244 

245 

246 

36902
c6bae4456741
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents:
36899
diff
changeset

247 
subsection {* Schematic rules for Z3 proof reconstruction *} 
36898  248 

249 
text {* 

250 
Several prof rules of Z3 are not very well documented. There are two 

251 
lemma groups which can turn failing Z3 proof reconstruction attempts 

252 
into succeeding ones: the facts in @{text z3_rule} are tried prior to 

253 
any implemented reconstruction procedure for all uncertain Z3 proof 

254 
rules; the facts in @{text z3_simp} are only fed to invocations of 

255 
the simplifier when reconstructing theoryspecific proof steps. 

256 
*} 

257 

258 
lemmas [z3_rule] = 

259 
refl eq_commute conj_commute disj_commute simp_thms nnf_simps 

260 
ring_distribs field_simps times_divide_eq_right times_divide_eq_left 

261 
if_True if_False not_not 

262 

263 
lemma [z3_rule]: 

264 
"(P \<longrightarrow> Q) = (Q \<or> \<not>P)" 

265 
"(\<not>P \<longrightarrow> Q) = (P \<or> Q)" 

266 
"(\<not>P \<longrightarrow> Q) = (Q \<or> P)" 

267 
by auto 

268 

269 
lemma [z3_rule]: 

270 
"((P = Q) \<longrightarrow> R) = (R  (Q = (\<not>P)))" 

271 
by auto 

272 

273 
lemma [z3_rule]: 

274 
"((\<not>P) = P) = False" 

275 
"(P = (\<not>P)) = False" 

276 
"(P \<noteq> Q) = (Q = (\<not>P))" 

277 
"(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))" 

278 
"(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))" 

279 
by auto 

280 

281 
lemma [z3_rule]: 

282 
"(if P then P else \<not>P) = True" 

283 
"(if \<not>P then \<not>P else P) = True" 

284 
"(if P then True else False) = P" 

285 
"(if P then False else True) = (\<not>P)" 

286 
"(if \<not>P then x else y) = (if P then y else x)" 

287 
by auto 

288 

289 
lemma [z3_rule]: 

290 
"P = Q \<or> P \<or> Q" 

291 
"P = Q \<or> \<not>P \<or> \<not>Q" 

292 
"(\<not>P) = Q \<or> \<not>P \<or> Q" 

293 
"(\<not>P) = Q \<or> P \<or> \<not>Q" 

294 
"P = (\<not>Q) \<or> \<not>P \<or> Q" 

295 
"P = (\<not>Q) \<or> P \<or> \<not>Q" 

296 
"P \<noteq> Q \<or> P \<or> \<not>Q" 

297 
"P \<noteq> Q \<or> \<not>P \<or> Q" 

298 
"P \<noteq> (\<not>Q) \<or> P \<or> Q" 

299 
"(\<not>P) \<noteq> Q \<or> P \<or> Q" 

300 
"P \<or> Q \<or> P \<noteq> (\<not>Q)" 

301 
"P \<or> Q \<or> (\<not>P) \<noteq> Q" 

302 
"P \<or> \<not>Q \<or> P \<noteq> Q" 

303 
"\<not>P \<or> Q \<or> P \<noteq> Q" 

304 
by auto 

305 

306 
lemma [z3_rule]: 

307 
"0 + (x::int) = x" 

308 
"x + 0 = x" 

309 
"0 * x = 0" 

310 
"1 * x = x" 

311 
"x + y = y + x" 

312 
by auto 

313 

37124  314 

315 

316 
hide_type (open) pattern 

317 
hide_const Pattern "apply" term_eq 

37151  318 
hide_const (open) trigger pat nopat z3div z3mod 
37124  319 

36898  320 
end 