author  boehmes 
Mon, 17 Jan 2011 17:45:52 +0100  
changeset 41601  fda8511006f9 
parent 41462  5f4939d46b63 
child 41762  00060198de12 
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 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

8 
imports Record 
36898  9 
uses 
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41121
diff
changeset

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

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" 
41174
10eb369f8c01
fixed trigger inference: testing if a theorem already has a trigger was too strict;
boehmes
parents:
41127
diff
changeset

13 
("Tools/SMT/smt_monomorph.ML") 
40277  14 
("Tools/SMT/smt_builtin.ML") 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

15 
("Tools/SMT/smt_datatypes.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") 

41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41281
diff
changeset

20 
("Tools/SMT/z3_interface.ML") 
36898  21 
("Tools/SMT/z3_proof_parser.ML") 
22 
("Tools/SMT/z3_proof_tools.ML") 

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

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

24 
("Tools/SMT/z3_proof_methods.ML") 
36898  25 
("Tools/SMT/z3_proof_reconstruction.ML") 
26 
("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

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

41125  35 
Some SMT solvers support patterns as a quantifier instantiation 
36 
heuristics. Patterns may either be positive terms (tagged by "pat") 

37 
triggering quantifier instantiations  when the solver finds a 

38 
term matching a positive pattern, it instantiates the corresponding 

39 
quantifier accordingly  or negative terms (tagged by "nopat") 

40 
inhibiting quantifier instantiations. A list of patterns 

41 
of the same kind is called a multipattern, and all patterns in a 

42 
multipattern are considered conjunctively for quantifier instantiation. 

43 
A list of multipatterns is called a trigger, and their multipatterns 

44 
act disjunctively during quantifier instantiation. Each multipattern 

45 
should mention at least all quantified variables of the preceding 

46 
quantifier block. 

36898  47 
*} 
48 

49 
datatype pattern = Pattern 

50 

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

36898  53 

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

57 

58 

40664  59 
subsection {* Quantifier weights *} 
60 

61 
text {* 

62 
Weight annotations to quantifiers influence the priority of quantifier 

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

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

65 
*} 

66 

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

68 

69 
text {* 

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

71 
no weight at all. 

72 

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

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

75 

76 
\begin{itemize} 

77 
\item 

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

79 
\item 

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

81 
\end{itemize} 

82 
*} 

83 

84 

85 

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

86 
subsection {* Higherorder encoding *} 
36898  87 

88 
text {* 

89 
Application is made explicit for constants occurring with varying 

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

91 
following constant. 

92 
*} 

93 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

94 
definition fun_app where "fun_app f = f" 
36898  95 

96 
text {* 

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

98 
higherorder functions. The following set of lemmas specifies the 

99 
properties of such (extensional) arrays. 

100 
*} 

101 

102 
lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other 

37157  103 
fun_upd_upd fun_app_def 
36898  104 

105 

106 

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

107 
subsection {* Firstorder logic *} 
36898  108 

109 
text {* 

41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40806
diff
changeset

110 
Some SMT solvers only accept problems in firstorder logic, i.e., 
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40806
diff
changeset

111 
where formulas and terms are syntactically separated. When 
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40806
diff
changeset

112 
translating higherorder into firstorder problems, all 
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40806
diff
changeset

113 
uninterpreted constants (those not builtin in the target solver) 
36898  114 
are treated as function symbols in the firstorder sense. Their 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40806
diff
changeset

115 
occurrences as head symbols in atoms (i.e., as predicate symbols) are 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset

116 
turned into terms by logically equating such atoms with @{term True}. 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset

117 
For technical reasons, @{term True} and @{term False} occurring inside 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset

118 
terms are replaced by the following constants. 
36898  119 
*} 
120 

41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset

121 
definition term_true where "term_true = True" 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset

122 
definition term_false where "term_false = False" 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset

123 

36898  124 

125 

37151  126 
subsection {* Integer division and modulo for Z3 *} 
127 

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

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

130 

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

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

133 

134 

135 

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

136 
subsection {* Setup *} 
36898  137 

