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