# HG changeset patch
# User blanchet
# Date 1280677431 -7200
# Node ID b730aac146127d78d8682f59e8accda4519cf1e8
# Parent  99440c205e4abfd6e59a04e989d479fb69a6fb9d# Parent  83933448e9b7ad950ebaef516d4455cf6a3dbb6e
merged

diff -r 99440c205e4a -r b730aac14612 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Sun Aug 01 10:26:55 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Sun Aug 01 17:43:51 2010 +0200
@@ -818,7 +818,7 @@
 \hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount]
 Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
 \hbox{}\qquad Empty assignment \\[2\smallskipamount]
-Nitpick could not find a better counterexample. \\[2\smallskipamount]
+Nitpick could not find a better counterexample. It checked 1 of 1 scope. \\[2\smallskipamount]
 Total time: 2274 ms.
 \postw
 
@@ -2371,6 +2371,15 @@
 which you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
 version of MiniSat, the JNI version can be used incrementally.
 
+\item[$\bullet$] \textbf{\textit{CryptoMiniSat}:} CryptoMiniSat is the winner of
+the 2010 SAT Race. To use CryptoMiniSat, set the environment variable
+\texttt{CRYPTO\-MINISAT\_}\discretionary{}{}{}\texttt{HOME} to the directory that contains the \texttt{crypto\-minisat}
+executable.%
+\footref{cygwin-paths}
+The \cpp{} sources and executables for Crypto\-Mini\-Sat are available at
+\url{http://planete.inrialpes.fr/~soos/}\allowbreak\url{CryptoMiniSat2/index.php}.
+Nitpick has been tested with version 2.51.
+
 \item[$\bullet$] \textbf{\textit{PicoSAT}:} PicoSAT is an efficient solver
 written in C. You can install a standard version of
 PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
@@ -2433,11 +2442,9 @@
 optimized for small problems. It can also be used incrementally.
 
 \item[$\bullet$] \textbf{\textit{smart}:} If \textit{sat\_solver} is set to
-\textit{smart}, Nitpick selects the first solver among MiniSat,
-PicoSAT, zChaff, RSat, BerkMin, BerkMin\_Alloy, Jerusat, MiniSat\_JNI, and zChaff\_JNI
-that is recognized by Isabelle. If none is found, it falls back on SAT4J, which
-should always be available. If \textit{verbose} (\S\ref{output-format}) is
-enabled, Nitpick displays which SAT solver was chosen.
+\textit{smart}, Nitpick selects the first solver among the above that is
+recognized by Isabelle. If \textit{verbose} (\S\ref{output-format}) is enabled,
+Nitpick displays which SAT solver was chosen.
 \end{enum}
 \fussy
 
@@ -2493,6 +2500,18 @@
 Unless you are tracking down a bug in Nitpick or distrust the peephole
 optimizer, you should leave this option enabled.
 
+\opdefault{datatype\_sym\_break}{int}{5}
+Specifies an upper bound on the number of datatypes for which Nitpick generates
+symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
+considerably, especially for unsatisfiable problems, but too much of it can slow
+it down.
+
+\opdefault{kodkod\_sym\_break}{int}{15}
+Specifies an upper bound on the number of relations for which Kodkod generates
+symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
+considerably, especially for unsatisfiable problems, but too much of it can slow
+it down.
+
 \opdefault{max\_threads}{int}{0}
 Specifies the maximum number of threads to use in Kodkod. If this option is set
 to 0, Kodkod will compute an appropriate value based on the number of processor
diff -r 99440c205e4a -r b730aac14612 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Sun Aug 01 10:26:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sun Aug 01 17:43:51 2010 +0200
@@ -47,7 +47,7 @@
     Acyclic of n_ary_index |
     Function of n_ary_index * rel_expr * rel_expr |
     Functional of n_ary_index * rel_expr * rel_expr |
-    TotalOrdering of n_ary_index * n_ary_index * n_ary_index * n_ary_index |
+    TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr |
     Subset of rel_expr * rel_expr |
     RelEq of rel_expr * rel_expr |
     IntEq of int_expr * int_expr |
@@ -216,7 +216,7 @@
   Acyclic of n_ary_index |
   Function of n_ary_index * rel_expr * rel_expr |
   Functional of n_ary_index * rel_expr * rel_expr |
-  TotalOrdering of n_ary_index * n_ary_index * n_ary_index * n_ary_index |
+  TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr |
   Subset of rel_expr * rel_expr |
   RelEq of rel_expr * rel_expr |
   IntEq of int_expr * int_expr |
@@ -316,7 +316,15 @@
    rel_expr_func: rel_expr -> 'a -> 'a,
    int_expr_func: int_expr -> 'a -> 'a}
 
