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