author  boehmes 
Thu, 25 Aug 2011 11:15:31 +0200  
changeset 44488  587bf61a00a1 
parent 44087  8e491cb8841c 
child 45392  828e08541cee 
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" 
40277  13 
("Tools/SMT/smt_builtin.ML") 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

14 
("Tools/SMT/smt_datatypes.ML") 
36898  15 
("Tools/SMT/smt_normalize.ML") 
16 
("Tools/SMT/smt_translate.ML") 

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

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

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

19 
("Tools/SMT/z3_interface.ML") 
36898  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") 

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

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

29 

30 

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

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

33 
text {* 

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

36 
triggering quantifier instantiations  when the solver finds a 

37 
term matching a positive pattern, it instantiates the corresponding 

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

39 
inhibiting quantifier instantiations. A list of patterns 

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

41 
multipattern are considered conjunctively for quantifier instantiation. 

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

43 
act disjunctively during quantifier instantiation. Each multipattern 

44 
should mention at least all quantified variables of the preceding 

45 
quantifier block. 

36898  46 
*} 
47 

48 
datatype pattern = Pattern 

49 

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

36898  52 

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

56 

57 

40664  58 
subsection {* Quantifier weights *} 
59 

60 
text {* 

61 
Weight annotations to quantifiers influence the priority of quantifier 

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

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

64 
*} 

65 

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

67 

68 
text {* 

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

70 
no weight at all. 

71 

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

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

74 

75 
\begin{itemize} 

76 
\item 

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

78 
\item 

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

80 
\end{itemize} 

81 
*} 

82 

83 

84 

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

85 
subsection {* Higherorder encoding *} 
36898  86 

87 
text {* 

88 
Application is made explicit for constants occurring with varying 

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

90 
following constant. 

91 
*} 

92 

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

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

95 
text {* 

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

97 
higherorder functions. The following set of lemmas specifies the 

98 
properties of such (extensional) arrays. 

99 
*} 

100 

101 
lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other 

37157  102 
fun_upd_upd fun_app_def 
36898  103 

104 

105 

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

106 
subsection {* Firstorder logic *} 
36898  107 

108 
text {* 

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

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

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

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

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

114 
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

115 
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

116 
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

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

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

120 
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

121 
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

122 

36898  123 

124 

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

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

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

129 

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

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

132 

133 

134 

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

135 
subsection {* Setup *} 
36898  136 

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

138 
use "Tools/SMT/smt_datatypes.ML" 
36898  139 
use "Tools/SMT/smt_normalize.ML" 
140 
use "Tools/SMT/smt_translate.ML" 

141 
use "Tools/SMT/smt_solver.ML" 

142 
use "Tools/SMT/smtlib_interface.ML" 

143 
use "Tools/SMT/z3_interface.ML" 

144 
use "Tools/SMT/z3_proof_parser.ML" 

145 
use "Tools/SMT/z3_proof_tools.ML" 

146 
use "Tools/SMT/z3_proof_literals.ML" 

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

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

150 
use "Tools/SMT/smt_setup_solvers.ML" 
36898  151 

152 
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

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

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

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

157 
Z3_Interface.setup #> 
36898  158 
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

159 
SMT_Setup_Solvers.setup 
36898  160 
*} 
161 

162 

163 

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

164 
subsection {* Configuration *} 
36898  165 