41174
10eb369f8c01
fixed trigger inference: testing if a theorem already has a trigger was too strict;
boehmes
parents:
41127
diff
changeset

138 
use "Tools/SMT/smt_monomorph.ML" 
40277  139 
use "Tools/SMT/smt_builtin.ML" 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

140 
use "Tools/SMT/smt_datatypes.ML" 
36898  141 
use "Tools/SMT/smt_normalize.ML" 
142 
use "Tools/SMT/smt_translate.ML" 

143 
use "Tools/SMT/smt_solver.ML" 

144 
use "Tools/SMT/smtlib_interface.ML" 

145 
use "Tools/SMT/z3_interface.ML" 

146 
use "Tools/SMT/z3_proof_parser.ML" 

147 
use "Tools/SMT/z3_proof_tools.ML" 

148 
use "Tools/SMT/z3_proof_literals.ML" 

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

149 
use "Tools/SMT/z3_proof_methods.ML" 
36898  150 
use "Tools/SMT/z3_proof_reconstruction.ML" 
151 
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

152 
use "Tools/SMT/smt_setup_solvers.ML" 
36898  153 

154 
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

155 
SMT_Config.setup #> 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40806
diff
changeset

156 
SMT_Normalize.setup #> 
36898  157 
SMT_Solver.setup #> 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40806
diff
changeset

158 
SMTLIB_Interface.setup #> 
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40806
diff
changeset

159 
Z3_Interface.setup #> 
36898  160 
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

161 
SMT_Setup_Solvers.setup 
36898  162 
*} 
163 

164 

165 

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

166 
subsection {* Configuration *} 
36898  167 

168 
text {* 

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

169 
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

170 
@{text smt_status}, which shows the values of most options. 
36898  171 
*} 
172 

173 

174 

175 
subsection {* General configuration options *} 

176 

177 
text {* 

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

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41426
diff
changeset

179 
solver. The possible values can be obtained from the @{text smt_status} 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41426
diff
changeset

180 
command. 
41459
f0db8f40d656
added hints about licensing restrictions and how to enable Z3
boehmes
parents:
41432
diff
changeset

181 

f0db8f40d656
added hints about licensing restrictions and how to enable Z3
boehmes
parents:
41432
diff
changeset

182 
Due to licensing restrictions, Yices and Z3 are not installed/enabled 
f0db8f40d656
added hints about licensing restrictions and how to enable Z3
boehmes
parents:
41432
diff
changeset

183 
by default. Z3 is free for noncommercial applications and can be enabled 
41462  184 
by simply setting the environment variable @{text Z3_NON_COMMERCIAL} to 
185 
@{text yes}. 

36898  186 
*} 
187 

41601  188 
declare [[ smt_solver = z3 ]] 
36898  189 

190 
text {* 

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

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

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

194 
*} 

195 

196 
declare [[ smt_timeout = 20 ]] 

197 

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

198 
text {* 
41121
5c5d05963f93
added option to modify the random seed of SMT solvers
boehmes
parents:
41059
diff
changeset

199 
SMT solvers apply randomized heuristics. In case a problem is not 
5c5d05963f93
added option to modify the random seed of SMT solvers
boehmes
parents:
41059
diff
changeset

200 
solvable by an SMT solver, changing the following option might help. 
5c5d05963f93
added option to modify the random seed of SMT solvers
boehmes
parents:
41059
diff
changeset

201 
*} 
5c5d05963f93
added option to modify the random seed of SMT solvers
boehmes
parents:
41059
diff
changeset

202 

5c5d05963f93
added option to modify the random seed of SMT solvers
boehmes
parents:
41059
diff
changeset

203 
declare [[ smt_random_seed = 1 ]] 
5c5d05963f93
added option to modify the random seed of SMT solvers
boehmes
parents:
41059
diff
changeset

204 

5c5d05963f93
added option to modify the random seed of SMT solvers
boehmes
parents:
41059
diff
changeset

205 
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

206 
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

207 
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

208 
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

209 
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

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

211 

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

