author  wenzelm 
Mon, 13 Jan 2014 20:20:44 +0100  
changeset 55007  0c07990363a3 
parent 50317  4d1590544b91 
child 55049  327eafb594ba 
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 
begin 
11 

48892  12 
ML_file "Tools/SMT/smt_utils.ML" 
13 
ML_file "Tools/SMT/smt_failure.ML" 

14 
ML_file "Tools/SMT/smt_config.ML" 

36898  15 

16 

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

17 
subsection {* Triggers for quantifier instantiation *} 
36898  18 

19 
text {* 

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

22 
triggering quantifier instantiations  when the solver finds a 

23 
term matching a positive pattern, it instantiates the corresponding 

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

25 
inhibiting quantifier instantiations. A list of patterns 

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

27 
multipattern are considered conjunctively for quantifier instantiation. 

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

29 
act disjunctively during quantifier instantiation. Each multipattern 

30 
should mention at least all quantified variables of the preceding 

31 
quantifier block. 

36898  32 
*} 
33 

34 
datatype pattern = Pattern 

35 

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

36898  38 

37124  39 
definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool" 
36898  40 
where "trigger _ P = P" 
41 

42 

43 

40664  44 
subsection {* Quantifier weights *} 
45 

46 
text {* 

47 
Weight annotations to quantifiers influence the priority of quantifier 

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

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

50 
*} 

51 

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

53 

54 
text {* 

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

56 
no weight at all. 

57 

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

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

60 

61 
\begin{itemize} 

62 
\item 

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

64 
\item 

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

66 
\end{itemize} 

67 
*} 

68 

69 

70 

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

71 
subsection {* Higherorder encoding *} 
36898  72 

73 
text {* 

74 
Application is made explicit for constants occurring with varying 

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

76 
following constant. 

77 
*} 

78 

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

79 
definition fun_app where "fun_app f = f" 
36898  80 

81 
text {* 

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

83 
higherorder functions. The following set of lemmas specifies the 

84 
properties of such (extensional) arrays. 

85 
*} 

86 

87 
lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other 

37157  88 
fun_upd_upd fun_app_def 
36898  89 

90 

91 

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

92 
subsection {* Firstorder logic *} 
36898  93 

94 
text {* 

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

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

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

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

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

100 
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

101 
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

102 
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

103 
terms are replaced by the following constants. 
36898  104 
*} 
105 

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

106 
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

107 
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

108 

36898  109 

110 

37151  111 
subsection {* Integer division and modulo for Z3 *} 
112 

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

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

115 

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

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

118 

119 

120 

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

121 
subsection {* Setup *} 
36898  122 

48892  123 
ML_file "Tools/SMT/smt_builtin.ML" 
124 
ML_file "Tools/SMT/smt_datatypes.ML" 

125 
ML_file "Tools/SMT/smt_normalize.ML" 

126 
ML_file "Tools/SMT/smt_translate.ML" 

127 
ML_file "Tools/SMT/smt_solver.ML" 

128 
ML_file "Tools/SMT/smtlib_interface.ML" 

129 
ML_file "Tools/SMT/z3_interface.ML" 

130 
ML_file "Tools/SMT/z3_proof_parser.ML" 

131 
ML_file "Tools/SMT/z3_proof_tools.ML" 

132 
ML_file "Tools/SMT/z3_proof_literals.ML" 

133 
ML_file "Tools/SMT/z3_proof_methods.ML" 

134 
ML_file "Tools/SMT/z3_proof_reconstruction.ML" 

135 
ML_file "Tools/SMT/z3_model.ML" 

136 
ML_file "Tools/SMT/smt_setup_solvers.ML" 

36898  137 

138 
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

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

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

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

142 
Z3_Interface.setup #> 
36898  143 
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

144 
SMT_Setup_Solvers.setup 
36898  145 
*} 
146 

47701  147 
method_setup smt = {* 
148 
Scan.optional Attrib.thms [] >> 

149 
(fn thms => fn ctxt => 

150 
METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts)))) 

151 
*} "apply an SMT solver to the current goal" 

36898  152 

153 

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

154 
subsection {* Configuration *} 
36898  155 

156 
text {* 

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

157 
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

158 
@{text smt_status}, which shows the values of most options. 
36898  159 
*} 
160 

161 

162 

163 
subsection {* General configuration options *} 

164 

165 
text {* 

166 
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

167 
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

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

169 

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

170 
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

171 
by default. Z3 is free for noncommercial applications and can be enabled 
55007
0c07990363a3
activation of Z3 via "z3_non_commercial" system option (without requiring restart);
wenzelm
parents:
50317
diff
changeset

172 
by setting Isabelle system option @{text z3_non_commercial} to @{text yes}. 
36898  173 
*} 
174 

41601  175 
declare [[ smt_solver = z3 ]] 
36898  176 

177 
text {* 

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

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

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

181 
*} 

