summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/SMT.thy

author | haftmann |

Fri Jun 11 17:14:02 2010 +0200 (2010-06-11) | |

changeset 37407 | 61dd8c145da7 |

parent 37157 | 86872cbae9e9 |

child 37818 | dd65033fed78 |

permissions | -rw-r--r-- |

declare lex_prod_def [code del]

1 (* Title: HOL/SMT.thy

2 Author: Sascha Boehme, TU Muenchen

3 *)

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

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

29 subsection {* Triggers for quantifier instantiation *}

31 text {*

32 Some SMT solvers support triggers for quantifier instantiation.

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

34 be a list of positive subterms (each being tagged by "pat"), or a

35 list of negative subterms (each being tagged by "nopat").

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.

42 *}

44 datatype pattern = Pattern

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

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

49 definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool"

50 where "trigger _ P = P"

54 subsection {* Higher-order encoding *}

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 *}

62 definition fun_app where "fun_app f x = f x"

64 text {*

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

66 higher-order functions. The following set of lemmas specifies the

67 properties of such (extensional) arrays.

68 *}

70 lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other

71 fun_upd_upd fun_app_def

75 subsection {* First-order logic *}

77 text {*

78 Some SMT solvers require a strict separation between formulas and

79 terms. When translating higher-order into first-order problems,

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

81 are treated as function symbols in the first-order 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 term-level equation symbol.

85 *}

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

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

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)))"

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))"

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)

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)

114 subsection {* Setup *}

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"

131 setup {*

132 SMT_Solver.setup #>

133 Z3_Proof_Reconstruction.setup #>

134 Z3_Solver.setup #>

135 CVC3_Solver.setup #>

136 Yices_Solver.setup

137 *}

141 subsection {* Configuration *}

143 text {*

144 The current configuration can be printed by the command

145 @{text smt_status}, which shows the values of most options.

146 *}

150 subsection {* General configuration options *}

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 Internet-based service.

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 *}

164 declare [[ smt_solver = z3 ]]

166 text {*

167 Since SMT solvers are potentially non-terminating, 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 *}

172 declare [[ smt_timeout = 20 ]]

176 subsection {* Certificates *}

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) re-uses the cached certificate instead of invoking the

183 solver. An empty string disables caching certificates.

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 *}

190 declare [[ smt_certificates = "" ]]

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 *}

202 declare [[ smt_fixed = false ]]

206 subsection {* Tracing *}

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 *}

214 declare [[ smt_trace = false ]]

218 subsection {* Z3-specific options *}

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 *}

227 declare [[ z3_proofs = true ]]

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 *}

235 declare [[ z3_trace_assms = false ]]

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 *}

243 declare [[ z3_options = "" ]]

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

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 theory-specific proof steps.

256 *}

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

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

269 lemma [z3_rule]:

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

271 by auto

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

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

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

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

316 hide_type (open) pattern

317 hide_const Pattern term_eq

318 hide_const (open) trigger pat nopat fun_app z3div z3mod

320 end