src/HOL/Nitpick_Examples/minipick.ML
author blanchet
Wed Sep 21 15:55:16 2011 +0200 (2011-09-21)
changeset 45035 60d2c03d5c70
child 45062 9598cada31b3
permissions -rw-r--r--
reintroduced Minipick as Nitpick example
blanchet@45035
     1
(*  Title:      HOL/Nitpick_Examples/minipick.ML
blanchet@45035
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@45035
     3
    Copyright   2009-2010
blanchet@45035
     4
blanchet@45035
     5
Finite model generation for HOL formulas using Kodkod, minimalistic version.
blanchet@45035
     6
*)
blanchet@45035
     7
blanchet@45035
     8
signature MINIPICK =
blanchet@45035
     9
sig
blanchet@45035
    10
  datatype rep = S_Rep | R_Rep
blanchet@45035
    11
  type styp = Nitpick_Util.styp
blanchet@45035
    12
blanchet@45035
    13
  val vars_for_bound_var :
blanchet@45035
    14
    (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr list
blanchet@45035
    15
  val rel_expr_for_bound_var :
blanchet@45035
    16
    (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr
blanchet@45035
    17
  val decls_for : rep -> (typ -> int) -> typ list -> typ -> Kodkod.decl list
blanchet@45035
    18
  val false_atom : Kodkod.rel_expr
blanchet@45035
    19
  val true_atom : Kodkod.rel_expr
blanchet@45035
    20
  val formula_from_atom : Kodkod.rel_expr -> Kodkod.formula
blanchet@45035
    21
  val atom_from_formula : Kodkod.formula -> Kodkod.rel_expr
blanchet@45035
    22
  val kodkod_problem_from_term :
blanchet@45035
    23
    Proof.context -> (typ -> int) -> term -> Kodkod.problem
blanchet@45035
    24
  val solve_any_kodkod_problem : theory -> Kodkod.problem list -> string
blanchet@45035
    25
end;
blanchet@45035
    26
blanchet@45035
    27
structure Minipick : MINIPICK =
blanchet@45035
    28
struct
blanchet@45035
    29
blanchet@45035
    30
open Kodkod
blanchet@45035
    31
open Nitpick_Util
blanchet@45035
    32
open Nitpick_HOL
blanchet@45035
    33
open Nitpick_Peephole
blanchet@45035
    34
open Nitpick_Kodkod
blanchet@45035
    35
blanchet@45035
    36
datatype rep = S_Rep | R_Rep
blanchet@45035
    37
blanchet@45035
    38
fun check_type ctxt (Type (@{type_name fun}, Ts)) =
blanchet@45035
    39
    List.app (check_type ctxt) Ts
blanchet@45035
    40
  | check_type ctxt (Type (@{type_name prod}, Ts)) =
blanchet@45035
    41
    List.app (check_type ctxt) Ts
blanchet@45035
    42
  | check_type _ @{typ bool} = ()
blanchet@45035
    43
  | check_type _ (TFree (_, @{sort "{}"})) = ()
blanchet@45035
    44
  | check_type _ (TFree (_, @{sort HOL.type})) = ()
blanchet@45035
    45
  | check_type ctxt T =
blanchet@45035
    46
    raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
blanchet@45035
    47
blanchet@45035
    48
fun atom_schema_of S_Rep card (Type (@{type_name fun}, [T1, T2])) =
blanchet@45035
    49
    replicate_list (card T1) (atom_schema_of S_Rep card T2)
blanchet@45035
    50
  | atom_schema_of R_Rep card (Type (@{type_name fun}, [T1, @{typ bool}])) =
blanchet@45035
    51
    atom_schema_of S_Rep card T1
blanchet@45035
    52
  | atom_schema_of R_Rep card (Type (@{type_name fun}, [T1, T2])) =
blanchet@45035
    53
    atom_schema_of S_Rep card T1 @ atom_schema_of R_Rep card T2
blanchet@45035
    54
  | atom_schema_of _ card (Type (@{type_name prod}, Ts)) =
blanchet@45035
    55
    maps (atom_schema_of S_Rep card) Ts
blanchet@45035
    56
  | atom_schema_of _ card T = [card T]
blanchet@45035
    57
val arity_of = length ooo atom_schema_of
blanchet@45035
    58
blanchet@45035
    59
fun index_for_bound_var _ [_] 0 = 0
blanchet@45035
    60
  | index_for_bound_var card (_ :: Ts) 0 =
blanchet@45035
    61
    index_for_bound_var card Ts 0 + arity_of S_Rep card (hd Ts)
blanchet@45035
    62
  | index_for_bound_var card Ts n = index_for_bound_var card (tl Ts) (n - 1)
blanchet@45035
    63
fun vars_for_bound_var card R Ts j =
blanchet@45035
    64
  map (curry Var 1) (index_seq (index_for_bound_var card Ts j)
blanchet@45035
    65
                               (arity_of R card (nth Ts j)))
blanchet@45035
    66
val rel_expr_for_bound_var = foldl1 Product oooo vars_for_bound_var
blanchet@45035
    67
fun decls_for R card Ts T =
blanchet@45035
    68
  map2 (curry DeclOne o pair 1)
blanchet@45035
    69
       (index_seq (index_for_bound_var card (T :: Ts) 0)
blanchet@45035
    70
                  (arity_of R card (nth (T :: Ts) 0)))
blanchet@45035
    71
       (map (AtomSeq o rpair 0) (atom_schema_of R card T))
blanchet@45035
    72
blanchet@45035
    73
val atom_product = foldl1 Product o map Atom
blanchet@45035
    74
blanchet@45035
    75
val false_atom = Atom 0
blanchet@45035
    76
val true_atom = Atom 1
blanchet@45035
    77
blanchet@45035
    78
fun formula_from_atom r = RelEq (r, true_atom)
blanchet@45035
    79
fun atom_from_formula f = RelIf (f, true_atom, false_atom)
blanchet@45035
    80
blanchet@45035
    81
fun kodkod_formula_from_term ctxt card frees =
blanchet@45035
    82
  let
blanchet@45035
    83
    fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, @{typ bool}])) r =
