33 binary_ints: bool option, |
33 binary_ints: bool option, |
34 destroy_constrs: bool, |
34 destroy_constrs: bool, |
35 specialize: bool, |
35 specialize: bool, |
36 star_linear_preds: bool, |
36 star_linear_preds: bool, |
37 total_consts: bool option, |
37 total_consts: bool option, |
38 needs: (term option * bool option) list, |
38 needs: term list option, |
39 peephole_optim: bool, |
39 peephole_optim: bool, |
40 datatype_sym_break: int, |
40 datatype_sym_break: int, |
41 kodkod_sym_break: int, |
41 kodkod_sym_break: int, |
42 timeout: Time.time option, |
42 timeout: Time.time option, |
43 tac_timeout: Time.time option, |
43 tac_timeout: Time.time option, |
108 binary_ints: bool option, |
108 binary_ints: bool option, |
109 destroy_constrs: bool, |
109 destroy_constrs: bool, |
110 specialize: bool, |
110 specialize: bool, |
111 star_linear_preds: bool, |
111 star_linear_preds: bool, |
112 total_consts: bool option, |
112 total_consts: bool option, |
113 needs: (term option * bool option) list, |
113 needs: term list option, |
114 peephole_optim: bool, |
114 peephole_optim: bool, |
115 datatype_sym_break: int, |
115 datatype_sym_break: int, |
116 kodkod_sym_break: int, |
116 kodkod_sym_break: int, |
117 timeout: Time.time option, |
117 timeout: Time.time option, |
118 tac_timeout: Time.time option, |
118 tac_timeout: Time.time option, |
256 "goal")) [Logic.list_implies (assm_ts, orig_t)])) |
256 "goal")) [Logic.list_implies (assm_ts, orig_t)])) |
257 val _ = print_v (enclose "Timestamp: " "." o Date.fmt "%H:%M:%S" |
257 val _ = print_v (enclose "Timestamp: " "." o Date.fmt "%H:%M:%S" |
258 o Date.fromTimeLocal o Time.now) |
258 o Date.fromTimeLocal o Time.now) |
259 val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False}) |
259 val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False}) |
260 else orig_t |
260 else orig_t |
261 val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst needs |
261 val conj_ts = neg_t :: assm_ts @ evals @ these needs |
262 val tfree_table = |
262 val tfree_table = |
263 if merge_type_vars then merged_type_var_table_for_terms thy conj_ts |
263 if merge_type_vars then merged_type_var_table_for_terms thy conj_ts |
264 else [] |
264 else [] |
265 val merge_tfrees = merge_type_vars_in_term thy merge_type_vars tfree_table |
265 val merge_tfrees = merge_type_vars_in_term thy merge_type_vars tfree_table |
266 val neg_t = neg_t |> merge_tfrees |
266 val neg_t = neg_t |> merge_tfrees |
267 val assm_ts = assm_ts |> map merge_tfrees |
267 val assm_ts = assm_ts |> map merge_tfrees |
268 val evals = evals |> map merge_tfrees |
268 val evals = evals |> map merge_tfrees |
269 val needs = needs |> map (apfst (Option.map merge_tfrees)) |
269 val needs = needs |> Option.map (map merge_tfrees) |
270 val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst needs |
270 val conj_ts = neg_t :: assm_ts @ evals @ these needs |
271 val original_max_potential = max_potential |
271 val original_max_potential = max_potential |
272 val original_max_genuine = max_genuine |
272 val original_max_genuine = max_genuine |
273 val max_bisim_depth = fold Integer.max bisim_depths ~1 |
273 val max_bisim_depth = fold Integer.max bisim_depths ~1 |
274 val case_names = case_const_names ctxt stds |
274 val case_names = case_const_names ctxt stds |
275 val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst |
275 val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst |