src/HOL/Tools/Nitpick/nitpick_tests.ML
author blanchet
Sat Apr 24 16:17:30 2010 +0200 (2010-04-24)
changeset 36384 76d5fd5a45fb
parent 35866 513074557e06
child 36385 ff5f88702590
permissions -rw-r--r--
cosmetics
blanchet@33982
     1
(*  Title:      HOL/Tools/Nitpick/nitpick_tests.ML
blanchet@33192
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@34982
     3
    Copyright   2008, 2009, 2010
blanchet@33192
     4
blanchet@33192
     5
Unit tests for Nitpick.
blanchet@33192
     6
*)
blanchet@33192
     7
blanchet@33192
     8
signature NITPICK_TESTS =
blanchet@33192
     9
sig
blanchet@33192
    10
  val run_all_tests : unit -> unit
blanchet@35866
    11
end;
blanchet@33192
    12
blanchet@33232
    13
structure Nitpick_Tests =
blanchet@33192
    14
struct
blanchet@33192
    15
blanchet@33232
    16
open Nitpick_Util
blanchet@33232
    17
open Nitpick_Peephole
blanchet@33232
    18
open Nitpick_Rep
blanchet@33232
    19
open Nitpick_Nut
blanchet@33232
    20
open Nitpick_Kodkod
blanchet@33192
    21
blanchet@35388
    22
val settings = [("solver", "\"DefaultSAT4J\"")]
blanchet@33192
    23
blanchet@33192
    24
fun cast_to_rep R u = Op1 (Cast, type_of u, R, u)
blanchet@33192
    25
blanchet@33192
    26
val unit_T = @{typ unit}
blanchet@33192
    27
val dummy_T = @{typ 'a}
blanchet@33192
    28
blanchet@33192
    29
val unity = Cst (Unity, unit_T, Unit)
blanchet@33192
    30
val atom1_v1 = FreeName ("atom1_v1", dummy_T, Atom (1, 0))
blanchet@33192
    31
val atom2_v1 = FreeName ("atom2_v1", dummy_T, Atom (2, 0))
blanchet@33192
    32
val atom6_v1 = FreeName ("atom6_v1", dummy_T, Atom (6, 0))
blanchet@33192
    33
val atom16_v1 = FreeName ("atom16_v1", dummy_T, Atom (16, 0))
blanchet@33192
    34
val atom24_v1 = FreeName ("atom24_v1", dummy_T, Atom (24, 0))
blanchet@33192
    35
val atom36_v1 = FreeName ("atom36_v1", dummy_T, Atom (36, 0))
blanchet@33192
    36
val atom81_v1 = FreeName ("atom81_v1", dummy_T, Atom (81, 0))
blanchet@33192
    37
val struct_atom1_atom1_v1 =
blanchet@33192
    38
  FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Atom (1, 0), Atom (1, 0)])
blanchet@33192
    39
val struct_atom1_unit_v1 =
blanchet@33192
    40
  FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Atom (1, 0), Unit])
blanchet@33192
    41
val struct_unit_atom1_v1 =
blanchet@33192
    42
  FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Unit, Atom (1, 0)])
blanchet@33192
    43
blanchet@33192
    44
(*
blanchet@33192
    45
              Formula    Unit   Atom    Struct    Vect    Func
blanchet@33192
    46
    Formula      X       N/A     X        X       N/A     N/A
blanchet@33192
    47
    Unit        N/A      N/A    N/A      N/A      N/A     N/A
blanchet@33192
    48
    Atom         X       N/A     X        X        X       X
blanchet@33192
    49
    Struct      N/A      N/A     X        X       N/A     N/A
blanchet@33192
    50
    Vect        N/A      N/A     X       N/A       X       X
blanchet@33192
    51
    Func        N/A      N/A     X       N/A       X       X
blanchet@33192
    52
*)
blanchet@33192
    53
blanchet@33192
    54
