55 ("binary_ints", "smart"), |
55 ("binary_ints", "smart"), |
56 ("destroy_constrs", "true"), |
56 ("destroy_constrs", "true"), |
57 ("specialize", "true"), |
57 ("specialize", "true"), |
58 ("skolemize", "true"), |
58 ("skolemize", "true"), |
59 ("star_linear_preds", "true"), |
59 ("star_linear_preds", "true"), |
60 ("uncurry", "true"), |
|
61 ("fast_descrs", "true"), |
60 ("fast_descrs", "true"), |
62 ("peephole_optim", "true"), |
61 ("peephole_optim", "true"), |
63 ("timeout", "30 s"), |
62 ("timeout", "30 s"), |
64 ("tac_timeout", "500 ms"), |
63 ("tac_timeout", "500 ms"), |
65 ("max_threads", "0"), |
64 ("max_threads", "0"), |
90 ("unary_ints", "binary_ints"), |
89 ("unary_ints", "binary_ints"), |
91 ("dont_destroy_constrs", "destroy_constrs"), |
90 ("dont_destroy_constrs", "destroy_constrs"), |
92 ("dont_specialize", "specialize"), |
91 ("dont_specialize", "specialize"), |
93 ("dont_skolemize", "skolemize"), |
92 ("dont_skolemize", "skolemize"), |
94 ("dont_star_linear_preds", "star_linear_preds"), |
93 ("dont_star_linear_preds", "star_linear_preds"), |
95 ("dont_uncurry", "uncurry"), |
|
96 ("full_descrs", "fast_descrs"), |
94 ("full_descrs", "fast_descrs"), |
97 ("no_peephole_optim", "peephole_optim"), |
95 ("no_peephole_optim", "peephole_optim"), |
98 ("no_debug", "debug"), |
96 ("no_debug", "debug"), |
99 ("quiet", "verbose"), |
97 ("quiet", "verbose"), |
100 ("no_overlord", "overlord"), |
98 ("no_overlord", "overlord"), |
252 val binary_ints = lookup_bool_option "binary_ints" |
250 val binary_ints = lookup_bool_option "binary_ints" |
253 val destroy_constrs = lookup_bool "destroy_constrs" |
251 val destroy_constrs = lookup_bool "destroy_constrs" |
254 val specialize = lookup_bool "specialize" |
252 val specialize = lookup_bool "specialize" |
255 val skolemize = lookup_bool "skolemize" |
253 val skolemize = lookup_bool "skolemize" |
256 val star_linear_preds = lookup_bool "star_linear_preds" |
254 val star_linear_preds = lookup_bool "star_linear_preds" |
257 val uncurry = lookup_bool "uncurry" |
|
258 val fast_descrs = lookup_bool "fast_descrs" |
255 val fast_descrs = lookup_bool "fast_descrs" |
259 val peephole_optim = lookup_bool "peephole_optim" |
256 val peephole_optim = lookup_bool "peephole_optim" |
260 val timeout = if auto then NONE else lookup_time "timeout" |
257 val timeout = if auto then NONE else lookup_time "timeout" |
261 val tac_timeout = lookup_time "tac_timeout" |
258 val tac_timeout = lookup_time "tac_timeout" |
262 val max_threads = Int.max (0, lookup_int "max_threads") |
259 val max_threads = Int.max (0, lookup_int "max_threads") |
283 debug = debug, verbose = verbose, overlord = overlord, |
280 debug = debug, verbose = verbose, overlord = overlord, |
284 user_axioms = user_axioms, assms = assms, |
281 user_axioms = user_axioms, assms = assms, |
285 merge_type_vars = merge_type_vars, binary_ints = binary_ints, |
282 merge_type_vars = merge_type_vars, binary_ints = binary_ints, |
286 destroy_constrs = destroy_constrs, specialize = specialize, |
283 destroy_constrs = destroy_constrs, specialize = specialize, |
287 skolemize = skolemize, star_linear_preds = star_linear_preds, |
284 skolemize = skolemize, star_linear_preds = star_linear_preds, |
288 uncurry = uncurry, fast_descrs = fast_descrs, |
285 fast_descrs = fast_descrs, peephole_optim = peephole_optim, |
289 peephole_optim = peephole_optim, timeout = timeout, |
286 timeout = timeout, tac_timeout = tac_timeout, max_threads = max_threads, |
290 tac_timeout = tac_timeout, max_threads = max_threads, |
|
291 show_skolems = show_skolems, show_datatypes = show_datatypes, |
287 show_skolems = show_skolems, show_datatypes = show_datatypes, |
292 show_consts = show_consts, formats = formats, evals = evals, |
288 show_consts = show_consts, formats = formats, evals = evals, |
293 max_potential = max_potential, max_genuine = max_genuine, |
289 max_potential = max_potential, max_genuine = max_genuine, |
294 check_potential = check_potential, check_genuine = check_genuine, |
290 check_potential = check_potential, check_genuine = check_genuine, |
295 batch_size = batch_size, expect = expect} |
291 batch_size = batch_size, expect = expect} |