# HG changeset patch # User blanchet # Date 1280587172 -7200 # Node ID 6538e25cf5ddd7684282e1be9120ee818e04eee6 # Parent 36f649db4a6c60134eb59a6ca614738886e7c34e started implementation of custom sym break diff -r 36f649db4a6c -r 6538e25cf5dd src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Jul 31 12:29:56 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Jul 31 16:39:32 2010 +0200 @@ -35,6 +35,8 @@ star_linear_preds: bool, fast_descrs: bool, peephole_optim: bool, + datatype_sym_break: int, + kodkod_sym_break: int, timeout: Time.time option, tac_timeout: Time.time option, max_threads: int, @@ -106,6 +108,8 @@ star_linear_preds: bool, fast_descrs: bool, peephole_optim: bool, + datatype_sym_break: int, + kodkod_sym_break: int, timeout: Time.time option, tac_timeout: Time.time option, max_threads: int, @@ -191,9 +195,10 @@ boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug, verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints, destroy_constrs, specialize, star_linear_preds, fast_descrs, - peephole_optim, tac_timeout, max_threads, show_datatypes, show_consts, - evals, formats, atomss, max_potential, max_genuine, check_potential, - check_genuine, batch_size, ...} = params + peephole_optim, datatype_sym_break, kodkod_sym_break, tac_timeout, + max_threads, show_datatypes, show_consts, evals, formats, atomss, + max_potential, max_genuine, check_potential, check_genuine, batch_size, + ...} = params val state_ref = Unsynchronized.ref state val pprint = if auto then @@ -493,7 +498,7 @@ 0 val settings = [("solver", commas_quote kodkod_sat_solver), ("bit_width", string_of_int bit_width), - ("symmetry_breaking", "20"), + ("symmetry_breaking", string_of_int kodkod_sym_break), ("sharing", "3"), ("flatten", "false"), ("delay", signed_string_of_int delay)] @@ -508,7 +513,7 @@ val univ_card = Int.max (univ_card nat_card int_card main_j0 (plain_bounds @ sel_bounds) formula, main_j0 |> bits > 0 ? Integer.add (bits + 1)) - val built_in_bounds = bounds_for_built_in_rels_in_formula debug + val built_in_bounds = bounds_for_built_in_rels_in_formula debug ofs univ_card nat_card int_card main_j0 formula val bounds = built_in_bounds @ plain_bounds @ sel_bounds |> not debug ? merge_bounds diff -r 36f649db4a6c -r 6538e25cf5dd src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Jul 31 12:29:56 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Jul 31 16:39:32 2010 +0200 @@ -56,6 +56,8 @@ ("star_linear_preds", "true"), ("fast_descrs", "true"), ("peephole_optim", "true"), + ("datatype_sym_break", "20"), + ("kodkod_sym_break", "20"), ("timeout", "30 s"), ("tac_timeout", "500 ms"), ("max_threads", "0"), @@ -245,6 +247,8 @@ val star_linear_preds = lookup_bool "star_linear_preds" val fast_descrs = lookup_bool "fast_descrs" val peephole_optim = lookup_bool "peephole_optim" + val datatype_sym_break = lookup_int "datatype_sym_break" + val kodkod_sym_break = lookup_int "kodkod_sym_break" val timeout = if auto then NONE else lookup_time "timeout" val tac_timeout = lookup_time "tac_timeout" val max_threads = Int.max (0, lookup_int "max_threads") @@ -273,7 +277,8 @@ merge_type_vars = merge_type_vars, binary_ints = binary_ints, destroy_constrs = destroy_constrs, specialize = specialize, star_linear_preds = star_linear_preds, fast_descrs = fast_descrs, - peephole_optim = peephole_optim, timeout = timeout, + peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break, + kodkod_sym_break = kodkod_sym_break, timeout = timeout, tac_timeout = tac_timeout, max_threads = max_threads, show_datatypes = show_datatypes, show_consts = show_consts, formats = formats, atomss = atomss, evals = evals, diff -r 36f649db4a6c -r 6538e25cf5dd src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Sat Jul 31 12:29:56 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Sat Jul 31 16:39:32 2010 +0200 @@ -26,7 +26,8 @@ val sequential_int_bounds : int -> Kodkod.int_bound list val pow_of_two_int_bounds : int -> int -> Kodkod.int_bound list val bounds_for_built_in_rels_in_formula : - bool -> int -> int -> int -> int -> Kodkod.formula -> Kodkod.bound list + bool -> int Typtab.table -> int -> int -> int -> int -> Kodkod.formula + -> Kodkod.bound list val bound_for_plain_rel : Proof.context -> bool -> nut -> Kodkod.bound val bound_for_sel_rel : Proof.context -> bool -> dtype_spec list -> nut -> Kodkod.bound @@ -201,13 +202,24 @@ else if m = 0 orelse n = 0 then (0, 1) else let val p = isa_zgcd (m, n) in (isa_div (m, p), isa_div (n, p)) end -fun tabulate_built_in_rel debug univ_card nat_card int_card j0 (x as (n, _)) = +fun tabulate_suc debug ofs univ_card main_j0 = + let + val j0s = Typtab.fold (insert (op =) o snd) ofs [main_j0] |> sort int_ord + val ks = map (op -) (tl (j0s @ [univ_card]) ~~ j0s) + in + map2 (fn j0 => fn k => + tabulate_func1 debug univ_card (k - 1, j0) (Integer.add 1)) + j0s ks + |> List.concat + end + +fun tabulate_built_in_rel debug ofs univ_card nat_card int_card j0 + (x as (n, _)) = (check_arity univ_card n; if x = not3_rel then ("not3", tabulate_func1 debug univ_card (2, j0) (curry (op -) 1)) else if x = suc_rel then - ("suc", tabulate_func1 debug univ_card (univ_card - j0 - 1, j0) - (Integer.add 1)) + ("suc", tabulate_suc debug ofs univ_card j0) else if x = nat_add_rel then ("nat_add", tabulate_nat_op2 debug univ_card (nat_card, j0) (op +)) else if x = int_add_rel then @@ -241,14 +253,15 @@ else raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation")) -fun bound_for_built_in_rel debug univ_card nat_card int_card j0 x = +fun bound_for_built_in_rel debug ofs univ_card nat_card int_card j0 x = let - val (nick, ts) = tabulate_built_in_rel debug univ_card nat_card int_card + val (nick, ts) = tabulate_built_in_rel debug ofs univ_card nat_card int_card j0 x in ([(x, nick)], [KK.TupleSet ts]) end -fun bounds_for_built_in_rels_in_formula debug univ_card nat_card int_card j0 = - map (bound_for_built_in_rel debug univ_card nat_card int_card j0) +fun bounds_for_built_in_rels_in_formula debug ofs univ_card nat_card int_card + j0 = + map (bound_for_built_in_rel debug ofs univ_card nat_card int_card j0) o built_in_rels_in_formula fun bound_comment ctxt debug nick T R = diff -r 36f649db4a6c -r 6538e25cf5dd src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Sat Jul 31 12:29:56 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Sat Jul 31 16:39:32 2010 +0200 @@ -361,7 +361,7 @@ end handle Option.Option => NONE -fun offset_table_for_card_assigns assigns dtypes = +fun offset_table_for_card_assigns dtypes assigns = let fun aux next _ [] = Typtab.update_new (dummyT, next) | aux next reusable ((T, k) :: assigns) = @@ -376,7 +376,7 @@ SOME j0 => Typtab.update_new (T, j0) #> aux next reusable assigns | NONE => Typtab.update_new (T, next) #> aux (next + k) ((k, next) :: reusable) assigns - in aux 0 [] assigns Typtab.empty end + in Typtab.empty |> aux 0 [] assigns end fun domain_card max card_assigns = Integer.prod o map (bounded_card_of_type max max card_assigns) o binder_types @@ -473,7 +473,7 @@ in {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns, datatypes = datatypes, bits = bits, bisim_depth = bisim_depth, - ofs = offset_table_for_card_assigns card_assigns datatypes} + ofs = offset_table_for_card_assigns datatypes card_assigns} end fun repair_cards_assigns_wrt_boxing_etc _ _ [] = []