56 ("merge_type_vars", "false"), |
56 ("merge_type_vars", "false"), |
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 ("fast_descrs", "true"), |
|
62 ("peephole_optim", "true"), |
61 ("peephole_optim", "true"), |
63 ("datatype_sym_break", "5"), |
62 ("datatype_sym_break", "5"), |
64 ("kodkod_sym_break", "15"), |
63 ("kodkod_sym_break", "15"), |
65 ("timeout", "30 s"), |
64 ("timeout", "30 s"), |
66 ("tac_timeout", "500 ms"), |
65 ("tac_timeout", "500 ms"), |
89 ("dont_merge_type_vars", "merge_type_vars"), |
88 ("dont_merge_type_vars", "merge_type_vars"), |
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_star_linear_preds", "star_linear_preds"), |
92 ("dont_star_linear_preds", "star_linear_preds"), |
94 ("full_descrs", "fast_descrs"), |
|
95 ("no_peephole_optim", "peephole_optim"), |
93 ("no_peephole_optim", "peephole_optim"), |
96 ("no_debug", "debug"), |
94 ("no_debug", "debug"), |
97 ("quiet", "verbose"), |
95 ("quiet", "verbose"), |
98 ("no_overlord", "overlord"), |
96 ("no_overlord", "overlord"), |
99 ("hide_datatypes", "show_datatypes"), |
97 ("hide_datatypes", "show_datatypes"), |
249 val merge_type_vars = lookup_bool "merge_type_vars" |
247 val merge_type_vars = lookup_bool "merge_type_vars" |
250 val binary_ints = lookup_bool_option "binary_ints" |
248 val binary_ints = lookup_bool_option "binary_ints" |
251 val destroy_constrs = lookup_bool "destroy_constrs" |
249 val destroy_constrs = lookup_bool "destroy_constrs" |
252 val specialize = lookup_bool "specialize" |
250 val specialize = lookup_bool "specialize" |
253 val star_linear_preds = lookup_bool "star_linear_preds" |
251 val star_linear_preds = lookup_bool "star_linear_preds" |
254 val fast_descrs = lookup_bool "fast_descrs" |
|
255 val peephole_optim = lookup_bool "peephole_optim" |
252 val peephole_optim = lookup_bool "peephole_optim" |
256 val datatype_sym_break = lookup_int "datatype_sym_break" |
253 val datatype_sym_break = lookup_int "datatype_sym_break" |
257 val kodkod_sym_break = lookup_int "kodkod_sym_break" |
254 val kodkod_sym_break = lookup_int "kodkod_sym_break" |
258 val timeout = if auto then NONE else lookup_time "timeout" |
255 val timeout = if auto then NONE else lookup_time "timeout" |
259 val tac_timeout = lookup_time "tac_timeout" |
256 val tac_timeout = lookup_time "tac_timeout" |
280 wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify, |
277 wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify, |
281 debug = debug, verbose = verbose, overlord = overlord, |
278 debug = debug, verbose = verbose, overlord = overlord, |
282 user_axioms = user_axioms, assms = assms, whacks = whacks, |
279 user_axioms = user_axioms, assms = assms, whacks = whacks, |
283 merge_type_vars = merge_type_vars, binary_ints = binary_ints, |
280 merge_type_vars = merge_type_vars, binary_ints = binary_ints, |
284 destroy_constrs = destroy_constrs, specialize = specialize, |
281 destroy_constrs = destroy_constrs, specialize = specialize, |
285 star_linear_preds = star_linear_preds, fast_descrs = fast_descrs, |
282 star_linear_preds = star_linear_preds, peephole_optim = peephole_optim, |
286 peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break, |
283 datatype_sym_break = datatype_sym_break, |
287 kodkod_sym_break = kodkod_sym_break, timeout = timeout, |
284 kodkod_sym_break = kodkod_sym_break, timeout = timeout, |
288 tac_timeout = tac_timeout, max_threads = max_threads, |
285 tac_timeout = tac_timeout, max_threads = max_threads, |
289 show_datatypes = show_datatypes, show_consts = show_consts, |
286 show_datatypes = show_datatypes, show_consts = show_consts, |
290 formats = formats, atomss = atomss, evals = evals, |
287 formats = formats, atomss = atomss, evals = evals, |
291 max_potential = max_potential, max_genuine = max_genuine, |
288 max_potential = max_potential, max_genuine = max_genuine, |