37 [("card", ["1\<midarrow>8"]), |
37 [("card", ["1\<midarrow>8"]), |
38 ("iter", ["0,1,2,4,8,12,16,24"]), |
38 ("iter", ["0,1,2,4,8,12,16,24"]), |
39 ("bits", ["1,2,3,4,6,8,10,12"]), |
39 ("bits", ["1,2,3,4,6,8,10,12"]), |
40 ("bisim_depth", ["7"]), |
40 ("bisim_depth", ["7"]), |
41 ("box", ["smart"]), |
41 ("box", ["smart"]), |
|
42 ("finitize", ["smart"]), |
42 ("mono", ["smart"]), |
43 ("mono", ["smart"]), |
43 ("std", ["true"]), |
44 ("std", ["true"]), |
44 ("wf", ["smart"]), |
45 ("wf", ["smart"]), |
45 ("sat_solver", ["smart"]), |
46 ("sat_solver", ["smart"]), |
46 ("batch_size", ["smart"]), |
47 ("batch_size", ["smart"]), |
76 ("check_potential", ["false"]), |
77 ("check_potential", ["false"]), |
77 ("check_genuine", ["false"])] |
78 ("check_genuine", ["false"])] |
78 |
79 |
79 val negated_params = |
80 val negated_params = |
80 [("dont_box", "box"), |
81 [("dont_box", "box"), |
|
82 ("dont_finitize", "finitize"), |
81 ("non_mono", "mono"), |
83 ("non_mono", "mono"), |
82 ("non_std", "std"), |
84 ("non_std", "std"), |
83 ("non_wf", "wf"), |
85 ("non_wf", "wf"), |
84 ("non_blocking", "blocking"), |
86 ("non_blocking", "blocking"), |
85 ("satisfy", "falsify"), |
87 ("satisfy", "falsify"), |
109 fun is_known_raw_param s = |
111 fun is_known_raw_param s = |
110 AList.defined (op =) default_default_params s orelse |
112 AList.defined (op =) default_default_params s orelse |
111 AList.defined (op =) negated_params s orelse |
113 AList.defined (op =) negated_params s orelse |
112 s = "max" orelse s = "eval" orelse s = "expect" orelse |
114 s = "max" orelse s = "eval" orelse s = "expect" orelse |
113 exists (fn p => String.isPrefix (p ^ " ") s) |
115 exists (fn p => String.isPrefix (p ^ " ") s) |
114 ["card", "max", "iter", "box", "dont_box", "mono", "non_mono", "std", |
116 ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize", |
115 "non_std", "wf", "non_wf", "format"] |
117 "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format"] |
116 |
118 |
117 (* string * 'a -> unit *) |
119 (* string * 'a -> unit *) |
118 fun check_raw_param (s, _) = |
120 fun check_raw_param (s, _) = |
119 if is_known_raw_param s then () |
121 if is_known_raw_param s then () |
120 else error ("Unknown parameter " ^ quote s ^ ".") |
122 else error ("Unknown parameter " ^ quote s ^ ".") |
295 val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1 |
297 val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1 |
296 val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1 |
298 val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1 |
297 val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0 |
299 val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0 |
298 val bitss = lookup_int_seq "bits" 1 |
300 val bitss = lookup_int_seq "bits" 1 |
299 val bisim_depths = lookup_int_seq "bisim_depth" ~1 |
301 val bisim_depths = lookup_int_seq "bisim_depth" ~1 |
300 val boxes = |
302 val boxes = lookup_bool_option_assigns read_type_polymorphic "box" |
301 lookup_bool_option_assigns read_type_polymorphic "box" @ |
303 val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize" |
302 map_filter (fn (SOME T, _) => |
|
303 if is_fun_type T orelse is_pair_type T then |
|
304 SOME (SOME T, SOME true) |
|
305 else |
|
306 NONE |
|
307 | (NONE, _) => NONE) cards_assigns |
|
308 val monos = lookup_bool_option_assigns read_type_polymorphic "mono" |
304 val monos = lookup_bool_option_assigns read_type_polymorphic "mono" |
309 val stds = lookup_bool_assigns read_type_polymorphic "std" |
305 val stds = lookup_bool_assigns read_type_polymorphic "std" |
310 val wfs = lookup_bool_option_assigns read_const_polymorphic "wf" |
306 val wfs = lookup_bool_option_assigns read_const_polymorphic "wf" |
311 val sat_solver = lookup_string "sat_solver" |
307 val sat_solver = lookup_string "sat_solver" |
312 val blocking = not auto andalso lookup_bool "blocking" |
308 val blocking = not auto andalso lookup_bool "blocking" |
347 | NONE => if debug then 1 else 64 |
343 | NONE => if debug then 1 else 64 |
348 val expect = lookup_string "expect" |
344 val expect = lookup_string "expect" |
349 in |
345 in |
350 {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns, |
346 {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns, |
351 iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths, |
347 iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths, |
352 boxes = boxes, monos = monos, stds = stds, wfs = wfs, |
348 boxes = boxes, finitizes = finitizes, monos = monos, stds = stds, |
353 sat_solver = sat_solver, blocking = blocking, falsify = falsify, |
349 wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify, |
354 debug = debug, verbose = verbose, overlord = overlord, |
350 debug = debug, verbose = verbose, overlord = overlord, |
355 user_axioms = user_axioms, assms = assms, |
351 user_axioms = user_axioms, assms = assms, |
356 merge_type_vars = merge_type_vars, binary_ints = binary_ints, |
352 merge_type_vars = merge_type_vars, binary_ints = binary_ints, |
357 destroy_constrs = destroy_constrs, specialize = specialize, |
353 destroy_constrs = destroy_constrs, specialize = specialize, |
358 skolemize = skolemize, star_linear_preds = star_linear_preds, |
354 skolemize = skolemize, star_linear_preds = star_linear_preds, |