src/HOL/Nitpick_Examples/minipick.ML
author hoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 51474 1e9e68247ad1
parent 50487 9486641e691b
child 54845 10df188349b3
permissions -rw-r--r--
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
     1 (*  Title:      HOL/Nitpick_Examples/minipick.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2009-2010
     4 
     5 Finite model generation for HOL formulas using Kodkod, minimalistic version.
     6 *)
     7 
     8 signature MINIPICK =
     9 sig
    10   val minipick : Proof.context -> int -> term -> string
    11   val minipick_expect : Proof.context -> string -> int -> term -> unit
    12 end;
    13 
    14 structure Minipick : MINIPICK =
    15 struct
    16 
    17 open Kodkod
    18 open Nitpick_Util
    19 open Nitpick_HOL
    20 open Nitpick_Peephole
    21 open Nitpick_Kodkod
    22 
    23 datatype rep =
    24   S_Rep |
    25   R_Rep of bool
    26 
    27 fun check_type ctxt raw_infinite (Type (@{type_name fun}, Ts)) =
    28     List.app (check_type ctxt raw_infinite) Ts
    29   | check_type ctxt raw_infinite (Type (@{type_name prod}, Ts)) =
    30     List.app (check_type ctxt raw_infinite) Ts
    31   | check_type _ _ @{typ bool} = ()
    32   | check_type _ _ (TFree (_, @{sort "{}"})) = ()
    33   | check_type _ _ (TFree (_, @{sort HOL.type})) = ()
    34   | check_type ctxt raw_infinite T =
    35     if raw_infinite T then
    36       ()
    37     else
    38       error ("Not supported: Type " ^ quote (Syntax.string_of_typ ctxt T) ^ ".")
    39 
    40 fun atom_schema_of S_Rep card (Type (@{type_name fun}, [T1, T2])) =
    41     replicate_list (card T1) (atom_schema_of S_Rep card T2)
    42   | atom_schema_of (R_Rep true) card
    43                    (Type (@{type_name fun}, [T1, @{typ bool}])) =
    44     atom_schema_of S_Rep card T1
    45   | atom_schema_of (rep as R_Rep _) card (Type (@{type_name fun}, [T1, T2])) =
    46     atom_schema_of S_Rep card T1 @ atom_schema_of rep card T2
    47   | atom_schema_of _ card (Type (@{type_name prod}, Ts)) =
    48     maps (atom_schema_of S_Rep card) Ts
    49   | atom_schema_of _ card T = [card T]
    50 val arity_of = length ooo atom_schema_of
    51 val atom_seqs_of = map (AtomSeq o rpair 0) ooo atom_schema_of
    52 val atom_seq_product_of = foldl1 Product ooo atom_seqs_of
    53 
    54 fun index_for_bound_var _ [_] 0 = 0
    55   | index_for_bound_var card (_ :: Ts) 0 =
    56     index_for_bound_var card Ts 0 + arity_of S_Rep card (hd Ts)
    57   | index_for_bound_var card Ts n = index_for_bound_var card (tl Ts) (n - 1)
    58 fun vars_for_bound_var card R Ts j =
    59   map (curry Var 1) (index_seq (index_for_bound_var card Ts j)
    60                                (arity_of R card (nth Ts j)))
    61 val rel_expr_for_bound_var = foldl1 Product oooo vars_for_bound_var
    62 fun decls_for R card Ts T =
    63   map2 (curry DeclOne o pair 1)
    64        (index_seq (index_for_bound_var card (T :: Ts) 0)
    65                   (arity_of R card (nth (T :: Ts) 0)))
    66        (atom_seqs_of R card T)
    67 
    68 val atom_product = foldl1 Product o map Atom
    69 
    70 val false_atom_num = 0
    71 val true_atom_num = 1
    72 val false_atom = Atom false_atom_num
    73 val true_atom = Atom true_atom_num
    74 
    75 fun kodkod_formula_from_term ctxt total card complete concrete frees =
    76   let
    77     fun F_from_S_rep (SOME false) r = Not (RelEq (r, false_atom))
    78       | F_from_S_rep _ r = RelEq (r, true_atom)
    79     fun S_rep_from_F NONE f = RelIf (f, true_atom, false_atom)
    80       | S_rep_from_F (SOME true) f = RelIf (f, true_atom, None)
    81       | S_rep_from_F (SOME false) f = RelIf (Not f, false_atom, None)
    82     fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
    83         if total andalso T2 = bool_T then
    84           let
    85             val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
    86                       |> all_combinations
    87           in
    88             map2 (fn i => fn js =>
    89 (*
    90                      RelIf (F_from_S_rep NONE (Project (r, [Num i])),
    91                             atom_product js, empty_n_ary_rel (length js))
    92 *)
    93                      Join (Project (r, [Num i]),
    94                            atom_product (false_atom_num :: js))
    95                  ) (index_seq 0 (length jss)) jss
    96             |> foldl1 Union
    97           end
    98         else
    99           let
   100             val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
   101                       |> all_combinations
   102             val arity2 = arity_of S_Rep card T2
   103           in
   104             map2 (fn i => fn js =>
   105                      Product (atom_product js,
   106                               Project (r, num_seq (i * arity2) arity2)
   107                               |> R_rep_from_S_rep T2))
   108                  (index_seq 0 (length jss)) jss
   109             |> foldl1 Union
   110           end
   111       | R_rep_from_S_rep _ r = r
   112     fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
   113         Comprehension (decls_for S_Rep card Ts T,
   114             RelEq (R_rep_from_S_rep T
   115                        (rel_expr_for_bound_var card S_Rep (T :: Ts) 0), r))
   116       | S_rep_from_R_rep _ _ r = r
   117     fun partial_eq pos Ts (Type (@{type_name fun}, [T1, T2])) t1 t2 =
   118         HOLogic.mk_all ("x", T1,
   119                         HOLogic.eq_const T2 $ (incr_boundvars 1 t1 $ Bound 0)
   120                         $ (incr_boundvars 1 t2 $ Bound 0))
   121         |> to_F (SOME pos) Ts
   122       | partial_eq pos Ts T t1 t2 =
   123         if pos andalso not (concrete T) then
   124           False
   125         else
   126           (t1, t2) |> pairself (to_R_rep Ts)
   127                    |> (if pos then Some o Intersect else Lone o Union)
   128     and to_F pos Ts t =
   129       (case t of
   130          @{const Not} $ t1 => Not (to_F (Option.map not pos) Ts t1)
   131        | @{const False} => False
   132        | @{const True} => True
   133        | Const (@{const_name All}, _) $ Abs (_, T, t') =>
   134          if pos = SOME true andalso not (complete T) then False
   135          else All (decls_for S_Rep card Ts T, to_F pos (T :: Ts) t')
   136        | (t0 as Const (@{const_name All}, _)) $ t1 =>
   137          to_F pos Ts (t0 $ eta_expand Ts t1 1)
   138        | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
   139          if pos = SOME false andalso not (complete T) then True
   140          else Exist (decls_for S_Rep card Ts T, to_F pos (T :: Ts) t')
   141        | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   142          to_F pos Ts (t0 $ eta_expand Ts t1 1)
   143        | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
   144          (case pos of
   145             NONE => RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
   146           | SOME pos => partial_eq pos Ts T t1 t2)
   147        | Const (@{const_name ord_class.less_eq},
   148                 Type (@{type_name fun},
   149                       [Type (@{type_name fun}, [T', @{typ bool}]), _]))
   150          $ t1 $ t2 =>
   151          (case pos of
   152             NONE => Subset (to_R_rep Ts t1, to_R_rep Ts t2)
   153           | SOME true =>
   154             Subset (Difference (atom_seq_product_of S_Rep card T',
   155                                 Join (to_R_rep Ts t1, false_atom)),
   156                     Join (to_R_rep Ts t2, true_atom))
   157           | SOME false =>
   158             Subset (Join (to_R_rep Ts t1, true_atom),
   159                     Difference (atom_seq_product_of S_Rep card T',
   160                                 Join (to_R_rep Ts t2, false_atom))))
   161        | @{const HOL.conj} $ t1 $ t2 => And (to_F pos Ts t1, to_F pos Ts t2)
   162        | @{const HOL.disj} $ t1 $ t2 => Or (to_F pos Ts t1, to_F pos Ts t2)
   163        | @{const HOL.implies} $ t1 $ t2 =>
   164          Implies (to_F (Option.map not pos) Ts t1, to_F pos Ts t2)
   165        | Const (@{const_name Set.member}, _) $ t1 $ t2 => to_F pos Ts (t2 $ t1)
   166        | t1 $ t2 =>
   167          (case pos of
   168             NONE => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
   169           | SOME pos =>
   170             let
   171               val kt1 = to_R_rep Ts t1
   172               val kt2 = to_S_rep Ts t2
   173               val kT = atom_seq_product_of S_Rep card (fastype_of1 (Ts, t2))
   174             in
   175               if pos then
   176                 Not (Subset (kt2, Difference (kT, Join (kt1, true_atom))))
   177               else
   178                 Subset (kt2, Difference (kT, Join (kt1, false_atom)))
   179             end)
   180        | _ => raise SAME ())
   181       handle SAME () => F_from_S_rep pos (to_R_rep Ts t)
   182     and to_S_rep Ts t =
   183       case t of
   184         Const (@{const_name Pair}, _) $ t1 $ t2 =>
   185         Product (to_S_rep Ts t1, to_S_rep Ts t2)
   186       | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts (eta_expand Ts t 1)
   187       | Const (@{const_name Pair}, _) => to_S_rep Ts (eta_expand Ts t 2)
   188       | Const (@{const_name fst}, _) $ t1 =>
   189         let val fst_arity = arity_of S_Rep card (fastype_of1 (Ts, t)) in
   190           Project (to_S_rep Ts t1, num_seq 0 fst_arity)
   191         end
   192       | Const (@{const_name fst}, _) => to_S_rep Ts (eta_expand Ts t 1)
   193       | Const (@{const_name snd}, _) $ t1 =>
   194         let
   195           val pair_arity = arity_of S_Rep card (fastype_of1 (Ts, t1))
   196           val snd_arity = arity_of S_Rep card (fastype_of1 (Ts, t))
   197           val fst_arity = pair_arity - snd_arity
   198         in Project (to_S_rep Ts t1, num_seq fst_arity snd_arity) end
   199       | Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)
   200       | Bound j => rel_expr_for_bound_var card S_Rep Ts j
   201       | _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)
   202     and partial_set_op swap1 swap2 op1 op2 Ts t1 t2 =
   203       let
   204         val kt1 = to_R_rep Ts t1
   205         val kt2 = to_R_rep Ts t2
   206         val (a11, a21) = (false_atom, true_atom) |> swap1 ? swap
   207         val (a12, a22) = (false_atom, true_atom) |> swap2 ? swap
   208       in
   209         Union (Product (op1 (Join (kt1, a11), Join (kt2, a12)), true_atom),
   210                Product (op2 (Join (kt1, a21), Join (kt2, a22)), false_atom))
   211       end
   212     and to_R_rep Ts t =
   213       (case t of
   214          @{const Not} => to_R_rep Ts (eta_expand Ts t 1)
   215        | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
   216        | Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
   217        | Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
   218        | Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)
   219        | Const (@{const_name ord_class.less_eq},
   220                 Type (@{type_name fun},
   221                       [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
   222          to_R_rep Ts (eta_expand Ts t 1)
   223        | Const (@{const_name ord_class.less_eq}, _) =>
   224          to_R_rep Ts (eta_expand Ts t 2)
   225        | @{const HOL.conj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   226        | @{const HOL.conj} => to_R_rep Ts (eta_expand Ts t 2)
   227        | @{const HOL.disj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   228        | @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)
   229        | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   230        | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
   231        | Const (@{const_name Set.member}, _) $ _ =>
   232          to_R_rep Ts (eta_expand Ts t 1)
   233        | Const (@{const_name Set.member}, _) => to_R_rep Ts (eta_expand Ts t 2)
   234        | Const (@{const_name Collect}, _) $ t' => to_R_rep Ts t'
   235        | Const (@{const_name Collect}, _) => to_R_rep Ts (eta_expand Ts t 1)
   236        | Const (@{const_name bot_class.bot},
   237                 T as Type (@{type_name fun}, [T', @{typ bool}])) =>
   238          if total then empty_n_ary_rel (arity_of (R_Rep total) card T)
   239          else Product (atom_seq_product_of (R_Rep total) card T', false_atom)
   240        | Const (@{const_name top_class.top},
   241                 T as Type (@{type_name fun}, [T', @{typ bool}])) =>
   242          if total then atom_seq_product_of (R_Rep total) card T
   243          else Product (atom_seq_product_of (R_Rep total) card T', true_atom)
   244        | Const (@{const_name insert}, Type (_, [T, _])) $ t1 $ t2 =>
   245          if total then
   246            Union (to_S_rep Ts t1, to_R_rep Ts t2)
   247          else
   248            let
   249              val kt1 = to_S_rep Ts t1
   250              val kt2 = to_R_rep Ts t2
   251            in
   252              RelIf (Some kt1,
   253                     if arity_of S_Rep card T = 1 then
   254                       Override (kt2, Product (kt1, true_atom))
   255                     else
   256                       Union (Difference (kt2, Product (kt1, false_atom)),
   257                              Product (kt1, true_atom)),
   258                     Difference (kt2, Product (atom_seq_product_of S_Rep card T,
   259                                               false_atom)))
   260            end
   261        | Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
   262        | Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2)
   263        | Const (@{const_name trancl},
   264                 Type (_, [Type (_, [Type (_, [T', _]), _]), _])) $ t1 =>
   265          if arity_of S_Rep card T' = 1 then
   266            if total then
   267              Closure (to_R_rep Ts t1)
   268            else
   269              let
   270                val kt1 = to_R_rep Ts t1
   271                val true_core_kt = Closure (Join (kt1, true_atom))
   272                val kTx =
   273                  atom_seq_product_of S_Rep card (HOLogic.mk_prodT (`I T'))
   274                val false_mantle_kt =
   275                  Difference (kTx,
   276                      Closure (Difference (kTx, Join (kt1, false_atom))))
   277              in
   278                Union (Product (Difference (false_mantle_kt, true_core_kt),
   279                                false_atom),
   280                       Product (true_core_kt, true_atom))
   281              end
   282          else
   283            error "Not supported: Transitive closure for function or pair type."
   284        | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
   285        | Const (@{const_name inf_class.inf},
   286                 Type (@{type_name fun},
   287                       [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   288          $ t1 $ t2 =>
   289          if total then Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
   290          else partial_set_op true true Intersect Union Ts t1 t2
   291        | Const (@{const_name inf_class.inf}, _) $ _ =>
   292          to_R_rep Ts (eta_expand Ts t 1)
   293        | Const (@{const_name inf_class.inf}, _) =>
   294          to_R_rep Ts (eta_expand Ts t 2)
   295        | Const (@{const_name sup_class.sup},
   296                 Type (@{type_name fun},
   297                       [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   298          $ t1 $ t2 =>
   299          if total then Union (to_R_rep Ts t1, to_R_rep Ts t2)
   300          else partial_set_op true true Union Intersect Ts t1 t2
   301        | Const (@{const_name sup_class.sup}, _) $ _ =>
   302          to_R_rep Ts (eta_expand Ts t 1)
   303        | Const (@{const_name sup_class.sup}, _) =>
   304          to_R_rep Ts (eta_expand Ts t 2)
   305        | Const (@{const_name minus_class.minus},
   306                 Type (@{type_name fun},
   307                       [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   308          $ t1 $ t2 =>
   309          if total then Difference (to_R_rep Ts t1, to_R_rep Ts t2)
   310          else partial_set_op true false Intersect Union Ts t1 t2
   311        | Const (@{const_name minus_class.minus},
   312                 Type (@{type_name fun},
   313                       [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
   314          to_R_rep Ts (eta_expand Ts t 1)
   315        | Const (@{const_name minus_class.minus},
   316                 Type (@{type_name fun},
   317                       [Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
   318          to_R_rep Ts (eta_expand Ts t 2)
   319        | Const (@{const_name Pair}, _) $ _ $ _ => to_S_rep Ts t
   320        | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts t
   321        | Const (@{const_name Pair}, _) => to_S_rep Ts t
   322        | Const (@{const_name fst}, _) $ _ => raise SAME ()
   323        | Const (@{const_name fst}, _) => raise SAME ()
   324        | Const (@{const_name snd}, _) $ _ => raise SAME ()
   325        | Const (@{const_name snd}, _) => raise SAME ()
   326        | @{const False} => false_atom
   327        | @{const True} => true_atom
   328        | Free (x as (_, T)) =>
   329          Rel (arity_of (R_Rep total) card T, find_index (curry (op =) x) frees)
   330        | Term.Var _ => error "Not supported: Schematic variables."
   331        | Bound _ => raise SAME ()
   332        | Abs (_, T, t') =>
   333          (case (total, fastype_of1 (T :: Ts, t')) of
   334             (true, @{typ bool}) =>
   335             Comprehension (decls_for S_Rep card Ts T, to_F NONE (T :: Ts) t')
   336           | (_, T') =>
   337             Comprehension (decls_for S_Rep card Ts T @
   338                            decls_for (R_Rep total) card (T :: Ts) T',
   339                            Subset (rel_expr_for_bound_var card (R_Rep total)
   340                                                           (T' :: T :: Ts) 0,
   341                                    to_R_rep (T :: Ts) t')))
   342        | t1 $ t2 =>
   343          (case fastype_of1 (Ts, t) of
   344             @{typ bool} =>
   345             if total then
   346               S_rep_from_F NONE (to_F NONE Ts t)
   347             else
   348               RelIf (to_F (SOME true) Ts t, true_atom,
   349                      RelIf (Not (to_F (SOME false) Ts t), false_atom,
   350                      None))
   351           | T =>
   352             let val T2 = fastype_of1 (Ts, t2) in
   353               case arity_of S_Rep card T2 of
   354                 1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)
   355               | arity2 =>
   356                 let val res_arity = arity_of (R_Rep total) card T in
   357                   Project (Intersect
   358                       (Product (to_S_rep Ts t2,
   359                                 atom_seq_product_of (R_Rep total) card T),
   360                        to_R_rep Ts t1),
   361                       num_seq arity2 res_arity)
   362                 end
   363             end)
   364        | _ => error ("Not supported: Term " ^
   365                      quote (Syntax.string_of_term ctxt t) ^ "."))
   366       handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)
   367   in to_F (if total then NONE else SOME true) [] end
   368 
   369 fun bound_for_free total card i (s, T) =
   370   let val js = atom_schema_of (R_Rep total) card T in
   371     ([((length js, i), s)],
   372      [TupleSet [], atom_schema_of (R_Rep total) card T |> map (rpair 0)
   373                    |> tuple_set_from_atom_schema])
   374   end
   375 
   376 fun declarative_axiom_for_rel_expr total card Ts
   377                                    (Type (@{type_name fun}, [T1, T2])) r =
   378     if total andalso body_type T2 = bool_T then
   379       True
   380     else
   381       All (decls_for S_Rep card Ts T1,
   382            declarative_axiom_for_rel_expr total card (T1 :: Ts) T2
   383                (List.foldl Join r (vars_for_bound_var card S_Rep (T1 :: Ts) 0)))
   384   | declarative_axiom_for_rel_expr total _ _ _ r =
   385     (if total then One else Lone) r
   386 fun declarative_axiom_for_free total card i (_, T) =
   387   declarative_axiom_for_rel_expr total card [] T
   388       (Rel (arity_of (R_Rep total) card T, i))
   389 
   390 (* Hack to make the old code work as is with sets. *)
   391 fun unsetify_type (Type (@{type_name set}, [T])) = unsetify_type T --> bool_T
   392   | unsetify_type (Type (s, Ts)) = Type (s, map unsetify_type Ts)
   393   | unsetify_type T = T
   394 
   395 fun kodkod_problem_from_term ctxt total raw_card raw_infinite t =
   396   let
   397     val thy = Proof_Context.theory_of ctxt
   398     fun card (Type (@{type_name fun}, [T1, T2])) =
   399         reasonable_power (card T2) (card T1)
   400       | card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2
   401       | card @{typ bool} = 2
   402       | card T = Int.max (1, raw_card T)
   403     fun complete (Type (@{type_name fun}, [T1, T2])) =
   404         concrete T1 andalso complete T2
   405       | complete (Type (@{type_name prod}, Ts)) = forall complete Ts
   406       | complete T = not (raw_infinite T)
   407     and concrete (Type (@{type_name fun}, [T1, T2])) =
   408         complete T1 andalso concrete T2
   409       | concrete (Type (@{type_name prod}, Ts)) = forall concrete Ts
   410       | concrete _ = true
   411     val neg_t =
   412       @{const Not} $ Object_Logic.atomize_term thy t
   413       |> map_types unsetify_type
   414     val _ = fold_types (K o check_type ctxt raw_infinite) neg_t ()
   415     val frees = Term.add_frees neg_t []
   416     val bounds =
   417       map2 (bound_for_free total card) (index_seq 0 (length frees)) frees
   418     val declarative_axioms =
   419       map2 (declarative_axiom_for_free total card)
   420            (index_seq 0 (length frees)) frees
   421     val formula =
   422       neg_t |> kodkod_formula_from_term ctxt total card complete concrete frees 
   423             |> fold_rev (curry And) declarative_axioms
   424     val univ_card = univ_card 0 0 0 bounds formula
   425   in
   426     {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
   427      bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
   428   end
   429 
   430 fun solve_any_kodkod_problem thy problems =
   431   let
   432     val {debug, overlord, ...} = Nitpick_Isar.default_params thy []
   433     val max_threads = 1
   434     val max_solutions = 1
   435   in
   436     case solve_any_problem debug overlord NONE max_threads max_solutions
   437                            problems of
   438       JavaNotFound => "unknown"
   439     | JavaTooOld => "unknown"
   440     | KodkodiNotInstalled => "unknown"
   441     | KodkodiTooOld => "unknown"
   442     | Normal ([], _, _) => "none"
   443     | Normal _ => "genuine"
   444     | TimedOut _ => "unknown"
   445     | Error (s, _) => error ("Kodkod error: " ^ s)
   446   end
   447 
   448 val default_raw_infinite = member (op =) [@{typ nat}, @{typ int}]
   449 
   450 fun minipick ctxt n t =
   451   let
   452     val thy = Proof_Context.theory_of ctxt
   453     val {total_consts, ...} = Nitpick_Isar.default_params thy []
   454     val totals =
   455       total_consts |> Option.map single |> the_default [true, false]
   456     fun problem_for (total, k) =
   457       kodkod_problem_from_term ctxt total (K k) default_raw_infinite t
   458   in
   459     (totals, 1 upto n)
   460     |-> map_product pair
   461     |> map problem_for
   462     |> solve_any_kodkod_problem (Proof_Context.theory_of ctxt)
   463   end
   464 
   465 fun minipick_expect ctxt expect n t =
   466   if getenv "KODKODI" <> "" then
   467     if minipick ctxt n t = expect then ()
   468     else error ("\"minipick_expect\" expected " ^ quote expect)
   469   else
   470     ()
   471 
   472 end;