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, |
44 max_threads: int, |
44 max_threads: int, |
45 show_datatypes: bool, |
45 show_datatypes: bool, |
|
46 show_skolems: bool, |
46 show_consts: bool, |
47 show_consts: bool, |
47 evals: term list, |
48 evals: term list, |
48 formats: (term option * int list) list, |
49 formats: (term option * int list) list, |
49 atomss: (typ option * string list) list, |
50 atomss: (typ option * string list) list, |
50 max_potential: int, |
51 max_potential: int, |
116 kodkod_sym_break: int, |
117 kodkod_sym_break: int, |
117 timeout: Time.time option, |
118 timeout: Time.time option, |
118 tac_timeout: Time.time option, |
119 tac_timeout: Time.time option, |
119 max_threads: int, |
120 max_threads: int, |
120 show_datatypes: bool, |
121 show_datatypes: bool, |
|
122 show_skolems: bool, |
121 show_consts: bool, |
123 show_consts: bool, |
122 evals: term list, |
124 evals: term list, |
123 formats: (term option * int list) list, |
125 formats: (term option * int list) list, |
124 atomss: (typ option * string list) list, |
126 atomss: (typ option * string list) list, |
125 max_potential: int, |
127 max_potential: int, |
213 boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug, |
215 boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug, |
214 verbose, overlord, user_axioms, assms, whacks, merge_type_vars, |
216 verbose, overlord, user_axioms, assms, whacks, merge_type_vars, |
215 binary_ints, destroy_constrs, specialize, star_linear_preds, |
217 binary_ints, destroy_constrs, specialize, star_linear_preds, |
216 total_consts, needs, peephole_optim, datatype_sym_break, |
218 total_consts, needs, peephole_optim, datatype_sym_break, |
217 kodkod_sym_break, tac_timeout, max_threads, show_datatypes, |
219 kodkod_sym_break, tac_timeout, max_threads, show_datatypes, |
218 show_consts, evals, formats, atomss, max_potential, max_genuine, |
220 show_skolems, show_consts, evals, formats, atomss, max_potential, |
219 check_potential, check_genuine, batch_size, ...} = params |
221 max_genuine, check_potential, check_genuine, batch_size, ...} = params |
220 val state_ref = Unsynchronized.ref state |
222 val state_ref = Unsynchronized.ref state |
221 val pprint = |
223 val pprint = |
222 if auto then |
224 if auto then |
223 Unsynchronized.change state_ref o Proof.goal_message o K |
225 Unsynchronized.change state_ref o Proof.goal_message o K |
224 o Pretty.chunks o cons (Pretty.str "") o single |
226 o Pretty.chunks o cons (Pretty.str "") o single |
636 fun print_and_check_model genuine bounds |
638 fun print_and_check_model genuine bounds |
637 ({free_names, sel_names, nonsel_names, rel_table, scope, ...} |
639 ({free_names, sel_names, nonsel_names, rel_table, scope, ...} |
638 : problem_extension) = |
640 : problem_extension) = |
639 let |
641 let |
640 val (reconstructed_model, codatatypes_ok) = |
642 val (reconstructed_model, codatatypes_ok) = |
641 reconstruct_hol_model {show_datatypes = show_datatypes, |
643 reconstruct_hol_model |
642 show_consts = show_consts} |
644 {show_datatypes = show_datatypes, show_skolems = show_skolems, |
|
645 show_consts = show_consts} |
643 scope formats atomss real_frees pseudo_frees free_names sel_names |
646 scope formats atomss real_frees pseudo_frees free_names sel_names |
644 nonsel_names rel_table bounds |
647 nonsel_names rel_table bounds |
645 val genuine_means_genuine = |
648 val genuine_means_genuine = |
646 got_all_user_axioms andalso none_true wfs andalso |
649 got_all_user_axioms andalso none_true wfs andalso |
647 sound_finitizes andalso total_consts <> SOME true andalso |
650 sound_finitizes andalso total_consts <> SOME true andalso |