blanchet@45035
    84
        let
blanchet@45035
    85
          val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
blanchet@45035
    86
                    |> all_combinations
blanchet@45035
    87
        in
blanchet@45035
    88
          map2 (fn i => fn js =>
blanchet@45035
    89
                   RelIf (formula_from_atom (Project (r, [Num i])),
blanchet@45035
    90
                          atom_product js, empty_n_ary_rel (length js)))
blanchet@45035
    91
               (index_seq 0 (length jss)) jss
blanchet@45035
    92
          |> foldl1 Union
blanchet@45035
    93
        end
blanchet@45035
    94
      | R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
blanchet@45035
    95
        let
blanchet@45035
    96
          val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
blanchet@45035
    97
                    |> all_combinations
blanchet@45035
    98
          val arity2 = arity_of S_Rep card T2
blanchet@45035
    99
        in
blanchet@45035
   100
          map2 (fn i => fn js =>
blanchet@45035
   101
                   Product (atom_product js,
blanchet@45035
   102
                            Project (r, num_seq (i * arity2) arity2)
blanchet@45035
   103
                            |> R_rep_from_S_rep T2))
blanchet@45035
   104
               (index_seq 0 (length jss)) jss
blanchet@45035
   105
          |> foldl1 Union
blanchet@45035
   106
        end
blanchet@45035
   107
      | R_rep_from_S_rep _ r = r
blanchet@45035
   108
    fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
blanchet@45035
   109
        Comprehension (decls_for S_Rep card Ts T,
blanchet@45035
   110
            RelEq (R_rep_from_S_rep T
blanchet@45035
   111
                       (rel_expr_for_bound_var card S_Rep (T :: Ts) 0), r))
blanchet@45035
   112
      | S_rep_from_R_rep _ _ r = r
blanchet@45035
   113
    fun to_F Ts t =
