src/HOL/Tools/Nitpick/nitpick_tests.ML
author blanchet
Thu Oct 22 14:51:47 2009 +0200 (2009-10-22)
changeset 33192 08a39a957ed7
child 33232 f93390060bbe
permissions -rw-r--r--
added Nitpick's theory and ML files to Isabelle/HOL;
the examples and the documentation are on their way.
blanchet@33192
     1
(*  Title:      HOL/Nitpick/Tools/nitpick_tests.ML
blanchet@33192
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@33192
     3
    Copyright   2008, 2009
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@33192
    13
structure NitpickTests =
blanchet@33192
    14
struct
blanchet@33192
    15
blanchet@33192
    16
open NitpickUtil
blanchet@33192
    17
open NitpickPeephole
blanchet@33192
    18
open NitpickRep
blanchet@33192
    19
open NitpickNut
blanchet@33192
    20
open NitpickKodkod
blanchet@33192
    21
open Nitpick
blanchet@33192
    22
blanchet@33192
    23
val settings =
blanchet@33192
    24
  [("solver", "\"zChaff\""),
blanchet@33192
    25
   ("skolem_depth", "-1")]
blanchet@33192
    26
blanchet@33192
    27
fun cast_to_rep R u = Op1 (Cast, type_of u, R, u)
blanchet@33192
    28
blanchet@33192
    29
val unit_T = @{typ unit}
blanchet@33192
    30
val dummy_T = @{typ 'a}
blanchet@33192
    31
blanchet@33192
    32
val unity = Cst (Unity, unit_T, Unit)
blanchet@33192
    33
val atom1_v1 = FreeName ("atom1_v1", dummy_T, Atom (1, 0))
blanchet@33192
    34
val atom2_v1 = FreeName ("atom2_v1", dummy_T, Atom (2, 0))
blanchet@33192
    35
val atom6_v1 = FreeName ("atom6_v1", dummy_T, Atom (6, 0))
blanchet@33192
    36
val atom16_v1 = FreeName ("atom16_v1", dummy_T, Atom (16, 0))
blanchet@33192
    37
val atom24_v1 = FreeName ("atom24_v1", dummy_T, Atom (24, 0))
blanchet@33192
    38
val atom36_v1 = FreeName ("atom36_v1", dummy_T, Atom (36, 0))
blanchet@33192
    39
val atom81_v1 = FreeName ("atom81_v1", dummy_T, Atom (81, 0))
blanchet@33192
    40
val struct_atom1_atom1_v1 =
blanchet@33192
    41
  FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Atom (1, 0), Atom (1, 0)])
blanchet@33192
    42
val struct_atom1_unit_v1 =
blanchet@33192
    43
  FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Atom (1, 0), Unit])
blanchet@33192
    44
val struct_unit_atom1_v1 =
blanchet@33192
    45
  FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Unit, Atom (1, 0)])
blanchet@33192
    46
blanchet@33192
    47
(*
blanchet@33192
    48
              Formula    Unit   Atom    Struct    Vect    Func
blanchet@33192
    49
    Formula      X       N/A     X        X       N/A     N/A
blanchet@33192
    50
    Unit        N/A      N/A    N/A      N/A      N/A     N/A
blanchet@33192
    51
    Atom         X       N/A     X        X        X       X
blanchet@33192
    52
    Struct      N/A      N/A     X        X       N/A     N/A
blanchet@33192
    53
    Vect        N/A      N/A     X       N/A       X       X
blanchet@33192
    54
    Func        N/A      N/A     X       N/A       X       X
blanchet@33192
    55
*)
blanchet@33192
    56
blanchet@33192
    57
val tests =
blanchet@33192
    58
  [("rep_conversion_formula_formula",
blanchet@33192
    59
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    60
         cast_to_rep (Formula Neut)
blanchet@33192
    61
                     (cast_to_rep (Formula Neut) atom2_v1), atom2_v1)),
blanchet@33192
    62
   ("rep_conversion_atom_atom",
blanchet@33192
    63
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    64
         cast_to_rep (Atom (16, 0)) (cast_to_rep (Atom (16, 0)) atom16_v1),
blanchet@33192
    65
         atom16_v1)),
