57 ("binary_ints", "smart"), |
57 ("binary_ints", "smart"), |
58 ("destroy_constrs", "true"), |
58 ("destroy_constrs", "true"), |
59 ("specialize", "true"), |
59 ("specialize", "true"), |
60 ("star_linear_preds", "true"), |
60 ("star_linear_preds", "true"), |
61 ("total_consts", "smart"), |
61 ("total_consts", "smart"), |
62 ("preconstr", "smart"), |
62 ("need", "smart"), |
63 ("peephole_optim", "true"), |
63 ("peephole_optim", "true"), |
64 ("datatype_sym_break", "5"), |
64 ("datatype_sym_break", "5"), |
65 ("kodkod_sym_break", "15"), |
65 ("kodkod_sym_break", "15"), |
66 ("timeout", "30"), |
66 ("timeout", "30"), |
67 ("tac_timeout", "0.5"), |
67 ("tac_timeout", "0.5"), |
91 ("unary_ints", "binary_ints"), |
91 ("unary_ints", "binary_ints"), |
92 ("dont_destroy_constrs", "destroy_constrs"), |
92 ("dont_destroy_constrs", "destroy_constrs"), |
93 ("dont_specialize", "specialize"), |
93 ("dont_specialize", "specialize"), |
94 ("dont_star_linear_preds", "star_linear_preds"), |
94 ("dont_star_linear_preds", "star_linear_preds"), |
95 ("partial_consts", "total_consts"), |
95 ("partial_consts", "total_consts"), |
96 ("dont_preconstr", "preconstr"), |
96 ("dont_need", "need"), |
97 ("no_peephole_optim", "peephole_optim"), |
97 ("no_peephole_optim", "peephole_optim"), |
98 ("no_debug", "debug"), |
98 ("no_debug", "debug"), |
99 ("quiet", "verbose"), |
99 ("quiet", "verbose"), |
100 ("no_overlord", "overlord"), |
100 ("no_overlord", "overlord"), |
101 ("hide_datatypes", "show_datatypes"), |
101 ("hide_datatypes", "show_datatypes"), |
107 AList.defined (op =) default_default_params s orelse |
107 AList.defined (op =) default_default_params s orelse |
108 AList.defined (op =) negated_params s orelse |
108 AList.defined (op =) negated_params s orelse |
109 member (op =) ["max", "show_all", "whack", "eval", "atoms", "expect"] s orelse |
109 member (op =) ["max", "show_all", "whack", "eval", "atoms", "expect"] s orelse |
110 exists (fn p => String.isPrefix (p ^ " ") s) |
110 exists (fn p => String.isPrefix (p ^ " ") s) |
111 ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize", |
111 ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize", |
112 "mono", "non_mono", "std", "non_std", "wf", "non_wf", "preconstr", |
112 "mono", "non_mono", "std", "non_std", "wf", "non_wf", "need", |
113 "dont_preconstr", "format", "atoms"] |
113 "dont_need", "format", "atoms"] |
114 |
114 |
115 fun check_raw_param (s, _) = |
115 fun check_raw_param (s, _) = |
116 if is_known_raw_param s then () |
116 if is_known_raw_param s then () |
117 else error ("Unknown parameter: " ^ quote s ^ ".") |
117 else error ("Unknown parameter: " ^ quote s ^ ".") |
118 |
118 |
254 val binary_ints = lookup_bool_option "binary_ints" |
254 val binary_ints = lookup_bool_option "binary_ints" |
255 val destroy_constrs = lookup_bool "destroy_constrs" |
255 val destroy_constrs = lookup_bool "destroy_constrs" |
256 val specialize = lookup_bool "specialize" |
256 val specialize = lookup_bool "specialize" |
257 val star_linear_preds = lookup_bool "star_linear_preds" |
257 val star_linear_preds = lookup_bool "star_linear_preds" |
258 val total_consts = lookup_bool_option "total_consts" |
258 val total_consts = lookup_bool_option "total_consts" |
259 val preconstrs = |
259 val needs = lookup_bool_option_assigns read_term_polymorphic "need" |
260 lookup_bool_option_assigns read_term_polymorphic "preconstr" |
|
261 val peephole_optim = lookup_bool "peephole_optim" |
260 val peephole_optim = lookup_bool "peephole_optim" |
262 val datatype_sym_break = lookup_int "datatype_sym_break" |
261 val datatype_sym_break = lookup_int "datatype_sym_break" |
263 val kodkod_sym_break = lookup_int "kodkod_sym_break" |
262 val kodkod_sym_break = lookup_int "kodkod_sym_break" |
264 val timeout = if auto then NONE else lookup_time "timeout" |
263 val timeout = if auto then NONE else lookup_time "timeout" |
265 val tac_timeout = lookup_time "tac_timeout" |
264 val tac_timeout = lookup_time "tac_timeout" |
287 debug = debug, verbose = verbose, overlord = overlord, |
286 debug = debug, verbose = verbose, overlord = overlord, |
288 user_axioms = user_axioms, assms = assms, whacks = whacks, |
287 user_axioms = user_axioms, assms = assms, whacks = whacks, |
289 merge_type_vars = merge_type_vars, binary_ints = binary_ints, |
288 merge_type_vars = merge_type_vars, binary_ints = binary_ints, |
290 destroy_constrs = destroy_constrs, specialize = specialize, |
289 destroy_constrs = destroy_constrs, specialize = specialize, |
291 star_linear_preds = star_linear_preds, total_consts = total_consts, |
290 star_linear_preds = star_linear_preds, total_consts = total_consts, |
292 preconstrs = preconstrs, peephole_optim = peephole_optim, |
291 needs = needs, peephole_optim = peephole_optim, |
293 datatype_sym_break = datatype_sym_break, |
292 datatype_sym_break = datatype_sym_break, |
294 kodkod_sym_break = kodkod_sym_break, timeout = timeout, |
293 kodkod_sym_break = kodkod_sym_break, timeout = timeout, |
295 tac_timeout = tac_timeout, max_threads = max_threads, |
294 tac_timeout = tac_timeout, max_threads = max_threads, |
296 show_datatypes = show_datatypes, show_consts = show_consts, |
295 show_datatypes = show_datatypes, show_consts = show_consts, |
297 evals = evals, formats = formats, atomss = atomss, |
296 evals = evals, formats = formats, atomss = atomss, |