author  boehmes 
Mon, 22 Nov 2010 23:37:00 +0100  
changeset 40664  e023788a91a1 
parent 40662  798aad2229c0 
child 40681  872b08416fb4 
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 

39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

10 
"Tools/Datatype/datatype_selectors.ML" 
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40277
diff
changeset

11 
"Tools/SMT/smt_failure.ML" 
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40277
diff
changeset

12 
"Tools/SMT/smt_config.ML" 
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40424
diff
changeset

13 
"Tools/SMT/smt_utils.ML" 
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40277
diff
changeset

14 
"Tools/SMT/smt_monomorph.ML" 
40277  15 
("Tools/SMT/smt_builtin.ML") 
36898  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") 

40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40424
diff
changeset

23 
("Tools/SMT/z3_proof_methods.ML") 
36898  24 
("Tools/SMT/z3_proof_reconstruction.ML") 
25 
("Tools/SMT/z3_model.ML") 

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

40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

27 
("Tools/SMT/smt_setup_solvers.ML") 
36898  28 
begin 
29 

30 

31 

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

32 
subsection {* Triggers for quantifier instantiation *} 
36898  33 

34 
text {* 

35 
Some SMT solvers support triggers for quantifier instantiation. 

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

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

39 

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. 

36898  45 
*} 
46 

47 
datatype pattern = Pattern 

48 

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

36898  51 

37124  52 
definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool" 
36898  53 
where "trigger _ P = P" 
54 

55 

56 

40664  57 
subsection {* Quantifier weights *} 
58 

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

64 

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

66 

67 
text {* 

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

69 
no weight at all. 

70 

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: 

73 

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

81 

82 

83 

40274
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

84 
subsection {* Distinctness *} 
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

85 

6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

86 
text {* 
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

87 
As an abbreviation for a quadratic number of inequalities, SMT solvers 
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

88 
provide a builtin @{text distinct}. To avoid confusion with the 
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

89 
already defined (and more general) @{term List.distinct}, a separate 
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

90 
constant is defined. 
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

91 
*} 
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

92 

6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

93 
definition distinct :: "'a list \<Rightarrow> bool" 
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

94 
where "distinct xs = List.distinct xs" 
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

95 

6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

96 

6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

97 

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

98 
subsection {* Higherorder encoding *} 
36898  99 

100 
text {* 

101 
Application is made explicit for constants occurring with varying 

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

103 
following constant. 

104 
*} 

105 

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

106 
definition fun_app where "fun_app f x = f x" 
36898  107 

108 
text {* 

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

110 
higherorder functions. The following set of lemmas specifies the 

111 
properties of such (extensional) arrays. 

112 
*} 

113 

114 
lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other 

37157  115 
fun_upd_upd fun_app_def 
36898  116 

117 

118 

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

119 
subsection {* Firstorder logic *} 
36898  120 

121 
text {* 

122 
Some SMT solvers require a strict separation between formulas and 

123 
terms. When translating higherorder into firstorder problems, 

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

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

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

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

128 
following termlevel equation symbol. 

129 
*} 

130 

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

133 

134 

37151  135 
subsection {* Integer division and modulo for Z3 *} 
136 

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

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

139 

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

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

142 

143 
lemma div_by_z3div: "k div l = ( 

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

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

146 
else z3div (k) (l))" 

147 
by (auto simp add: z3div_def) 

148 

149 
lemma mod_by_z3mod: "k mod l = ( 

150 
if l = 0 then k 

151 
else if k = 0 then 0 

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

153 
else  z3mod (k) (l))" 

154 
by (auto simp add: z3mod_def) 

155 

156 

157 

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

158 
subsection {* Setup *} 
36898  159 

40277  160 
use "Tools/SMT/smt_builtin.ML" 
36898  161 
use "Tools/SMT/smt_normalize.ML" 
162 
use "Tools/SMT/smt_translate.ML" 

163 
use "Tools/SMT/smt_solver.ML" 

164 
use "Tools/SMT/smtlib_interface.ML" 

165 
use "Tools/SMT/z3_interface.ML" 

166 
use "Tools/SMT/z3_proof_parser.ML" 

167 
use "Tools/SMT/z3_proof_tools.ML" 

168 
use "Tools/SMT/z3_proof_literals.ML" 

40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40424
diff
changeset

169 
use "Tools/SMT/z3_proof_methods.ML" 
36898  170 
use "Tools/SMT/z3_proof_reconstruction.ML" 
171 
use "Tools/SMT/z3_model.ML" 

40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

172 
use "Tools/SMT/smt_setup_solvers.ML" 
36898  173 

174 
setup {* 

40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40277
diff
changeset

175 
SMT_Config.setup #> 
36898  176 
SMT_Solver.setup #> 
177 
Z3_Proof_Reconstruction.setup #> 

40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

178 
SMT_Setup_Solvers.setup 
36898  179 
*} 
180 

181 

182 

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

183 
subsection {* Configuration *} 
36898  184 

185 
text {* 

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

186 
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

187 
@{text smt_status}, which shows the values of most options. 
36898  188 
*} 
189 