val tests =
blanchet@33192
    55
  [("rep_conversion_formula_formula",
blanchet@33192
    56
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    57
         cast_to_rep (Formula Neut)
blanchet@33192
    58
                     (cast_to_rep (Formula Neut) atom2_v1), atom2_v1)),
blanchet@33192
    59
   ("rep_conversion_atom_atom",
blanchet@33192
    60
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    61
         cast_to_rep (Atom (16, 0)) (cast_to_rep (Atom (16, 0)) atom16_v1),
blanchet@33192
    62
         atom16_v1)),
blanchet@33192
    63
   ("rep_conversion_struct_struct_1",
blanchet@33192
    64
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    65
         cast_to_rep (Struct [Atom (4, 0), Atom (6, 0)])
blanchet@33192
    66
             (cast_to_rep (Struct [Atom (4, 0), Atom (6, 0)]) atom24_v1),
blanchet@33192
    67
         atom24_v1)),
blanchet@33192
    68
   ("rep_conversion_struct_struct_2",
blanchet@33192
    69
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    70
         cast_to_rep (Struct [Atom (4, 0), Struct [Atom (2, 0), Atom (3, 0)]])
blanchet@33192
    71
             (cast_to_rep (Struct [Atom (4, 0), Atom (6, 0)]) atom24_v1),
blanchet@33192
    72
         atom24_v1)),
blanchet@33192
    73
   ("rep_conversion_struct_struct_3",
blanchet@33192
    74
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    75
         cast_to_rep (Struct [Atom (4, 0), Atom (6, 0)])
blanchet@33192
    76
             (cast_to_rep (Struct [Atom (4, 0),
blanchet@33192
    77
                                   Struct [Atom (2, 0), Atom (3, 0)]])
blanchet@33192
    78
                          atom24_v1),
blanchet@33192
    79
         atom24_v1)),
blanchet@33192
    80
   ("rep_conversion_struct_struct_4",
blanchet@33192
    81
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    82
         cast_to_rep (Struct [Atom (24, 0), Unit])
blanchet@33192
    83
             (cast_to_rep (Struct [Atom (24, 0), Atom (1, 0)]) atom24_v1),
blanchet@33192
    84
         atom24_v1)),
blanchet@33192
    85
   ("rep_conversion_struct_struct_5",
blanchet@33192
    86
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    87
         cast_to_rep (Struct [Atom (24, 0), Atom (1, 0)])
blanchet@33192
    88
             (cast_to_rep (Struct [Atom (24, 0), Unit]) atom24_v1),
blanchet@33192
    89
         atom24_v1)),
blanchet@33192
    90
   ("rep_conversion_struct_struct_6",
blanchet@33192
    91
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    92
         cast_to_rep (Struct [Atom (1, 0), Atom (1, 0)])
blanchet@33192
    93
             (cast_to_rep (Struct [Atom (1, 0), Unit])
blanchet@33192
    94
                 (cast_to_rep (Struct [Unit, Atom (1, 0)]) atom1_v1)),
blanchet@33192
    95
         atom1_v1)),
blanchet@33192
    96
   ("rep_conversion_vect_vect_1",
blanchet@33192
    97
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    98
         cast_to_rep (Atom (16, 0))
blanchet@33192
    99
             (cast_to_rep (Vect (2, Atom (4, 0)))
blanchet@33192
   100
                  (cast_to_rep (Vect (2, Struct [Atom (2, 0), Atom (2, 0)]))
blanchet@33192
   101
                               atom16_v1)),
blanchet@33192
   102
         atom16_v1)),
blanchet@33192
   103
   ("rep_conversion_vect_vect_2",
blanchet@33192
   104
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   105
         cast_to_rep (Atom (16, 0))
blanchet@33192
   106
             (cast_to_rep (Vect (2, Struct [Atom (2, 0), Atom (2, 0)]))
blanchet@33192
   107
                  (cast_to_rep (Vect (2, Atom (4, 0))) atom16_v1)),
blanchet@33192
   108
         atom16_v1)),
