author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47152  446cfc760ccf 
child 47701  157e6108a342 
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 
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
45392
diff
changeset

9 
keywords "smt_status" :: diag 
36898  10 
uses 
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41121
diff
changeset

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

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

13 
"Tools/SMT/smt_config.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 

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

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

142 
use "Tools/SMT/smt_solver.ML" 

143 
use "Tools/SMT/smtlib_interface.ML" 

144 
use "Tools/SMT/z3_interface.ML" 

145 
use "Tools/SMT/z3_proof_parser.ML" 

146 
use "Tools/SMT/z3_proof_tools.ML" 

147 
use "Tools/SMT/z3_proof_literals.ML" 

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

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

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

153 
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

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

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

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

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

160 
SMT_Setup_Solvers.setup 
36898  161 
*} 
162 

163 

164 

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

165 
subsection {* Configuration *} 
36898  166 

167 
text {* 

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

168 
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

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

172 

173 

174 
subsection {* General configuration options *} 

175 

176 
text {* 

177 
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

178 
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

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

180 

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

181 
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

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

36898  185 
*} 
186 

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

189 
text {* 

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

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

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

193 
*} 

194 

195 
declare [[ smt_timeout = 20 ]] 

196 

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

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

198 
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

199 
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

200 
*} 
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 
declare [[ smt_random_seed = 1 ]] 
5c5d05963f93
added option to modify the random seed of SMT solvers
boehmes
parents:
41059
diff
changeset

203 

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

204 
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

205 
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

206 
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

207 
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

208 
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

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 

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

212 

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

214 
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

215 
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

216 
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

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

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

219 
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

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

221 
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

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

224 
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

225 
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

226 
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

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 

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

230 

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

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

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

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

236 
*} 

237 

238 
declare [[ smt_infer_triggers = false ]] 

239 

240 
text {* 

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

242 
instantiate all schematic type variables with fixed types occurring 

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

244 
construction whose cycles are limited by the following option. 

245 
*} 

246 

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

247 
declare [[ monomorph_max_rounds = 5 ]] 
41125  248 

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

249 
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

250 
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

251 
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

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

253 

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

254 
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

255 

36898  256 

257 

258 
subsection {* Certificates *} 

259 

260 
text {* 

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

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

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

264 
configuration) reuses the cached certificate instead of invoking the 

265 
solver. An empty string disables caching certificates. 

266 

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

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

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

270 
*} 

271 

272 
declare [[ smt_certificates = "" ]] 

273 

274 
text {* 

47152
446cfc760ccf
renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents:
46950
diff
changeset

275 
The option @{text smt_read_only_certificates} controls whether only 
446cfc760ccf
renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents:
46950
diff
changeset

276 
stored certificates are should be used or invocation of an SMT solver 
446cfc760ccf
renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents:
46950
diff
changeset

277 
is allowed. When set to @{text true}, no SMT solver will ever be 
36898  278 
invoked and only the existing certificates found in the configured 
279 
cache are used; when set to @{text false} and there is no cached 

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

281 
invoked. 

282 
*} 

283 

47152
446cfc760ccf
renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents:
46950
diff
changeset

284 
declare [[ smt_read_only_certificates = false ]] 
36898  285 

286 

287 

288 
subsection {* Tracing *} 

289 

290 
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

291 
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

292 
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

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 

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

296 

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

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

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

301 
*} 

302 

303 
declare [[ smt_trace = false ]] 

304 

305 
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

306 
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

307 
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

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

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

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

312 
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

313 

36898  314 

315 

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

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

318 
text {* 

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

320 
lemma groups which can turn failing Z3 proof reconstruction attempts 

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

322 
any implemented reconstruction procedure for all uncertain Z3 proof 

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

324 
the simplifier when reconstructing theoryspecific proof steps. 

325 
*} 

326 

327 
lemmas [z3_rule] = 

328 
refl eq_commute conj_commute disj_commute simp_thms nnf_simps 

329 
ring_distribs field_simps times_divide_eq_right times_divide_eq_left 

330 
if_True if_False not_not 

331 

332 
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

333 
"(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

334 
"(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

335 
"(\<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

336 
"(\<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

337 
"(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

338 
"(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

339 
"(\<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

340 
"(\<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

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

342 

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

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

346 
"(\<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

347 
"(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

348 
"(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

349 
"(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

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

353 
lemma [z3_rule]: 

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

355 
by auto 

356 

357 
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

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

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

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

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

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

363 
"(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

364 
"(False = P) = (\<not>P)" 
36898  365 
"((\<not>P) = P) = False" 
366 
"(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

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

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

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

373 
by auto 

374 

375 
lemma [z3_rule]: 

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

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

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

379 
"(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

380 
"(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

381 
"(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

382 
"(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

383 
"(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

384 
"(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

385 
"(if P then \<not>Q else Q) = ((\<not>Q) = P)" 
36898  386 
"(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

387 
"(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

388 
"(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

389 
"(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

390 
"(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

391 
"(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

392 
"(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

393 
"(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

394 
"(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

395 
"(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

396 
"(if P then x = y else z = y) = (y = (if P then x else z))" 
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 