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

src/HOL/SMT.thy

author | boehmes |

Wed Dec 15 08:39:24 2010 +0100 (2010-12-15) | |

changeset 41124 | 1de17a2de5ad |

parent 41121 | 5c5d05963f93 |

child 41125 | 4a9eec045f2a |

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

moved SMT classes and dictionary functions to SMT_Utils

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 "Tools/Datatype/datatype_selectors.ML"

11 "Tools/SMT/smt_utils.ML"

12 "Tools/SMT/smt_failure.ML"

13 "Tools/SMT/smt_config.ML"

14 "Tools/SMT/smt_monomorph.ML"

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

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

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

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

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

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

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

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

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

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

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

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

27 ("Tools/SMT/smt_setup_solvers.ML")

28 begin

32 subsection {* Triggers for quantifier instantiation *}

34 text {*

35 Some SMT solvers support triggers for quantifier instantiation.

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

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

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

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

41 pattern with positive subterms only), it instantiates the

42 corresponding quantifier accordingly. Negative patterns inhibit

43 quantifier instantiations. Each pattern should mention all preceding

44 bound variables.

45 *}

47 datatype pattern = Pattern

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

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

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

53 where "trigger _ P = P"

57 subsection {* Quantifier weights *}

59 text {*

60 Weight annotations to quantifiers influence the priority of quantifier

61 instantiations. They should be handled with care for solvers, which support

62 them, because incorrect choices of weights might render a problem unsolvable.

63 *}

65 definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"

67 text {*

68 Weights must be non-negative. The value @{text 0} is equivalent to providing

69 no weight at all.

71 Weights should only be used at quantifiers and only inside triggers (if the

72 quantifier has triggers). Valid usages of weights are as follows:

74 \begin{itemize}

75 \item

76 @{term "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"}

77 \item

78 @{term "\<forall>x. weight 3 (P x)"}

79 \end{itemize}

80 *}

84 subsection {* Higher-order encoding *}

86 text {*

87 Application is made explicit for constants occurring with varying

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

89 following constant.

90 *}

92 definition fun_app where "fun_app f x = f x"

94 text {*

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

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

97 properties of such (extensional) arrays.

98 *}

100 lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other

101 fun_upd_upd fun_app_def

105 subsection {* First-order logic *}

107 text {*

108 Some SMT solvers only accept problems in first-order logic, i.e.,

109 where formulas and terms are syntactically separated. When

110 translating higher-order into first-order problems, all

111 uninterpreted constants (those not built-in in the target solver)

112 are treated as function symbols in the first-order sense. Their

113 occurrences as head symbols in atoms (i.e., as predicate symbols) are

114 turned into terms by equating such atoms with @{term True}.

115 Whenever the boolean type occurs in first-order terms, it is replaced

116 by the following type.

117 *}

119 typedecl term_bool

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

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

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

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

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

131 lemma div_by_z3div: "k div l = (

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

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

134 else z3div (-k) (-l))"

135 by (auto simp add: z3div_def)

137 lemma mod_by_z3mod: "k mod l = (

138 if l = 0 then k

139 else if k = 0 then 0

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

141 else - z3mod (-k) (-l))"

142 by (auto simp add: z3mod_def)

146 subsection {* Setup *}

148 use "Tools/SMT/smt_builtin.ML"

149 use "Tools/SMT/smt_normalize.ML"

150 use "Tools/SMT/smt_translate.ML"

151 use "Tools/SMT/smt_solver.ML"

152 use "Tools/SMT/smtlib_interface.ML"

153 use "Tools/SMT/z3_interface.ML"

154 use "Tools/SMT/z3_proof_parser.ML"

155 use "Tools/SMT/z3_proof_tools.ML"

156 use "Tools/SMT/z3_proof_literals.ML"

157 use "Tools/SMT/z3_proof_methods.ML"

158 use "Tools/SMT/z3_proof_reconstruction.ML"

159 use "Tools/SMT/z3_model.ML"

160 use "Tools/SMT/smt_setup_solvers.ML"

