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