-(** Auxiliary functions on ML representation of Kodkod problems **)
+fun is_new_kodkodi_version () =
+  case getenv "KODKODI_VERSION" of
+    "" => false
+  | s => dict_ord int_ord (s |> space_explode "."
+                             |> map (the o Int.fromString),
+                           [1, 2, 13]) = GREATER
+         handle Option.Option => false
+
+(** Auxiliary functions on Kodkod problems **)
 
 fun fold_formula (F : 'a fold_expr_funcs) formula =
   case formula of
@@ -335,9 +343,9 @@
     fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
   | Functional (x, r1, r2) =>
     fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
-  | TotalOrdering (x1, x2, x3, x4) =>
-    fold_rel_expr F (Rel x1) #> fold_rel_expr F (Rel x2)
-    #> fold_rel_expr F (Rel x3) #> fold_rel_expr F (Rel x4)
+  | TotalOrdering (x, r1, r2, r3) =>
+    fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
+    #> fold_rel_expr F r3
   | Subset (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   | RelEq (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   | IntEq (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
@@ -518,7 +526,10 @@
 fun int_reg_name j = "$i" ^ base_name j
 
 fun tuple_name x = n_ary_name x "A" "P" "T"
-fun rel_name x = n_ary_name x "s" "r" "m"
+fun rel_name new_kodkodi (n, j) =
+  n_ary_name (n, if new_kodkodi then j
+                 else if j >= 0 then 2 * j
+                 else 2 * ~j - 1) "s" "r" "m"
 fun var_name x = n_ary_name x "S" "R" "M"
 fun tuple_reg_name x = n_ary_name x "$A" "$P" "$T"
 fun tuple_set_reg_name x = n_ary_name x "$a" "$p" "$t"
@@ -530,7 +541,8 @@
 fun block_comment "" = ""
   | block_comment comment = prefix_lines "// " comment ^ "\n"
 
-fun commented_rel_name (x, s) = rel_name x ^ inline_comment s
+fun commented_rel_name new_kodkodi (x, s) =
+  rel_name new_kodkodi x ^ inline_comment s
 
 fun string_for_tuple (Tuple js) = "[" ^ commas (map atom_name js) ^ "]"
   | string_for_tuple (TupleIndex x) = tuple_name x
@@ -581,8 +593,8 @@
   | string_for_tuple_assign (AssignTupleSet (x, ts)) =
     tuple_set_reg_name x ^ " := " ^ string_for_tuple_set ts ^ "\n"
 
-fun string_for_bound (zs, tss) =
-  "bounds " ^ commas (map commented_rel_name zs) ^ ": " ^
+fun string_for_bound new_kodkodi (zs, tss) =
+  "bounds " ^ commas (map (commented_rel_name new_kodkodi) zs) ^ ": " ^
   (if length tss = 1 then "" else "[") ^ commas (map string_for_tuple_set tss) ^
   (if length tss = 1 then "" else "]") ^ "\n"
 
@@ -685,6 +697,8 @@
 
 fun write_problem_file out problems =
   let
+    val new_kodkodi = is_new_kodkodi_version ()
+    val rel_name = rel_name new_kodkodi
     fun out_outmost_f (And (f1, f2)) =
         (out_outmost_f f1; out "\n   && "; out_outmost_f f2)
       | out_outmost_f f = out_f f prec_And
@@ -715,9 +729,9 @@
          | Functional (x, r1, r2) =>
            (out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " -> lone ";
             out_r r2 0; out ")")
-         | TotalOrdering (x1, x2, x3, x4) =>
-           out ("TOTAL_ORDERING(" ^ rel_name x1 ^ ", " ^ rel_name x2 ^ ", "
-                ^ rel_name x3 ^ ", " ^ rel_name x4 ^ ")")
+         | TotalOrdering (x, r1, r2, r3) =>
+           (out ("TOTAL_ORDERING(" ^ rel_name x ^ ", "); out_r r1 0; out ", ";
+            out_r r2 0; out ", "; out_r r3 0; out ")")
          | Subset (r1, r2) => (out_r r1 prec; out " in "; out_r r2 prec)
          | RelEq (r1, r2) => (out_r r1 prec; out " = "; out_r r2 prec)
          | IntEq (i1, i2) => (out_i i1 prec; out " = "; out_i i2 prec)
@@ -837,7 +851,7 @@
                             settings) ^
               "univ: " ^ atom_seq_name (univ_card, 0) ^ "\n" ^
               implode (map string_for_tuple_assign tuple_assigns) ^
-              implode (map string_for_bound bounds) ^
+              implode (map (string_for_bound new_kodkodi) bounds) ^
               (if int_bounds = [] then
                  ""
                else
@@ -871,22 +885,29 @@
 fun scan_list scan = scan_non_empty_list scan || Scan.succeed []
 val scan_nat = Scan.repeat1 (Scan.one Symbol.is_ascii_digit)
                >> (the o Int.fromString o space_implode "")
-val scan_rel_name = $$ "s" |-- scan_nat >> pair 1
-                    || $$ "r" |-- scan_nat >> pair 2
-                    || ($$ "m" |-- scan_nat --| $$ "_") -- scan_nat
+fun scan_rel_name new_kodkodi =
+  ($$ "s" |-- scan_nat >> pair 1
+   || $$ "r" |-- scan_nat >> pair 2
+   || ($$ "m" |-- scan_nat --| $$ "_") -- scan_nat) -- Scan.option ($$ "'")
+  >> (fn ((n, j), SOME _) => (n, ~j - 1)
+       | ((n, j), NONE) => (n, if new_kodkodi then j
+                               else if j mod 2 = 0 then j div 2
+                               else ~(j - 1) div 2))
 val scan_atom = $$ "A" |-- scan_nat
 val scan_tuple = $$ "[" |-- scan_list scan_atom --| $$ "]"
 val scan_tuple_set = $$ "[" |-- scan_list scan_tuple --| $$ "]"
-val scan_assignment = (scan_rel_name --| $$ "=") -- scan_tuple_set
-val scan_instance = Scan.this_string "relations:" |--
-                    $$ "{" |-- scan_list scan_assignment --| $$ "}"
+fun scan_assignment new_kodkodi =
+  (scan_rel_name new_kodkodi --| $$ "=") -- scan_tuple_set
+fun scan_instance new_kodkodi =
+  Scan.this_string "relations:"
+  |-- $$ "{" |-- scan_list (scan_assignment new_kodkodi) --| $$ "}"
 
-val parse_instance =
+fun parse_instance new_kodkodi =
   fst o Scan.finite Symbol.stopper
             (Scan.error (!! (fn _ =>
                                 raise SYNTAX ("Kodkod.parse_instance",
                                               "ill-formed Kodkodi output"))
-                            scan_instance))
+                            (scan_instance new_kodkodi)))
   o strip_blanks o explode
 
 val problem_marker = "*** PROBLEM "
@@ -897,15 +918,15 @@
   Substring.string o fst o Substring.position "\n\n"
   o Substring.triml (size marker)
 
-fun read_next_instance s =
+fun read_next_instance new_kodkodi s =
   let val s = Substring.position instance_marker s |> snd in
     if Substring.isEmpty s then
       raise SYNTAX ("Kodkod.read_next_instance", "expected \"INSTANCE\" marker")
     else
-      read_section_body instance_marker s |> parse_instance
+      read_section_body instance_marker s |> parse_instance new_kodkodi
   end
 
-fun read_next_outcomes j (s, ps, js) =
+fun read_next_outcomes new_kodkodi j (s, ps, js) =
   let val (s1, s2) = Substring.position outcome_marker s in
     if Substring.isEmpty s2 orelse
        not (Substring.isEmpty (Substring.position problem_marker s1
@@ -917,16 +938,17 @@
         val s = Substring.triml (size outcome_marker) s2
       in
         if String.isSuffix "UNSATISFIABLE" outcome then
-          read_next_outcomes j (s, ps, j :: js)
+          read_next_outcomes new_kodkodi j (s, ps, j :: js)
         else if String.isSuffix "SATISFIABLE" outcome then
-          read_next_outcomes j (s, (j, read_next_instance s2) :: ps, js)
+          read_next_outcomes new_kodkodi j
+                           (s, (j, read_next_instance new_kodkodi s2) :: ps, js)
         else
           raise SYNTAX ("Kodkod.read_next_outcomes",
                         "unknown outcome " ^ quote outcome)
       end
   end
 
-fun read_next_problems (s, ps, js) =
+fun read_next_problems new_kodkodi (s, ps, js) =
   let val s = Substring.position problem_marker s |> snd in
     if Substring.isEmpty s then
       (ps, js)
@@ -936,14 +958,18 @@
         val j_plus_1 = s |> Substring.takel (not_equal #" ") |> Substring.string
                          |> Int.fromString |> the
         val j = j_plus_1 - 1
-      in read_next_problems (read_next_outcomes j (s, ps, js)) end
+      in
+        read_next_problems new_kodkodi
+                           (read_next_outcomes new_kodkodi j (s, ps, js))
+      end
   end
   handle Option.Option => raise SYNTAX ("Kodkod.read_next_problems",
                                         "expected number after \"PROBLEM\"")
 
-fun read_output_file path =
-  (false, read_next_problems (Substring.full (File.read path), [], [])
-          |>> rev ||> rev)
+fun read_output_file new_kodkodi path =
+  (false,
+   read_next_problems new_kodkodi (Substring.full (File.read path), [], [])
+   |>> rev ||> rev)
   handle IO.Io _ => (true, ([], [])) | OS.SysErr _ => (true, ([], []))
 
 (** Main Kodkod entry point **)
@@ -973,6 +999,7 @@
 fun uncached_solve_any_problem overlord deadline max_threads max_solutions
                                problems =
   let
+    val new_kodkodi = is_new_kodkodi_version ()
     val j = find_index (curry (op =) True o #formula) problems
     val indexed_problems = if j >= 0 then
                              [(j, nth problems j)]
@@ -1026,7 +1053,7 @@
                       " > " ^ File.shell_path out_path ^
                       " 2> " ^ File.shell_path err_path)
               val (io_error, (ps, nontriv_js)) =
-                read_output_file out_path
+                read_output_file new_kodkodi out_path
                 ||> apfst (map (apfst reindex)) ||> apsnd (map reindex)
               val js = triv_js @ nontriv_js
               val first_error =
@@ -1063,7 +1090,8 @@
         handle Exn.Interrupt =>
                let
                  val nontriv_js =
-                   read_output_file out_path |> snd |> snd |> map reindex
+                   read_output_file new_kodkodi out_path
+                   |> snd |> snd |> map reindex
                in
                  (remove_temporary_files ();
                   Interrupted (SOME (triv_js @ nontriv_js)))
diff -r 99440c205e4a -r b730aac14612 src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Sun Aug 01 10:26:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Sun Aug 01 17:43:51 2010 +0200
@@ -26,16 +26,21 @@
   External of sink * string * string * string list |
   ExternalV2 of sink * string * string * string list * string * string * string
 
+(* for compatibility with "SatSolver" *)
 val berkmin_exec = getenv "BERKMIN_EXE"
 
 (* (string * sat_solver_info) list *)
 val static_list =
   [("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
                            "UNSAT")),
+   ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
+   ("CryptoMiniSat", External (ToStdout, "CRYPTOMINISAT_HOME", "cryptominisat",
+                               [])),
    ("PicoSAT", External (ToStdout, "PICOSAT_HOME", "picosat", [])),
    ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
                           "Instance Satisfiable", "",
                           "Instance Unsatisfiable")),
+   ("zChaff_JNI", Internal (JNI, Batch, ["zChaff"])),
    ("RSat", ExternalV2 (ToStdout, "RSAT_HOME", "rsat", ["-s"],
                         "s SATISFIABLE", "v ", "s UNSATISFIABLE")),
    ("BerkMin", ExternalV2 (ToStdout, "BERKMIN_HOME",
@@ -44,8 +49,6 @@
                            "solution =", "UNSATISFIABLE          !!")),
    ("BerkMin_Alloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])),
    ("Jerusat", External (ToStdout, "JERUSAT_HOME", "Jerusat1.3", [])),
-   ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
-   ("zChaff_JNI", Internal (JNI, Batch, ["zChaff"])),
    ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
    ("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"]))]
 
diff -r 99440c205e4a -r b730aac14612 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Sun Aug 01 10:26:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sun Aug 01 17:43:51 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)]
@@ -502,19 +507,22 @@
         val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
         val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
         val dtype_axioms =