190 

191 

192 
subsection {* General configuration options *} 

193 

194 
text {* 

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

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

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

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

199 
can also be used over an Internetbased service. 

200 

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

202 
declared by setting the following environment variables: 

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

204 
*} 

205 

206 
declare [[ smt_solver = z3 ]] 

207 

208 
text {* 

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

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

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

212 
*} 

213 

214 
declare [[ smt_timeout = 20 ]] 

215 

40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

216 
text {* 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

217 
In general, the binding to SMT solvers runs as an oracle, i.e, the SMT 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

218 
solvers are fully trusted without additional checks. The following 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

219 
option can cause the SMT solver to run in proofproducing mode, giving 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

220 
a checkable certificate. This is currently only implemented for Z3. 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

221 
*} 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

222 

7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

223 
declare [[ smt_oracle = false ]] 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

224 

7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

225 
text {* 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

226 
Each SMT solver provides several commandline options to tweak its 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

227 
behaviour. They can be passed to the solver by setting the following 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

228 
options. 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

229 
*} 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

230 

7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

231 
declare [[ cvc3_options = "", yices_options = "", z3_options = "" ]] 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

232 

7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

233 
text {* 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

234 
Enable the following option to use builtin support for datatypes and 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

235 
records. Currently, this is only implemented for Z3 running in oracle 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

236 
mode. 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

237 
*} 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

238 

7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

239 
declare [[ smt_datatypes = false ]] 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

240 

36898  241 

242 

243 
subsection {* Certificates *} 

244 

245 
text {* 

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

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

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

249 
configuration) reuses the cached certificate instead of invoking the 

250 
solver. An empty string disables caching certificates. 

251 

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

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

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

255 
*} 

256 

257 
declare [[ smt_certificates = "" ]] 

258 

259 
text {* 

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

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

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

263 
invoked and only the existing certificates found in the configured 

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

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

266 
invoked. 

267 
*} 

268 

269 
declare [[ smt_fixed = false ]] 

270 

271 

272 

273 
subsection {* Tracing *} 

274 

275 
text {* 

40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40277
diff
changeset

276 
The SMT method, when applied, traces important information. To 
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40277
diff
changeset

277 
make it entirely silent, set the following option to @{text false}. 
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40277
diff
changeset

278 
*} 
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40277
diff
changeset

279 

7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40277
diff
changeset

280 
declare [[ smt_verbose = true ]] 
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40277
diff
changeset

281 

7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40277
diff
changeset

282 
text {* 
36898  283 
For tracing the generated problem file given to the SMT solver as 
284 
well as the returned result of the solver, the option 

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

286 
*} 

287 

288 
declare [[ smt_trace = false ]] 

289 

290 
text {* 

40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

291 
From the set of assumptions given to the SMT solver, those assumptions 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

292 
used in the proof are traced when the following option is set to 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

293 
@{term true}. This only works for Z3 when it runs in nonoracle mode 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

294 
(see options @{text smt_solver} and @{text smt_oracle} above). 
36898  295 
*} 
296 

40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

297 
declare [[ smt_trace_used_facts = false ]] 
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37818
diff
changeset

298 

36898  299 

300 

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

301 
subsection {* Schematic rules for Z3 proof reconstruction *} 
36898  302 

303 
text {* 

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

305 
lemma groups which can turn failing Z3 proof reconstruction attempts 

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

307 
any implemented reconstruction procedure for all uncertain Z3 proof 

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

309 
the simplifier when reconstructing theoryspecific proof steps. 

310 
*} 

311 

312 
lemmas [z3_rule] = 

313 
refl eq_commute conj_commute disj_commute simp_thms nnf_simps 

314 
ring_distribs field_simps times_divide_eq_right times_divide_eq_left 

315 
if_True if_False not_not 

316 

317 
lemma [z3_rule]: 

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

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

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

321 
by auto 

322 

323 
lemma [z3_rule]: 

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

325 
by auto 

326 

327 
lemma [z3_rule]: 

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

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

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

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

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

333 
by auto 

334 

335 
lemma [z3_rule]: 

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

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

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

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

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

341 
by auto 

342 

343 
lemma [z3_rule]: 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

358 
by auto 

359 

360 
lemma [z3_rule]: 

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

362 
"x + 0 = x" 

363 
"0 * x = 0" 

364 
"1 * x = x" 

365 
"x + y = y + x" 

366 
by auto 

367 

37124  368 

369 

370 
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

371 
hide_const Pattern term_eq 
40664  372 
hide_const (open) trigger pat nopat weight distinct fun_app z3div z3mod 
37124  373 

39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

374 

9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

375 

9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

376 
subsection {* Selectors for datatypes *} 
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

377 

9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

378 
setup {* Datatype_Selectors.setup *} 
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

379 

9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

380 
declare [[ selector Pair 1 = fst, selector Pair 2 = snd ]] 
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

381 
declare [[ selector Cons 1 = hd, selector Cons 2 = tl ]] 
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

382 

36898  383 
end 