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