blanchet@33192
   109
   ("rep_conversion_vect_vect_3",
blanchet@33192
   110
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   111
         cast_to_rep (Atom (16, 0))
blanchet@33192
   112
             (cast_to_rep (Vect (2, Atom (4, 0)))
blanchet@33192
   113
                  (cast_to_rep (Vect (2, Vect (2, Atom (2, 0)))) atom16_v1)),
blanchet@33192
   114
         atom16_v1)),
blanchet@33192
   115
   ("rep_conversion_vect_vect_4",
blanchet@33192
   116
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   117
         cast_to_rep (Atom (16, 0))
blanchet@33192
   118
             (cast_to_rep (Vect (2, Vect (2, Atom (2, 0))))
blanchet@33192
   119
                  (cast_to_rep (Vect (2, Atom (4, 0))) atom16_v1)),
blanchet@33192
   120
         atom16_v1)),
blanchet@33192
   121
   ("rep_conversion_func_func_1",
blanchet@33192
   122
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   123
         cast_to_rep (Atom (36, 0))
blanchet@33192
   124
             (cast_to_rep (Func (Atom (2, 0),
blanchet@33192
   125
                                 Struct [Atom (2, 0), Atom (3, 0)]))
blanchet@33192
   126
                  (cast_to_rep (Func (Atom (2, 0), Atom (6, 0))) atom36_v1)),
blanchet@33192
   127
         atom36_v1)),
blanchet@33192
   128
   ("rep_conversion_func_func_2",
blanchet@33192
   129
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   130
         cast_to_rep (Atom (36, 0))
blanchet@33192
   131
             (cast_to_rep (Func (Atom (2, 0), Atom (6, 0)))
blanchet@33192
   132
                  (cast_to_rep (Func (Atom (2, 0),
blanchet@33192
   133
                                Struct [Atom (2, 0), Atom (3, 0)]))
blanchet@33192
   134
                       atom36_v1)),
blanchet@33192
   135
         atom36_v1)),
blanchet@33192
   136
   ("rep_conversion_func_func_3",
blanchet@33192
   137
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   138
         cast_to_rep (Atom (36, 0))
blanchet@33192
   139
             (cast_to_rep (Func (Unit, Struct [Atom (6, 0), Atom (6, 0)]))
blanchet@33192
   140
                  (cast_to_rep (Func (Atom (1, 0), Atom (36, 0))) atom36_v1)),
blanchet@33192
   141
         atom36_v1)),
blanchet@33192
   142
   ("rep_conversion_func_func_4",
blanchet@33192
   143
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   144
         cast_to_rep (Atom (36, 0))
blanchet@33192
   145
             (cast_to_rep (Func (Atom (1, 0), Atom (36, 0)))
blanchet@33192
   146
                  (cast_to_rep (Func (Unit, Struct [Atom (6, 0), Atom (6, 0)]))
blanchet@33192
   147
                       atom36_v1)),
blanchet@33192
   148
         atom36_v1)),
blanchet@33192
   149
   ("rep_conversion_func_func_5",
blanchet@33192
   150
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   151
         cast_to_rep (Atom (36, 0))
blanchet@33192
   152
             (cast_to_rep (Func (Unit, Vect (2, Atom (6, 0))))
blanchet@33192
   153
                  (cast_to_rep (Func (Atom (1, 0), Atom (36, 0))) atom36_v1)),
blanchet@33192
   154
         atom36_v1)),
blanchet@33192
   155
   ("rep_conversion_func_func_6",
blanchet@33192
   156
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   157
         cast_to_rep (Atom (36, 0))
blanchet@33192
   158
             (cast_to_rep (Func (Atom (1, 0), Atom (36, 0)))
blanchet@33192
   159
                  (cast_to_rep (Func (Unit, Vect (2, Atom (6, 0))))
blanchet@33192
   160
                       atom36_v1)),
blanchet@33192
   161
         atom36_v1)),