162 setup {*

163 SMT_Config.setup #>

164 SMT_Normalize.setup #>

165 SMT_Solver.setup #>

166 SMTLIB_Interface.setup #>

167 Z3_Interface.setup #>

168 Z3_Proof_Reconstruction.setup #>

169 SMT_Setup_Solvers.setup

170 *}

174 subsection {* Configuration *}

176 text {*

177 The current configuration can be printed by the command

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

179 *}

183 subsection {* General configuration options *}

185 text {*

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

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

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

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

190 can also be used over an Internet-based service.

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

193 declared by setting the following environment variables:

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

195 *}

197 declare [[ smt_solver = z3 ]]

199 text {*

200 Since SMT solvers are potentially non-terminating, there is a timeout

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

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

203 *}

205 declare [[ smt_timeout = 20 ]]

207 text {*

208 SMT solvers apply randomized heuristics. In case a problem is not

209 solvable by an SMT solver, changing the following option might help.

210 *}

212 declare [[ smt_random_seed = 1 ]]

214 text {*

215 In general, the binding to SMT solvers runs as an oracle, i.e, the SMT

216 solvers are fully trusted without additional checks. The following

217 option can cause the SMT solver to run in proof-producing mode, giving

218 a checkable certificate. This is currently only implemented for Z3.

219 *}

221 declare [[ smt_oracle = false ]]

223 text {*

224 Each SMT solver provides several commandline options to tweak its

225 behaviour. They can be passed to the solver by setting the following

226 options.

227 *}

229 declare [[ cvc3_options = "", yices_options = "", z3_options = "" ]]

231 text {*

232 Enable the following option to use built-in support for datatypes and

233 records. Currently, this is only implemented for Z3 running in oracle

234 mode.

235 *}

237 declare [[ smt_datatypes = false ]]

241 subsection {* Certificates *}

243 text {*

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

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

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

247 configuration) re-uses the cached certificate instead of invoking the

248 solver. An empty string disables caching certificates.

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

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

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

253 *}

255 declare [[ smt_certificates = "" ]]

257 text {*

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

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

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

261 invoked and only the existing certificates found in the configured

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

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

264 invoked.

265 *}

267 declare [[ smt_fixed = false ]]

271 subsection {* Tracing *}

273 text {*

274 The SMT method, when applied, traces important information. To

275 make it entirely silent, set the following option to @{text false}.

276 *}

278 declare [[ smt_verbose = true ]]

280 text {*

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

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

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

284 *}

286 declare [[ smt_trace = false ]]

288 text {*

289 From the set of assumptions given to the SMT solver, those assumptions

290 used in the proof are traced when the following option is set to

291 @{term true}. This only works for Z3 when it runs in non-oracle mode

292 (see options @{text smt_solver} and @{text smt_oracle} above).

293 *}

295 declare [[ smt_trace_used_facts = false ]]

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

301 text {*

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

303 lemma groups which can turn failing Z3 proof reconstruction attempts

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

305 any implemented reconstruction procedure for all uncertain Z3 proof

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

307 the simplifier when reconstructing theory-specific proof steps.

308 *}

310 lemmas [z3_rule] =

311 refl eq_commute conj_commute disj_commute simp_thms nnf_simps

312 ring_distribs field_simps times_divide_eq_right times_divide_eq_left

313 if_True if_False not_not

315 lemma [z3_rule]:

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

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

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

319 by auto

321 lemma [z3_rule]:

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

323 by auto

325 lemma [z3_rule]:

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

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

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

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

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

331 by auto

333 lemma [z3_rule]:

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

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

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

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

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

339 "f (if P then x else y) = (if P then f x else f y)"

340 by auto

342 lemma [z3_rule]:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

357 by auto

359 lemma [z3_rule]:

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

361 "x + 0 = x"

362 "0 * x = 0"

363 "1 * x = x"

364 "x + y = y + x"

365 by auto

369 hide_type term_bool

370 hide_type (open) pattern

371 hide_const Pattern fun_app

372 hide_const (open) trigger pat nopat weight z3div z3mod

376 subsection {* Selectors for datatypes *}

378 setup {* Datatype_Selectors.setup *}

380 declare [[ selector Pair 1 = fst, selector Pair 2 = snd ]]

381 declare [[ selector Cons 1 = hd, selector Cons 2 = tl ]]

383 end