blanchet@33192
    66
   ("rep_conversion_struct_struct_1",
blanchet@33192
    67
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    68
         cast_to_rep (Struct [Atom (4, 0), Atom (6, 0)])
blanchet@33192
    69
             (cast_to_rep (Struct [Atom (4, 0), Atom (6, 0)]) atom24_v1),
blanchet@33192
    70
         atom24_v1)),
blanchet@33192
    71
   ("rep_conversion_struct_struct_2",
blanchet@33192
    72
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    73
         cast_to_rep (Struct [Atom (4, 0), Struct [Atom (2, 0), Atom (3, 0)]])
blanchet@33192
    74
             (cast_to_rep (Struct [Atom (4, 0), Atom (6, 0)]) atom24_v1),
blanchet@33192
    75
         atom24_v1)),
blanchet@33192
    76
   ("rep_conversion_struct_struct_3",
blanchet@33192
    77
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    78
         cast_to_rep (Struct [Atom (4, 0), Atom (6, 0)])
blanchet@33192
    79
             (cast_to_rep (Struct [Atom (4, 0),
blanchet@33192
    80
                                   Struct [Atom (2, 0), Atom (3, 0)]])
blanchet@33192
    81
                          atom24_v1),
blanchet@33192
    82
         atom24_v1)),
blanchet@33192
    83
   ("rep_conversion_struct_struct_4",
blanchet@33192
    84
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    85
         cast_to_rep (Struct [Atom (24, 0), Unit])
blanchet@33192
    86
             (cast_to_rep (Struct [Atom (24, 0), Atom (1, 0)]) atom24_v1),
blanchet@33192
    87
         atom24_v1)),
blanchet@33192
    88
   ("rep_conversion_struct_struct_5",
blanchet@33192
    89
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    90
         cast_to_rep (Struct [Atom (24, 0), Atom (1, 0)])
blanchet@33192
    91
             (cast_to_rep (Struct [Atom (24, 0), Unit]) atom24_v1),
blanchet@33192
    92
         atom24_v1)),
blanchet@33192
    93
   ("rep_conversion_struct_struct_6",
blanchet@33192
    94
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    95
         cast_to_rep (Struct [Atom (1, 0), Atom (1, 0)])
blanchet@33192
    96
             (cast_to_rep (Struct [Atom (1, 0), Unit])
blanchet@33192
    97
                 (cast_to_rep (Struct [Unit, Atom (1, 0)]) atom1_v1)),
blanchet@33192
    98
         atom1_v1)),
blanchet@33192
    99
   ("rep_conversion_vect_vect_1",
blanchet@33192
   100
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   101
         cast_to_rep (Atom (16, 0))
blanchet@33192
   102
             (cast_to_rep (Vect (2, Atom (4, 0)))
blanchet@33192
   103
                  (cast_to_rep (Vect (2, Struct [Atom (2, 0), Atom (2, 0)]))
blanchet@33192
   104
                               atom16_v1)),
blanchet@33192
   105
         atom16_v1)),
blanchet@33192
   106
   ("rep_conversion_vect_vect_2",
blanchet@33192
   107
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   108
         cast_to_rep (Atom (16, 0))
blanchet@33192
   109
             (cast_to_rep (Vect (2, Struct [Atom (2, 0), Atom (2, 0)]))
blanchet@33192
   110
                  (cast_to_rep (Vect (2, Atom (4, 0))) atom16_v1)),
blanchet@33192
   111
         atom16_v1)),
blanchet@33192
   112
   ("rep_conversion_vect_vect_3",
blanchet@33192
   113
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   114
         cast_to_rep (Atom (16, 0))
blanchet@33192
   115
             (cast_to_rep (Vect (2, Atom (4, 0)))
blanchet@33192
   116
                  (cast_to_rep (Vect (2, Vect (2, Atom (2, 0)))) atom16_v1)),
blanchet@33192
   117
         atom16_v1)),
blanchet@33192
   118
   ("rep_conversion_vect_vect_4",
blanchet@33192
   119
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   120
         cast_to_rep (Atom (16, 0))
blanchet@33192
   121
             (cast_to_rep (Vect (2, Vect (2, Atom (2, 0))))
blanchet@33192
   122
                  (cast_to_rep (Vect (2, Atom (4, 0))) atom16_v1)),
blanchet@33192
   123
         atom16_v1)),
