author  boehmes 
Mon, 22 Nov 2010 15:45:42 +0100  
changeset 40662  798aad2229c0 
parent 40424  7550b2cba1cb 
child 40664  e023788a91a1 
permissions  rwrr 
36898  1 
(* Title: HOL/SMT.thy 
2 
Author: Sascha Boehme, TU Muenchen 

3 
*) 

4 

5 
header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *} 

6 

7 
theory SMT 

8 
imports List 

9 
uses 

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

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

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

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

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

14 
"Tools/SMT/smt_monomorph.ML" 
40277  15 
("Tools/SMT/smt_builtin.ML") 
36898  16 
("Tools/SMT/smt_normalize.ML") 
17 
("Tools/SMT/smt_translate.ML") 

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

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

20 
("Tools/SMT/z3_proof_parser.ML") 

21 
("Tools/SMT/z3_proof_tools.ML") 

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

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

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

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

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

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

30 

31 

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

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

34 
text {* 

35 
Some SMT solvers support triggers for quantifier instantiation. 

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

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

39 

40 
When an SMT solver finds a term matching a positive pattern (a 

41 
pattern with positive subterms only), it instantiates the 

42 
corresponding quantifier accordingly. Negative patterns inhibit 

43 
quantifier instantiations. Each pattern should mention all preceding 

44 
bound variables. 

36898  45 
*} 
46 

47 
datatype pattern = Pattern 

48 

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

36898  51 

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

55 

56 

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

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

58 

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

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

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

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

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

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

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

65 

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

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

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

68 

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

69 

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

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 

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

79 
definition fun_app where "fun_app f x = f x" 
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 {* 

95 
Some SMT solvers require a strict separation between formulas and 

96 
terms. When translating higherorder into firstorder problems, 

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

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

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

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

101 
following termlevel equation symbol. 

102 
*} 

103 

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

106 

107 

37151  108 
subsection {* Integer division and modulo for Z3 *} 
109 

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

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

112 

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

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

115 

116 
lemma div_by_z3div: "k div l = ( 

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

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

119 
else z3div (k) (l))" 

120 
by (auto simp add: z3div_def) 

121 

122 
lemma mod_by_z3mod: "k mod l = ( 

123 
if l = 0 then k 

124 
else if k = 0 then 0 

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

126 
else  z3mod (k) (l))" 

127 
by (auto simp add: z3mod_def) 

128 

129 

130 

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

131 
subsection {* Setup *} 
36898  132 

40277  133 
use "Tools/SMT/smt_builtin.ML" 
36898  134 
use "Tools/SMT/smt_normalize.ML" 
135 
use "Tools/SMT/smt_translate.ML" 

136 
use "Tools/SMT/smt_solver.ML" 

137 
use "Tools/SMT/smtlib_interface.ML" 

138 
use "Tools/SMT/z3_interface.ML" 

139 
use "Tools/SMT/z3_proof_parser.ML" 

140 
use "Tools/SMT/z3_proof_tools.ML" 

141 
use "Tools/SMT/z3_proof_literals.ML" 

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

142 
use "Tools/SMT/z3_proof_methods.ML" 
36898  143 
use "Tools/SMT/z3_proof_reconstruction.ML" 
144 
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

145 
use "Tools/SMT/smt_setup_solvers.ML" 
36898  146 

147 
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

148 
SMT_Config.setup #> 
36898  149 
SMT_Solver.setup #> 
150 
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

151 
SMT_Setup_Solvers.setup 
36898  152 
*} 
153 

154 

155 

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

156 
subsection {* Configuration *} 
36898  157 

158 
text {* 

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

159 
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

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

163 

164 

165 
subsection {* General configuration options *} 

166 

167 
text {* 

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

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

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

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

172 
can also be used over an Internetbased service. 

173 

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

175 
declared by setting the following environment variables: 

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

177 
*} 

178 

179 
declare [[ smt_solver = z3 ]] 

180 

181 
text {* 

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

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

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

185 
*} 

186 

187 
declare [[ smt_timeout = 20 ]] 

188 

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

189 
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

190 
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

191 
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

192 
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

193 
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

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

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

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

199 
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

200 
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

201 
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

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

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

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

207 
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

208 
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

209 
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

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

211 

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

212 
declare [[ smt_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

213 

36898  214 

215 

216 
subsection {* Certificates *} 

217 

218 
text {* 

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

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

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

222 
configuration) reuses the cached certificate instead of invoking the 

223 
solver. An empty string disables caching certificates. 

224 

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

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

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

228 
*} 

229 

230 
declare [[ smt_certificates = "" ]] 

231 

232 
text {* 

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

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

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

236 
invoked and only the existing certificates found in the configured 

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

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

239 
invoked. 

240 
*} 

241 

242 
declare [[ smt_fixed = false ]] 

243 

244 

245 

246 
subsection {* Tracing *} 

247 

248 
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

249 
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

250 
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

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

252 

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

253 
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

254 

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

255 
text {* 
36898  256 
For tracing the generated problem file given to the SMT solver as 
257 
well as the returned result of the solver, the option 

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

259 
*} 

260 

261 
declare [[ smt_trace = false ]] 

262 

263 
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

264 
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

265 
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

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

267 
(see options @{text smt_solver} and @{text smt_oracle} above). 
36898  268 
*} 
269 

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

270 
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

271 

36898  272 

273 

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

274 
subsection {* Schematic rules for Z3 proof reconstruction *} 
36898  275 

276 
text {* 

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

278 
lemma groups which can turn failing Z3 proof reconstruction attempts 

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

280 
any implemented reconstruction procedure for all uncertain Z3 proof 

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

282 
the simplifier when reconstructing theoryspecific proof steps. 

283 
*} 

284 

285 
lemmas [z3_rule] = 

286 
refl eq_commute conj_commute disj_commute simp_thms nnf_simps 

287 
ring_distribs field_simps times_divide_eq_right times_divide_eq_left 

288 
if_True if_False not_not 

289 

290 
lemma [z3_rule]: 

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

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

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

294 
by auto 

295 

296 
lemma [z3_rule]: 

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

298 
by auto 

299 

300 
lemma [z3_rule]: 

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

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

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

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

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

306 
by auto 

307 

308 
lemma [z3_rule]: 

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

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

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

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

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

314 
by auto 

315 

316 
lemma [z3_rule]: 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

331 
by auto 

332 

333 
lemma [z3_rule]: 

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

335 
"x + 0 = x" 

336 
"0 * x = 0" 

337 
"1 * x = x" 

338 
"x + y = y + x" 

339 
by auto 

340 

37124  341 

342 

343 
hide_type (open) pattern 

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

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

345 
hide_const (open) trigger pat nopat distinct fun_app z3div z3mod 
37124  346 

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

347 

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

348 

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

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

350 

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

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

352 

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

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

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

355 

36898  356 
end 