blanchet@33192
   162
   ("rep_conversion_func_func_7",
blanchet@33192
   163
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   164
         cast_to_rep (Atom (2, 0))
blanchet@33192
   165
             (cast_to_rep (Func (Unit, Atom (2, 0)))
blanchet@33192
   166
                  (cast_to_rep (Func (Atom (1, 0), Formula Neut)) atom2_v1)),
blanchet@33192
   167
         atom2_v1)),
blanchet@33192
   168
   ("rep_conversion_func_func_8",
blanchet@33192
   169
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   170
         cast_to_rep (Atom (2, 0))
blanchet@33192
   171
             (cast_to_rep (Func (Atom (1, 0), Formula Neut))
blanchet@33192
   172
                  (cast_to_rep (Func (Unit, Atom (2, 0))) atom2_v1)),
blanchet@33192
   173
         atom2_v1)),
blanchet@33192
   174
   ("rep_conversion_atom_formula_atom",
blanchet@33192
   175
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   176
         cast_to_rep (Atom (2, 0)) (cast_to_rep (Formula Neut) atom2_v1),
blanchet@33192
   177
         atom2_v1)),
blanchet@33192
   178
   ("rep_conversion_unit_atom",
blanchet@33192
   179
    Op2 (Eq, bool_T, Formula Neut, cast_to_rep (Atom (1, 0)) unity, unity)),
blanchet@33192
   180
   ("rep_conversion_atom_struct_atom1",
blanchet@33192
   181
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   182
         cast_to_rep (Atom (6, 0))
blanchet@33192
   183
                     (cast_to_rep (Struct [Atom (3, 0), Atom (2, 0)]) atom6_v1),
blanchet@33192
   184
         atom6_v1)),
blanchet@33192
   185
   ("rep_conversion_atom_struct_atom_2",
blanchet@33192
   186
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   187
         cast_to_rep (Atom (24, 0))
blanchet@33192
   188
             (cast_to_rep (Struct [Struct [Atom (3, 0), Atom (4, 0)],
blanchet@33192
   189
                                   Atom (2, 0)]) atom24_v1),
blanchet@33192
   190
         atom24_v1)),
blanchet@33192
   191
   ("rep_conversion_atom_struct_atom_3",
blanchet@33192
   192
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   193
         cast_to_rep (Atom (6, 0))
blanchet@33192
   194
                     (cast_to_rep (Struct [Atom (6, 0), Unit]) atom6_v1),
blanchet@33192
   195
         atom6_v1)),
blanchet@33192
   196
   ("rep_conversion_atom_struct_atom_4",
blanchet@33192
   197
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   198
         cast_to_rep (Atom (6, 0))
blanchet@33192
   199
             (cast_to_rep (Struct [Struct [Atom (3, 0), Unit], Atom (2, 0)]) 
blanchet@33192
   200
             atom6_v1),
blanchet@33192
   201
         atom6_v1)),
blanchet@33192
   202
   ("rep_conversion_atom_vect_func_atom_1",
blanchet@33192
   203
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   204
         cast_to_rep (Atom (16, 0))
blanchet@33192
   205
             (cast_to_rep (Vect (4, Atom (2, 0)))
blanchet@33192
   206
                  (cast_to_rep (Func (Atom (4, 0), Atom (2, 0))) atom16_v1)),
blanchet@33192
   207
         atom16_v1)),
blanchet@33192
   208
   ("rep_conversion_atom_vect_func_atom_2",
blanchet@33192
   209
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   210
         cast_to_rep (Atom (16, 0))
blanchet@33192
   211
             (cast_to_rep (Vect (4, Atom (2, 0)))
blanchet@33192
   212
                  (cast_to_rep (Func (Atom (4, 0), Atom (2, 0))) atom16_v1)),
blanchet@33192
   213
         atom16_v1)),
