author  haftmann 
Wed, 14 Jul 2010 14:16:12 +0200  
changeset 37818  dd65033fed78 
parent 37157  86872cbae9e9 
child 39298  5aefb5bc8a93 
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 
("Tools/SMT/smt_monomorph.ML") 

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

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

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

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

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

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

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

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

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

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

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

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

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

24 
begin 

25 

26 

27 

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

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

30 
text {* 

31 
Some SMT solvers support triggers for quantifier instantiation. 

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

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

35 

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

37 
pattern with positive subterms only), it instantiates the 

38 
corresponding quantifier accordingly. Negative patterns inhibit 

39 
quantifier instantiations. Each pattern should mention all preceding 

40 
bound variables. 

36898  41 
*} 
42 

43 
datatype pattern = Pattern 

44 

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

36898  47 

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

51 

52 

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

53 
subsection {* Higherorder encoding *} 
36898  54 

55 
text {* 

56 
Application is made explicit for constants occurring with varying 

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

58 
following constant. 

59 
*} 

60 

37153
8feed34275ce
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
boehmes
parents:
37151
diff
changeset

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

63 
text {* 

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

65 
higherorder functions. The following set of lemmas specifies the 

66 
properties of such (extensional) arrays. 

67 
*} 

68 

69 
lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other 

37157  70 
fun_upd_upd fun_app_def 
36898  71 

72 

73 

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

74 
subsection {* Firstorder logic *} 
36898  75 

76 
text {* 

77 
Some SMT solvers require a strict separation between formulas and 

78 
terms. When translating higherorder into firstorder problems, 

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

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

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

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

83 
following termlevel equation symbol. 

84 
*} 

85 

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

88 

89 

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

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

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

94 

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

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

97 

98 
lemma div_by_z3div: "k div l = ( 

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

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

101 
else z3div (k) (l))" 

102 
by (auto simp add: z3div_def) 

103 

104 
lemma mod_by_z3mod: "k mod l = ( 

105 
if l = 0 then k 

106 
else if k = 0 then 0 

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

108 
else  z3mod (k) (l))" 

109 
by (auto simp add: z3mod_def) 

110 

111 

112 

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

113 
subsection {* Setup *} 
36898  114 

115 
use "Tools/SMT/smt_monomorph.ML" 

116 
use "Tools/SMT/smt_normalize.ML" 

117 
use "Tools/SMT/smt_translate.ML" 

118 
use "Tools/SMT/smt_solver.ML" 

119 
use "Tools/SMT/smtlib_interface.ML" 

120 
use "Tools/SMT/z3_interface.ML" 

121 
use "Tools/SMT/z3_proof_parser.ML" 

122 
use "Tools/SMT/z3_proof_tools.ML" 

123 
use "Tools/SMT/z3_proof_literals.ML" 

124 
use "Tools/SMT/z3_proof_reconstruction.ML" 

125 
use "Tools/SMT/z3_model.ML" 

126 
use "Tools/SMT/z3_solver.ML" 

127 
use "Tools/SMT/cvc3_solver.ML" 

128 
use "Tools/SMT/yices_solver.ML" 

129 

130 
setup {* 

131 
SMT_Solver.setup #> 

132 
Z3_Proof_Reconstruction.setup #> 

133 
Z3_Solver.setup #> 

134 
CVC3_Solver.setup #> 

135 
Yices_Solver.setup 

136 
*} 

137 

138 

139 

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

140 
subsection {* Configuration *} 
36898  141 

142 
text {* 

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

143 
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

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

147 

148 

149 
subsection {* General configuration options *} 

150 

151 
text {* 

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

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

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

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

156 
can also be used over an Internetbased service. 

157 

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

159 
declared by setting the following environment variables: 

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

161 
*} 

162 

163 
declare [[ smt_solver = z3 ]] 

164 

165 
text {* 

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

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

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

169 
*} 

170 

171 
declare [[ smt_timeout = 20 ]] 

172 

173 

174 

175 
subsection {* Certificates *} 

176 

177 
text {* 

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

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

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

181 
configuration) reuses the cached certificate instead of invoking the 

182 
solver. An empty string disables caching certificates. 

183 

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

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

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

187 
*} 

188 

189 
declare [[ smt_certificates = "" ]] 

190 

191 
text {* 

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

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

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

195 
invoked and only the existing certificates found in the configured 

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

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

198 
invoked. 

199 
*} 

200 

201 
declare [[ smt_fixed = false ]] 

202 

203 

204 

205 
subsection {* Tracing *} 

206 

207 
text {* 

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

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

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

211 
*} 

212 

213 
declare [[ smt_trace = false ]] 

214 

215 

216 

217 
subsection {* Z3specific options *} 

218 

219 
text {* 

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

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

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

223 
@{text z3_proofs}. 

224 
*} 

225 

226 
declare [[ z3_proofs = true ]] 

227 

228 
text {* 

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

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

231 
@{term true}. 

232 
*} 

233 

234 
declare [[ z3_trace_assms = false ]] 

235 

236 
text {* 

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

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

239 
@{text z3_options}. 

240 
*} 

241 

242 
declare [[ z3_options = "" ]] 

243 

244 

245 

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

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

248 
text {* 

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

250 
lemma groups which can turn failing Z3 proof reconstruction attempts 

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

252 
any implemented reconstruction procedure for all uncertain Z3 proof 

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

254 
the simplifier when reconstructing theoryspecific proof steps. 

255 
*} 

256 

257 
lemmas [z3_rule] = 

258 
refl eq_commute conj_commute disj_commute simp_thms nnf_simps 

259 
ring_distribs field_simps times_divide_eq_right times_divide_eq_left 

260 
if_True if_False not_not 

261 

262 
lemma [z3_rule]: 

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

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

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

266 
by auto 

267 

268 
lemma [z3_rule]: 

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

270 
by auto 

271 

272 
lemma [z3_rule]: 

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

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

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

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

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

278 
by auto 

279 

280 
lemma [z3_rule]: 

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

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

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

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

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

286 
by auto 

287 

288 
lemma [z3_rule]: 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

303 
by auto 

304 

305 
lemma [z3_rule]: 

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

307 
"x + 0 = x" 

308 
"0 * x = 0" 

309 
"1 * x = x" 

310 
"x + y = y + x" 

311 
by auto 

312 

37124  313 

314 

315 
hide_type (open) pattern 

37153
8feed34275ce
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
boehmes
parents:
37151
diff
changeset

316 
hide_const Pattern term_eq 
8feed34275ce
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
boehmes
parents:
37151
diff
changeset

317 
hide_const (open) trigger pat nopat fun_app z3div z3mod 
37124  318 

36898  319 
end 