-          declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk
-                                           rel_table datatypes
+          declarative_axioms_for_datatypes hol_ctxt binarize datatype_sym_break
+                                           bits ofs kk rel_table datatypes
         val declarative_axioms = plain_axioms @ dtype_axioms
         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
-                                  univ_card nat_card int_card main_j0 formula
+        val (built_in_bounds, built_in_axioms) =
+          bounds_and_axioms_for_built_in_rels_in_formulas debug ofs
+              univ_card nat_card int_card main_j0
+              (formula :: declarative_axioms)
         val bounds = built_in_bounds @ plain_bounds @ sel_bounds
                      |> not debug ? merge_bounds
+        val axioms = built_in_axioms @ declarative_axioms
         val highest_arity =
           fold Integer.max (map (fst o fst) (maps fst bounds)) 0
-        val formula = fold_rev s_and declarative_axioms formula
+        val formula = fold_rev s_and axioms formula
         val _ = if bits = 0 then () else check_bits bits formula
         val _ = if formula = KK.False then ()
                 else check_arity univ_card highest_arity
@@ -904,9 +912,13 @@
                     "")); if skipped > 0 then "unknown" else "none")
           else
             (print_m (fn () =>
-                 "Nitpick could not find a" ^
-                 (if max_genuine = 1 then " better " ^ das_wort_model ^ "."
-                  else "ny better " ^ das_wort_model ^ "s.")); "potential")
+                 excipit ("could not find a" ^
+                          (if max_genuine = 1 then
+                             " better " ^ das_wort_model ^ "."
+                           else
+                             "ny better " ^ das_wort_model ^ "s.") ^
+                          " It checked"));
+             "potential")
         else if found_really_genuine then
           "genuine"
         else