blanchet@45035
   114
      (case t of
blanchet@45035
   115
         @{const Not} $ t1 => Not (to_F Ts t1)
blanchet@45035
   116
       | @{const False} => False
blanchet@45035
   117
       | @{const True} => True
blanchet@45035
   118
       | Const (@{const_name All}, _) $ Abs (_, T, t') =>
blanchet@45035
   119
         All (decls_for S_Rep card Ts T, to_F (T :: Ts) t')
blanchet@45035
   120
       | (t0 as Const (@{const_name All}, _)) $ t1 =>
blanchet@45035
   121
         to_F Ts (t0 $ eta_expand Ts t1 1)
blanchet@45035
   122
       | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
blanchet@45035
   123
         Exist (decls_for S_Rep card Ts T, to_F (T :: Ts) t')
blanchet@45035
   124
       | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
blanchet@45035
   125
         to_F Ts (t0 $ eta_expand Ts t1 1)
blanchet@45035
   126
       | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
blanchet@45035
   127
         RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
blanchet@45035
   128
       | Const (@{const_name ord_class.less_eq},
blanchet@45035
   129
                Type (@{type_name fun},
blanchet@45035
   130
                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
blanchet@45035
   131
         $ t1 $ t2 =>
blanchet@45035
   132
         Subset (to_R_rep Ts t1, to_R_rep Ts t2)
blanchet@45035
   133
       | @{const HOL.conj} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
blanchet@45035
   134
       | @{const HOL.disj} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
blanchet@45035
   135
       | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
blanchet@45035
   136
       | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
blanchet@45035
   137
       | Free _ => raise SAME ()
blanchet@45035
   138
       | Term.Var _ => raise SAME ()
blanchet@45035
   139
       | Bound _ => raise SAME ()
blanchet@45035
   140
       | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
blanchet@45035
   141
       | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
blanchet@45035
   142
      handle SAME () => formula_from_atom (to_R_rep Ts t)
blanchet@45035
   143
    and to_S_rep Ts t =
blanchet@45035
   144
      case t of
blanchet@45035
   145
        Const (@{const_name Pair}, _) $ t1 $ t2 =>
blanchet@45035
   146
        Product (to_S_rep Ts t1, to_S_rep Ts t2)
blanchet@45035
   147
      | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts (eta_expand Ts t 1)
blanchet@45035
   148
      | Const (@{const_name Pair}, _) => to_S_rep Ts (eta_expand Ts t 2)
blanchet@45035
   149
      | Const (@{const_name fst}, _) $ t1 =>
blanchet@45035
   150
        let val fst_arity = arity_of S_Rep card (fastype_of1 (Ts, t)) in
blanchet@45035
   151
          Project (to_S_rep Ts t1, num_seq 0 fst_arity)
blanchet@45035
   152
        end
blanchet@45035
   153
      | Const (@{const_name fst}, _) => to_S_rep Ts (eta_expand Ts t 1)
blanchet@45035
   154
      | Const (@{const_name snd}, _) $ t1 =>
blanchet@45035
   155
        let
blanchet@45035
   156
          val pair_arity = arity_of S_Rep card (fastype_of1 (Ts, t1))
blanchet@45035
   157
          val snd_arity = arity_of S_Rep card (fastype_of1 (Ts, t))
blanchet@45035
   158
          val fst_arity = pair_arity - snd_arity
blanchet@45035
   159
        in Project (to_S_rep Ts t1, num_seq fst_arity snd_arity) end
blanchet@45035
   160
      | Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)
blanchet@45035
   161
      | Bound j => rel_expr_for_bound_var card S_Rep Ts j
blanchet@45035
   162
      | _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)
blanchet@45035
   163
    and to_R_rep Ts t =
blanchet@45035
   164
      (case t of
blanchet@45035
   165
         @{const Not} => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   166
       | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   167
       | Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   168
       | Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   169
       | Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)
blanchet@45035
   170
       | Const (@{const_name ord_class.less_eq},
blanchet@45035
   171
                Type (@{type_name fun},
blanchet@45035
   172
                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
blanchet@45035
   173
         to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   174
       | Const (@{const_name ord_class.less_eq}, _) =>
blanchet@45035
   175
         to_R_rep Ts (eta_expand Ts t 2)
blanchet@45035
   176
       | @{const HOL.conj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   177
       | @{const HOL.conj} => to_R_rep Ts (eta_expand Ts t 2)
blanchet@45035
   178
       | @{const HOL.disj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   179
       | @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)
blanchet@45035
   180
       | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   181
       | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
blanchet@45035
   182
       | Const (@{const_name bot_class.bot},
blanchet@45035
   183
                T as Type (@{type_name fun}, [_, @{typ bool}])) =>
blanchet@45035
   184
         empty_n_ary_rel (arity_of R_Rep card T)
blanchet@45035
   185
       | Const (@{const_name insert}, _) $ t1 $ t2 =>
blanchet@45035
   186
         Union (to_S_rep Ts t1, to_R_rep Ts t2)
blanchet@45035
   187
       | Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   188
       | Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2)
blanchet@45035
   189
       | Const (@{const_name trancl}, _) $ t1 =>
blanchet@45035
   190
         if arity_of R_Rep card (fastype_of1 (Ts, t1)) = 2 then
blanchet@45035
   191
           Closure (to_R_rep Ts t1)
blanchet@45035
   192
         else
blanchet@45035
   193
           raise NOT_SUPPORTED "transitive closure for function or pair type"
blanchet@45035
   194
       | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   195
       | Const (@{const_name inf_class.inf},
blanchet@45035
   196
                Type (@{type_name fun},
blanchet@45035
   197
                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
blanchet@45035
   198
         $ t1 $ t2 =>
blanchet@45035
   199
         Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
blanchet@45035
   200
       | Const (@{const_name inf_class.inf}, _) $ _ =>
blanchet@45035
   201
         to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   202
       | Const (@{const_name inf_class.inf}, _) =>
blanchet@45035
   203
         to_R_rep Ts (eta_expand Ts t 2)
blanchet@45035
   204
       | Const (@{const_name sup_class.sup},
blanchet@45035
   205
                Type (@{type_name fun},
blanchet@45035
   206
                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
blanchet@45035
   207
         $ t1 $ t2 =>
blanchet@45035
   208
         Union (to_R_rep Ts t1, to_R_rep Ts t2)
blanchet@45035
   209
       | Const (@{const_name sup_class.sup}, _) $ _ =>
blanchet@45035
   210
         to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   211
       | Const (@{const_name sup_class.sup}, _) =>
blanchet@45035
   212
         to_R_rep Ts (eta_expand Ts t 2)
blanchet@45035
   213
       | Const (@{const_name minus_class.minus},
blanchet@45035
   214
                Type (@{type_name fun},
blanchet@45035
   215
                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
blanchet@45035
   216
         $ t1 $ t2 =>
blanchet@45035
   217
         Difference (to_R_rep Ts t1, to_R_rep Ts t2)
blanchet@45035
   218
       | Const (@{const_name minus_class.minus},
blanchet@45035
   219
                Type (@{type_name fun},
blanchet@45035
   220
                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
blanchet@45035
   221
         to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   222
       | Const (@{const_name minus_class.minus},
blanchet@45035
   223
                Type (@{type_name fun},
blanchet@45035
   224
                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
blanchet@45035
   225
         to_R_rep Ts (eta_expand Ts t 2)
blanchet@45035
   226
       | Const (@{const_name Pair}, _) $ _ $ _ => raise SAME ()
blanchet@45035
   227
       | Const (@{const_name Pair}, _) $ _ => raise SAME ()
blanchet@45035
   228
       | Const (@{const_name Pair}, _) => raise SAME ()
blanchet@45035
   229
       | Const (@{const_name fst}, _) $ _ => raise SAME ()
blanchet@45035
   230
       | Const (@{const_name fst}, _) => raise SAME ()
blanchet@45035
   231
       | Const (@{const_name snd}, _) $ _ => raise SAME ()
blanchet@45035
   232
       | Const (@{const_name snd}, _) => raise SAME ()
blanchet@45035
   233
       | Const (_, @{typ bool}) => atom_from_formula (to_F Ts t)
blanchet@45035
   234
       | Free (x as (_, T)) =>
blanchet@45035
   235
         Rel (arity_of R_Rep card T, find_index (curry (op =) x) frees)
blanchet@45035
   236
       | Term.Var _ => raise NOT_SUPPORTED "schematic variables"
blanchet@45035
   237
       | Bound _ => raise SAME ()
blanchet@45035
   238
       | Abs (_, T, t') =>
blanchet@45035
   239
         (case fastype_of1 (T :: Ts, t') of
blanchet@45035
   240
            @{typ bool} => Comprehension (decls_for S_Rep card Ts T,
blanchet@45035
   241
                                          to_F (T :: Ts) t')
blanchet@45035
   242
          | T' => Comprehension (decls_for S_Rep card Ts T @
blanchet@45035
   243
                                 decls_for R_Rep card (T :: Ts) T',
blanchet@45035
   244
                                 Subset (rel_expr_for_bound_var card R_Rep
blanchet@45035
   245
                                                              (T' :: T :: Ts) 0,
blanchet@45035
   246
                                         to_R_rep (T :: Ts) t')))
blanchet@45035
   247
       | t1 $ t2 =>
blanchet@45035
   248
         (case fastype_of1 (Ts, t) of
blanchet@45035
   249
            @{typ bool} => atom_from_formula (to_F Ts t)
blanchet@45035
   250
          | T =>
blanchet@45035
   251
            let val T2 = fastype_of1 (Ts, t2) in
blanchet@45035
   252
              case arity_of S_Rep card T2 of
blanchet@45035
   253
                1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)
blanchet@45035
   254
              | arity2 =>
blanchet@45035
   255
                let val res_arity = arity_of R_Rep card T in
blanchet@45035
   256
                  Project (Intersect
blanchet@45035
   257
                      (Product (to_S_rep Ts t2,
blanchet@45035
   258
                                atom_schema_of R_Rep card T
blanchet@45035
   259
                                |> map (AtomSeq o rpair 0) |> foldl1 Product),
blanchet@45035
   260
                       to_R_rep Ts t1),
blanchet@45035
   261
                      num_seq arity2 res_arity)
blanchet@45035
   262
                end
blanchet@45035
   263
            end)
blanchet@45035
   264
       | _ => raise NOT_SUPPORTED ("term " ^
blanchet@45035
   265
                                   quote (Syntax.string_of_term ctxt t)))
blanchet@45035
   266
      handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)
blanchet@45035
   267
  in to_F [] end
blanchet@45035
   268
blanchet@45035
   269
fun bound_for_free card i (s, T) =
blanchet@45035
   270
  let val js = atom_schema_of R_Rep card T in
blanchet@45035
   271
    ([((length js, i), s)],
blanchet@45035
   272
     [TupleSet [], atom_schema_of R_Rep card T |> map (rpair 0)
blanchet@45035
   273
                   |> tuple_set_from_atom_schema])
blanchet@45035
   274
  end
blanchet@45035
   275
blanchet@45035
   276
fun declarative_axiom_for_rel_expr card Ts (Type (@{type_name fun}, [T1, T2]))
blanchet@45035
   277
                                   r =
blanchet@45035
   278
    if body_type T2 = bool_T then
blanchet@45035
   279
      True
blanchet@45035
   280
    else
blanchet@45035
   281
      All (decls_for S_Rep card Ts T1,
blanchet@45035
   282
           declarative_axiom_for_rel_expr card (T1 :: Ts) T2
blanchet@45035
   283
               (List.foldl Join r (vars_for_bound_var card S_Rep (T1 :: Ts) 0)))
blanchet@45035
   284
  | declarative_axiom_for_rel_expr _ _ _ r = One r
blanchet@45035
   285
fun declarative_axiom_for_free card i (_, T) =
blanchet@45035
   286
  declarative_axiom_for_rel_expr card [] T (Rel (arity_of R_Rep card T, i))
blanchet@45035
   287
blanchet@45035
   288
fun kodkod_problem_from_term ctxt raw_card t =
blanchet@45035
   289
  let
blanchet@45035
   290
    val thy = ProofContext.theory_of ctxt
blanchet@45035
   291
    fun card (Type (@{type_name fun}, [T1, T2])) =
blanchet@45035
   292
        reasonable_power (card T2) (card T1)
blanchet@45035
   293
      | card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2
blanchet@45035
   294
      | card @{typ bool} = 2
blanchet@45035
   295
      | card T = Int.max (1, raw_card T)
blanchet@45035
   296
    val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
blanchet@45035
   297
    val _ = fold_types (K o check_type ctxt) neg_t ()
blanchet@45035
   298
    val frees = Term.add_frees neg_t []
blanchet@45035
   299
    val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
blanchet@45035
   300
    val declarative_axioms =
blanchet@45035
   301
      map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
blanchet@45035
   302
    val formula = kodkod_formula_from_term ctxt card frees neg_t
blanchet@45035
   303
                  |> fold_rev (curry And) declarative_axioms
blanchet@45035
   304
    val univ_card = univ_card 0 0 0 bounds formula
blanchet@45035
   305
  in
blanchet@45035
   306
    {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
blanchet@45035
   307
     bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
blanchet@45035
   308
  end
blanchet@45035
   309
blanchet@45035
   310
fun solve_any_kodkod_problem thy problems =
blanchet@45035
   311
  let
blanchet@45035
   312
    val {debug, overlord, ...} = Nitpick_Isar.default_params thy []
blanchet@45035
   313
    val max_threads = 1
blanchet@45035
   314
    val max_solutions = 1
blanchet@45035
   315
  in
blanchet@45035
   316
    case solve_any_problem debug overlord NONE max_threads max_solutions
blanchet@45035
   317
                           problems of
blanchet@45035
   318
      JavaNotInstalled => "unknown"
blanchet@45035
   319
    | JavaTooOld => "unknown"
blanchet@45035
   320
    | KodkodiNotInstalled => "unknown"
blanchet@45035
   321
    | Normal ([], _, _) => "none"
blanchet@45035
   322
    | Normal _ => "genuine"
blanchet@45035
   323
    | TimedOut _ => "unknown"
blanchet@45035
   324
    | Error (s, _) => error ("Kodkod error: " ^ s)
blanchet@45035
   325
  end
blanchet@45035
   326
blanchet@45035
   327
end;