182 

183 
declare [[ smt_timeout = 20 ]] 

184 

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

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

186 
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

187 
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

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

189 

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

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

191 

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

192 
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

193 
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

194 
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

195 
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

196 
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

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

198 

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

199 
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

200 

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

201 
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

202 
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

203 
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

204 
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

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

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

207 
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

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

209 
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

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

212 
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

213 
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

214 
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

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

218 

41125  219 
text {* 
220 
The SMT method provides an inference mechanism to detect simple triggers 

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

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

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

224 
*} 

225 

226 
declare [[ smt_infer_triggers = false ]] 

227 

228 
text {* 

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

230 
instantiate all schematic type variables with fixed types occurring 

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

232 
construction whose cycles are limited by the following option. 

233 
*} 

234 

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

235 
declare [[ monomorph_max_rounds = 5 ]] 
41125  236 

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

237 
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

238 
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

239 
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

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

241 

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

242 
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

243 

36898  244 

245 

246 
subsection {* Certificates *} 

247 

248 
text {* 

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

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

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

252 
configuration) reuses the cached certificate instead of invoking the 

253 
solver. An empty string disables caching certificates. 

254 

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

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

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

50317
4d1590544b91
synchronized read access to cache file  avoid potential conflict with ongoing write (which is nonatomic);
wenzelm
parents:
48892
diff
changeset

258 
Certificate files should be used at most once in a certain theory context, 
4d1590544b91
synchronized read access to cache file  avoid potential conflict with ongoing write (which is nonatomic);
wenzelm
parents:
48892
diff
changeset

259 
to avoid race conditions with other concurrent accesses. 
36898  260 
*} 
261 

262 
declare [[ smt_certificates = "" ]] 

263 

264 
text {* 

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

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

266 
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

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

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

271 
invoked. 

272 
*} 

273 

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

274 
declare [[ smt_read_only_certificates = false ]] 
36898  275 

276 

277 

278 
subsection {* Tracing *} 

279 

280 
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

281 
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

282 
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

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

284 

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

285 
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

286 

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

287 
text {* 
36898  288 
For tracing the generated problem file given to the SMT solver as 
289 
well as the returned result of the solver, the option 

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

291 
*} 

292 

293 
declare [[ smt_trace = false ]] 

294 

295 
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

296 
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

297 
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

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

299 
(see options @{text smt_solver} and @{text smt_oracle} above). 
36898  300 
*} 
301 

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

302 
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

303 

36898  304 

305 

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

306 
subsection {* Schematic rules for Z3 proof reconstruction *} 
36898  307 

308 
text {* 

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

310 
lemma groups which can turn failing Z3 proof reconstruction attempts 

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

312 
any implemented reconstruction procedure for all uncertain Z3 proof 

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

314 
the simplifier when reconstructing theoryspecific proof steps. 

315 
*} 

316 

317 
lemmas [z3_rule] = 

318 
refl eq_commute conj_commute disj_commute simp_thms nnf_simps 

319 
ring_distribs field_simps times_divide_eq_right times_divide_eq_left 

320 
if_True if_False not_not 

321 

322 
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

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

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

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

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

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

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

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

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

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

332 

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

333 
lemma [z3_rule]: 
36898  334 
"(P \<longrightarrow> Q) = (Q \<or> \<not>P)" 
335 
"(\<not>P \<longrightarrow> Q) = (P \<or> Q)" 

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

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

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

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

340 
"(P \<longrightarrow> P) = True" 
36898  341 
by auto 
342 

343 
lemma [z3_rule]: 

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

345 
by auto 

346 

347 
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

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

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

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

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

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

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

354 
"(False = P) = (\<not>P)" 
36898  355 
"((\<not>P) = P) = False" 
356 
"(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

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

358 
"\<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

359 
"\<not>((\<not>P) = Q) = (P = Q)" 
36898  360 
"(P \<noteq> Q) = (Q = (\<not>P))" 
361 
"(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))" 

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

363 
by auto 

364 

365 
lemma [z3_rule]: 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

386 
"(if P then x = y else z = y) = (y = (if P then x else z))" 
36898  387 
by auto 
388 

389 
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

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

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

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

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

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

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

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

397 

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

398 
lemma [z3_rule]: (* for defaxiom *) 
36898  399 
"P = Q \<or> P \<or> Q" 
400 
"P = Q \<or> \<not>P \<or> \<not>Q" 

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

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

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

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

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

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

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

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

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

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

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

412 
"\<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

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

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

415 
"\<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

416 
"\<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

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

418 
"\<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

419 
"\<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

420 
"\<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

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

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

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

424 
"(if P then Q else \<not>R) \<or> P \<or> R" 
36898  425 
by auto 
426 

37124  427 

428 

429 
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

430 
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

431 
hide_const (open) trigger pat nopat weight 
37124  432 

36898  433 
end 