diff -r 99440c205e4a -r b730aac14612 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sun Aug 01 10:26:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sun Aug 01 17:43:51 2010 +0200
@@ -56,6 +56,8 @@
    ("star_linear_preds", "true"),
    ("fast_descrs", "true"),
    ("peephole_optim", "true"),
+   ("datatype_sym_break", "5"),
+   ("kodkod_sym_break", "15"),
    ("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 99440c205e4a -r b730aac14612 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Sun Aug 01 10:26:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Sun Aug 01 17:43:51 2010 +0200
@@ -8,12 +8,9 @@
 signature NITPICK_KODKOD =
 sig
   type hol_context = Nitpick_HOL.hol_context
-  type dtype_spec = Nitpick_Scope.dtype_spec
+  type datatype_spec = Nitpick_Scope.datatype_spec
   type kodkod_constrs = Nitpick_Peephole.kodkod_constrs
   type nut = Nitpick_Nut.nut
-  type nfa_transition = Kodkod.rel_expr * typ
-  type nfa_entry = typ * nfa_transition list
-  type nfa_table = nfa_entry list
 
   structure NameTable : TABLE
 
@@ -25,16 +22,17 @@
   val tuple_set_from_atom_schema : (int * int) list -> Kodkod.tuple_set
   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
+  val bounds_and_axioms_for_built_in_rels_in_formulas :
+    bool -> int Typtab.table -> int -> int -> int -> int -> Kodkod.formula list
+    -> Kodkod.bound list * Kodkod.formula 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
+    Proof.context -> bool -> datatype_spec list -> nut -> Kodkod.bound
   val merge_bounds : Kodkod.bound list -> Kodkod.bound list
   val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
   val declarative_axioms_for_datatypes :
-    hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
-    -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
+    hol_context -> bool -> int -> int -> int Typtab.table -> kodkod_constrs
+    -> nut NameTable.table -> datatype_spec list -> Kodkod.formula list
   val kodkod_formula_from_nut :
     int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
 end;
@@ -51,11 +49,13 @@
 
 structure KK = Kodkod
 
-type nfa_transition = KK.rel_expr * typ
-type nfa_entry = typ * nfa_transition list
-type nfa_table = nfa_entry list
+structure NfaGraph = Typ_Graph
+
+fun pull x xs = x :: filter_out (curry (op =) x) xs
 
-structure NfaGraph = Typ_Graph
+fun is_datatype_good_and_old ({co = false, standard = true, deep = true, ...}
+                              : datatype_spec) = true
+  | is_datatype_good_and_old _ = false
 
 fun flip_nums n = index_seq 1 n @ [0] |> map KK.Num
 
@@ -122,19 +122,16 @@
         aux (iter - 1) (2 * pow_of_two) (j + 1)
   in aux (bits + 1) 1 j0 end
 
-fun built_in_rels_in_formula formula =
+fun built_in_rels_in_formulas formulas =
   let
     fun rel_expr_func (KK.Rel (x as (n, j))) =
-        if x = unsigned_bit_word_sel_rel orelse x = signed_bit_word_sel_rel then
-          I
-        else
-          (case AList.lookup (op =) (#rels initial_pool) n of
-             SOME k => j < k ? insert (op =) x
-           | NONE => I)
+        (j < 0 andalso x <> unsigned_bit_word_sel_rel andalso
+         x <> signed_bit_word_sel_rel)
+        ? insert (op =) x
       | rel_expr_func _ = I
     val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func,
                   int_expr_func = K I}
-  in KK.fold_formula expr_F formula [] end
+  in fold (KK.fold_formula expr_F) formulas [] end
 
 val max_table_size = 65536
 
@@ -201,7 +198,8 @@
   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_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))
@@ -241,15 +239,40 @@
    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 =
-  let
-    val (nick, ts) = tabulate_built_in_rel debug univ_card nat_card int_card
-                                           j0 x
-  in ([(x, nick)], [KK.TupleSet ts]) end
+fun bound_for_built_in_rel debug ofs univ_card nat_card int_card main_j0
+                           (x as (n, j)) =
+  if n = 2 andalso j <= suc_rels_base then
+    let val (y as (k, j0), tabulate) = atom_seq_for_suc_rel x in
+      ([(x, "suc")],
+       if tabulate then
+         [KK.TupleSet (tabulate_func1 debug univ_card (k - 1, j0)
+                       (Integer.add 1))]
+       else
+         [KK.TupleSet [], tuple_set_from_atom_schema [y, y]])
+    end
+  else
+    let
+      val (nick, ts) = tabulate_built_in_rel debug ofs univ_card nat_card
+                                             int_card main_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)
-  o built_in_rels_in_formula
+fun axiom_for_built_in_rel (x as (n, j)) =
+  if n = 2 andalso j <= suc_rels_base then
+    let val (y as (k, j0), tabulate) = atom_seq_for_suc_rel x in
+      if tabulate orelse k < 2 then
+        NONE
+      else
+        SOME (KK.TotalOrdering (x, KK.AtomSeq y, KK.Atom j0, KK.Atom (j0 + 1)))
+    end
+  else
+    NONE
+fun bounds_and_axioms_for_built_in_rels_in_formulas debug ofs univ_card nat_card
+                                                    int_card main_j0 formulas =
+  let val rels = built_in_rels_in_formulas formulas in
+    (map (bound_for_built_in_rel debug ofs univ_card nat_card int_card main_j0)
+         rels,
+     map_filter axiom_for_built_in_rel rels)
+  end 
 
 fun bound_comment ctxt debug nick T R =
   short_name nick ^
@@ -284,11 +307,10 @@
            else
              [KK.TupleSet [],
               if T1 = T2 andalso epsilon > delta andalso
-                 (datatype_spec dtypes T1 |> the |> pairf #co #standard)
-                 = (false, true) then
+                 is_datatype_good_and_old (the (datatype_spec dtypes T1)) then
                 index_seq delta (epsilon - delta)
                 |> map (fn j =>
-                           KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]],
+                           KK.TupleProduct (KK.TupleSet [KK.Tuple [j + j0]],
                                             KK.TupleAtomSeq (j, j0)))
                 |> foldl1 KK.TupleUnion
               else
@@ -334,8 +356,6 @@
   map2 (fn j => fn x => KK.DeclOne ((1, j), KK.AtomSeq x))
        (index_seq j0 (length schema)) schema
 