166 
text {* 

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

167 
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

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

171 

172 

173 
subsection {* General configuration options *} 

174 

175 
text {* 

176 
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

177 
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

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

179 

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

180 
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

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

36898  184 
*} 
185 

41601  186 
declare [[ smt_solver = z3 ]] 
36898  187 

188 
text {* 

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

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

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

192 
*} 

193 

194 
declare [[ smt_timeout = 20 ]] 

195 

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

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

197 
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

198 
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

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

200 

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

201 
declare [[ smt_random_seed = 1 ]] 
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 
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

204 
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

205 
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

206 
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

207 
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

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

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

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

213 
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

214 
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

215 
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

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

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

218 
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

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

220 
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

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

223 
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

224 
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

225 
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

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

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

229 

41125  230 
text {* 
231 
The SMT method provides an inference mechanism to detect simple triggers 

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

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

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

235 
*} 

236 

237 
declare [[ smt_infer_triggers = false ]] 

238 

239 
text {* 

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

241 
instantiate all schematic type variables with fixed types occurring 

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

243 
construction whose cycles are limited by the following option. 

244 
*} 

245 

43230
dabf6e311213
clarified meaning of monomorphization configuration option by renaming it
boehmes
parents:
41762
diff
changeset

246 
declare [[ monomorph_max_rounds = 5 ]] 
41125  247 

41762
00060198de12
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
boehmes
parents:
41601
diff
changeset

248 
text {* 
00060198de12
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
boehmes
parents:
41601
diff
changeset

249 
In addition, the number of generated monomorphic instances is limited 
00060198de12
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
boehmes
parents:
41601
diff
changeset

250 
by the following option. 
00060198de12
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
boehmes
parents:
41601
diff
changeset

251 
*} 
00060198de12
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
boehmes
parents:
41601
diff
changeset

252 

43230
dabf6e311213
clarified meaning of monomorphization configuration option by renaming it
boehmes
parents:
41762
diff
changeset

253 
declare [[ monomorph_max_new_instances = 500 ]] 
41762
00060198de12
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
boehmes
parents:
41601
diff
changeset

254 

36898  255 

256 

257 
subsection {* Certificates *} 

258 

259 
text {* 

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

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

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

263 
configuration) reuses the cached certificate instead of invoking the 

264 
solver. An empty string disables caching certificates. 

265 

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

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

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

269 
*} 

270 

271 
declare [[ smt_certificates = "" ]] 

272 

273 
text {* 

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

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

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

277 
invoked and only the existing certificates found in the configured 

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

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

280 
invoked. 

281 
*} 

282 

283 
declare [[ smt_fixed = false ]] 

284 

285 

286 

287 
subsection {* Tracing *} 

288 

289 
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

290 
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

291 
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

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

293 

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

294 
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

295 

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

296 
text {* 
36898  297 
For tracing the generated problem file given to the SMT solver as 
298 
well as the returned result of the solver, the option 

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

300 
*} 

301 

302 
declare [[ smt_trace = false ]] 

303 

304 
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

305 
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

306 
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

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

308 
(see options @{text smt_solver} and @{text smt_oracle} above). 
36898  309 
*} 
310 

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

311 
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

312 

36898  313 

314 

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

315 
subsection {* Schematic rules for Z3 proof reconstruction *} 
36898  316 

317 
text {* 

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

319 
lemma groups which can turn failing Z3 proof reconstruction attempts 

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

321 
any implemented reconstruction procedure for all uncertain Z3 proof 

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

323 
the simplifier when reconstructing theoryspecific proof steps. 

324 
*} 

325 

326 
lemmas [z3_rule] = 

327 
refl eq_commute conj_commute disj_commute simp_thms nnf_simps 

328 
ring_distribs field_simps times_divide_eq_right times_divide_eq_left 

329 
if_True if_False not_not 

330 

331 
lemma [z3_rule]: 

44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

332 
"(P \<and> Q) = (\<not>(\<not>P \<or> \<not>Q))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

333 
"(P \<and> Q) = (\<not>(\<not>Q \<or> \<not>P))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

334 
"(\<not>P \<and> Q) = (\<not>(P \<or> \<not>Q))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

335 
"(\<not>P \<and> Q) = (\<not>(\<not>Q \<or> P))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

336 
"(P \<and> \<not>Q) = (\<not>(\<not>P \<or> Q))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

337 
"(P \<and> \<not>Q) = (\<not>(Q \<or> \<not>P))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

338 
"(\<not>P \<and> \<not>Q) = (\<not>(P \<or> Q))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

339 
"(\<not>P \<and> \<not>Q) = (\<not>(Q \<or> P))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

340 
by auto 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

341 

587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

342 
lemma [z3_rule]: 
36898  343 
"(P \<longrightarrow> Q) = (Q \<or> \<not>P)" 
344 
"(\<not>P \<longrightarrow> Q) = (P \<or> Q)" 

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

44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

346 
"(True \<longrightarrow> P) = P" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

347 
"(P \<longrightarrow> True) = True" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

348 
"(False \<longrightarrow> P) = True" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

349 
"(P \<longrightarrow> P) = True" 
36898  350 
by auto 
351 