blanchet@33192
   214
   ("rep_conversion_atom_vect_func_atom_3",
blanchet@33192
   215
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   216
         cast_to_rep (Atom (16, 0))
blanchet@33192
   217
             (cast_to_rep (Vect (4, Atom (2, 0)))
blanchet@33192
   218
                  (cast_to_rep (Func (Atom (4, 0), Formula Neut)) atom16_v1)),
blanchet@33192
   219
         atom16_v1)),
blanchet@33192
   220
   ("rep_conversion_atom_vect_func_atom_4",
blanchet@33192
   221
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   222
         cast_to_rep (Atom (16, 0))
blanchet@33192
   223
             (cast_to_rep (Vect (1, Atom (16, 0)))
blanchet@33192
   224
                  (cast_to_rep (Func (Unit, Atom (16, 0))) atom16_v1)),
blanchet@33192
   225
         atom16_v1)),
blanchet@33192
   226
   ("rep_conversion_atom_vect_func_atom_5",
blanchet@33192
   227
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   228
         cast_to_rep (Atom (16, 0))
blanchet@33192
   229
             (cast_to_rep (Vect (1, Atom (16, 0)))
blanchet@33192
   230
                  (cast_to_rep (Func (Unit, Atom (16, 0))) atom16_v1)),
blanchet@33192
   231
         atom16_v1)),
blanchet@33192
   232
   ("rep_conversion_atom_func_vect_atom_1",
blanchet@33192
   233
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   234
         cast_to_rep (Atom (16, 0))
blanchet@33192
   235
             (cast_to_rep (Func (Atom (4, 0), Atom (2, 0)))
blanchet@33192
   236
                  (cast_to_rep (Vect (4, Atom (2, 0))) atom16_v1)),
blanchet@33192
   237
         atom16_v1)),
blanchet@33192
   238
   ("rep_conversion_atom_func_vect_atom_2",
blanchet@33192
   239
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   240
         cast_to_rep (Atom (16, 0))
blanchet@33192
   241
             (cast_to_rep (Func (Atom (4, 0), Atom (2, 0)))
blanchet@33192
   242
                  (cast_to_rep (Vect (4, Atom (2, 0))) atom16_v1)),
blanchet@33192
   243
         atom16_v1)),
blanchet@33192
   244
   ("rep_conversion_atom_func_vect_atom_3",
blanchet@33192
   245
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   246
         cast_to_rep (Atom (16, 0))
blanchet@33192
   247
             (cast_to_rep (Func (Atom (4, 0), Formula Neut))
blanchet@33192
   248
                  (cast_to_rep (Vect (4, Atom (2, 0))) atom16_v1)),
blanchet@33192
   249
         atom16_v1)),
blanchet@33192
   250
   ("rep_conversion_atom_func_vect_atom_4",
blanchet@33192
   251
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   252
         cast_to_rep (Atom (16, 0))
blanchet@33192
   253
             (cast_to_rep (Func (Unit, Atom (16, 0)))
blanchet@33192
   254
                  (cast_to_rep (Vect (1, Atom (16, 0))) atom16_v1)),
blanchet@33192
   255
         atom16_v1)),
blanchet@33192
   256
   ("rep_conversion_atom_func_vect_atom_5",
blanchet@33192
   257
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   258
         cast_to_rep (Atom (16, 0))
blanchet@33192
   259
             (cast_to_rep (Func (Atom (1, 0), Atom (16, 0)))
blanchet@33192
   260
                  (cast_to_rep (Vect (1, Atom (16, 0))) atom16_v1)),
blanchet@33192
   261
         atom16_v1)),
blanchet@33192
   262
   ("rep_conversion_atom_vect_atom",
blanchet@33192
   263
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   264
         cast_to_rep (Atom (36, 0))
blanchet@33192
   265
             (cast_to_rep (Vect (2, Struct [Atom (2, 0), Atom (3, 0)]))
blanchet@33192
   266
                          atom36_v1),
blanchet@33192
   267
         atom36_v1)),