-(* The type constraint below is a workaround for a Poly/ML bug. *)
-
 fun d_n_ary_function ({kk_all, kk_join, kk_lone, kk_one, ...} : kodkod_constrs)
                      R r =
   let val body_R = body_rep R in
@@ -670,7 +690,7 @@
 
 fun nfa_transitions_for_sel hol_ctxt binarize
                             ({kk_project, ...} : kodkod_constrs) rel_table
-                            (dtypes : dtype_spec list) constr_x n =
+                            (dtypes : datatype_spec list) constr_x n =
   let
     val x as (_, T) =
       binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize constr_x n
@@ -679,14 +699,14 @@
   in
     map_filter (fn (j, T) =>
                    if forall (not_equal T o #typ) dtypes then NONE
-                   else SOME (kk_project r (map KK.Num [0, j]), T))
+                   else SOME ((x, kk_project r (map KK.Num [0, j])), T))
                (index_seq 1 (arity - 1) ~~ tl type_schema)
   end
 fun nfa_transitions_for_constr hol_ctxt binarize kk rel_table dtypes
                                (x as (_, T)) =
   maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
        (index_seq 0 (num_sels_for_constr_type T))
-fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
+fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : datatype_spec) = NONE
   | nfa_entry_for_datatype _ _ _ _ _ {standard = false, ...} = NONE
   | nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
   | nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes
@@ -698,7 +718,7 @@
 
 fun direct_path_rel_exprs nfa start_T final_T =
   case AList.lookup (op =) nfa final_T of
-    SOME trans => map fst (filter (curry (op =) start_T o snd) trans)
+    SOME trans => map (snd o fst) (filter (curry (op =) start_T o snd) trans)
   | NONE => []
 and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T
                       final_T =
@@ -736,14 +756,168 @@
   nfa |> graph_for_nfa |> NfaGraph.strong_conn
       |> map (fn keys => filter (member (op =) keys o fst) nfa)
 
