src/HOL/Tools/Nitpick/nitpick_kodkod.ML
author blanchet
Mon Mar 03 22:33:22 2014 +0100 (2014-03-03)
changeset 55888 cac1add157e8
parent 54632 7a14f831d02d
child 55889 6bfbec3dff62
permissions -rw-r--r--
removed nonstandard models from Nitpick
     1 (*  Title:      HOL/Tools/Nitpick/nitpick_kodkod.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2008, 2009, 2010
     4 
     5 Kodkod problem generator part of Kodkod.
     6 *)
     7 
     8 signature NITPICK_KODKOD =
     9 sig
    10   type hol_context = Nitpick_HOL.hol_context
    11   type datatype_spec = Nitpick_Scope.datatype_spec
    12   type kodkod_constrs = Nitpick_Peephole.kodkod_constrs
    13   type nut = Nitpick_Nut.nut
    14 
    15   structure NameTable : TABLE
    16 
    17   val univ_card :
    18     int -> int -> int -> Kodkod.bound list -> Kodkod.formula -> int
    19   val check_bits : int -> Kodkod.formula -> unit
    20   val check_arity : string -> int -> int -> unit
    21   val kk_tuple : bool -> int -> int list -> Kodkod.tuple
    22   val tuple_set_from_atom_schema : (int * int) list -> Kodkod.tuple_set
    23   val sequential_int_bounds : int -> Kodkod.int_bound list
    24   val pow_of_two_int_bounds : int -> int -> Kodkod.int_bound list
    25   val bounds_and_axioms_for_built_in_rels_in_formulas :
    26     bool -> int -> int -> int -> int -> Kodkod.formula list
    27     -> Kodkod.bound list * Kodkod.formula list
    28   val bound_for_plain_rel : Proof.context -> bool -> nut -> Kodkod.bound
    29   val bound_for_sel_rel :
    30     Proof.context -> bool -> (typ * (nut * int) list option) list
    31     -> datatype_spec list -> nut -> Kodkod.bound
    32   val merge_bounds : Kodkod.bound list -> Kodkod.bound list
    33   val kodkod_formula_from_nut :
    34     int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
    35   val needed_values_for_datatype :
    36     nut list -> int Typtab.table -> datatype_spec -> (nut * int) list option
    37   val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
    38   val declarative_axioms_for_datatypes :
    39     hol_context -> bool -> nut list -> (typ * (nut * int) list option) list
    40     -> int -> int -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
    41     -> datatype_spec list -> Kodkod.formula list
    42 end;
    43 
    44 structure Nitpick_Kodkod : NITPICK_KODKOD =
    45 struct
    46 
    47 open Nitpick_Util
    48 open Nitpick_HOL
    49 open Nitpick_Scope
    50 open Nitpick_Peephole
    51 open Nitpick_Rep
    52 open Nitpick_Nut
    53 
    54 structure KK = Kodkod
    55 
    56 fun pull x xs = x :: filter_out (curry (op =) x) xs
    57 
    58 fun is_datatype_acyclic ({co = false, deep = true, ...} : datatype_spec) = true
    59   | is_datatype_acyclic _ = false
    60 
    61 fun flip_nums n = index_seq 1 n @ [0] |> map KK.Num
    62 
    63 fun univ_card nat_card int_card main_j0 bounds formula =
    64   let
    65     fun rel_expr_func r k =
    66       Int.max (k, case r of
    67                     KK.Atom j => j + 1
    68                   | KK.AtomSeq (k', j0) => j0 + k'
    69                   | _ => 0)
    70     fun tuple_func t k =
    71       case t of
    72         KK.Tuple js => fold Integer.max (map (Integer.add 1) js) k
    73       | _ => k
    74     fun tuple_set_func ts k =
    75       Int.max (k, case ts of KK.TupleAtomSeq (k', j0) => j0 + k' | _ => 0)
    76     val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func,
    77                   int_expr_func = K I}
    78     val tuple_F = {tuple_func = tuple_func, tuple_set_func = tuple_set_func}
    79     val card = fold (KK.fold_bound expr_F tuple_F) bounds 1
    80                |> KK.fold_formula expr_F formula
    81   in Int.max (main_j0 + fold Integer.max [2, nat_card, int_card] 0, card) end
    82 
    83 fun check_bits bits formula =
    84   let
    85     fun int_expr_func (KK.Num k) () =
    86         if is_twos_complement_representable bits k then
    87           ()
    88         else
    89           raise TOO_SMALL ("Nitpick_Kodkod.check_bits",
    90                            "\"bits\" value " ^ string_of_int bits ^
    91                            " too small for problem")
    92       | int_expr_func _ () = ()
    93     val expr_F = {formula_func = K I, rel_expr_func = K I,
    94                   int_expr_func = int_expr_func}
    95   in KK.fold_formula expr_F formula () end
    96 
    97 fun check_arity guilty_party univ_card n =
    98   if n > KK.max_arity univ_card then
    99     raise TOO_LARGE ("Nitpick_Kodkod.check_arity",
   100                      "arity " ^ string_of_int n ^
   101                      (if guilty_party = "" then
   102                         ""
   103                       else
   104                         " of Kodkod relation associated with " ^
   105                         quote (original_name guilty_party)) ^
   106                      " too large for a universe of size " ^
   107                      string_of_int univ_card)
   108   else
   109     ()
   110 
   111 fun kk_tuple debug univ_card js =
   112   if debug then
   113     KK.Tuple js
   114   else
   115     KK.TupleIndex (length js,
   116                    fold (fn j => fn accum => accum * univ_card + j) js 0)
   117 
   118 (* This code is not just a silly optimization: It works around a limitation in
   119    Kodkodi, whereby {} (i.e., KK.TupleProduct) is always given the cardinality
   120    of the bound in which it appears, resulting in Kodkod arity errors. *)
   121 fun tuple_product (ts as KK.TupleSet []) _ = ts
   122   | tuple_product _ (ts as KK.TupleSet []) = ts
   123   | tuple_product ts1 ts2 = KK.TupleProduct (ts1, ts2)
   124 
   125 val tuple_set_from_atom_schema = fold1 tuple_product o map KK.TupleAtomSeq
   126 val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep
   127 
   128 val single_atom = KK.TupleSet o single o KK.Tuple o single
   129 fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))]
   130 fun pow_of_two_int_bounds bits j0 =
   131   let
   132     fun aux 0  _ _ = []
   133       | aux 1 pow_of_two j = [(SOME (~ pow_of_two), [single_atom j])]
   134       | aux iter pow_of_two j =
   135         (SOME pow_of_two, [single_atom j]) ::
   136         aux (iter - 1) (2 * pow_of_two) (j + 1)
   137   in aux (bits + 1) 1 j0 end
   138 
   139 fun built_in_rels_in_formulas formulas =
   140   let
   141     fun rel_expr_func (KK.Rel (x as (_, j))) =
   142         (j < 0 andalso x <> unsigned_bit_word_sel_rel andalso
   143          x <> signed_bit_word_sel_rel)
   144         ? insert (op =) x
   145       | rel_expr_func _ = I
   146     val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func,
   147                   int_expr_func = K I}
   148   in fold (KK.fold_formula expr_F) formulas [] end
   149 
   150 val max_table_size = 65536
   151 
   152 fun check_table_size k =
   153   if k > max_table_size then
   154     raise TOO_LARGE ("Nitpick_Kodkod.check_table_size",
   155                      "precomputed table too large (" ^ string_of_int k ^ ")")
   156   else
   157     ()
   158 
   159 fun tabulate_func1 debug univ_card (k, j0) f =
   160   (check_table_size k;
   161    map_filter (fn j1 => let val j2 = f j1 in
   162                           if j2 >= 0 then
   163                             SOME (kk_tuple debug univ_card [j1 + j0, j2 + j0])
   164                           else
   165                             NONE
   166                         end) (index_seq 0 k))
   167 fun tabulate_op2 debug univ_card (k, j0) res_j0 f =
   168   (check_table_size (k * k);
   169    map_filter (fn j => let
   170                          val j1 = j div k
   171                          val j2 = j - j1 * k
   172                          val j3 = f (j1, j2)
   173                        in
   174                          if j3 >= 0 then
   175                            SOME (kk_tuple debug univ_card
   176                                           [j1 + j0, j2 + j0, j3 + res_j0])
   177                          else
   178                            NONE
   179                        end) (index_seq 0 (k * k)))
   180 fun tabulate_op2_2 debug univ_card (k, j0) res_j0 f =
   181   (check_table_size (k * k);
   182    map_filter (fn j => let
   183                          val j1 = j div k
   184                          val j2 = j - j1 * k
   185                          val (j3, j4) = f (j1, j2)
   186                        in
   187                          if j3 >= 0 andalso j4 >= 0 then
   188                            SOME (kk_tuple debug univ_card
   189                                           [j1 + j0, j2 + j0, j3 + res_j0,
   190                                            j4 + res_j0])
   191                          else
   192                            NONE
   193                        end) (index_seq 0 (k * k)))
   194 fun tabulate_nat_op2 debug univ_card (k, j0) f =
   195   tabulate_op2 debug univ_card (k, j0) j0 (atom_for_nat (k, 0) o f)
   196 fun tabulate_int_op2 debug univ_card (k, j0) f =
   197   tabulate_op2 debug univ_card (k, j0) j0
   198                (atom_for_int (k, 0) o f o pairself (int_for_atom (k, 0)))
   199 fun tabulate_int_op2_2 debug univ_card (k, j0) f =
   200   tabulate_op2_2 debug univ_card (k, j0) j0
   201                  (pairself (atom_for_int (k, 0)) o f
   202                   o pairself (int_for_atom (k, 0)))
   203 
   204 fun isa_div (m, n) = m div n handle General.Div => 0
   205 fun isa_mod (m, n) = m mod n handle General.Div => m
   206 fun isa_gcd (m, 0) = m
   207   | isa_gcd (m, n) = isa_gcd (n, isa_mod (m, n))
   208 fun isa_lcm (m, n) = isa_div (m * n, isa_gcd (m, n))
   209 val isa_zgcd = isa_gcd o pairself abs
   210 fun isa_norm_frac (m, n) =
   211   if n < 0 then isa_norm_frac (~m, ~n)
   212   else if m = 0 orelse n = 0 then (0, 1)
   213   else let val p = isa_zgcd (m, n) in (isa_div (m, p), isa_div (n, p)) end
   214 
   215 fun tabulate_built_in_rel debug univ_card nat_card int_card j0
   216                           (x as (n, _)) =
   217   (check_arity "" univ_card n;
   218    if x = not3_rel then
   219      ("not3", tabulate_func1 debug univ_card (2, j0) (curry (op -) 1))
   220    else if x = suc_rel then
   221      ("suc", tabulate_func1 debug univ_card (univ_card - j0 - 1, j0)
   222                             (Integer.add 1))
   223    else if x = nat_add_rel then
   224      ("nat_add", tabulate_nat_op2 debug univ_card (nat_card, j0) (op +))
   225    else if x = int_add_rel then
   226      ("int_add", tabulate_int_op2 debug univ_card (int_card, j0) (op +))
   227    else if x = nat_subtract_rel then
   228      ("nat_subtract",
   229       tabulate_op2 debug univ_card (nat_card, j0) j0 (uncurry nat_minus))
   230    else if x = int_subtract_rel then
   231      ("int_subtract", tabulate_int_op2 debug univ_card (int_card, j0) (op -))
   232    else if x = nat_multiply_rel then
   233      ("nat_multiply", tabulate_nat_op2 debug univ_card (nat_card, j0) (op * ))
   234    else if x = int_multiply_rel then
   235      ("int_multiply", tabulate_int_op2 debug univ_card (int_card, j0) (op * ))
   236    else if x = nat_divide_rel then
   237      ("nat_divide", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_div)
   238    else if x = int_divide_rel then
   239      ("int_divide", tabulate_int_op2 debug univ_card (int_card, j0) isa_div)
   240    else if x = nat_less_rel then
   241      ("nat_less", tabulate_nat_op2 debug univ_card (nat_card, j0)
   242                                    (int_from_bool o op <))
   243    else if x = int_less_rel then
   244      ("int_less", tabulate_int_op2 debug univ_card (int_card, j0)
   245                                    (int_from_bool o op <))
   246    else if x = gcd_rel then
   247      ("gcd", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_gcd)
   248    else if x = lcm_rel then
   249      ("lcm", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_lcm)
   250    else if x = norm_frac_rel then
   251      ("norm_frac", tabulate_int_op2_2 debug univ_card (int_card, j0)
   252                                       isa_norm_frac)
   253    else
   254      raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation"))
   255 
   256 fun bound_for_built_in_rel debug univ_card nat_card int_card main_j0
   257                            (x as (n, j)) =
   258   if n = 2 andalso j <= suc_rels_base then
   259     let val (y as (k, j0), tabulate) = atom_seq_for_suc_rel x in
   260       ([(x, "suc")],
   261        if tabulate then
   262          [KK.TupleSet (tabulate_func1 debug univ_card (k - 1, j0)
   263                        (Integer.add 1))]
   264        else
   265          [KK.TupleSet [], tuple_set_from_atom_schema [y, y]])
   266     end
   267   else
   268     let
   269       val (nick, ts) = tabulate_built_in_rel debug univ_card nat_card int_card
   270                                              main_j0 x
   271     in ([(x, nick)], [KK.TupleSet ts]) end
   272 
   273 fun axiom_for_built_in_rel (x as (n, j)) =
   274   if n = 2 andalso j <= suc_rels_base then
   275     let val (y as (k, j0), tabulate) = atom_seq_for_suc_rel x in
   276       if tabulate then
   277         NONE
   278       else if k < 2 then
   279         SOME (KK.No (KK.Rel x))
   280       else
   281         SOME (KK.TotalOrdering (x, KK.AtomSeq y, KK.Atom j0, KK.Atom (j0 + 1)))
   282     end
   283   else
   284     NONE
   285 fun bounds_and_axioms_for_built_in_rels_in_formulas debug univ_card nat_card
   286                                                     int_card main_j0 formulas =
   287   let val rels = built_in_rels_in_formulas formulas in
   288     (map (bound_for_built_in_rel debug univ_card nat_card int_card main_j0)
   289          rels,
   290      map_filter axiom_for_built_in_rel rels)
   291   end
   292 
   293 fun bound_comment ctxt debug nick T R =
   294   short_name nick ^
   295   (if debug then " :: " ^ unyxml (Syntax.string_of_typ ctxt T) else "") ^
   296   " : " ^ string_for_rep R
   297 
   298 fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) =
   299     ([(x, bound_comment ctxt debug nick T R)],
   300      if nick = @{const_name bisim_iterator_max} then
   301        case R of
   302          Atom (k, j0) => [single_atom (k - 1 + j0)]
   303        | _ => raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
   304      else
   305        [KK.TupleSet [], upper_bound_for_rep R])
   306   | bound_for_plain_rel _ _ u =
   307     raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
   308 
   309 fun is_datatype_nat_like ({typ, constrs, ...} : datatype_spec) =
   310   case constrs of
   311     [_, _] =>
   312     (case constrs |> map (snd o #const) |> List.partition is_fun_type of
   313        ([Type (_, Ts1)], [T2]) => forall (curry (op =) typ) (T2 :: Ts1)
   314      | _ => false)
   315   | _ => false
   316 
   317 fun needed_values need_vals T =
   318   AList.lookup (op =) need_vals T |> the_default NONE |> these
   319 
   320 fun all_values_are_needed need_vals ({typ, card, ...} : datatype_spec) =
   321   length (needed_values need_vals typ) = card
   322 
   323 fun is_sel_of_constr x (Construct (sel_us, _, _, _), _) =
   324     exists (fn FreeRel (x', _, _, _) => x = x' | _ => false) sel_us
   325   | is_sel_of_constr _ _ = false
   326 
   327 fun bound_for_sel_rel ctxt debug need_vals dtypes
   328         (FreeRel (x, T as Type (@{type_name fun}, [T1, T2]),
   329                   R as Func (Atom (_, j0), R2), nick)) =
   330     let
   331       val constr_s = original_name nick
   332       val {delta, epsilon, exclusive, explicit_max, ...} =
   333         constr_spec dtypes (constr_s, T1)
   334       val dtype as {card, ...} = datatype_spec dtypes T1 |> the
   335       val T1_need_vals = needed_values need_vals T1
   336     in
   337       ([(x, bound_comment ctxt debug nick T R)],
   338        let
   339          val discr = (R2 = Formula Neut)
   340          val complete_need_vals = (length T1_need_vals = card)
   341          val (my_need_vals, other_need_vals) =
   342            T1_need_vals |> List.partition (is_sel_of_constr x)
   343          fun atom_seq_for_self_rec j =
   344            if is_datatype_nat_like dtype then (1, j + j0 - 1) else (j, j0)
   345          fun exact_bound_for_perhaps_needy_atom j =
   346            case AList.find (op =) my_need_vals j of
   347              [constr_u] =>
   348              let
   349                val n = sel_no_from_name nick
   350                val arg_u =
   351                  case constr_u of
   352                    Construct (_, _, _, arg_us) => nth arg_us n
   353                  | _ => raise Fail "expected \"Construct\""
   354                val T2_need_vals = needed_values need_vals T2
   355              in
   356                case AList.lookup (op =) T2_need_vals arg_u of
   357                  SOME arg_j => SOME (KK.TupleAtomSeq (1, arg_j))
   358                | _ => NONE
   359              end
   360            | _ => NONE
   361          fun n_fold_tuple_union [] = KK.TupleSet []
   362            | n_fold_tuple_union (ts :: tss) =
   363              fold (curry (KK.TupleUnion o swap)) tss ts
   364          fun tuple_perhaps_needy_atom upper j =
   365            single_atom j
   366            |> not discr
   367               ? (fn ts => tuple_product ts
   368                               (case exact_bound_for_perhaps_needy_atom j of
   369                                  SOME ts => ts
   370                                | NONE => if upper then upper_bound_for_rep R2
   371                                          else KK.TupleSet []))
   372          fun bound_tuples upper =
   373            if null T1_need_vals then
   374              if upper then
   375                KK.TupleAtomSeq (epsilon - delta, delta + j0)
   376                |> not discr
   377                   ? (fn ts => tuple_product ts (upper_bound_for_rep R2))
   378              else
   379                KK.TupleSet []
   380            else
   381              (if complete_need_vals then
   382                 my_need_vals |> map snd
   383               else
   384                 index_seq (delta + j0) (epsilon - delta)
   385                 |> filter_out (member (op = o apsnd snd) other_need_vals))
   386              |> map (tuple_perhaps_needy_atom upper)
   387              |> n_fold_tuple_union
   388        in
   389          if explicit_max = 0 orelse
   390             (complete_need_vals andalso null my_need_vals) then
   391            [KK.TupleSet []]
   392          else
   393            if discr then
   394              [bound_tuples true]
   395              |> not (exclusive orelse all_values_are_needed need_vals dtype)
   396                 ? cons (KK.TupleSet [])
   397            else
   398              [bound_tuples false,
   399               if T1 = T2 andalso epsilon > delta andalso
   400                  is_datatype_acyclic dtype then
   401                 index_seq delta (epsilon - delta)
   402                 |> map (fn j => tuple_product (KK.TupleSet [KK.Tuple [j + j0]])
   403                                     (KK.TupleAtomSeq (atom_seq_for_self_rec j)))
   404                 |> n_fold_tuple_union
   405               else
   406                 bound_tuples true]
   407              |> distinct (op =)
   408          end)
   409     end
   410   | bound_for_sel_rel _ _ _ _ u =
   411     raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u])
   412 
   413 fun merge_bounds bs =
   414   let
   415     fun arity (zs, _) = fst (fst (hd zs))
   416     fun add_bound ds b [] = List.revAppend (ds, [b])
   417       | add_bound ds b (c :: cs) =
   418         if arity b = arity c andalso snd b = snd c then
   419           List.revAppend (ds, (fst c @ fst b, snd c) :: cs)
   420         else
   421           add_bound (c :: ds) b cs
   422   in fold (add_bound []) bs [] end
   423 
   424 fun unary_var_seq j0 n = map (curry KK.Var 1) (index_seq j0 n)
   425 
   426 val singleton_from_combination = foldl1 KK.Product o map KK.Atom
   427 fun all_singletons_for_rep R =
   428   if is_lone_rep R then
   429     all_combinations_for_rep R |> map singleton_from_combination
   430   else
   431     raise REP ("Nitpick_Kodkod.all_singletons_for_rep", [R])
   432 
   433 fun unpack_products (KK.Product (r1, r2)) =
   434     unpack_products r1 @ unpack_products r2
   435   | unpack_products r = [r]
   436 fun unpack_joins (KK.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2
   437   | unpack_joins r = [r]
   438 
   439 val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep
   440 fun full_rel_for_rep R =
   441   case atom_schema_of_rep R of
   442     [] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R])
   443   | schema => foldl1 KK.Product (map KK.AtomSeq schema)
   444 
   445 fun decls_for_atom_schema j0 schema =
   446   map2 (fn j => fn x => KK.DeclOne ((1, j), KK.AtomSeq x))
   447        (index_seq j0 (length schema)) schema
   448 
   449 fun d_n_ary_function ({kk_all, kk_join, kk_lone, kk_one, ...} : kodkod_constrs)
   450                      R r =
   451   let val body_R = body_rep R in
   452     if is_lone_rep body_R then
   453       let
   454         val binder_schema = atom_schema_of_reps (binder_reps R)
   455         val body_schema = atom_schema_of_rep body_R
   456         val one = is_one_rep body_R
   457         val opt_x = case r of KK.Rel x => SOME x | _ => NONE
   458       in
   459         if opt_x <> NONE andalso length binder_schema = 1 andalso
   460            length body_schema = 1 then
   461           (if one then KK.Function else KK.Functional)
   462               (the opt_x, KK.AtomSeq (hd binder_schema),
   463                KK.AtomSeq (hd body_schema))
   464         else
   465           let
   466             val decls = decls_for_atom_schema ~1 binder_schema
   467             val vars = unary_var_seq ~1 (length binder_schema)
   468             val kk_xone = if one then kk_one else kk_lone
   469           in kk_all decls (kk_xone (fold kk_join vars r)) end
   470       end
   471     else
   472       KK.True
   473   end
   474 fun kk_n_ary_function kk R (r as KK.Rel x) =
   475     if not (is_opt_rep R) then
   476       if x = suc_rel then
   477         KK.False
   478       else if x = nat_add_rel then
   479         formula_for_bool (card_of_rep (body_rep R) = 1)
   480       else if x = nat_multiply_rel then
   481         formula_for_bool (card_of_rep (body_rep R) <= 2)
   482       else
   483         d_n_ary_function kk R r
   484     else if x = nat_subtract_rel then
   485       KK.True
   486     else
   487       d_n_ary_function kk R r
   488   | kk_n_ary_function kk R r = d_n_ary_function kk R r
   489 
   490 fun kk_disjoint_sets _ [] = KK.True
   491   | kk_disjoint_sets (kk as {kk_and, kk_no, kk_intersect, ...} : kodkod_constrs)
   492                      (r :: rs) =
   493     fold (kk_and o kk_no o kk_intersect r) rs (kk_disjoint_sets kk rs)
   494 
   495 fun basic_rel_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r =
   496   if inline_rel_expr r then
   497     f r
   498   else
   499     let val x = (KK.arity_of_rel_expr r, j) in
   500       kk_rel_let [KK.AssignRelReg (x, r)] (f (KK.RelReg x))
   501     end
   502 val single_rel_rel_let = basic_rel_rel_let 0
   503 fun double_rel_rel_let kk f r1 r2 =
   504   single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1
   505 fun triple_rel_rel_let kk f r1 r2 r3 =
   506   double_rel_rel_let kk
   507       (fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2
   508 
   509 fun atom_from_formula ({kk_rel_if, ...} : kodkod_constrs) j0 f =
   510   kk_rel_if f (KK.Atom (j0 + 1)) (KK.Atom j0)
   511 fun rel_expr_from_formula kk R f =
   512   case unopt_rep R of
   513     Atom (2, j0) => atom_from_formula kk j0 f
   514   | _ => raise REP ("Nitpick_Kodkod.rel_expr_from_formula", [R])
   515 
   516 fun unpack_vect_in_chunks ({kk_project_seq, ...} : kodkod_constrs) chunk_arity
   517                           num_chunks r =
   518   List.tabulate (num_chunks, fn j => kk_project_seq r (j * chunk_arity)
   519                                                     chunk_arity)
   520 
   521 fun kk_n_fold_join
   522         (kk as {kk_intersect, kk_product, kk_join, kk_project_seq, ...}) one R1
   523         res_R r1 r2 =
   524   case arity_of_rep R1 of
   525     1 => kk_join r1 r2
   526   | arity1 =>
   527     let val unpacked_rs1 = unpack_products r1 in
   528       if one andalso length unpacked_rs1 = arity1 then
   529         fold kk_join unpacked_rs1 r2
   530       else if one andalso inline_rel_expr r1 then
   531         fold kk_join (unpack_vect_in_chunks kk 1 arity1 r1) r2
   532       else
   533         kk_project_seq
   534             (kk_intersect (kk_product r1 (full_rel_for_rep res_R)) r2)
   535             arity1 (arity_of_rep res_R)
   536     end
   537 
   538 fun kk_case_switch (kk as {kk_union, kk_product, ...}) R1 R2 r rs1 rs2 =
   539   if rs1 = rs2 then r
   540   else kk_n_fold_join kk true R1 R2 r (fold1 kk_union (map2 kk_product rs1 rs2))
   541 
   542 val lone_rep_fallback_max_card = 4096
   543 val some_j0 = 0
   544 
   545 fun lone_rep_fallback kk new_R old_R r =
   546   if old_R = new_R then
   547     r
   548   else
   549     let val card = card_of_rep old_R in
   550       if is_lone_rep old_R andalso is_lone_rep new_R andalso
   551          card = card_of_rep new_R then
   552         if card >= lone_rep_fallback_max_card then
   553           raise TOO_LARGE ("Nitpick_Kodkod.lone_rep_fallback",
   554                            "too high cardinality (" ^ string_of_int card ^ ")")
   555         else
   556           kk_case_switch kk old_R new_R r (all_singletons_for_rep old_R)
   557                          (all_singletons_for_rep new_R)
   558       else
   559         raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R])
   560     end
   561 and atom_from_rel_expr kk x old_R r =
   562   case old_R of
   563     Func (R1, R2) =>
   564     let
   565       val dom_card = card_of_rep R1
   566       val R2' = case R2 of Atom _ => R2 | _ => Atom (card_of_rep R2, some_j0)
   567     in
   568       atom_from_rel_expr kk x (Vect (dom_card, R2'))
   569                          (vect_from_rel_expr kk dom_card R2' old_R r)
   570     end
   571   | Opt _ => raise REP ("Nitpick_Kodkod.atom_from_rel_expr", [old_R])
   572   | _ => lone_rep_fallback kk (Atom x) old_R r
   573 and struct_from_rel_expr kk Rs old_R r =
   574   case old_R of
   575     Atom _ => lone_rep_fallback kk (Struct Rs) old_R r
   576   | Struct Rs' =>
   577     if Rs' = Rs then
   578       r
   579     else if map card_of_rep Rs' = map card_of_rep Rs then
   580       let
   581         val old_arities = map arity_of_rep Rs'
   582         val old_offsets = offset_list old_arities
   583         val old_rs = map2 (#kk_project_seq kk r) old_offsets old_arities
   584       in
   585         fold1 (#kk_product kk)
   586               (map3 (rel_expr_from_rel_expr kk) Rs Rs' old_rs)
   587       end
   588     else
   589       lone_rep_fallback kk (Struct Rs) old_R r
   590   | _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R])
   591 and vect_from_rel_expr kk k R old_R r =
   592   case old_R of
   593     Atom _ => lone_rep_fallback kk (Vect (k, R)) old_R r
   594   | Vect (k', R') =>
   595     if k = k' andalso R = R' then r
   596     else lone_rep_fallback kk (Vect (k, R)) old_R r
   597   | Func (R1, Formula Neut) =>
   598     if k = card_of_rep R1 then
   599       fold1 (#kk_product kk)
   600             (map (fn arg_r =>
   601                      rel_expr_from_formula kk R (#kk_subset kk arg_r r))
   602                  (all_singletons_for_rep R1))
   603     else
   604       raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R])
   605   | Func (R1, R2) =>
   606     fold1 (#kk_product kk)
   607           (map (fn arg_r =>
   608                    rel_expr_from_rel_expr kk R R2
   609                                          (kk_n_fold_join kk true R1 R2 arg_r r))
   610                (all_singletons_for_rep R1))
   611   | _ => raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R])
   612 and func_from_no_opt_rel_expr kk R1 R2 (Atom x) r =
   613     let
   614       val dom_card = card_of_rep R1
   615       val R2' = case R2 of Atom _ => R2 | _ => Atom (card_of_rep R2, some_j0)
   616     in
   617       func_from_no_opt_rel_expr kk R1 R2 (Vect (dom_card, R2'))
   618                                 (vect_from_rel_expr kk dom_card R2' (Atom x) r)
   619     end
   620   | func_from_no_opt_rel_expr kk R1 (Formula Neut) old_R r =
   621     (case old_R of
   622        Vect (k, Atom (2, j0)) =>
   623        let
   624          val args_rs = all_singletons_for_rep R1
   625          val vals_rs = unpack_vect_in_chunks kk 1 k r
   626          fun empty_or_singleton_set_for arg_r val_r =
   627            #kk_join kk val_r (#kk_product kk (KK.Atom (j0 + 1)) arg_r)
   628        in
   629          fold1 (#kk_union kk) (map2 empty_or_singleton_set_for args_rs vals_rs)
   630        end
   631      | Func (R1', Formula Neut) =>
   632        if R1 = R1' then
   633          r
   634        else
   635          let
   636            val schema = atom_schema_of_rep R1
   637            val r1 = fold1 (#kk_product kk) (unary_var_seq ~1 (length schema))
   638                     |> rel_expr_from_rel_expr kk R1' R1
   639            val kk_xeq = (if is_one_rep R1' then #kk_subset else #kk_rel_eq) kk
   640          in
   641            #kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r)
   642          end
   643      | Func (R1', Atom (2, j0)) =>
   644        func_from_no_opt_rel_expr kk R1 (Formula Neut)
   645            (Func (R1', Formula Neut)) (#kk_join kk r (KK.Atom (j0 + 1)))
   646      | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
   647                        [old_R, Func (R1, Formula Neut)]))
   648   | func_from_no_opt_rel_expr kk R1 R2 old_R r =
   649     case old_R of
   650       Vect (k, R) =>
   651       let
   652         val args_rs = all_singletons_for_rep R1
   653         val vals_rs = unpack_vect_in_chunks kk (arity_of_rep R) k r
   654                       |> map (rel_expr_from_rel_expr kk R2 R)
   655       in fold1 (#kk_union kk) (map2 (#kk_product kk) args_rs vals_rs) end
   656     | Func (R1', Formula Neut) =>
   657       (case R2 of
   658          Atom (x as (2, j0)) =>
   659          let val schema = atom_schema_of_rep R1 in
   660            if length schema = 1 then
   661              #kk_override kk (#kk_product kk (KK.AtomSeq (hd schema))
   662                                              (KK.Atom j0))
   663                              (#kk_product kk r (KK.Atom (j0 + 1)))
   664            else
   665              let
   666                val r1 = fold1 (#kk_product kk) (unary_var_seq ~1 (length schema))
   667                         |> rel_expr_from_rel_expr kk R1' R1
   668                val r2 = KK.Var (1, ~(length schema) - 1)
   669                val r3 = atom_from_formula kk j0 (#kk_subset kk r1 r)
   670              in
   671                #kk_comprehension kk (decls_for_atom_schema ~1 (schema @ [x]))
   672                                  (#kk_subset kk r2 r3)
   673              end
   674            end
   675          | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
   676                            [old_R, Func (R1, R2)]))
   677     | Func (R1', R2') =>
   678       if R1 = R1' andalso R2 = R2' then
   679         r
   680       else
   681         let
   682           val dom_schema = atom_schema_of_rep R1
   683           val ran_schema = atom_schema_of_rep R2
   684           val dom_prod = fold1 (#kk_product kk)
   685                                (unary_var_seq ~1 (length dom_schema))
   686                          |> rel_expr_from_rel_expr kk R1' R1
   687           val ran_prod = fold1 (#kk_product kk)
   688                                (unary_var_seq (~(length dom_schema) - 1)
   689                                               (length ran_schema))
   690                          |> rel_expr_from_rel_expr kk R2' R2
   691           val app = kk_n_fold_join kk true R1' R2' dom_prod r
   692           val kk_xeq = (if is_one_rep R2' then #kk_subset else #kk_rel_eq) kk
   693         in
   694           #kk_comprehension kk (decls_for_atom_schema ~1
   695                                                       (dom_schema @ ran_schema))
   696                                (kk_xeq ran_prod app)
   697         end
   698     | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
   699                       [old_R, Func (R1, R2)])
   700 and rel_expr_from_rel_expr kk new_R old_R r =
   701   let
   702     val unopt_old_R = unopt_rep old_R
   703     val unopt_new_R = unopt_rep new_R
   704   in
   705     if unopt_old_R <> old_R andalso unopt_new_R = new_R then
   706       raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", [old_R, new_R])
   707     else if unopt_new_R = unopt_old_R then
   708       r
   709     else
   710       (case unopt_new_R of
   711          Atom x => atom_from_rel_expr kk x
   712        | Struct Rs => struct_from_rel_expr kk Rs
   713        | Vect (k, R') => vect_from_rel_expr kk k R'
   714        | Func (R1, R2) => func_from_no_opt_rel_expr kk R1 R2
   715        | _ => raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr",
   716                          [old_R, new_R]))
   717           unopt_old_R r
   718   end
   719 and rel_expr_to_func kk R1 R2 = rel_expr_from_rel_expr kk (Func (R1, R2))
   720 
   721 fun bit_set_from_atom ({kk_join, ...} : kodkod_constrs) T r =
   722   kk_join r (KK.Rel (if T = @{typ "unsigned_bit word"} then
   723                        unsigned_bit_word_sel_rel
   724                      else
   725                        signed_bit_word_sel_rel))
   726 val int_expr_from_atom = KK.SetSum ooo bit_set_from_atom
   727 fun atom_from_int_expr (kk as {kk_rel_eq, kk_comprehension, ...}
   728                         : kodkod_constrs) T R i =
   729   kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R))
   730                    (kk_rel_eq (bit_set_from_atom kk T (KK.Var (1, ~1)))
   731                               (KK.Bits i))
   732 
   733 fun kodkod_formula_from_nut ofs
   734         (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
   735                 kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
   736                 kk_lone, kk_some, kk_rel_let, kk_rel_if, kk_union,
   737                 kk_difference, kk_intersect, kk_product, kk_join, kk_closure,
   738                 kk_comprehension, kk_project, kk_project_seq, kk_not3,
   739                 kk_nat_less, kk_int_less, ...}) u =
   740   let
   741     val main_j0 = offset_of_type ofs bool_T
   742     val bool_j0 = main_j0
   743     val bool_atom_R = Atom (2, main_j0)
   744     val false_atom = KK.Atom bool_j0
   745     val true_atom = KK.Atom (bool_j0 + 1)
   746     fun formula_from_opt_atom polar j0 r =
   747       case polar of
   748         Neg => kk_not (kk_rel_eq r (KK.Atom j0))
   749       | _ => kk_rel_eq r (KK.Atom (j0 + 1))
   750     val formula_from_atom = formula_from_opt_atom Pos
   751     val unpack_formulas =
   752       map (formula_from_atom bool_j0) oo unpack_vect_in_chunks kk 1
   753     fun kk_vect_set_bool_op connective k r1 r2 =
   754       fold1 kk_and (map2 connective (unpack_formulas k r1)
   755                          (unpack_formulas k r2))
   756     fun to_f u =
   757       case rep_of u of
   758         Formula polar =>
   759         (case u of
   760            Cst (False, _, _) => KK.False
   761          | Cst (True, _, _) => KK.True
   762          | Op1 (Not, _, _, u1) =>
   763            kk_not (to_f_with_polarity (flip_polarity polar) u1)
   764          | Op1 (Finite, _, _, u1) =>
   765            let val opt1 = is_opt_rep (rep_of u1) in
   766              case polar of
   767                Neut =>
   768                if opt1 then raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u])
   769                else KK.True
   770              | Pos => formula_for_bool (not opt1)
   771              | Neg => KK.True
   772            end
   773          | Op1 (IsUnknown, _, _, u1) => kk_no (to_r u1)
   774          | Op1 (Cast, _, _, u1) => to_f_with_polarity polar u1
   775          | Op2 (All, _, _, u1, u2) =>
   776            kk_all (untuple to_decl u1) (to_f_with_polarity polar u2)
   777          | Op2 (Exist, _, _, u1, u2) =>
   778            kk_exist (untuple to_decl u1) (to_f_with_polarity polar u2)
   779          | Op2 (Or, _, _, u1, u2) =>
   780            kk_or (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
   781          | Op2 (And, _, _, u1, u2) =>
   782            kk_and (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
   783          | Op2 (Less, T, Formula polar, u1, u2) =>
   784            formula_from_opt_atom polar bool_j0
   785                (to_r (Op2 (Less, T, Opt bool_atom_R, u1, u2)))
   786          | Op2 (Subset, _, _, u1, u2) =>
   787            let
   788              val dom_T = pseudo_domain_type (type_of u1)
   789              val R1 = rep_of u1
   790              val R2 = rep_of u2
   791              val (dom_R, ran_R) =
   792                case min_rep R1 R2 of
   793                  Func Rp => Rp
   794                | R => (Atom (card_of_domain_from_rep 2 R,
   795                              offset_of_type ofs dom_T),
   796                        if is_opt_rep R then Opt bool_atom_R else Formula Neut)
   797              val set_R = Func (dom_R, ran_R)
   798            in
   799              if not (is_opt_rep ran_R) then
   800                to_set_bool_op kk_implies kk_subset u1 u2
   801              else if polar = Neut then
   802                raise NUT ("Nitpick_Kodkod.to_f (Subset)", [u])
   803              else
   804                let
   805                  (* FIXME: merge with similar code below *)
   806                  fun set_to_r widen u =
   807                    if widen then
   808                      kk_difference (full_rel_for_rep dom_R)
   809                                    (kk_join (to_rep set_R u) false_atom)
   810                    else
   811                      kk_join (to_rep set_R u) true_atom
   812                  val widen1 = (polar = Pos andalso is_opt_rep R1)
   813                  val widen2 = (polar = Neg andalso is_opt_rep R2)
   814                in kk_subset (set_to_r widen1 u1) (set_to_r widen2 u2) end
   815            end
   816          | Op2 (DefEq, _, _, u1, u2) =>
   817            (case min_rep (rep_of u1) (rep_of u2) of
   818               Formula polar =>
   819               kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
   820             | min_R =>
   821               let
   822                 fun args (Op2 (Apply, _, _, u1, u2)) = u2 :: args u1
   823                   | args (Tuple (_, _, us)) = us
   824                   | args _ = []
   825                 val opt_arg_us = filter (is_opt_rep o rep_of) (args u1)
   826               in
   827                 if null opt_arg_us orelse not (is_Opt min_R) orelse
   828                    is_eval_name u1 then
   829                   fold (kk_or o (kk_no o to_r)) opt_arg_us
   830                        (kk_rel_eq (to_rep min_R u1) (to_rep min_R u2))
   831                 else
   832                   kk_subset (to_rep min_R u1) (to_rep min_R u2)
   833               end)
   834          | Op2 (Eq, _, _, u1, u2) =>
   835            (case min_rep (rep_of u1) (rep_of u2) of
   836               Formula polar =>
   837               kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
   838             | min_R =>
   839               if is_opt_rep min_R then
   840                 if polar = Neut then
   841                   (* continuation of hackish optimization *)
   842                   kk_rel_eq (to_rep min_R u1) (to_rep min_R u2)
   843                 else if is_Cst Unrep u1 then
   844                   to_could_be_unrep (polar = Neg) u2
   845                 else if is_Cst Unrep u2 then
   846                   to_could_be_unrep (polar = Neg) u1
   847                 else
   848                   let
   849                     val r1 = to_rep min_R u1
   850                     val r2 = to_rep min_R u2
   851                     val both_opt = forall (is_opt_rep o rep_of) [u1, u2]
   852                   in
   853                     (if polar = Pos then
   854                        if not both_opt then
   855                          kk_rel_eq r1 r2
   856                        else if is_lone_rep min_R andalso
   857                                arity_of_rep min_R = 1 then
   858                          kk_some (kk_intersect r1 r2)
   859                        else
   860                          raise SAME ()
   861                      else
   862                        if is_lone_rep min_R then
   863                          if arity_of_rep min_R = 1 then
   864                            kk_lone (kk_union r1 r2)
   865                          else if not both_opt then
   866                            (r1, r2) |> is_opt_rep (rep_of u2) ? swap
   867                                     |-> kk_subset
   868                          else
   869                            raise SAME ()
   870                        else
   871                          raise SAME ())
   872                     handle SAME () =>
   873                            formula_from_opt_atom polar bool_j0
   874                                (to_guard [u1, u2] bool_atom_R
   875                                          (rel_expr_from_formula kk bool_atom_R
   876                                                             (kk_rel_eq r1 r2)))
   877                   end
   878               else
   879                 let
   880                   val r1 = to_rep min_R u1
   881                   val r2 = to_rep min_R u2
   882                 in
   883                   if is_one_rep min_R then
   884                     let
   885                       val rs1 = unpack_products r1
   886                       val rs2 = unpack_products r2
   887                     in
   888                       if length rs1 = length rs2 andalso
   889                          map KK.arity_of_rel_expr rs1
   890                          = map KK.arity_of_rel_expr rs2 then
   891                         fold1 kk_and (map2 kk_subset rs1 rs2)
   892                       else
   893                         kk_subset r1 r2
   894                     end
   895                   else
   896                     kk_rel_eq r1 r2
   897                 end)
   898          | Op2 (Apply, T, _, u1, u2) =>
   899            (case (polar, rep_of u1) of
   900               (Neg, Func (R, Formula Neut)) => kk_subset (to_opt R u2) (to_r u1)
   901             | _ =>
   902               to_f_with_polarity polar
   903                  (Op2 (Apply, T, Opt (Atom (2, offset_of_type ofs T)), u1, u2)))
   904          | Op3 (Let, _, _, u1, u2, u3) =>
   905            kk_formula_let [to_expr_assign u1 u2] (to_f_with_polarity polar u3)
   906          | Op3 (If, _, _, u1, u2, u3) =>
   907            kk_formula_if (to_f u1) (to_f_with_polarity polar u2)
   908                          (to_f_with_polarity polar u3)
   909          | FormulaReg (j, _, _) => KK.FormulaReg j
   910          | _ => raise NUT ("Nitpick_Kodkod.to_f", [u]))
   911       | Atom (2, j0) => formula_from_atom j0 (to_r u)
   912       | _ => raise NUT ("Nitpick_Kodkod.to_f", [u])
   913     and to_f_with_polarity polar u =
   914       case rep_of u of
   915         Formula _ => to_f u
   916       | Atom (2, j0) => formula_from_atom j0 (to_r u)
   917       | Opt (Atom (2, j0)) => formula_from_opt_atom polar j0 (to_r u)
   918       | _ => raise NUT ("Nitpick_Kodkod.to_f_with_polarity", [u])
   919     and to_r u =
   920       case u of
   921         Cst (False, _, Atom _) => false_atom
   922       | Cst (True, _, Atom _) => true_atom
   923       | Cst (Iden, _, Func (Struct [R1, R2], Formula Neut)) =>
   924         if R1 = R2 andalso arity_of_rep R1 = 1 then
   925           kk_intersect KK.Iden (kk_product (full_rel_for_rep R1) KK.Univ)
   926         else
   927           let
   928             val schema1 = atom_schema_of_rep R1
   929             val schema2 = atom_schema_of_rep R2
   930             val arity1 = length schema1
   931             val arity2 = length schema2
   932             val r1 = fold1 kk_product (unary_var_seq 0 arity1)
   933             val r2 = fold1 kk_product (unary_var_seq arity1 arity2)
   934             val min_R = min_rep R1 R2
   935           in
   936             kk_comprehension
   937                 (decls_for_atom_schema 0 (schema1 @ schema2))
   938                 (kk_rel_eq (rel_expr_from_rel_expr kk min_R R1 r1)
   939                            (rel_expr_from_rel_expr kk min_R R2 r2))
   940           end
   941       | Cst (Iden, _, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0
   942       | Cst (Iden, T as Type (@{type_name set}, [T1]), R as Func (R1, _)) =>
   943         to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut)))
   944       | Cst (Num j, T, R) =>
   945         if is_word_type T then
   946           atom_from_int_expr kk T R (KK.Num j)
   947         else if T = int_T then
   948           case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of
   949             ~1 => if is_opt_rep R then KK.None
   950                   else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])
   951           | j' => KK.Atom j'
   952         else
   953           if j < card_of_rep R then KK.Atom (j + offset_of_type ofs T)
   954           else if is_opt_rep R then KK.None
   955           else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])
   956       | Cst (Unknown, _, R) => empty_rel_for_rep R
   957       | Cst (Unrep, _, R) => empty_rel_for_rep R
   958       | Cst (Suc, T as @{typ "unsigned_bit word => unsigned_bit word"}, R) =>
   959         to_bit_word_unary_op T R (curry KK.Add (KK.Num 1))
   960       | Cst (Suc, @{typ "nat => nat"}, Func (Atom x, _)) =>
   961         kk_intersect (KK.Rel suc_rel) (kk_product KK.Univ (KK.AtomSeq x))
   962       | Cst (Suc, _, Func (Atom _, _)) => KK.Rel suc_rel
   963       | Cst (Add, Type (_, [@{typ nat}, _]), _) => KK.Rel nat_add_rel
   964       | Cst (Add, Type (_, [@{typ int}, _]), _) => KK.Rel int_add_rel
   965       | Cst (Add, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
   966         to_bit_word_binary_op T R NONE (SOME (curry KK.Add))
   967       | Cst (Add, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
   968         to_bit_word_binary_op T R
   969             (SOME (fn i1 => fn i2 => fn i3 =>
   970                  kk_implies (KK.LE (KK.Num 0, KK.BitXor (i1, i2)))
   971                             (KK.LE (KK.Num 0, KK.BitXor (i2, i3)))))
   972             (SOME (curry KK.Add))
   973       | Cst (Subtract, Type (_, [@{typ nat}, _]), _) =>
   974         KK.Rel nat_subtract_rel
   975       | Cst (Subtract, Type (_, [@{typ int}, _]), _) =>
   976         KK.Rel int_subtract_rel
   977       | Cst (Subtract, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
   978         to_bit_word_binary_op T R NONE
   979             (SOME (fn i1 => fn i2 =>
   980                       KK.IntIf (KK.LE (i1, i2), KK.Num 0, KK.Sub (i1, i2))))
   981       | Cst (Subtract, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
   982         to_bit_word_binary_op T R
   983             (SOME (fn i1 => fn i2 => fn i3 =>
   984                  kk_implies (KK.LT (KK.BitXor (i1, i2), KK.Num 0))
   985                             (KK.LT (KK.BitXor (i2, i3), KK.Num 0))))
   986             (SOME (curry KK.Sub))
   987       | Cst (Multiply, Type (_, [@{typ nat}, _]), _) =>
   988         KK.Rel nat_multiply_rel
   989       | Cst (Multiply, Type (_, [@{typ int}, _]), _) =>
   990         KK.Rel int_multiply_rel
   991       | Cst (Multiply,
   992              T as Type (_, [Type (@{type_name word}, [bit_T]), _]), R) =>
   993         to_bit_word_binary_op T R
   994             (SOME (fn i1 => fn i2 => fn i3 =>
   995                 kk_or (KK.IntEq (i2, KK.Num 0))
   996                       (KK.IntEq (KK.Div (i3, i2), i1)
   997                        |> bit_T = @{typ signed_bit}
   998                           ? kk_and (KK.LE (KK.Num 0,
   999                                            foldl1 KK.BitAnd [i1, i2, i3])))))
  1000             (SOME (curry KK.Mult))
  1001       | Cst (Divide, Type (_, [@{typ nat}, _]), _) => KK.Rel nat_divide_rel
  1002       | Cst (Divide, Type (_, [@{typ int}, _]), _) => KK.Rel int_divide_rel
  1003       | Cst (Divide, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
  1004         to_bit_word_binary_op T R NONE
  1005             (SOME (fn i1 => fn i2 =>
  1006                       KK.IntIf (KK.IntEq (i2, KK.Num 0),
  1007                                 KK.Num 0, KK.Div (i1, i2))))
  1008       | Cst (Divide, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
  1009         to_bit_word_binary_op T R
  1010             (SOME (fn i1 => fn i2 => fn i3 =>
  1011                       KK.LE (KK.Num 0, foldl1 KK.BitAnd [i1, i2, i3])))
  1012             (SOME (fn i1 => fn i2 =>
  1013                  KK.IntIf (kk_and (KK.LT (i1, KK.Num 0))
  1014                                   (KK.LT (KK.Num 0, i2)),
  1015                      KK.Sub (KK.Div (KK.Add (i1, KK.Num 1), i2), KK.Num 1),
  1016                      KK.IntIf (kk_and (KK.LT (KK.Num 0, i1))
  1017                                       (KK.LT (i2, KK.Num 0)),
  1018                          KK.Sub (KK.Div (KK.Sub (i1, KK.Num 1), i2), KK.Num 1),
  1019                          KK.IntIf (KK.IntEq (i2, KK.Num 0),
  1020                                    KK.Num 0, KK.Div (i1, i2))))))
  1021       | Cst (Gcd, _, _) => KK.Rel gcd_rel
  1022       | Cst (Lcm, _, _) => KK.Rel lcm_rel
  1023       | Cst (Fracs, _, Func (Atom (1, _), _)) => KK.None
  1024       | Cst (Fracs, _, Func (Struct _, _)) =>
  1025         kk_project_seq (KK.Rel norm_frac_rel) 2 2
  1026       | Cst (NormFrac, _, _) => KK.Rel norm_frac_rel
  1027       | Cst (NatToInt, Type (_, [@{typ nat}, _]), Func (Atom _, Atom _)) =>
  1028         KK.Iden
  1029       | Cst (NatToInt, Type (_, [@{typ nat}, _]),
  1030              Func (Atom (_, nat_j0), Opt (Atom (int_k, int_j0)))) =>
  1031         if nat_j0 = int_j0 then
  1032           kk_intersect KK.Iden
  1033               (kk_product (KK.AtomSeq (max_int_for_card int_k + 1, nat_j0))
  1034                           KK.Univ)
  1035         else
  1036           raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"")
  1037       | Cst (NatToInt, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
  1038         to_bit_word_unary_op T R I
  1039       | Cst (IntToNat, Type (_, [@{typ int}, _]),
  1040              Func (Atom (int_k, int_j0), nat_R)) =>
  1041         let
  1042           val abs_card = max_int_for_card int_k + 1
  1043           val (nat_k, nat_j0) = the_single (atom_schema_of_rep nat_R)
  1044           val overlap = Int.min (nat_k, abs_card)
  1045         in
  1046           if nat_j0 = int_j0 then
  1047             kk_union (kk_product (KK.AtomSeq (int_k - abs_card,
  1048                                               int_j0 + abs_card))
  1049                                  (KK.Atom nat_j0))
  1050                      (kk_intersect KK.Iden
  1051                           (kk_product (KK.AtomSeq (overlap, int_j0)) KK.Univ))
  1052           else
  1053             raise BAD ("Nitpick_Kodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"")
  1054         end
  1055       | Cst (IntToNat, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
  1056         to_bit_word_unary_op T R
  1057             (fn i => KK.IntIf (KK.LE (i, KK.Num 0), KK.Num 0, i))
  1058       | Op1 (Not, _, R, u1) => kk_not3 (to_rep R u1)
  1059       | Op1 (Finite, _, Opt (Atom _), _) => KK.None
  1060       | Op1 (Converse, T, R, u1) =>
  1061         let
  1062           val (b_T, a_T) = HOLogic.dest_prodT (pseudo_domain_type T)
  1063           val (b_R, a_R) =
  1064             case R of
  1065               Func (Struct [R1, R2], _) => (R1, R2)
  1066             | Func (R1, _) =>
  1067               if card_of_rep R1 <> 1 then
  1068                 raise REP ("Nitpick_Kodkod.to_r (Converse)", [R])
  1069               else
  1070                 pairself (Atom o pair 1 o offset_of_type ofs) (b_T, a_T)
  1071             | _ => raise REP ("Nitpick_Kodkod.to_r (Converse)", [R])
  1072           val body_R = body_rep R
  1073           val a_arity = arity_of_rep a_R
  1074           val b_arity = arity_of_rep b_R
  1075           val ab_arity = a_arity + b_arity
  1076           val body_arity = arity_of_rep body_R
  1077         in
  1078           kk_project (to_rep (Func (Struct [a_R, b_R], body_R)) u1)
  1079                      (map KK.Num (index_seq a_arity b_arity @
  1080                                   index_seq 0 a_arity @
  1081                                   index_seq ab_arity body_arity))
  1082           |> rel_expr_from_rel_expr kk R (Func (Struct [b_R, a_R], body_R))
  1083         end
  1084       | Op1 (Closure, _, R, u1) =>
  1085         if is_opt_rep R then
  1086           let
  1087             val T1 = type_of u1
  1088             val R' = rep_to_binary_rel_rep ofs T1 (unopt_rep (rep_of u1))
  1089             val R'' = opt_rep ofs T1 R'
  1090           in
  1091             single_rel_rel_let kk
  1092                 (fn r =>
  1093                     let
  1094                       val true_r = kk_closure (kk_join r true_atom)
  1095                       val full_r = full_rel_for_rep R'
  1096                       val false_r = kk_difference full_r
  1097                                         (kk_closure (kk_difference full_r
  1098                                                         (kk_join r false_atom)))
  1099                     in
  1100                       rel_expr_from_rel_expr kk R R''
  1101                           (kk_union (kk_product true_r true_atom)
  1102                                     (kk_product false_r false_atom))
  1103                     end) (to_rep R'' u1)
  1104           end
  1105         else
  1106           let val R' = rep_to_binary_rel_rep ofs (type_of u1) (rep_of u1) in
  1107             rel_expr_from_rel_expr kk R R' (kk_closure (to_rep R' u1))
  1108           end
  1109       | Op1 (SingletonSet, _, Func (R1, Opt _), Cst (Unrep, _, _)) =>
  1110         kk_product (full_rel_for_rep R1) false_atom
  1111       | Op1 (SingletonSet, _, R, u1) =>
  1112         (case R of
  1113            Func (R1, Formula Neut) => to_rep R1 u1
  1114          | Func (R1, Opt _) =>
  1115            single_rel_rel_let kk
  1116                (fn r => kk_rel_if (kk_no r) (empty_rel_for_rep R)
  1117                             (rel_expr_to_func kk R1 bool_atom_R
  1118                                               (Func (R1, Formula Neut)) r))
  1119                (to_opt R1 u1)
  1120          | _ => raise NUT ("Nitpick_Kodkod.to_r (SingletonSet)", [u]))
  1121       | Op1 (SafeThe, _, R, u1) =>
  1122         if is_opt_rep R then
  1123           kk_join (to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1) true_atom
  1124         else
  1125           to_rep (Func (R, Formula Neut)) u1
  1126       | Op1 (First, _, R, u1) => to_nth_pair_sel 0 R u1
  1127       | Op1 (Second, _, R, u1) => to_nth_pair_sel 1 R u1
  1128       | Op1 (Cast, _, R, u1) =>
  1129         ((case rep_of u1 of
  1130             Formula _ =>
  1131             (case unopt_rep R of
  1132                Atom (2, j0) => atom_from_formula kk j0 (to_f u1)
  1133              | _ => raise SAME ())
  1134           | _ => raise SAME ())
  1135          handle SAME () => rel_expr_from_rel_expr kk R (rep_of u1) (to_r u1))
  1136       | Op2 (All, T, R as Opt _, u1, u2) =>
  1137         to_r (Op1 (Not, T, R,
  1138                    Op2 (Exist, T, R, u1, Op1 (Not, T, rep_of u2, u2))))
  1139       | Op2 (Exist, _, Opt _, u1, u2) =>
  1140         let val rs1 = untuple to_decl u1 in
  1141           if not (is_opt_rep (rep_of u2)) then
  1142             kk_rel_if (kk_exist rs1 (to_f u2)) true_atom KK.None
  1143           else
  1144             let val r2 = to_r u2 in
  1145               kk_union (kk_rel_if (kk_exist rs1 (kk_rel_eq r2 true_atom))
  1146                                   true_atom KK.None)
  1147                        (kk_rel_if (kk_all rs1 (kk_rel_eq r2 false_atom))
  1148                                   false_atom KK.None)
  1149             end
  1150         end
  1151       | Op2 (Or, _, _, u1, u2) =>
  1152         if is_opt_rep (rep_of u1) then kk_rel_if (to_f u2) true_atom (to_r u1)
  1153         else kk_rel_if (to_f u1) true_atom (to_r u2)
  1154       | Op2 (And, _, _, u1, u2) =>
  1155         if is_opt_rep (rep_of u1) then kk_rel_if (to_f u2) (to_r u1) false_atom
  1156         else kk_rel_if (to_f u1) (to_r u2) false_atom
  1157       | Op2 (Less, _, _, u1, u2) =>
  1158         (case type_of u1 of
  1159            @{typ nat} =>
  1160            if is_Cst Unrep u1 then to_compare_with_unrep u2 false_atom
  1161            else if is_Cst Unrep u2 then to_compare_with_unrep u1 true_atom
  1162            else kk_nat_less (to_integer u1) (to_integer u2)
  1163          | @{typ int} => kk_int_less (to_integer u1) (to_integer u2)
  1164          | _ =>
  1165            let
  1166              val R1 = Opt (Atom (card_of_rep (rep_of u1),
  1167                                  offset_of_type ofs (type_of u1)))
  1168            in
  1169              double_rel_rel_let kk
  1170                  (fn r1 => fn r2 =>
  1171                      kk_rel_if
  1172                          (fold kk_and (map_filter (fn (u, r) =>
  1173                               if is_opt_rep (rep_of u) then SOME (kk_some r)
  1174                               else NONE) [(u1, r1), (u2, r2)]) KK.True)
  1175                          (atom_from_formula kk bool_j0 (KK.LT (pairself
  1176                              (int_expr_from_atom kk (type_of u1)) (r1, r2))))
  1177                          KK.None)
  1178                  (to_rep R1 u1) (to_rep R1 u2)
  1179             end)
  1180       | Op2 (Triad, _, Opt (Atom (2, j0)), u1, u2) =>
  1181         let
  1182           val f1 = to_f u1
  1183           val f2 = to_f u2
  1184         in
  1185           if f1 = f2 then
  1186             atom_from_formula kk j0 f1
  1187           else
  1188             kk_union (kk_rel_if f1 true_atom KK.None)
  1189                      (kk_rel_if f2 KK.None false_atom)
  1190         end
  1191       | Op2 (Composition, _, R, u1, u2) =>
  1192         let
  1193           val (a_T, b_T) = HOLogic.dest_prodT (pseudo_domain_type (type_of u1))
  1194           val (_, c_T) = HOLogic.dest_prodT (pseudo_domain_type (type_of u2))
  1195           val ab_k = card_of_domain_from_rep 2 (rep_of u1)
  1196           val bc_k = card_of_domain_from_rep 2 (rep_of u2)
  1197           val ac_k = card_of_domain_from_rep 2 R
  1198           val a_k = exact_root 2 (ac_k * ab_k div bc_k)
  1199           val b_k = exact_root 2 (ab_k * bc_k div ac_k)
  1200           val c_k = exact_root 2 (bc_k * ac_k div ab_k)
  1201           val a_R = Atom (a_k, offset_of_type ofs a_T)
  1202           val b_R = Atom (b_k, offset_of_type ofs b_T)
  1203           val c_R = Atom (c_k, offset_of_type ofs c_T)
  1204           val body_R = body_rep R
  1205         in
  1206           (case body_R of
  1207              Formula Neut =>
  1208              kk_join (to_rep (Func (Struct [a_R, b_R], Formula Neut)) u1)
  1209                      (to_rep (Func (Struct [b_R, c_R], Formula Neut)) u2)
  1210            | Opt (Atom (2, _)) =>
  1211              let
  1212                (* FIXME: merge with similar code above *)
  1213                fun must R1 R2 u =
  1214                  kk_join (to_rep (Func (Struct [R1, R2], body_R)) u) true_atom
  1215                fun may R1 R2 u =
  1216                  kk_difference
  1217                      (full_rel_for_rep (Struct [R1, R2]))
  1218                      (kk_join (to_rep (Func (Struct [R1, R2], body_R)) u)
  1219                               false_atom)
  1220              in
  1221                kk_union
  1222                    (kk_product (kk_join (must a_R b_R u1) (must b_R c_R u2))
  1223                                true_atom)
  1224                    (kk_product (kk_difference
  1225                                    (full_rel_for_rep (Struct [a_R, c_R]))
  1226                                    (kk_join (may a_R b_R u1) (may b_R c_R u2)))
  1227                                false_atom)
  1228              end
  1229            | _ => raise NUT ("Nitpick_Kodkod.to_r (Composition)", [u]))
  1230           |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, c_R], body_R))
  1231         end
  1232       | Op2 (Apply, @{typ nat}, _,
  1233              Op2 (Apply, _, _, Cst (Subtract, _, _), u1), u2) =>
  1234         if is_Cst Unrep u2 andalso not (is_opt_rep (rep_of u1)) then
  1235           KK.Atom (offset_of_type ofs nat_T)
  1236         else
  1237           fold kk_join (map to_integer [u1, u2]) (KK.Rel nat_subtract_rel)
  1238       | Op2 (Apply, _, R, u1, u2) => to_apply R u1 u2
  1239       | Op2 (Lambda, _, R as Opt (Atom (1, j0)), u1, u2) =>
  1240         to_guard [u1, u2] R (KK.Atom j0)
  1241       | Op2 (Lambda, _, Func (_, Formula Neut), u1, u2) =>
  1242         kk_comprehension (untuple to_decl u1) (to_f u2)
  1243       | Op2 (Lambda, _, Func (_, R2), u1, u2) =>
  1244         let
  1245           val dom_decls = untuple to_decl u1
  1246           val ran_schema = atom_schema_of_rep R2
  1247           val ran_decls = decls_for_atom_schema ~1 ran_schema
  1248           val ran_vars = unary_var_seq ~1 (length ran_decls)
  1249         in
  1250           kk_comprehension (dom_decls @ ran_decls)
  1251                            (kk_subset (fold1 kk_product ran_vars)
  1252                                       (to_rep R2 u2))
  1253         end
  1254       | Op3 (Let, _, R, u1, u2, u3) =>
  1255         kk_rel_let [to_expr_assign u1 u2] (to_rep R u3)
  1256       | Op3 (If, _, R, u1, u2, u3) =>
  1257         if is_opt_rep (rep_of u1) then
  1258           triple_rel_rel_let kk
  1259               (fn r1 => fn r2 => fn r3 =>
  1260                   let val empty_r = empty_rel_for_rep R in
  1261                     fold1 kk_union
  1262                           [kk_rel_if (kk_rel_eq r1 true_atom) r2 empty_r,
  1263                            kk_rel_if (kk_rel_eq r1 false_atom) r3 empty_r,
  1264                            kk_rel_if (kk_rel_eq r2 r3)
  1265                                 (if inline_rel_expr r2 then r2 else r3) empty_r]
  1266                   end)
  1267               (to_r u1) (to_rep R u2) (to_rep R u3)
  1268         else
  1269           kk_rel_if (to_f u1) (to_rep R u2) (to_rep R u3)
  1270       | Tuple (_, R, us) =>
  1271         (case unopt_rep R of
  1272            Struct Rs => to_product Rs us
  1273          | Vect (k, R) => to_product (replicate k R) us
  1274          | Atom (1, j0) =>
  1275            kk_rel_if (kk_some (fold1 kk_product (map to_r us)))
  1276                      (KK.Atom j0) KK.None
  1277          | _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u]))
  1278       | Construct ([u'], _, _, []) => to_r u'
  1279       | Construct (discr_u :: sel_us, _, _, arg_us) =>
  1280         let
  1281           val set_rs =
  1282             map2 (fn sel_u => fn arg_u =>
  1283                      let
  1284                        val (R1, R2) = dest_Func (rep_of sel_u)
  1285                        val sel_r = to_r sel_u
  1286                        val arg_r = to_opt R2 arg_u
  1287                      in
  1288                        if is_one_rep R2 then
  1289                          kk_n_fold_join kk true R2 R1 arg_r
  1290                               (kk_project sel_r (flip_nums (arity_of_rep R2)))
  1291                        else
  1292                          kk_comprehension [KK.DeclOne ((1, ~1), to_r discr_u)]
  1293                              (kk_rel_eq (kk_join (KK.Var (1, ~1)) sel_r) arg_r)
  1294                          |> is_opt_rep (rep_of arg_u) ? to_guard [arg_u] R1
  1295                      end) sel_us arg_us
  1296         in fold1 kk_intersect set_rs end
  1297       | BoundRel (x, _, _, _) => KK.Var x
  1298       | FreeRel (x, _, _, _) => KK.Rel x
  1299       | RelReg (j, _, R) => KK.RelReg (arity_of_rep R, j)
  1300       | u => raise NUT ("Nitpick_Kodkod.to_r", [u])
  1301     and to_decl (BoundRel (x, _, R, _)) =
  1302         KK.DeclOne (x, KK.AtomSeq (the_single (atom_schema_of_rep R)))
  1303       | to_decl u = raise NUT ("Nitpick_Kodkod.to_decl", [u])
  1304     and to_expr_assign (FormulaReg (j, _, _)) u =
  1305         KK.AssignFormulaReg (j, to_f u)
  1306       | to_expr_assign (RelReg (j, _, R)) u =
  1307         KK.AssignRelReg ((arity_of_rep R, j), to_r u)
  1308       | to_expr_assign u1 _ = raise NUT ("Nitpick_Kodkod.to_expr_assign", [u1])
  1309     and to_atom (x as (_, j0)) u =
  1310       case rep_of u of
  1311         Formula _ => atom_from_formula kk j0 (to_f u)
  1312       | R => atom_from_rel_expr kk x R (to_r u)
  1313     and to_struct Rs u = struct_from_rel_expr kk Rs (rep_of u) (to_r u)
  1314     and to_vect k R u = vect_from_rel_expr kk k R (rep_of u) (to_r u)
  1315     and to_func R1 R2 u = rel_expr_to_func kk R1 R2 (rep_of u) (to_r u)
  1316     and to_opt R u =
  1317       let val old_R = rep_of u in
  1318         if is_opt_rep old_R then
  1319           rel_expr_from_rel_expr kk (Opt R) old_R (to_r u)
  1320         else
  1321           to_rep R u
  1322       end
  1323     and to_rep (Atom x) u = to_atom x u
  1324       | to_rep (Struct Rs) u = to_struct Rs u
  1325       | to_rep (Vect (k, R)) u = to_vect k R u
  1326       | to_rep (Func (R1, R2)) u = to_func R1 R2 u
  1327       | to_rep (Opt R) u = to_opt R u
  1328       | to_rep R _ = raise REP ("Nitpick_Kodkod.to_rep", [R])
  1329     and to_integer u = to_opt (one_rep ofs (type_of u) (rep_of u)) u
  1330     and to_guard guard_us R r =
  1331       let
  1332         val unpacked_rs = unpack_joins r
  1333         val plain_guard_rs =
  1334           map to_r (filter (is_Opt o rep_of) guard_us)
  1335           |> filter_out (member (op =) unpacked_rs)
  1336         val func_guard_us =
  1337           filter ((is_Func andf is_opt_rep) o rep_of) guard_us
  1338         val func_guard_rs = map to_r func_guard_us
  1339         val guard_fs =
  1340           map kk_no plain_guard_rs @
  1341           map2 (kk_not oo kk_n_ary_function kk)
  1342                (map (unopt_rep o rep_of) func_guard_us) func_guard_rs
  1343       in
  1344         if null guard_fs then r
  1345         else kk_rel_if (fold1 kk_or guard_fs) (empty_rel_for_rep R) r
  1346       end
  1347     and to_project new_R old_R r j0 =
  1348       rel_expr_from_rel_expr kk new_R old_R
  1349                              (kk_project_seq r j0 (arity_of_rep old_R))
  1350     and to_product Rs us = fold1 kk_product (map (uncurry to_opt) (Rs ~~ us))
  1351     and to_nth_pair_sel n res_R u =
  1352       case u of
  1353         Tuple (_, _, us) => to_rep res_R (nth us n)
  1354       | _ => let
  1355                val R = rep_of u
  1356                val (a_T, b_T) = HOLogic.dest_prodT (type_of u)
  1357                val Rs =
  1358                  case unopt_rep R of
  1359                    Struct (Rs as [_, _]) => Rs
  1360                  | _ =>
  1361                    let
  1362                      val res_card = card_of_rep res_R
  1363                      val other_card = card_of_rep R div res_card
  1364                      val (a_card, b_card) = (res_card, other_card)
  1365                                             |> n = 1 ? swap
  1366                    in
  1367                      [Atom (a_card, offset_of_type ofs a_T),
  1368                       Atom (b_card, offset_of_type ofs b_T)]
  1369                    end
  1370                val nth_R = nth Rs n
  1371                val j0 = if n = 0 then 0 else arity_of_rep (hd Rs)
  1372              in to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0 end
  1373     and to_set_bool_op connective set_oper u1 u2 =
  1374       let
  1375         val min_R = min_rep (rep_of u1) (rep_of u2)
  1376         val r1 = to_rep min_R u1
  1377         val r2 = to_rep min_R u2
  1378       in
  1379         case min_R of
  1380           Vect (k, Atom _) => kk_vect_set_bool_op connective k r1 r2
  1381         | Func (_, R') =>
  1382           (case body_rep R' of
  1383              Formula Neut => set_oper r1 r2
  1384            | Atom _ => set_oper (kk_join r1 true_atom) (kk_join r2 true_atom)
  1385            | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R]))
  1386         | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R])
  1387       end
  1388     and to_bit_word_unary_op T R oper =
  1389       let
  1390         val Ts = strip_type T ||> single |> op @
  1391         fun int_arg j = int_expr_from_atom kk (nth Ts j) (KK.Var (1, j))
  1392       in
  1393         kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R))
  1394             (KK.FormulaLet
  1395                  (map (fn j => KK.AssignIntReg (j, int_arg j)) (0 upto 1),
  1396                   KK.IntEq (KK.IntReg 1, oper (KK.IntReg 0))))
  1397       end
  1398     and to_bit_word_binary_op T R opt_guard opt_oper =
  1399       let
  1400         val Ts = strip_type T ||> single |> op @
  1401         fun int_arg j = int_expr_from_atom kk (nth Ts j) (KK.Var (1, j))
  1402       in
  1403         kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R))
  1404             (KK.FormulaLet
  1405                  (map (fn j => KK.AssignIntReg (j, int_arg j)) (0 upto 2),
  1406                   fold1 kk_and
  1407                         ((case opt_guard of
  1408                             NONE => []
  1409                           | SOME guard =>
  1410                             [guard (KK.IntReg 0) (KK.IntReg 1) (KK.IntReg 2)]) @
  1411                          (case opt_oper of
  1412                             NONE => []
  1413                           | SOME oper =>
  1414                             [KK.IntEq (KK.IntReg 2,
  1415                                        oper (KK.IntReg 0) (KK.IntReg 1))]))))
  1416       end
  1417     and to_apply (R as Formula _) _ _ =
  1418         raise REP ("Nitpick_Kodkod.to_apply", [R])
  1419       | to_apply res_R func_u arg_u =
  1420         case unopt_rep (rep_of func_u) of
  1421           Atom (1, j0) =>
  1422           to_guard [arg_u] res_R
  1423                    (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (to_r func_u))
  1424         | Atom (k, _) =>
  1425           let
  1426             val dom_card = card_of_rep (rep_of arg_u)
  1427             val ran_R =
  1428               Atom (exact_root dom_card k,
  1429                     offset_of_type ofs (pseudo_range_type (type_of func_u)))
  1430           in
  1431             to_apply_vect dom_card ran_R res_R (to_vect dom_card ran_R func_u)
  1432                           arg_u
  1433           end
  1434         | Vect (1, R') =>
  1435           to_guard [arg_u] res_R
  1436                    (rel_expr_from_rel_expr kk res_R R' (to_r func_u))
  1437         | Vect (k, R') => to_apply_vect k R' res_R (to_r func_u) arg_u
  1438         | Func (R, Formula Neut) =>
  1439           to_guard [arg_u] res_R (rel_expr_from_formula kk res_R
  1440                                       (kk_subset (to_opt R arg_u) (to_r func_u)))
  1441         | Func (R1, R2) =>
  1442           rel_expr_from_rel_expr kk res_R R2
  1443               (kk_n_fold_join kk true R1 R2 (to_opt R1 arg_u) (to_r func_u))
  1444           |> body_rep R2 = Formula Neut ? to_guard [arg_u] res_R
  1445         | _ => raise NUT ("Nitpick_Kodkod.to_apply", [func_u])
  1446     and to_apply_vect k R' res_R func_r arg_u =
  1447       let
  1448         val arg_R = one_rep ofs (type_of arg_u) (unopt_rep (rep_of arg_u))
  1449         val vect_r = vect_from_rel_expr kk k res_R (Vect (k, R')) func_r
  1450         val vect_rs = unpack_vect_in_chunks kk (arity_of_rep res_R) k vect_r
  1451       in
  1452         kk_case_switch kk arg_R res_R (to_opt arg_R arg_u)
  1453                        (all_singletons_for_rep arg_R) vect_rs
  1454       end
  1455     and to_could_be_unrep neg u =
  1456       if neg andalso is_opt_rep (rep_of u) then kk_no (to_r u) else KK.False
  1457     and to_compare_with_unrep u r =
  1458       if is_opt_rep (rep_of u) then
  1459         kk_rel_if (kk_some (to_r u)) r (empty_rel_for_rep (rep_of u))
  1460       else
  1461         r
  1462   in to_f_with_polarity Pos u end
  1463 
  1464 fun declarative_axiom_for_plain_rel kk (FreeRel (x, _, R as Func _, nick)) =
  1465     kk_n_ary_function kk (R |> nick = @{const_name List.set} ? unopt_rep)
  1466                       (KK.Rel x)
  1467   | declarative_axiom_for_plain_rel ({kk_lone, kk_one, ...} : kodkod_constrs)
  1468                                     (FreeRel (x, _, R, _)) =
  1469     if is_one_rep R then kk_one (KK.Rel x)
  1470     else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (KK.Rel x)
  1471     else KK.True
  1472   | declarative_axiom_for_plain_rel _ u =
  1473     raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u])
  1474 
  1475 fun const_triple rel_table (x as (s, T)) =
  1476   case the_name rel_table (ConstName (s, T, Any)) of
  1477     FreeRel ((n, j), _, R, _) => (KK.Rel (n, j), R, n)
  1478   | _ => raise TERM ("Nitpick_Kodkod.const_triple", [Const x])
  1479 
  1480 fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
  1481 
  1482 fun nfa_transitions_for_sel hol_ctxt binarize
  1483                             ({kk_project, ...} : kodkod_constrs) rel_table
  1484                             (dtypes : datatype_spec list) constr_x n =
  1485   let
  1486     val x as (_, T) =
  1487       binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize constr_x n
  1488     val (r, R, arity) = const_triple rel_table x
  1489     val type_schema = type_schema_of_rep T R
  1490   in
  1491     map_filter (fn (j, T) =>
  1492                    if forall (not_equal T o #typ) dtypes then NONE
  1493                    else SOME ((x, kk_project r (map KK.Num [0, j])), T))
  1494                (index_seq 1 (arity - 1) ~~ tl type_schema)
  1495   end
  1496 fun nfa_transitions_for_constr hol_ctxt binarize kk rel_table dtypes
  1497                                (x as (_, T)) =
  1498   maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
  1499        (index_seq 0 (num_sels_for_constr_type T))
  1500 fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : datatype_spec) = NONE
  1501   | nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
  1502   | nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes
  1503                            {typ, constrs, ...} =
  1504     SOME (typ, maps (nfa_transitions_for_constr hol_ctxt binarize kk rel_table
  1505                                                 dtypes o #const) constrs)
  1506 
  1507 val empty_rel = KK.Product (KK.None, KK.None)
  1508 
  1509 fun direct_path_rel_exprs nfa start_T final_T =
  1510   case AList.lookup (op =) nfa final_T of
  1511     SOME trans => map (snd o fst) (filter (curry (op =) start_T o snd) trans)
  1512   | NONE => []
  1513 and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T
  1514                       final_T =
  1515     fold kk_union (direct_path_rel_exprs nfa start_T final_T)
  1516          (if start_T = final_T then KK.Iden else empty_rel)
  1517   | any_path_rel_expr (kk as {kk_union, ...}) nfa (T :: Ts) start_T final_T =
  1518     kk_union (any_path_rel_expr kk nfa Ts start_T final_T)
  1519              (knot_path_rel_expr kk nfa Ts start_T T final_T)
  1520 and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa Ts
  1521                        start_T knot_T final_T =
  1522   kk_join (kk_join (any_path_rel_expr kk nfa Ts knot_T final_T)
  1523                    (kk_reflexive_closure (loop_path_rel_expr kk nfa Ts knot_T)))
  1524           (any_path_rel_expr kk nfa Ts start_T knot_T)
  1525 and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T =
  1526     fold kk_union (direct_path_rel_exprs nfa start_T start_T) empty_rel
  1527   | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (T :: Ts)
  1528                        start_T =
  1529     if start_T = T then
  1530       kk_closure (loop_path_rel_expr kk nfa Ts start_T)
  1531     else
  1532       kk_union (loop_path_rel_expr kk nfa Ts start_T)
  1533                (knot_path_rel_expr kk nfa Ts start_T T start_T)
  1534 
  1535 fun add_nfa_to_graph [] = I
  1536   | add_nfa_to_graph ((_, []) :: nfa) = add_nfa_to_graph nfa
  1537   | add_nfa_to_graph ((T, ((_, T') :: transitions)) :: nfa) =
  1538     add_nfa_to_graph ((T, transitions) :: nfa) o Typ_Graph.add_edge (T, T') o
  1539     Typ_Graph.default_node (T', ()) o Typ_Graph.default_node (T, ())
  1540 
  1541 fun strongly_connected_sub_nfas nfa =
  1542   add_nfa_to_graph nfa Typ_Graph.empty
  1543   |> Typ_Graph.strong_conn
  1544   |> map (fn keys => filter (member (op =) keys o fst) nfa)
  1545 
  1546 (* Cycle breaking in the bounds takes care of singly recursive datatypes, hence
  1547    the first equation. *)
  1548 fun acyclicity_axioms_for_datatype _ [_] _ = []
  1549   | acyclicity_axioms_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa
  1550                                    start_T =
  1551     [kk_no (kk_intersect
  1552                 (loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T)
  1553                 KK.Iden)]
  1554 fun acyclicity_axioms_for_datatypes kk =
  1555   maps (fn nfa => maps (acyclicity_axioms_for_datatype kk nfa o fst) nfa)
  1556 
  1557 fun atom_equation_for_nut ofs kk (u, j) =
  1558   let val dummy_u = RelReg (0, type_of u, rep_of u) in
  1559     case Op2 (DefEq, bool_T, Formula Pos, dummy_u, u)
  1560          |> kodkod_formula_from_nut ofs kk of
  1561       KK.RelEq (KK.RelReg _, r) => SOME (KK.RelEq (KK.Atom j, r))
  1562     | _ => raise BAD ("Nitpick_Kodkod.atom_equation_for_nut",
  1563                       "malformed Kodkod formula")
  1564   end
  1565 
  1566 fun needed_values_for_datatype [] _ _ = SOME []
  1567   | needed_values_for_datatype need_us ofs
  1568                                ({typ, card, constrs, ...} : datatype_spec) =
  1569     let
  1570       fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) =
  1571           fold aux us
  1572           #> (fn NONE => NONE
  1573                | accum as SOME (loose, fixed) =>
  1574                  if T = typ then
  1575                    case AList.lookup (op =) fixed u of
  1576                      SOME _ => accum
  1577                    | NONE =>
  1578                      let
  1579                        val constr_s = constr_name_for_sel_like s
  1580                        val {delta, epsilon, ...} =
  1581                          constrs
  1582                          |> List.find (fn {const, ...} => fst const = constr_s)
  1583                          |> the
  1584                        val j0 = offset_of_type ofs T
  1585                      in
  1586                        case find_first (fn j => j >= delta andalso
  1587                                         j < delta + epsilon) loose of
  1588                          SOME j =>
  1589                          SOME (remove (op =) j loose, (u, j0 + j) :: fixed)
  1590                        | NONE => NONE
  1591                      end
  1592                  else
  1593                    accum)
  1594         | aux _ = I
  1595     in
  1596       SOME (index_seq 0 card, []) |> fold aux need_us |> Option.map (rev o snd)
  1597     end
  1598 
  1599 fun needed_value_axioms_for_datatype _ _ _ (_, NONE) = [KK.False]
  1600   | needed_value_axioms_for_datatype ofs kk dtypes (T, SOME fixed) =
  1601     if is_datatype_nat_like (the (datatype_spec dtypes T)) then []
  1602     else fixed |> map_filter (atom_equation_for_nut ofs kk)
  1603 
  1604 fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r =
  1605   kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z)))
  1606 fun gt ({kk_subset, kk_join, kk_closure, ...} : kodkod_constrs) z r1 r2 =
  1607   kk_subset r1 (kk_join r2 (kk_closure (KK.Rel (suc_rel_for_atom_seq z))))
  1608 
  1609 fun constr_quadruple ({const = (s, T), delta, epsilon, ...} : constr_spec) =
  1610   (delta, (epsilon, (num_binder_types T, s)))
  1611 val constr_ord =
  1612   prod_ord int_ord (prod_ord int_ord (prod_ord int_ord string_ord))
  1613   o pairself constr_quadruple
  1614 
  1615 fun datatype_ord (({card = card1, self_rec = self_rec1, constrs = constr1, ...},
  1616                    {card = card2, self_rec = self_rec2, constrs = constr2, ...})
  1617                   : datatype_spec * datatype_spec) =
  1618   prod_ord int_ord (prod_ord bool_ord int_ord)
  1619            ((card1, (self_rec1, length constr1)),
  1620             (card2, (self_rec2, length constr2)))
  1621 
  1622 (* We must absolutely tabulate "suc" for all datatypes whose selector bounds
  1623    break cycles; otherwise, we may end up with two incompatible symmetry
  1624    breaking orders, leading to spurious models. *)
  1625 fun should_tabulate_suc_for_type dtypes T =
  1626   is_asymmetric_nondatatype T orelse
  1627   case datatype_spec dtypes T of
  1628     SOME {self_rec, ...} => self_rec
  1629   | NONE => false
  1630 
  1631 fun lex_order_rel_expr (kk as {kk_implies, kk_and, kk_subset, kk_join, ...})
  1632                        dtypes sel_quadruples =
  1633   case sel_quadruples of
  1634     [] => KK.True
  1635   | ((r, Func (Atom _, Atom x), 2), (_, Type (_, [_, T]))) :: sel_quadruples' =>
  1636     let val z = (x, should_tabulate_suc_for_type dtypes T) in
  1637       if null sel_quadruples' then
  1638         gt kk z (kk_join (KK.Var (1, 1)) r) (kk_join (KK.Var (1, 0)) r)
  1639       else
  1640         kk_and (kk_subset (kk_join (KK.Var (1, 1)) r)
  1641                           (all_ge kk z (kk_join (KK.Var (1, 0)) r)))
  1642                (kk_implies (kk_subset (kk_join (KK.Var (1, 1)) r)
  1643                                       (kk_join (KK.Var (1, 0)) r))
  1644                            (lex_order_rel_expr kk dtypes sel_quadruples'))
  1645     end
  1646     (* Skip constructors components that aren't atoms, since we cannot compare
  1647        these easily. *)
  1648   | _ :: sel_quadruples' => lex_order_rel_expr kk dtypes sel_quadruples'
  1649 
  1650 fun is_nil_like_constr_type dtypes T =
  1651   case datatype_spec dtypes T of
  1652     SOME {constrs, ...} =>
  1653     (case filter_out (is_self_recursive_constr_type o snd o #const) constrs of
  1654        [{const = (_, T'), ...}] => T = T'
  1655      | _ => false)
  1656   | NONE => false
  1657 
  1658 fun sym_break_axioms_for_constr_pair hol_ctxt binarize
  1659        (kk as {kk_all, kk_or, kk_implies, kk_and, kk_some, kk_intersect,
  1660                kk_join, ...}) rel_table nfas dtypes
  1661        (constr_ord,
  1662         ({const = const1 as (_, T1), delta = delta1, epsilon = epsilon1, ...},
  1663          {const = const2 as (_, _), delta = delta2, epsilon = epsilon2, ...})
  1664         : constr_spec * constr_spec) =
  1665   let
  1666     val dataT = body_type T1
  1667     val nfa = nfas |> find_first (exists (curry (op =) dataT o fst)) |> these
  1668     val rec_Ts = nfa |> map fst
  1669     fun rec_and_nonrec_sels (x as (_, T)) =
  1670       index_seq 0 (num_sels_for_constr_type T)
  1671       |> map (binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x)
  1672       |> List.partition (member (op =) rec_Ts o range_type o snd)
  1673     val sel_xs1 = rec_and_nonrec_sels const1 |> op @
  1674   in
  1675     if constr_ord = EQUAL andalso null sel_xs1 then
  1676       []
  1677     else
  1678       let
  1679         val z =
  1680           (case #2 (const_triple rel_table (discr_for_constr const1)) of
  1681              Func (Atom x, Formula _) => x
  1682            | R => raise REP ("Nitpick_Kodkod.sym_break_axioms_for_constr_pair",
  1683                              [R]), should_tabulate_suc_for_type dtypes dataT)
  1684         val (rec_sel_xs2, nonrec_sel_xs2) = rec_and_nonrec_sels const2
  1685         val sel_xs2 = rec_sel_xs2 @ nonrec_sel_xs2
  1686         fun sel_quadruples2 () = sel_xs2 |> map (`(const_triple rel_table))
  1687         (* If the two constructors are the same, we drop the first selector
  1688            because that one is always checked by the lexicographic order.
  1689            We sometimes also filter out direct subterms, because those are
  1690            already handled by the acyclicity breaking in the bound
  1691            declarations. *)
  1692         fun filter_out_sels no_direct sel_xs =
  1693           apsnd (filter_out
  1694                      (fn ((x, _), T) =>
  1695                          (constr_ord = EQUAL andalso x = hd sel_xs) orelse
  1696                          (T = dataT andalso
  1697                           (no_direct orelse not (member (op =) sel_xs x)))))
  1698         fun subterms_r no_direct sel_xs j =
  1699           loop_path_rel_expr kk (map (filter_out_sels no_direct sel_xs) nfa)
  1700                            (filter_out (curry (op =) dataT) (map fst nfa)) dataT
  1701           |> kk_join (KK.Var (1, j))
  1702       in
  1703         [kk_all [KK.DeclOne ((1, 0), discr_rel_expr rel_table const1),
  1704                  KK.DeclOne ((1, 1), discr_rel_expr rel_table const2)]
  1705              (kk_implies
  1706                  (if delta2 >= epsilon1 then KK.True
  1707                   else if delta1 >= epsilon2 - 1 then KK.False
  1708                   else gt kk z (KK.Var (1, 1)) (KK.Var (1, 0)))
  1709                  (kk_or
  1710                       (if is_nil_like_constr_type dtypes T1 then
  1711                          KK.True
  1712                        else
  1713                          kk_some (kk_intersect (subterms_r false sel_xs2 1)
  1714                                                (all_ge kk z (KK.Var (1, 0)))))
  1715                       (case constr_ord of
  1716                          EQUAL =>
  1717                          kk_and
  1718                              (lex_order_rel_expr kk dtypes (sel_quadruples2 ()))
  1719                              (kk_all [KK.DeclOne ((1, 2),
  1720                                                   subterms_r true sel_xs1 0)]
  1721                                      (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))))
  1722                        | LESS =>
  1723                          kk_all [KK.DeclOne ((1, 2),
  1724                                  subterms_r false sel_xs1 0)]
  1725                                 (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2)))
  1726                        | GREATER => KK.False)))]
  1727       end
  1728   end
  1729 
  1730 fun sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas dtypes
  1731                                   ({constrs, ...} : datatype_spec) =
  1732   let
  1733     val constrs = sort constr_ord constrs
  1734     val constr_pairs = all_distinct_unordered_pairs_of constrs
  1735   in
  1736     map (pair EQUAL) (constrs ~~ constrs) @
  1737     map (pair LESS) constr_pairs @
  1738     map (pair GREATER) (map swap constr_pairs)
  1739     |> maps (sym_break_axioms_for_constr_pair hol_ctxt binarize kk rel_table
  1740                                               nfas dtypes)
  1741   end
  1742 
  1743 fun is_datatype_in_needed_value T (Construct (_, T', _, us)) =
  1744     T = T' orelse exists (is_datatype_in_needed_value T) us
  1745   | is_datatype_in_needed_value _ _ = false
  1746 
  1747 val min_sym_break_card = 7
  1748 
  1749 fun sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break
  1750                                    kk rel_table nfas dtypes =
  1751   if datatype_sym_break = 0 then
  1752     []
  1753   else
  1754     dtypes |> filter is_datatype_acyclic
  1755            |> filter (fn {constrs = [_], ...} => false
  1756                        | {card, constrs, ...} =>
  1757                          card >= min_sym_break_card andalso
  1758                          forall (forall (not o is_higher_order_type)
  1759                                  o binder_types o snd o #const) constrs)
  1760            |> filter_out
  1761                   (fn {typ, ...} =>
  1762                       exists (is_datatype_in_needed_value typ) need_us)
  1763            |> (fn dtypes' =>
  1764                   dtypes' |> length dtypes' > datatype_sym_break
  1765                              ? (sort (datatype_ord o swap)
  1766                                 #> take datatype_sym_break))
  1767            |> maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table
  1768                                                   nfas dtypes)
  1769 
  1770 fun sel_axioms_for_sel hol_ctxt binarize j0
  1771         (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})
  1772         need_vals rel_table dom_r (dtype as {typ, ...})
  1773         ({const, delta, epsilon, exclusive, ...} : constr_spec) n =
  1774   let
  1775     val x = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
  1776     val (r, R, _) = const_triple rel_table x
  1777     val rel_x =
  1778       case r of
  1779         KK.Rel x => x
  1780       | _ => raise BAD ("Nitpick_Kodkod.sel_axioms_for_sel", "non-Rel")
  1781     val R2 = dest_Func R |> snd
  1782     val z = (epsilon - delta, delta + j0)
  1783   in
  1784     if exclusive then
  1785       [kk_n_ary_function kk (Func (Atom z, R2)) r]
  1786     else if all_values_are_needed need_vals dtype then
  1787       typ |> needed_values need_vals
  1788           |> filter (is_sel_of_constr rel_x)
  1789           |> map (fn (_, j) => kk_n_ary_function kk R2 (kk_join (KK.Atom j) r))
  1790     else
  1791       let val r' = kk_join (KK.Var (1, 0)) r in
  1792         [kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)]
  1793                 (kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r)
  1794                                (kk_n_ary_function kk R2 r') (kk_no r'))]
  1795       end
  1796   end
  1797 fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk need_vals rel_table
  1798         dtype (constr as {const, delta, epsilon, explicit_max, ...}) =
  1799   let
  1800     val honors_explicit_max =
  1801       explicit_max < 0 orelse epsilon - delta <= explicit_max
  1802   in
  1803     if explicit_max = 0 then
  1804       [formula_for_bool honors_explicit_max]
  1805     else
  1806       let
  1807         val dom_r = discr_rel_expr rel_table const
  1808         val max_axiom =
  1809           if honors_explicit_max then
  1810             KK.True
  1811           else if bits = 0 orelse
  1812                is_twos_complement_representable bits (epsilon - delta) then
  1813             KK.LE (KK.Cardinality dom_r, KK.Num explicit_max)
  1814           else
  1815             raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",
  1816                              "\"bits\" value " ^ string_of_int bits ^
  1817                              " too small for \"max\"")
  1818       in
  1819         max_axiom ::
  1820         maps (sel_axioms_for_sel hol_ctxt binarize j0 kk need_vals rel_table
  1821                                  dom_r dtype constr)
  1822              (index_seq 0 (num_sels_for_constr_type (snd const)))
  1823       end
  1824   end
  1825 fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table need_vals
  1826                             (dtype as {constrs, ...}) =
  1827   maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table need_vals
  1828                               dtype) constrs
  1829 
  1830 fun uniqueness_axioms_for_constr hol_ctxt binarize
  1831         ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
  1832          : kodkod_constrs) need_vals rel_table dtype
  1833         ({const, ...} : constr_spec) =
  1834   let
  1835     fun conjunct_for_sel r =
  1836       kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
  1837     val num_sels = num_sels_for_constr_type (snd const)
  1838     val triples =
  1839       map (const_triple rel_table
  1840            o binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const)
  1841           (~1 upto num_sels - 1)
  1842     val set_r = triples |> hd |> #1
  1843   in
  1844     if num_sels = 0 then
  1845       [kk_lone set_r]
  1846     else if all_values_are_needed need_vals dtype then
  1847       []
  1848     else
  1849       [kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1])
  1850               (kk_implies
  1851                    (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
  1852                    (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))]
  1853   end
  1854 fun uniqueness_axioms_for_datatype hol_ctxt binarize kk need_vals rel_table
  1855                                    (dtype as {constrs, ...}) =
  1856   maps (uniqueness_axioms_for_constr hol_ctxt binarize kk need_vals rel_table
  1857                                      dtype) constrs
  1858 
  1859 fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
  1860 fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...})
  1861         need_vals rel_table (dtype as {card, constrs, ...}) =
  1862   if forall #exclusive constrs then
  1863     [Integer.sum (map effective_constr_max constrs) = card |> formula_for_bool]
  1864   else if all_values_are_needed need_vals dtype then
  1865     []
  1866   else
  1867     let val rs = map (discr_rel_expr rel_table o #const) constrs in
  1868       [kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)),
  1869        kk_disjoint_sets kk rs]
  1870     end
  1871 
  1872 fun other_axioms_for_datatype _ _ _ _ _ _ _ {deep = false, ...} = []
  1873   | other_axioms_for_datatype hol_ctxt binarize need_vals bits ofs kk rel_table
  1874                               (dtype as {typ, ...}) =
  1875     let val j0 = offset_of_type ofs typ in
  1876       sel_axioms_for_datatype hol_ctxt binarize bits j0 kk need_vals rel_table
  1877                               dtype @
  1878       uniqueness_axioms_for_datatype hol_ctxt binarize kk need_vals rel_table
  1879                                      dtype @
  1880       partition_axioms_for_datatype j0 kk need_vals rel_table dtype
  1881     end
  1882 
  1883 fun declarative_axioms_for_datatypes hol_ctxt binarize need_us need_vals
  1884         datatype_sym_break bits ofs kk rel_table dtypes =
  1885   let
  1886     val nfas =
  1887       dtypes |> map_filter (nfa_entry_for_datatype hol_ctxt binarize kk
  1888                                                    rel_table dtypes)
  1889              |> strongly_connected_sub_nfas
  1890   in
  1891     acyclicity_axioms_for_datatypes kk nfas @
  1892     maps (needed_value_axioms_for_datatype ofs kk dtypes) need_vals @
  1893     sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break
  1894                                    kk rel_table nfas dtypes @
  1895     maps (other_axioms_for_datatype hol_ctxt binarize need_vals bits ofs kk
  1896                                     rel_table) dtypes
  1897   end
  1898 
  1899 end;