blanchet@33192
   268
   ("rep_conversion_atom_func_atom",
blanchet@33192
   269
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   270
         cast_to_rep (Atom (36, 0))
blanchet@33192
   271
             (cast_to_rep (Func (Atom (2, 0),
blanchet@33192
   272
                           Struct [Atom (2, 0), Atom (3, 0)])) atom36_v1),
blanchet@33192
   273
         atom36_v1)),
blanchet@33192
   274
   ("rep_conversion_struct_atom1_1",
blanchet@33192
   275
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   276
         cast_to_rep (Struct [Atom (1, 0), Atom (1, 0)]) atom1_v1,
blanchet@33192
   277
                      struct_atom1_atom1_v1)),
blanchet@33192
   278
   ("rep_conversion_struct_atom1_2",
blanchet@33192
   279
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   280
         cast_to_rep (Struct [Atom (1, 0), Unit]) atom1_v1,
blanchet@33192
   281
                      struct_atom1_unit_v1)),
blanchet@33192
   282
   ("rep_conversion_struct_atom1_3",
blanchet@33192
   283
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   284
         cast_to_rep (Struct [Unit, Atom (1, 0)]) atom1_v1,
blanchet@33192
   285
                      struct_unit_atom1_v1))
blanchet@33192
   286
(*
blanchet@33192
   287
   ("rep_conversion_struct_formula_struct_1",
blanchet@33192
   288
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   289
         cast_to_rep (Struct [Atom (2, 0), Unit])
blanchet@33192
   290
             (cast_to_rep (Formula Neut) struct_atom_2_unit_v1),
blanchet@33192
   291
         struct_atom_2_unit_v1))
blanchet@33192
   292
*)
blanchet@33192
   293
  ]
blanchet@33192
   294
blanchet@35284
   295
(* Proof.context -> string * nut -> Kodkod.problem *)
blanchet@35284
   296
fun problem_for_nut ctxt (name, u) =
blanchet@33192
   297
  let
blanchet@33192
   298
    val debug = false
blanchet@33192
   299
    val peephole_optim = true
blanchet@33192
   300
    val nat_card = 4
blanchet@33192
   301
    val int_card = 9
blanchet@34124
   302
    val bits = 8
blanchet@33192
   303
    val j0 = 0
blanchet@33192
   304
    val constrs = kodkod_constrs peephole_optim nat_card int_card j0
blanchet@33192
   305
    val (free_rels, pool, table) =
blanchet@33192
   306
      rename_free_vars (fst (add_free_and_const_names u ([], []))) initial_pool
blanchet@33192
   307
                       NameTable.empty
blanchet@33192
   308
    val u = Op1 (Not, type_of u, rep_of u, u)
blanchet@33192
   309
            |> rename_vars_in_nut pool table
blanchet@35280
   310
    val formula = kodkod_formula_from_nut Typtab.empty constrs u
blanchet@33192
   311
    val bounds = map (bound_for_plain_rel ctxt debug) free_rels
blanchet@33192
   312
    val univ_card = univ_card nat_card int_card j0 bounds formula
blanchet@33192
   313
    val declarative_axioms = map (declarative_axiom_for_plain_rel constrs)
blanchet@33192
   314
                                 free_rels
blanchet@33192
   315
    val formula = fold_rev s_and declarative_axioms formula
blanchet@33192
   316
  in
blanchet@33192
   317
    {comment = name, settings = settings, univ_card = univ_card,
blanchet@33192
   318
     tuple_assigns = [], bounds = bounds, int_bounds = [], expr_assigns = [],
blanchet@33192
   319
     formula = formula}
blanchet@33192
   320
  end
blanchet@33192
   321
blanchet@35284
   322
(* unit -> unit *)
blanchet@35284
   323
fun run_all_tests () =
blanchet@34287
   324
  case Kodkod.solve_any_problem false NONE 0 1
blanchet@35284
   325
                                (map (problem_for_nut @{context}) tests) of
blanchet@35333
   326
    Kodkod.Normal ([], _, _) => ()
blanchet@36384
   327
  | _ => error "Tests failed."
blanchet@33192
   328
blanchet@33192
   329
end;