-fun acyclicity_axiom_for_datatype kk nfa start_T =
-  #kk_no kk (#kk_intersect kk
-                 (loop_path_rel_expr kk nfa (map fst nfa) start_T) KK.Iden)
-fun acyclicity_axioms_for_datatypes hol_ctxt binarize kk rel_table dtypes =
-  map_filter (nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes)
-             dtypes
-  |> strongly_connected_sub_nfas
-  |> maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa)
+fun acyclicity_axiom_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa
+                                  start_T =
+  kk_no (kk_intersect
+             (loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T)
+             KK.Iden)
+fun acyclicity_axioms_for_datatypes kk nfas =
+  maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa) nfas
+
+fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r =
+  kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z)))
+fun gt ({kk_subset, kk_join, kk_closure, ...} : kodkod_constrs) z r1 r2 =
+  kk_subset r1 (kk_join r2 (kk_closure (KK.Rel (suc_rel_for_atom_seq z))))
+
+fun constr_ord (({const = (s1, _), delta = delta1, epsilon = epsilon1, ...},
+                 {const = (s2, _), delta = delta2, epsilon = epsilon2, ...})
+                : constr_spec * constr_spec) =
+  prod_ord int_ord (prod_ord int_ord string_ord)
+           ((delta1, (epsilon2, s1)), (delta2, (epsilon2, s2)))
+
+fun datatype_ord (({card = card1, self_rec = self_rec1, constrs = constr1, ...},
+                   {card = card2, self_rec = self_rec2, constrs = constr2, ...})
+                  : datatype_spec * datatype_spec) =
+  prod_ord int_ord (prod_ord bool_ord int_ord)
+           ((card1, (self_rec1, length constr1)),
+            (card2, (self_rec2, length constr2)))
+
+(* We must absolutely tabulate "suc" for all datatypes whose selector bounds
+   break cycles; otherwise, we may end up with two incompatible symmetry
+   breaking orders, leading to spurious models. *)
+fun should_tabulate_suc_for_type dtypes T =
+  is_asymmetric_nondatatype T orelse
+  case datatype_spec dtypes T of
+    SOME {self_rec, ...} => self_rec
+  | NONE => false
+
+fun lex_order_rel_expr (kk as {kk_implies, kk_and, kk_subset, kk_join, ...})
+                       dtypes sel_quadruples =
+  case sel_quadruples of
+    [] => KK.True
+  | ((r, Func (Atom _, Atom x), 2), (_, Type (_, [_, T]))) :: sel_quadruples' =>
+    let val z = (x, should_tabulate_suc_for_type dtypes T) in
+      if null sel_quadruples' then
+        gt kk z (kk_join (KK.Var (1, 1)) r) (kk_join (KK.Var (1, 0)) r)
+      else
+        kk_and (kk_subset (kk_join (KK.Var (1, 1)) r)
+                          (all_ge kk z (kk_join (KK.Var (1, 0)) r)))
+               (kk_implies (kk_subset (kk_join (KK.Var (1, 1)) r)
+                                      (kk_join (KK.Var (1, 0)) r))
+                           (lex_order_rel_expr kk dtypes sel_quadruples'))
+    end
+    (* Skip constructors components that aren't atoms, since we cannot compare
+       these easily. *)
+  | _ :: sel_quadruples' => lex_order_rel_expr kk dtypes sel_quadruples'
+
+fun has_nil_like_constr dtypes T =
+  case #constrs (the (datatype_spec dtypes T))
+       |> filter_out (is_self_recursive_constr_type o snd o #const) of
+    [{const = (_, T'), ...}] => T = T'
+  | _ => false
+
+fun sym_break_axioms_for_constr_pair hol_ctxt binarize
+       (kk as {kk_all, kk_or, kk_iff, kk_implies, kk_and, kk_some, kk_subset,
+               kk_intersect, kk_join, kk_project, ...}) rel_table nfas dtypes
+       (constr1 as {const = const1 as (_, T1), delta = delta1,
+                    epsilon = epsilon1, ...},
+        constr2 as {const = const2 as (_, T2), delta = delta2,
+                    epsilon = epsilon2, ...}) =
+  let
+    val dataT = body_type T1
+    val nfa = nfas |> find_first (exists (curry (op =) dataT o fst)) |> these
+    val rec_Ts = nfa |> map fst
+    val same_constr = (const1 = const2)
+    fun rec_and_nonrec_sels (x as (_, T)) =
+      index_seq 0 (num_sels_for_constr_type T)
+      |> map (binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x)
+      |> List.partition (member (op =) rec_Ts o range_type o snd)
+    val sel_xs1 = rec_and_nonrec_sels const1 |> op @
+  in
+    if same_constr andalso null sel_xs1 then
+      []
+    else
+      let
+        val z =
+          (case #2 (const_triple rel_table (discr_for_constr const1)) of
+             Func (Atom x, Formula _) => x
+           | R => raise REP ("Nitpick_Kodkod.sym_break_axioms_for_constr_pair",
+                             [R]), should_tabulate_suc_for_type dtypes dataT)
+        val (rec_sel_xs2, nonrec_sel_xs2) = rec_and_nonrec_sels const2
+        val sel_xs2 = rec_sel_xs2 @ nonrec_sel_xs2
+        fun sel_quadruples2 () = sel_xs2 |> map (`(const_triple rel_table))
+        (* If the two constructors are the same, we drop the first selector
+           because that one is always checked by the lexicographic order.
+           We sometimes also filter out direct subterms, because those are
+           already handled by the acyclicity breaking in the bound
+           declarations. *)
+        fun filter_out_sels no_direct sel_xs =
+          apsnd (filter_out
+                     (fn ((x, _), T) =>
+                         (same_constr andalso x = hd sel_xs) orelse
+                         (T = dataT andalso
+                          (no_direct orelse not (member (op =) sel_xs x)))))
+        fun subterms_r no_direct sel_xs j =
+          loop_path_rel_expr kk (map (filter_out_sels no_direct sel_xs) nfa)
+                           (filter_out (curry (op =) dataT) (map fst nfa)) dataT
+          |> kk_join (KK.Var (1, j))
+      in
+        [kk_all [KK.DeclOne ((1, 0), discr_rel_expr rel_table const1),
+                 KK.DeclOne ((1, 1), discr_rel_expr rel_table const2)]
+             ((if same_constr then kk_implies else kk_iff)
+                 (if delta2 >= epsilon1 then KK.True
+                  else gt kk z (KK.Var (1, 1)) (KK.Var (1, 0)))
+                 (kk_or
+                      (if has_nil_like_constr dtypes dataT andalso
+                          T1 = dataT then
+                         KK.True
+                       else
+                         kk_some (kk_intersect (subterms_r false sel_xs2 1)
+                                               (all_ge kk z (KK.Var (1, 0)))))
+                      (if same_constr then
+                         kk_and
+                             (lex_order_rel_expr kk dtypes (sel_quadruples2 ()))
+                             (if length rec_sel_xs2 > 1 then
+                                kk_all [KK.DeclOne ((1, 2),
+                                                    subterms_r true sel_xs1 0)]
+                                       (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2)))
+                              else
+                                KK.True)
+                       else
+                         kk_all [KK.DeclOne ((1, 2),
+                                 subterms_r false sel_xs1 0)]
+                                (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))))))]
+      end
+  end
+
+fun sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas dtypes
+                                  ({constrs, ...} : datatype_spec) =
+    let val constrs = sort constr_ord constrs in
+      maps (sym_break_axioms_for_constr_pair hol_ctxt binarize kk rel_table nfas
+                                             dtypes)
+           ((constrs ~~ constrs) @ all_distinct_unordered_pairs_of constrs)
+    end
+
+val min_sym_break_card = 7
+
+fun sym_break_axioms_for_datatypes hol_ctxt binarize datatype_sym_break kk
+                                   rel_table nfas dtypes =
+  if datatype_sym_break = 0 then
+    []
+  else
+    maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas
+                                        dtypes)
+         (dtypes |> filter is_datatype_good_and_old
+                 |> filter (fn {constrs = [_], ...} => false
+                             | {card, constrs, ...} =>
+                               card >= min_sym_break_card andalso
+                               forall (forall (not o is_higher_order_type)
+                                       o binder_types o snd o #const) constrs)
+                 |> (fn dtypes' =>
+                        dtypes'
+                        |> length dtypes' > datatype_sym_break
+                           ? (sort (rev_order o datatype_ord)
+                              #> take datatype_sym_break)))
 
 fun sel_axiom_for_sel hol_ctxt binarize j0
         (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})
@@ -778,7 +952,8 @@
         val max_axiom =
           if honors_explicit_max then
             KK.True
-          else if is_twos_complement_representable bits (epsilon - delta) then
+          else if bits = 0 orelse
+               is_twos_complement_representable bits (epsilon - delta) then
             KK.LE (KK.Cardinality dom_r, KK.Num explicit_max)
           else
             raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",
@@ -791,7 +966,7 @@
       end
   end
 fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table
-                            ({constrs, ...} : dtype_spec) =
+                            ({constrs, ...} : datatype_spec) =
   maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs
 
 fun uniqueness_axiom_for_constr hol_ctxt binarize
@@ -816,13 +991,13 @@
                   (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
   end
 fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table
-                                   ({constrs, ...} : dtype_spec) =
+                                   ({constrs, ...} : datatype_spec) =
   map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs
 
 fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
 fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...})
                                   rel_table
-                                  ({card, constrs, ...} : dtype_spec) =
+                                  ({card, constrs, ...} : datatype_spec) =
   if forall #exclusive constrs then
     [Integer.sum (map effective_constr_max constrs) = card |> formula_for_bool]
   else
@@ -840,11 +1015,20 @@
       partition_axioms_for_datatype j0 kk rel_table dtype
     end
 
-fun declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk rel_table
-                                     dtypes =
-  acyclicity_axioms_for_datatypes hol_ctxt binarize kk rel_table dtypes @
-  maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
-       dtypes
+fun declarative_axioms_for_datatypes hol_ctxt binarize datatype_sym_break bits
+                                     ofs kk rel_table dtypes =
+  let
+    val nfas =
+      dtypes |> map_filter (nfa_entry_for_datatype hol_ctxt binarize kk
+                                                   rel_table dtypes)
+             |> strongly_connected_sub_nfas
+  in
+    acyclicity_axioms_for_datatypes kk nfas @
+    sym_break_axioms_for_datatypes hol_ctxt binarize datatype_sym_break kk
+                                   rel_table nfas dtypes @
+    maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
+         dtypes
+  end
 
 fun kodkod_formula_from_nut ofs
         (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
diff -r 99440c205e4a -r b730aac14612 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Aug 01 10:26:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Aug 01 17:43:51 2010 +0200
@@ -902,8 +902,8 @@
     val all_values =
       all_values_of_type pool wacky_names scope atomss sel_names rel_table
                          bounds
-    fun is_codatatype_wellformed (cos : dtype_spec list)
-                                 ({typ, card, ...} : dtype_spec) =
+    fun is_codatatype_wellformed (cos : datatype_spec list)
+                                 ({typ, card, ...} : datatype_spec) =
       let
         val ts = all_values card typ
         val max_depth = Integer.sum (map #card cos)
@@ -935,7 +935,7 @@
             [setmp_show_all_types (Syntax.pretty_term ctxt) t1,
              Pretty.str oper, Syntax.pretty_term ctxt t2])
       end
-    fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
+    fun pretty_for_datatype ({typ, card, complete, ...} : datatype_spec) =
       Pretty.block (Pretty.breaks
           (Syntax.pretty_typ ctxt (uniterize_unarize_unbox_etc_type typ) ::
            (case typ of
@@ -950,8 +950,8 @@
                   else [Pretty.str (unrep ())]))]))
     fun integer_datatype T =
       [{typ = T, card = card_of_type card_assigns T, co = false,
-        standard = true, complete = (false, false), concrete = (true, true),
-        deep = true, constrs = []}]
+        standard = true, self_rec = true, complete = (false, false),
+        concrete = (true, true), deep = true, constrs = []}]
       handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
     val (codatatypes, datatypes) =
       datatypes |> filter #deep |> List.partition #co
diff -r 99440c205e4a -r b730aac14612 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Sun Aug 01 10:26:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Sun Aug 01 17:43:51 2010 +0200
@@ -721,7 +721,7 @@
 fun choose_rep_for_sels_for_constr scope (x as (_, T)) =
   fold_rev (choose_rep_for_nth_sel_for_constr scope x)
            (~1 upto num_sels_for_constr_type T - 1)
-fun choose_rep_for_sels_of_datatype _ ({deep = false, ...} : dtype_spec) = I
+fun choose_rep_for_sels_of_datatype _ ({deep = false, ...} : datatype_spec) = I
   | choose_rep_for_sels_of_datatype scope {constrs, ...} =
     fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
 fun choose_reps_for_all_sels (scope as {datatypes, ...}) =
diff -r 99440c205e4a -r b730aac14612 src/HOL/Tools/Nitpick/nitpick_peephole.ML
--- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Sun Aug 01 10:26:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Sun Aug 01 17:43:51 2010 +0200
@@ -23,6 +23,7 @@
   val initial_pool : name_pool
   val not3_rel : n_ary_index
   val suc_rel : n_ary_index
+  val suc_rels_base : int
   val unsigned_bit_word_sel_rel : n_ary_index
   val signed_bit_word_sel_rel : n_ary_index
   val nat_add_rel : n_ary_index
@@ -46,6 +47,8 @@
   val int_for_atom : int * int -> int -> int
   val atom_for_int : int * int -> int -> int
   val is_twos_complement_representable : int -> int -> bool
+  val suc_rel_for_atom_seq : (int * int) * bool -> n_ary_index
+  val atom_seq_for_suc_rel : n_ary_index -> (int * int) * bool
   val inline_rel_expr : rel_expr -> bool
   val empty_n_ary_rel : int -> rel_expr
   val num_seq : int -> int -> int_expr list
@@ -99,30 +102,27 @@
    formula_reg: int,
    rel_reg: int}
 
-(* If you add new built-in relations, make sure to increment the counters here
-   as well to avoid name clashes (which fortunately would be detected by
-   Kodkodi). *)
-val initial_pool =
-  {rels = [(2, 10), (3, 20), (4, 10)], vars = [], formula_reg = 10,
-   rel_reg = 10}
+(* FIXME: needed? *)
+val initial_pool = {rels = [], vars = [], formula_reg = 10, rel_reg = 10}
 
-val not3_rel = (2, 0)
-val suc_rel = (2, 1)
-val unsigned_bit_word_sel_rel = (2, 2)
-val signed_bit_word_sel_rel = (2, 3)
-val nat_add_rel = (3, 0)
-val int_add_rel = (3, 1)
-val nat_subtract_rel = (3, 2)
-val int_subtract_rel = (3, 3)
-val nat_multiply_rel = (3, 4)
-val int_multiply_rel = (3, 5)
-val nat_divide_rel = (3, 6)
-val int_divide_rel = (3, 7)
-val nat_less_rel = (3, 8)
-val int_less_rel = (3, 9)
-val gcd_rel = (3, 10)
-val lcm_rel = (3, 11)
-val norm_frac_rel = (4, 0)
+val not3_rel = (2, ~1)
+val unsigned_bit_word_sel_rel = (2, ~2)
+val signed_bit_word_sel_rel = (2, ~3)
+val suc_rel = (2, ~4)
+val suc_rels_base = ~5 (* must be the last of the binary series *)
+val nat_add_rel = (3, ~1)
+val int_add_rel = (3, ~2)
+val nat_subtract_rel = (3, ~3)
+val int_subtract_rel = (3, ~4)
+val nat_multiply_rel = (3, ~5)
+val int_multiply_rel = (3, ~6)
+val nat_divide_rel = (3, ~7)
+val int_divide_rel = (3, ~8)
+val nat_less_rel = (3, ~9)
+val int_less_rel = (3, ~10)
+val gcd_rel = (3, ~11)
+val lcm_rel = (3, ~12)
+val norm_frac_rel = (4, ~1)
 
 fun atom_for_bool j0 = Atom o Integer.add j0 o int_from_bool
 fun formula_for_bool b = if b then True else False
@@ -139,6 +139,23 @@
 fun is_twos_complement_representable bits n =
   let val max = reasonable_power 2 bits in n >= ~ max andalso n < max end
 
+val max_squeeze_card = 49
+
+fun squeeze (m, n) =
+  if n > max_squeeze_card then
+    raise TOO_LARGE ("Nitpick_Peephole.squeeze",
+                     "too large cardinality (" ^ string_of_int n ^ ")")
+  else
+    (max_squeeze_card + 1) * m + n
+fun unsqueeze p = (p div (max_squeeze_card + 1), p mod (max_squeeze_card + 1))
+
+fun boolify (j, b) = 2 * j + (if b then 0 else 1)
+fun unboolify j = (j div 2, j mod 2 = 0)
+
+fun suc_rel_for_atom_seq (x, tabulate) =
+  (2, suc_rels_base - boolify (squeeze x, tabulate))
+fun atom_seq_for_suc_rel (_, j) = unboolify (~ j + suc_rels_base) |>> unsqueeze
+
 fun is_none_product (Product (r1, r2)) =
     is_none_product r1 orelse is_none_product r2
   | is_none_product None = true
@@ -245,16 +262,18 @@
     fun to_nat j = j - main_j0
     val to_int = int_for_atom (int_card, main_j0)
 
+    val exists_empty_decl = exists (fn DeclOne (_, None) => true | _ => false)
+
     fun s_all _ True = True
       | s_all _ False = False
       | s_all [] f = f
-      | s_all ds (All (ds', f)) = All (ds @ ds', f)
-      | s_all ds f = All (ds, f)
+      | s_all ds (All (ds', f)) = s_all (ds @ ds') f
+      | s_all ds f = if exists_empty_decl ds then True else All (ds, f)
     fun s_exist _ True = True
       | s_exist _ False = False
       | s_exist [] f = f
-      | s_exist ds (Exist (ds', f)) = Exist (ds @ ds', f)
-      | s_exist ds f = Exist (ds, f)
+      | s_exist ds (Exist (ds', f)) = s_exist (ds @ ds') f
+      | s_exist ds f = if exists_empty_decl ds then False else Exist (ds, f)
 
     fun s_formula_let _ True = True
       | s_formula_let _ False = False
diff -r 99440c205e4a -r b730aac14612 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Sun Aug 01 10:26:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Sun Aug 01 17:43:51 2010 +0200
@@ -18,11 +18,12 @@
      explicit_max: int,
      total: bool}
 
-  type dtype_spec =
+  type datatype_spec =
     {typ: typ,
      card: int,
      co: bool,
      standard: bool,
+     self_rec: bool,
      complete: bool * bool,
      concrete: bool * bool,
      deep: bool,
@@ -34,20 +35,22 @@
      card_assigns: (typ * int) list,
      bits: int,
      bisim_depth: int,
-     datatypes: dtype_spec list,
+     datatypes: datatype_spec list,
      ofs: int Typtab.table}
 
-  val datatype_spec : dtype_spec list -> typ -> dtype_spec option
-  val constr_spec : dtype_spec list -> styp -> constr_spec
-  val is_complete_type : dtype_spec list -> bool -> typ -> bool
-  val is_concrete_type : dtype_spec list -> bool -> typ -> bool
-  val is_exact_type : dtype_spec list -> bool -> typ -> bool
+  val is_asymmetric_nondatatype : typ -> bool
+  val datatype_spec : datatype_spec list -> typ -> datatype_spec option
+  val constr_spec : datatype_spec list -> styp -> constr_spec
+  val is_complete_type : datatype_spec list -> bool -> typ -> bool
+  val is_concrete_type : datatype_spec list -> bool -> typ -> bool
+  val is_exact_type : datatype_spec list -> bool -> typ -> bool
   val offset_of_type : int Typtab.table -> typ -> int
   val spec_of_type : scope -> typ -> int * int
   val pretties_for_scope : scope -> bool -> Pretty.T list
   val multiline_string_for_scope : scope -> string
   val scopes_equivalent : scope * scope -> bool
   val scope_less_eq : scope -> scope -> bool
+  val is_self_recursive_constr_type : typ -> bool
   val all_scopes :
     hol_context -> bool -> (typ option * int list) list
     -> (styp option * int list) list -> (styp option * int list) list
@@ -69,11 +72,12 @@
    explicit_max: int,
    total: bool}
 
-type dtype_spec =
+type datatype_spec =
   {typ: typ,
    card: int,
    co: bool,
    standard: bool,
+   self_rec: bool,
    complete: bool * bool,
    concrete: bool * bool,
    deep: bool,
@@ -85,7 +89,7 @@
    card_assigns: (typ * int) list,
    bits: int,
    bisim_depth: int,
-   datatypes: dtype_spec list,
+   datatypes: datatype_spec list,
    ofs: int Typtab.table}
 
 datatype row_kind = Card of typ | Max of styp
@@ -93,11 +97,14 @@
 type row = row_kind * int list
 type block = row list
 
-fun datatype_spec (dtypes : dtype_spec list) T =
+val is_asymmetric_nondatatype =
+  is_iterator_type orf is_integer_type orf is_bit_type
+
+fun datatype_spec (dtypes : datatype_spec list) T =
   List.find (curry (op =) T o #typ) dtypes
 
 fun constr_spec [] x = raise TERM ("Nitpick_Scope.constr_spec", [Const x])
-  | constr_spec ({constrs, ...} :: dtypes : dtype_spec list) (x as (s, T)) =
+  | constr_spec ({constrs, ...} :: dtypes : datatype_spec list) (x as (s, T)) =
     case List.find (curry (op =) (s, body_type T) o (apsnd body_type o #const))
                    constrs of
       SOME c => c
@@ -361,12 +368,11 @@
   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) =
-        if k = 1 orelse is_iterator_type T orelse is_integer_type T
-           orelse is_bit_type T then
+        if k = 1 orelse is_asymmetric_nondatatype T then
           aux next reusable assigns
         else if length (these (Option.map #constrs (datatype_spec dtypes T)))
                 > 1 then
@@ -376,7 +382,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
@@ -438,6 +444,7 @@
     val self_recs = map (is_self_recursive_constr_type o snd) xs
     val (num_self_recs, num_non_self_recs) =
       List.partition I self_recs |> pairself length
+    val self_rec = num_self_recs > 0
     fun is_complete facto =
       has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T
     fun is_concrete facto =
@@ -454,8 +461,8 @@
                                 num_non_self_recs)
                (sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
   in
-    {typ = T, card = card, co = co, standard = standard, complete = complete,
-     concrete = concrete, deep = deep, constrs = constrs}
+    {typ = T, card = card, co = co, standard = standard, self_rec = self_rec,
+     complete = complete, concrete = concrete, deep = deep, constrs = constrs}
   end
 
 fun scope_from_descriptor (hol_ctxt as {ctxt, stds, ...}) binarize deep_dataTs
@@ -473,7 +480,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 _ _ [] = []