blanchet@33192
   124
   ("rep_conversion_func_func_1",
blanchet@33192
   125
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   126
         cast_to_rep (Atom (36, 0))
blanchet@33192
   127
             (cast_to_rep (Func (Atom (2, 0),
blanchet@33192
   128
                                 Struct [Atom (2, 0), Atom (3, 0)]))
blanchet@33192
   129
                  (cast_to_rep (Func (Atom (2, 0), Atom (6, 0))) atom36_v1)),
blanchet@33192
   130
         atom36_v1)),
blanchet@33192
   131
   ("rep_conversion_func_func_2",
blanchet@33192
   132
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   133
         cast_to_rep (Atom (36, 0))
blanchet@33192
   134
             (cast_to_rep (Func (Atom (2, 0), Atom (6, 0)))
blanchet@33192
   135
                  (cast_to_rep (Func (Atom (2, 0),
blanchet@33192
   136
                                Struct [Atom (2, 0), Atom (3, 0)]))
blanchet@33192
   137
                       atom36_v1)),
blanchet@33192
   138
         atom36_v1)),
blanchet@33192
   139
   ("rep_conversion_func_func_3",
blanchet@33192
   140
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   141
         cast_to_rep (Atom (36, 0))
blanchet@33192
   142
             (cast_to_rep (Func (Unit, Struct [Atom (6, 0), Atom (6, 0)]))
blanchet@33192
   143
                  (cast_to_rep (Func (Atom (1, 0), Atom (36, 0))) atom36_v1)),
blanchet@33192
   144
         atom36_v1)),
blanchet@33192
   145
   ("rep_conversion_func_func_4",
blanchet@33192
   146
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   147
         cast_to_rep (Atom (36, 0))
blanchet@33192
   148
             (cast_to_rep (Func (Atom (1, 0), Atom (36, 0)))
blanchet@33192
   149
                  (cast_to_rep (Func (Unit, Struct [Atom (6, 0), Atom (6, 0)]))
blanchet@33192
   150
                       atom36_v1)),
blanchet@33192
   151
         atom36_v1)),
blanchet@33192
   152
   ("rep_conversion_func_func_5",
blanchet@33192
   153
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   154
         cast_to_rep (Atom (36, 0))
blanchet@33192
   155
             (cast_to_rep (Func (Unit, Vect (2, Atom (6, 0))))
blanchet@33192
   156
                  (cast_to_rep (Func (Atom (1, 0), Atom (36, 0))) atom36_v1)),
blanchet@33192
   157
         atom36_v1)),
blanchet@33192
   158
   ("rep_conversion_func_func_6",
blanchet@33192
   159
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   160
         cast_to_rep (Atom (36, 0))
blanchet@33192
   161
             (cast_to_rep (Func (Atom (1, 0), Atom (36, 0)))
blanchet@33192
   162
                  (cast_to_rep (Func (Unit, Vect (2, Atom (6, 0))))
blanchet@33192
   163
                       atom36_v1)),
blanchet@33192
   164
         atom36_v1)),
blanchet@33192
   165
   ("rep_conversion_func_func_7",
blanchet@33192
   166
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   167
         cast_to_rep (Atom (2, 0))
blanchet@33192
   168
             (cast_to_rep (Func (Unit, Atom (2, 0)))
blanchet@33192
   169
                  (cast_to_rep (Func (Atom (1, 0), Formula Neut)) atom2_v1)),
blanchet@33192
   170
         atom2_v1)),
blanchet@33192
   171
   ("rep_conversion_func_func_8",
blanchet@33192
   172
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   173
         cast_to_rep (Atom (2, 0))
blanchet@33192
   174
             (cast_to_rep (Func (Atom (1, 0), Formula Neut))
blanchet@33192
   175
                  (cast_to_rep (Func (Unit, Atom (2, 0))) atom2_v1)),
blanchet@33192
   176
         atom2_v1)),
blanchet@33192
   177
   ("rep_conversion_atom_formula_atom",
blanchet@33192
   178
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   179
         cast_to_rep (Atom (2, 0)) (cast_to_rep (Formula Neut) atom2_v1),
blanchet@33192
   180
         atom2_v1)),
blanchet@33192
   181
   ("rep_conversion_unit_atom",
blanchet@33192
   182
    Op2 (Eq, bool_T, Formula Neut, cast_to_rep (Atom (1, 0)) unity, unity)),
