started implementation of custom sym break

--- 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

--- 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,

--- 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 =

--- 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 _ _ [] = []