27 multipattern are considered conjunctively for quantifier instantiation. |
27 multipattern are considered conjunctively for quantifier instantiation. |
28 A list of multipatterns is called a trigger, and their multipatterns |
28 A list of multipatterns is called a trigger, and their multipatterns |
29 act disjunctively during quantifier instantiation. Each multipattern |
29 act disjunctively during quantifier instantiation. Each multipattern |
30 should mention at least all quantified variables of the preceding |
30 should mention at least all quantified variables of the preceding |
31 quantifier block. |
31 quantifier block. |
32 *} |
32 \<close> |
33 |
33 |
34 typedecl pattern |
34 typedecl pattern |
35 |
35 |
36 consts |
36 consts |
37 pat :: "'a \<Rightarrow> pattern" |
37 pat :: "'a \<Rightarrow> pattern" |
38 nopat :: "'a \<Rightarrow> pattern" |
38 nopat :: "'a \<Rightarrow> pattern" |
39 |
39 |
40 definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool" where "trigger _ P = P" |
40 definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool" where "trigger _ P = P" |
41 |
41 |
42 |
42 |
43 subsection {* Quantifier weights *} |
43 subsection \<open>Quantifier weights\<close> |
44 |
44 |
45 text {* |
45 text \<open> |
46 Weight annotations to quantifiers influence the priority of quantifier |
46 Weight annotations to quantifiers influence the priority of quantifier |
47 instantiations. They should be handled with care for solvers, which support |
47 instantiations. They should be handled with care for solvers, which support |
48 them, because incorrect choices of weights might render a problem unsolvable. |
48 them, because incorrect choices of weights might render a problem unsolvable. |
49 *} |
49 \<close> |
50 |
50 |
51 definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P" |
51 definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P" |
52 |
52 |
53 text {* |
53 text \<open> |
54 Weights must be non-negative. The value @{text 0} is equivalent to providing |
54 Weights must be non-negative. The value @{text 0} is equivalent to providing |
55 no weight at all. |
55 no weight at all. |
56 |
56 |
57 Weights should only be used at quantifiers and only inside triggers (if the |
57 Weights should only be used at quantifiers and only inside triggers (if the |
58 quantifier has triggers). Valid usages of weights are as follows: |
58 quantifier has triggers). Valid usages of weights are as follows: |
61 \item |
61 \item |
62 @{term "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"} |
62 @{term "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"} |
63 \item |
63 \item |
64 @{term "\<forall>x. weight 3 (P x)"} |
64 @{term "\<forall>x. weight 3 (P x)"} |
65 \end{itemize} |
65 \end{itemize} |
66 *} |
66 \<close> |
67 |
67 |
68 |
68 |
69 subsection {* Higher-order encoding *} |
69 subsection \<open>Higher-order encoding\<close> |
70 |
70 |
71 text {* |
71 text \<open> |
72 Application is made explicit for constants occurring with varying |
72 Application is made explicit for constants occurring with varying |
73 numbers of arguments. This is achieved by the introduction of the |
73 numbers of arguments. This is achieved by the introduction of the |
74 following constant. |
74 following constant. |
75 *} |
75 \<close> |
76 |
76 |
77 definition fun_app where "fun_app f = f" |
77 definition fun_app where "fun_app f = f" |
78 |
78 |
79 text {* |
79 text \<open> |
80 Some solvers support a theory of arrays which can be used to encode |
80 Some solvers support a theory of arrays which can be used to encode |
81 higher-order functions. The following set of lemmas specifies the |
81 higher-order functions. The following set of lemmas specifies the |
82 properties of such (extensional) arrays. |
82 properties of such (extensional) arrays. |
83 *} |
83 \<close> |
84 |
84 |
85 lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other |
85 lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other |
86 fun_upd_upd fun_app_def |
86 fun_upd_upd fun_app_def |
87 |
87 |
88 |
88 |
89 subsection {* First-order logic *} |
89 subsection \<open>First-order logic\<close> |
90 |
90 |
91 text {* |
91 text \<open> |
92 Some SMT solvers only accept problems in first-order logic, i.e., |
92 Some SMT solvers only accept problems in first-order logic, i.e., |
93 where formulas and terms are syntactically separated. When |
93 where formulas and terms are syntactically separated. When |
94 translating higher-order into first-order problems, all |
94 translating higher-order into first-order problems, all |
95 uninterpreted constants (those not built-in in the target solver) |
95 uninterpreted constants (those not built-in in the target solver) |
96 are treated as function symbols in the first-order sense. Their |
96 are treated as function symbols in the first-order sense. Their |
97 occurrences as head symbols in atoms (i.e., as predicate symbols) are |
97 occurrences as head symbols in atoms (i.e., as predicate symbols) are |
98 turned into terms by logically equating such atoms with @{term True}. |
98 turned into terms by logically equating such atoms with @{term True}. |
99 For technical reasons, @{term True} and @{term False} occurring inside |
99 For technical reasons, @{term True} and @{term False} occurring inside |
100 terms are replaced by the following constants. |
100 terms are replaced by the following constants. |
101 *} |
101 \<close> |
102 |
102 |
103 definition term_true where "term_true = True" |
103 definition term_true where "term_true = True" |
104 definition term_false where "term_false = False" |
104 definition term_false where "term_false = False" |
105 |
105 |
106 |
106 |
107 subsection {* Integer division and modulo for Z3 *} |
107 subsection \<open>Integer division and modulo for Z3\<close> |
108 |
108 |
109 definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where |
109 definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where |
110 "z3div k l = (if 0 \<le> l then k div l else -(k div (-l)))" |
110 "z3div k l = (if 0 \<le> l then k div l else -(k div (-l)))" |
111 |
111 |
112 definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where |
112 definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where |
113 "z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))" |
113 "z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))" |
114 |
114 |
115 |
115 |
116 subsection {* Setup *} |
116 subsection \<open>Setup\<close> |
117 |
117 |
118 ML_file "Old_SMT/old_smt_builtin.ML" |
118 ML_file "Old_SMT/old_smt_builtin.ML" |
119 ML_file "Old_SMT/old_smt_datatypes.ML" |
119 ML_file "Old_SMT/old_smt_datatypes.ML" |
120 ML_file "Old_SMT/old_smt_normalize.ML" |
120 ML_file "Old_SMT/old_smt_normalize.ML" |
121 ML_file "Old_SMT/old_smt_translate.ML" |
121 ML_file "Old_SMT/old_smt_translate.ML" |
129 named_theorems old_z3_simp "simplification rules for Z3 proof reconstruction" |
129 named_theorems old_z3_simp "simplification rules for Z3 proof reconstruction" |
130 ML_file "Old_SMT/old_z3_proof_reconstruction.ML" |
130 ML_file "Old_SMT/old_z3_proof_reconstruction.ML" |
131 ML_file "Old_SMT/old_z3_model.ML" |
131 ML_file "Old_SMT/old_z3_model.ML" |
132 ML_file "Old_SMT/old_smt_setup_solvers.ML" |
132 ML_file "Old_SMT/old_smt_setup_solvers.ML" |
133 |
133 |
134 setup {* |
134 setup \<open> |
135 Old_SMT_Config.setup #> |
135 Old_SMT_Config.setup #> |
136 Old_SMT_Normalize.setup #> |
136 Old_SMT_Normalize.setup #> |
137 Old_SMTLIB_Interface.setup #> |
137 Old_SMTLIB_Interface.setup #> |
138 Old_Z3_Interface.setup #> |
138 Old_Z3_Interface.setup #> |
139 Old_SMT_Setup_Solvers.setup |
139 Old_SMT_Setup_Solvers.setup |
140 *} |
140 \<close> |
141 |
141 |
142 method_setup old_smt = {* |
142 method_setup old_smt = \<open> |
143 Scan.optional Attrib.thms [] >> |
143 Scan.optional Attrib.thms [] >> |
144 (fn thms => fn ctxt => |
144 (fn thms => fn ctxt => |
145 METHOD (fn facts => HEADGOAL (Old_SMT_Solver.smt_tac ctxt (thms @ facts)))) |
145 METHOD (fn facts => HEADGOAL (Old_SMT_Solver.smt_tac ctxt (thms @ facts)))) |
146 *} "apply an SMT solver to the current goal" |
146 \<close> "apply an SMT solver to the current goal" |
147 |
147 |
148 |
148 |
149 subsection {* Configuration *} |
149 subsection \<open>Configuration\<close> |
150 |
150 |
151 text {* |
151 text \<open> |
152 The current configuration can be printed by the command |
152 The current configuration can be printed by the command |
153 @{text old_smt_status}, which shows the values of most options. |
153 @{text old_smt_status}, which shows the values of most options. |
154 *} |
154 \<close> |
155 |
155 |
156 |
156 |
157 |
157 |
158 subsection {* General configuration options *} |
158 subsection \<open>General configuration options\<close> |
159 |
159 |
160 text {* |
160 text \<open> |
161 The option @{text old_smt_solver} can be used to change the target SMT |
161 The option @{text old_smt_solver} can be used to change the target SMT |
162 solver. The possible values can be obtained from the @{text old_smt_status} |
162 solver. The possible values can be obtained from the @{text old_smt_status} |
163 command. |
163 command. |
164 |
164 |
165 Due to licensing restrictions, Yices and Z3 are not installed/enabled |
165 Due to licensing restrictions, Yices and Z3 are not installed/enabled |
166 by default. Z3 is free for non-commercial applications and can be enabled |
166 by default. Z3 is free for non-commercial applications and can be enabled |
167 by setting the @{text OLD_Z3_NON_COMMERCIAL} environment variable to |
167 by setting the @{text OLD_Z3_NON_COMMERCIAL} environment variable to |
168 @{text yes}. |
168 @{text yes}. |
169 *} |
169 \<close> |
170 |
170 |
171 declare [[ old_smt_solver = z3 ]] |
171 declare [[ old_smt_solver = z3 ]] |
172 |
172 |
173 text {* |
173 text \<open> |
174 Since SMT solvers are potentially non-terminating, there is a timeout |
174 Since SMT solvers are potentially non-terminating, there is a timeout |
175 (given in seconds) to restrict their runtime. A value greater than |
175 (given in seconds) to restrict their runtime. A value greater than |
176 120 (seconds) is in most cases not advisable. |
176 120 (seconds) is in most cases not advisable. |
177 *} |
177 \<close> |
178 |
178 |
179 declare [[ old_smt_timeout = 20 ]] |
179 declare [[ old_smt_timeout = 20 ]] |
180 |
180 |
181 text {* |
181 text \<open> |
182 SMT solvers apply randomized heuristics. In case a problem is not |
182 SMT solvers apply randomized heuristics. In case a problem is not |
183 solvable by an SMT solver, changing the following option might help. |
183 solvable by an SMT solver, changing the following option might help. |
184 *} |
184 \<close> |
185 |
185 |
186 declare [[ old_smt_random_seed = 1 ]] |
186 declare [[ old_smt_random_seed = 1 ]] |
187 |
187 |
188 text {* |
188 text \<open> |
189 In general, the binding to SMT solvers runs as an oracle, i.e, the SMT |
189 In general, the binding to SMT solvers runs as an oracle, i.e, the SMT |
190 solvers are fully trusted without additional checks. The following |
190 solvers are fully trusted without additional checks. The following |
191 option can cause the SMT solver to run in proof-producing mode, giving |
191 option can cause the SMT solver to run in proof-producing mode, giving |
192 a checkable certificate. This is currently only implemented for Z3. |
192 a checkable certificate. This is currently only implemented for Z3. |
193 *} |
193 \<close> |
194 |
194 |
195 declare [[ old_smt_oracle = false ]] |
195 declare [[ old_smt_oracle = false ]] |
196 |
196 |
197 text {* |
197 text \<open> |
198 Each SMT solver provides several commandline options to tweak its |
198 Each SMT solver provides several commandline options to tweak its |
199 behaviour. They can be passed to the solver by setting the following |
199 behaviour. They can be passed to the solver by setting the following |
200 options. |
200 options. |
201 *} |
201 \<close> |
202 |
202 |
203 declare [[ old_cvc3_options = "" ]] |
203 declare [[ old_cvc3_options = "" ]] |
204 declare [[ old_yices_options = "" ]] |
204 declare [[ old_yices_options = "" ]] |
205 declare [[ old_z3_options = "" ]] |
205 declare [[ old_z3_options = "" ]] |
206 |
206 |
207 text {* |
207 text \<open> |
208 Enable the following option to use built-in support for datatypes and |
208 Enable the following option to use built-in support for datatypes and |
209 records. Currently, this is only implemented for Z3 running in oracle |
209 records. Currently, this is only implemented for Z3 running in oracle |
210 mode. |
210 mode. |
211 *} |
211 \<close> |
212 |
212 |
213 declare [[ old_smt_datatypes = false ]] |
213 declare [[ old_smt_datatypes = false ]] |
214 |
214 |
215 text {* |
215 text \<open> |
216 The SMT method provides an inference mechanism to detect simple triggers |
216 The SMT method provides an inference mechanism to detect simple triggers |
217 in quantified formulas, which might increase the number of problems |
217 in quantified formulas, which might increase the number of problems |
218 solvable by SMT solvers (note: triggers guide quantifier instantiations |
218 solvable by SMT solvers (note: triggers guide quantifier instantiations |
219 in the SMT solver). To turn it on, set the following option. |
219 in the SMT solver). To turn it on, set the following option. |
220 *} |
220 \<close> |
221 |
221 |
222 declare [[ old_smt_infer_triggers = false ]] |
222 declare [[ old_smt_infer_triggers = false ]] |
223 |
223 |
224 text {* |
224 text \<open> |
225 The SMT method monomorphizes the given facts, that is, it tries to |
225 The SMT method monomorphizes the given facts, that is, it tries to |
226 instantiate all schematic type variables with fixed types occurring |
226 instantiate all schematic type variables with fixed types occurring |
227 in the problem. This is a (possibly nonterminating) fixed-point |
227 in the problem. This is a (possibly nonterminating) fixed-point |
228 construction whose cycles are limited by the following option. |
228 construction whose cycles are limited by the following option. |
229 *} |
229 \<close> |
230 |
230 |
231 declare [[ monomorph_max_rounds = 5 ]] |
231 declare [[ monomorph_max_rounds = 5 ]] |
232 |
232 |
233 text {* |
233 text \<open> |
234 In addition, the number of generated monomorphic instances is limited |
234 In addition, the number of generated monomorphic instances is limited |
235 by the following option. |
235 by the following option. |
236 *} |
236 \<close> |
237 |
237 |
238 declare [[ monomorph_max_new_instances = 500 ]] |
238 declare [[ monomorph_max_new_instances = 500 ]] |
239 |
239 |
240 |
240 |
241 |
241 |
242 subsection {* Certificates *} |
242 subsection \<open>Certificates\<close> |
243 |
243 |
244 text {* |
244 text \<open> |
245 By setting the option @{text old_smt_certificates} to the name of a file, |
245 By setting the option @{text old_smt_certificates} to the name of a file, |
246 all following applications of an SMT solver a cached in that file. |
246 all following applications of an SMT solver a cached in that file. |
247 Any further application of the same SMT solver (using the very same |
247 Any further application of the same SMT solver (using the very same |
248 configuration) re-uses the cached certificate instead of invoking the |
248 configuration) re-uses the cached certificate instead of invoking the |
249 solver. An empty string disables caching certificates. |
249 solver. An empty string disables caching certificates. |
251 The filename should be given as an explicit path. It is good |
251 The filename should be given as an explicit path. It is good |
252 practice to use the name of the current theory (with ending |
252 practice to use the name of the current theory (with ending |
253 @{text ".certs"} instead of @{text ".thy"}) as the certificates file. |
253 @{text ".certs"} instead of @{text ".thy"}) as the certificates file. |
254 Certificate files should be used at most once in a certain theory context, |
254 Certificate files should be used at most once in a certain theory context, |
255 to avoid race conditions with other concurrent accesses. |
255 to avoid race conditions with other concurrent accesses. |
256 *} |
256 \<close> |
257 |
257 |
258 declare [[ old_smt_certificates = "" ]] |
258 declare [[ old_smt_certificates = "" ]] |
259 |
259 |
260 text {* |
260 text \<open> |
261 The option @{text old_smt_read_only_certificates} controls whether only |
261 The option @{text old_smt_read_only_certificates} controls whether only |
262 stored certificates are should be used or invocation of an SMT solver |
262 stored certificates are should be used or invocation of an SMT solver |
263 is allowed. When set to @{text true}, no SMT solver will ever be |
263 is allowed. When set to @{text true}, no SMT solver will ever be |
264 invoked and only the existing certificates found in the configured |
264 invoked and only the existing certificates found in the configured |
265 cache are used; when set to @{text false} and there is no cached |
265 cache are used; when set to @{text false} and there is no cached |
266 certificate for some proposition, then the configured SMT solver is |
266 certificate for some proposition, then the configured SMT solver is |
267 invoked. |
267 invoked. |
268 *} |
268 \<close> |
269 |
269 |
270 declare [[ old_smt_read_only_certificates = false ]] |
270 declare [[ old_smt_read_only_certificates = false ]] |
271 |
271 |
272 |
272 |
273 |
273 |
274 subsection {* Tracing *} |
274 subsection \<open>Tracing\<close> |
275 |
275 |
276 text {* |
276 text \<open> |
277 The SMT method, when applied, traces important information. To |
277 The SMT method, when applied, traces important information. To |
278 make it entirely silent, set the following option to @{text false}. |
278 make it entirely silent, set the following option to @{text false}. |
279 *} |
279 \<close> |
280 |
280 |
281 declare [[ old_smt_verbose = true ]] |
281 declare [[ old_smt_verbose = true ]] |
282 |
282 |
283 text {* |
283 text \<open> |
284 For tracing the generated problem file given to the SMT solver as |
284 For tracing the generated problem file given to the SMT solver as |
285 well as the returned result of the solver, the option |
285 well as the returned result of the solver, the option |
286 @{text old_smt_trace} should be set to @{text true}. |
286 @{text old_smt_trace} should be set to @{text true}. |
287 *} |
287 \<close> |
288 |
288 |
289 declare [[ old_smt_trace = false ]] |
289 declare [[ old_smt_trace = false ]] |
290 |
290 |
291 text {* |
291 text \<open> |
292 From the set of assumptions given to the SMT solver, those assumptions |
292 From the set of assumptions given to the SMT solver, those assumptions |
293 used in the proof are traced when the following option is set to |
293 used in the proof are traced when the following option is set to |
294 @{term true}. This only works for Z3 when it runs in non-oracle mode |
294 @{term true}. This only works for Z3 when it runs in non-oracle mode |
295 (see options @{text old_smt_solver} and @{text old_smt_oracle} above). |
295 (see options @{text old_smt_solver} and @{text old_smt_oracle} above). |
296 *} |
296 \<close> |
297 |
297 |
298 declare [[ old_smt_trace_used_facts = false ]] |
298 declare [[ old_smt_trace_used_facts = false ]] |
299 |
299 |
300 |
300 |
301 |
301 |
302 subsection {* Schematic rules for Z3 proof reconstruction *} |
302 subsection \<open>Schematic rules for Z3 proof reconstruction\<close> |
303 |
303 |
304 text {* |
304 text \<open> |
305 Several prof rules of Z3 are not very well documented. There are two |
305 Several prof rules of Z3 are not very well documented. There are two |
306 lemma groups which can turn failing Z3 proof reconstruction attempts |
306 lemma groups which can turn failing Z3 proof reconstruction attempts |
307 into succeeding ones: the facts in @{text z3_rule} are tried prior to |
307 into succeeding ones: the facts in @{text z3_rule} are tried prior to |
308 any implemented reconstruction procedure for all uncertain Z3 proof |
308 any implemented reconstruction procedure for all uncertain Z3 proof |
309 rules; the facts in @{text z3_simp} are only fed to invocations of |
309 rules; the facts in @{text z3_simp} are only fed to invocations of |
310 the simplifier when reconstructing theory-specific proof steps. |
310 the simplifier when reconstructing theory-specific proof steps. |
311 *} |
311 \<close> |
312 |
312 |
313 lemmas [old_z3_rule] = |
313 lemmas [old_z3_rule] = |
314 refl eq_commute conj_commute disj_commute simp_thms nnf_simps |
314 refl eq_commute conj_commute disj_commute simp_thms nnf_simps |
315 ring_distribs field_simps times_divide_eq_right times_divide_eq_left |
315 ring_distribs field_simps times_divide_eq_right times_divide_eq_left |
316 if_True if_False not_not |
316 if_True if_False not_not |