blanchet@33192
   183
   ("rep_conversion_atom_struct_atom1",
blanchet@33192
   184
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   185
         cast_to_rep (Atom (6, 0))
blanchet@33192
   186
                     (cast_to_rep (Struct [Atom (3, 0), Atom (2, 0)]) atom6_v1),
blanchet@33192
   187
         atom6_v1)),
blanchet@33192
   188
   ("rep_conversion_atom_struct_atom_2",
blanchet@33192
   189
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   190
         cast_to_rep (Atom (24, 0))
blanchet@33192
   191
             (cast_to_rep (Struct [Struct [Atom (3, 0), Atom (4, 0)],
blanchet@33192
   192
                                   Atom (2, 0)]) atom24_v1),
blanchet@33192
   193
         atom24_v1)),
blanchet@33192
   194
   ("rep_conversion_atom_struct_atom_3",
blanchet@33192
   195
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   196
         cast_to_rep (Atom (6, 0))
blanchet@33192
   197
                     (cast_to_rep (Struct [Atom (6, 0), Unit]) atom6_v1),
blanchet@33192
   198
         atom6_v1)),
blanchet@33192
   199
   ("rep_conversion_atom_struct_atom_4",
blanchet@33192
   200
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   201
         cast_to_rep (Atom (6, 0))
blanchet@33192
   202
             (cast_to_rep (Struct [Struct [Atom (3, 0), Unit], Atom (2, 0)]) 
blanchet@33192
   203
             atom6_v1),
blanchet@33192
   204
         atom6_v1)),
blanchet@33192
   205
   ("rep_conversion_atom_vect_func_atom_1",
blanchet@33192
   206
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   207
         cast_to_rep (Atom (16, 0))
blanchet@33192
   208
             (cast_to_rep (Vect (4, Atom (2, 0)))
blanchet@33192
   209
                  (cast_to_rep (Func (Atom (4, 0), Atom (2, 0))) atom16_v1)),
blanchet@33192
   210
         atom16_v1)),
blanchet@33192
   211
   ("rep_conversion_atom_vect_func_atom_2",
blanchet@33192
   212
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   213
         cast_to_rep (Atom (16, 0))
blanchet@33192
   214
             (cast_to_rep (Vect (4, Atom (2, 0)))
blanchet@33192
   215
                  (cast_to_rep (Func (Atom (4, 0), Atom (2, 0))) atom16_v1)),
blanchet@33192
   216
         atom16_v1)),
blanchet@33192
   217
   ("rep_conversion_atom_vect_func_atom_3",
blanchet@33192
   218
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   219
         cast_to_rep (Atom (16, 0))
blanchet@33192
   220
             (cast_to_rep (Vect (4, Atom (2, 0)))
blanchet@33192
   221
                  (cast_to_rep (Func (Atom (4, 0), Formula Neut)) atom16_v1)),
blanchet@33192
   222
         atom16_v1)),
blanchet@33192
   223
   ("rep_conversion_atom_vect_func_atom_4",
blanchet@33192
   224
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   225
         cast_to_rep (Atom (16, 0))
blanchet@33192
   226
             (cast_to_rep (Vect (1, Atom (16, 0)))
blanchet@33192
   227
                  (cast_to_rep (Func (Unit, Atom (16, 0))) atom16_v1)),
blanchet@33192
   228
         atom16_v1)),
blanchet@33192
   229
   ("rep_conversion_atom_vect_func_atom_5",
blanchet@33192
   230
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   231
         cast_to_rep (Atom (16, 0))
blanchet@33192
   232
             (cast_to_rep (Vect (1, Atom (16, 0)))
blanchet@33192
   233
                  (cast_to_rep (Func (Unit, Atom (16, 0))) atom16_v1)),
blanchet@33192
   234
         atom16_v1)),
blanchet@33192
   235
   ("rep_conversion_atom_func_vect_atom_1",
blanchet@33192
   236
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   237
         cast_to_rep (Atom (16, 0))
blanchet@33192
   238
             (cast_to_rep (Func (Atom (4, 0), Atom (2, 0)))
blanchet@33192
   239
                  (cast_to_rep (Vect (4, Atom (2, 0))) atom16_v1)),
blanchet@33192
   240
         atom16_v1)),
