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