212 
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

213 

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

214 
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

215 
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

216 
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

217 
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

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

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41426
diff
changeset

220 
declare [[ cvc3_options = "", remote_cvc3_options = "" ]] 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41426
diff
changeset

221 
declare [[ yices_options = "" ]] 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41426
diff
changeset

222 
declare [[ z3_options = "", remote_z3_options = "" ]] 
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

223 

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

225 
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

226 
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

227 
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

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

231 

41125  232 
text {* 
233 
The SMT method provides an inference mechanism to detect simple triggers 

234 
in quantified formulas, which might increase the number of problems 

235 
solvable by SMT solvers (note: triggers guide quantifier instantiations 

236 
in the SMT solver). To turn it on, set the following option. 

237 
*} 

238 

239 
declare [[ smt_infer_triggers = false ]] 

240 

241 
text {* 

242 
The SMT method monomorphizes the given facts, that is, it tries to 

243 
instantiate all schematic type variables with fixed types occurring 

244 
in the problem. This is a (possibly nonterminating) fixedpoint 

245 
construction whose cycles are limited by the following option. 

246 
*} 

247 

248 
declare [[ smt_monomorph_limit = 10 ]] 

249 

36898  250 

251 

252 
subsection {* Certificates *} 

253 

254 
text {* 

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

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

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

258 
configuration) reuses the cached certificate instead of invoking the 

259 
solver. An empty string disables caching certificates. 

260 

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

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

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

264 
*} 

265 

266 
declare [[ smt_certificates = "" ]] 

267 

268 
text {* 

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

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

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

272 
invoked and only the existing certificates found in the configured 

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

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

275 
invoked. 

276 
*} 

277 

278 
declare [[ smt_fixed = false ]] 

279 

280 

281 

282 
subsection {* Tracing *} 

283 

284 
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

285 
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

286 
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

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

288 

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

289 
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

290 

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

291 
text {* 
36898  292 
For tracing the generated problem file given to the SMT solver as 
293 
well as the returned result of the solver, the option 

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

295 
*} 

296 

297 
declare [[ smt_trace = false ]] 

298 

299 
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

300 
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

301 
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

302 
@{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

303 
(see options @{text smt_solver} and @{text smt_oracle} above). 
36898  304 
*} 
305 

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

306 
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

307 

36898  308 

309 

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

310 
subsection {* Schematic rules for Z3 proof reconstruction *} 
36898  311 

312 
text {* 

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

314 
lemma groups which can turn failing Z3 proof reconstruction attempts 

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

316 
any implemented reconstruction procedure for all uncertain Z3 proof 

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

318 
the simplifier when reconstructing theoryspecific proof steps. 

319 
*} 

320 

321 
lemmas [z3_rule] = 

322 
refl eq_commute conj_commute disj_commute simp_thms nnf_simps 

323 
ring_distribs field_simps times_divide_eq_right times_divide_eq_left 

324 
if_True if_False not_not 

325 

326 
lemma [z3_rule]: 

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

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

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

330 
by auto 

331 

332 
lemma [z3_rule]: 

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

334 
by auto 

335 

336 
lemma [z3_rule]: 

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

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

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

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

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

342 
by auto 

343 

344 
lemma [z3_rule]: 

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

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

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

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

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

40806
59d96f777da3
also support higherorder rules for Z3 proof reconstruction
boehmes
parents:
40681
diff
changeset

350 
"f (if P then x else y) = (if P then f x else f y)" 
36898  351 
by auto 
352 

353 
lemma [z3_rule]: 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

368 
by auto 

369 

370 
lemma [z3_rule]: 

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

372 
"x + 0 = x" 

373 
"0 * x = 0" 

374 
"1 * x = x" 

375 
"x + y = y + x" 

376 
by auto 

377 

37124  378 

379 

380 
hide_type (open) pattern 

41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset

381 
hide_const Pattern fun_app term_true term_false z3div z3mod 
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41174
diff
changeset

382 
hide_const (open) trigger pat nopat weight 
37124  383 

36898  384 
end 