blanchet@33192
   241
   ("rep_conversion_atom_func_vect_atom_2",
blanchet@33192
   242
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   243
         cast_to_rep (Atom (16, 0))
blanchet@33192
   244
             (cast_to_rep (Func (Atom (4, 0), Atom (2, 0)))
blanchet@33192
   245
                  (cast_to_rep (Vect (4, Atom (2, 0))) atom16_v1)),
blanchet@33192
   246
         atom16_v1)),
blanchet@33192
   247
   ("rep_conversion_atom_func_vect_atom_3",
blanchet@33192
   248
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   249
         cast_to_rep (Atom (16, 0))
blanchet@33192
   250
             (cast_to_rep (Func (Atom (4, 0), Formula Neut))
blanchet@33192
   251
                  (cast_to_rep (Vect (4, Atom (2, 0))) atom16_v1)),
blanchet@33192
   252
         atom16_v1)),
blanchet@33192
   253
   ("rep_conversion_atom_func_vect_atom_4",
blanchet@33192
   254
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   255
         cast_to_rep (Atom (16, 0))
blanchet@33192
   256
             (cast_to_rep (Func (Unit, Atom (16, 0)))
blanchet@33192
   257
                  (cast_to_rep (Vect (1, Atom (16, 0))) atom16_v1)),
blanchet@33192
   258
         atom16_v1)),
blanchet@33192
   259
   ("rep_conversion_atom_func_vect_atom_5",
blanchet@33192
   260
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   261
         cast_to_rep (Atom (16, 0))
blanchet@33192
   262
             (cast_to_rep (Func (Atom (1, 0), Atom (16, 0)))
blanchet@33192
   263
                  (cast_to_rep (Vect (1, Atom (16, 0))) atom16_v1)),
blanchet@33192
   264
         atom16_v1)),
blanchet@33192
   265
   ("rep_conversion_atom_vect_atom",
blanchet@33192
   266
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   267
         cast_to_rep (Atom (36, 0))
blanchet@33192
   268
             (cast_to_rep (Vect (2, Struct [Atom (2, 0), Atom (3, 0)]))
blanchet@33192
   269
                          atom36_v1),
blanchet@33192
   270
         atom36_v1)),
blanchet@33192
   271
   ("rep_conversion_atom_func_atom",
blanchet@33192
   272
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   273
         cast_to_rep (Atom (36, 0))
blanchet@33192
   274
             (cast_to_rep (Func (Atom (2, 0),
blanchet@33192
   275
                           Struct [Atom (2, 0), Atom (3, 0)])) atom36_v1),
blanchet@33192
   276
         atom36_v1)),
blanchet@33192
   277
   ("rep_conversion_struct_atom1_1",
blanchet@33192
   278
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   279
         cast_to_rep (Struct [Atom (1, 0), Atom (1, 0)]) atom1_v1,
blanchet@33192
   280
                      struct_atom1_atom1_v1)),
blanchet@33192
   281
   ("rep_conversion_struct_atom1_2",
blanchet@33192
   282
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   283
         cast_to_rep (Struct [Atom (1, 0), Unit]) atom1_v1,
blanchet@33192
   284
                      struct_atom1_unit_v1)),
blanchet@33192
   285
   ("rep_conversion_struct_atom1_3",
blanchet@33192
   286
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   287
         cast_to_rep (Struct [Unit, Atom (1, 0)]) atom1_v1,
blanchet@33192
   288
                      struct_unit_atom1_v1))
blanchet@33192
   289
(*
blanchet@33192
   290
   ("rep_conversion_struct_formula_struct_1",
blanchet@33192
   291
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   292
         cast_to_rep (Struct [Atom (2, 0), Unit])
blanchet@33192
   293
             (cast_to_rep (Formula Neut) struct_atom_2_unit_v1),
blanchet@33192
   294
         struct_atom_2_unit_v1))
blanchet@33192
   295
*)
blanchet@33192
   296
  ]
blanchet@33192
   297
blanchet@33192
   298
fun problem_for_nut ctxt name u =
blanchet@33192
   299
  let
blanchet@33192
   300
    val debug = false
blanchet@33192
   301
    val peephole_optim = true
blanchet@33192
   302
    val nat_card = 4
blanchet@33192
   303
    val int_card = 9
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@33192
   311
    val formula = kodkod_formula_from_nut Typtab.empty false 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@33192
   325
  case Kodkod.solve_any_problem true 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;