352 
lemma [z3_rule]: 

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

354 
by auto 

355 

356 
lemma [z3_rule]: 

44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

357 
"(\<not>True) = False" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

358 
"(\<not>False) = True" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

359 
"(x = x) = True" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

360 
"(P = True) = P" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

361 
"(True = P) = P" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

362 
"(P = False) = (\<not>P)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

363 
"(False = P) = (\<not>P)" 
36898  364 
"((\<not>P) = P) = False" 
365 
"(P = (\<not>P)) = False" 

44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

366 
"((\<not>P) = (\<not>Q)) = (P = Q)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

367 
"\<not>(P = (\<not>Q)) = (P = Q)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

368 
"\<not>((\<not>P) = Q) = (P = Q)" 
36898  369 
"(P \<noteq> Q) = (Q = (\<not>P))" 
370 
"(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))" 

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

372 
by auto 

373 

374 
lemma [z3_rule]: 

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

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

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

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

44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

379 
"(if P then Q else True) = ((\<not>P) \<or> Q)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

380 
"(if P then Q else True) = (Q \<or> (\<not>P))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

381 
"(if P then Q else \<not>Q) = (P = Q)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

382 
"(if P then Q else \<not>Q) = (Q = P)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

383 
"(if P then \<not>Q else Q) = (P = (\<not>Q))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

384 
"(if P then \<not>Q else Q) = ((\<not>Q) = P)" 
36898  385 
"(if \<not>P then x else y) = (if P then y else x)" 
44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

386 
"(if P then (if Q then x else y) else x) = (if P \<and> (\<not>Q) then y else x)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

387 
"(if P then (if Q then x else y) else x) = (if (\<not>Q) \<and> P then y else x)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

388 
"(if P then (if Q then x else y) else y) = (if P \<and> Q then x else y)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

389 
"(if P then (if Q then x else y) else y) = (if Q \<and> P then x else y)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

390 
"(if P then x else if P then y else z) = (if P then x else z)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

391 
"(if P then x else if Q then x else y) = (if P \<or> Q then x else y)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

392 
"(if P then x else if Q then x else y) = (if Q \<or> P then x else y)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

393 
"(if P then x = y else x = z) = (x = (if P then y else z))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

394 
"(if P then x = y else y = z) = (y = (if P then x else z))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

395 
"(if P then x = y else z = y) = (y = (if P then x else z))" 
40806
59d96f777da3
also support higherorder rules for Z3 proof reconstruction
boehmes
parents:
40681
diff
changeset

396 
"f (if P then x else y) = (if P then f x else f y)" 
36898  397 
by auto 
398 

399 
lemma [z3_rule]: 

44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

400 
"0 + (x::int) = x" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

401 
"x + 0 = x" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

402 
"x + x = 2 * x" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

403 
"0 * x = 0" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

404 
"1 * x = x" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

405 
"x + y = y + x" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

406 
by auto 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

407 

587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

408 
lemma [z3_rule]: (* for defaxiom *) 
36898  409 
"P = Q \<or> P \<or> Q" 
410 
"P = Q \<or> \<not>P \<or> \<not>Q" 

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

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

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

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

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

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

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

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

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

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

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

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

44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

423 
"P \<or> y = (if P then x else y)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

424 
"P \<or> (if P then x else y) = y" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

425 
"\<not>P \<or> x = (if P then x else y)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

426 
"\<not>P \<or> (if P then x else y) = x" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

427 
"P \<or> R \<or> \<not>(if P then Q else R)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

428 
"\<not>P \<or> Q \<or> \<not>(if P then Q else R)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

429 
"\<not>(if P then Q else R) \<or> \<not>P \<or> Q" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

430 
"\<not>(if P then Q else R) \<or> P \<or> R" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

431 
"(if P then Q else R) \<or> \<not>P \<or> \<not>Q" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

432 
"(if P then Q else R) \<or> P \<or> \<not>R" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

433 
"(if P then \<not>Q else R) \<or> \<not>P \<or> Q" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

434 
"(if P then Q else \<not>R) \<or> P \<or> R" 
36898  435 
by auto 
436 

37124  437 

438 

439 
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

440 
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

441 
hide_const (open) trigger pat nopat weight 
37124  442 

36898  443 
end 