src/HOL/Tools/Nitpick/nitpick_tests.ML
author blanchet
Mon Feb 17 22:54:38 2014 +0100 (2014-02-17)
changeset 55539 0819931d652d
parent 55203 e872d196a73b
child 63693 5b02f7757a4c
permissions -rw-r--r--
simplified data structure by reducing the incidence of clumsy indices
blanchet@55203
     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@55203
    13
structure Nitpick_Tests : 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 dummy_T = @{typ 'a}
blanchet@33192
    27
blanchet@33192
    28
val atom1_v1 = FreeName ("atom1_v1", dummy_T, Atom (1, 0))
blanchet@33192
    29
val atom2_v1 = FreeName ("atom2_v1", dummy_T, Atom (2, 0))
blanchet@33192
    30
val atom6_v1 = FreeName ("atom6_v1", dummy_T, Atom (6, 0))
blanchet@33192
    31
val atom16_v1 = FreeName ("atom16_v1", dummy_T, Atom (16, 0))
blanchet@33192
    32
val atom24_v1 = FreeName ("atom24_v1", dummy_T, Atom (24, 0))
blanchet@33192
    33
val atom36_v1 = FreeName ("atom36_v1", dummy_T, Atom (36, 0))
blanchet@33192
    34
val struct_atom1_atom1_v1 =
blanchet@33192
    35
  FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Atom (1, 0), Atom (1, 0)])
blanchet@33192
    36
blanchet@33192
    37
(*
blanchet@38190
    38
              Formula    Atom    Struct    Vect    Func
blanchet@38190
    39
    Formula      X       X        X       N/A     N/A
blanchet@38190
    40
    Atom         X       X        X        X       X
blanchet@38190
    41
    Struct      N/A      X        X       N/A     N/A
blanchet@38190
    42
    Vect        N/A      X       N/A       X       X
blanchet@38190
    43
    Func        N/A      X       N/A       X       X
blanchet@33192
    44
*)
blanchet@33192
    45
blanchet@33192
    46
val tests =
blanchet@33192
    47
  [("rep_conversion_formula_formula",
blanchet@33192
    48
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    49
         cast_to_rep (Formula Neut)
blanchet@33192
    50
                     (cast_to_rep (Formula Neut) atom2_v1), atom2_v1)),
blanchet@33192
    51
   ("rep_conversion_atom_atom",
blanchet@33192
    52
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    53
         cast_to_rep (Atom (16, 0)) (cast_to_rep (Atom (16, 0)) atom16_v1),
blanchet@33192
    54
         atom16_v1)),
blanchet@33192
    55
   ("rep_conversion_struct_struct_1",
blanchet@33192
    56
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    57
         cast_to_rep (Struct [Atom (4, 0), Atom (6, 0)])
blanchet@33192
    58
             (cast_to_rep (Struct [Atom (4, 0), Atom (6, 0)]) atom24_v1),
blanchet@33192
    59
         atom24_v1)),
blanchet@33192
    60
   ("rep_conversion_struct_struct_2",
blanchet@33192
    61
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    62
         cast_to_rep (Struct [Atom (4, 0), Struct [Atom (2, 0), Atom (3, 0)]])
blanchet@33192
    63
             (cast_to_rep (Struct [Atom (4, 0), Atom (6, 0)]) atom24_v1),
blanchet@33192
    64
         atom24_v1)),
blanchet@33192
    65
   ("rep_conversion_struct_struct_3",
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),
blanchet@33192
    69
                                   Struct [Atom (2, 0), Atom (3, 0)]])
blanchet@33192
    70
                          atom24_v1),
blanchet@33192
    71
         atom24_v1)),
blanchet@33192
    72
   ("rep_conversion_vect_vect_1",
blanchet@33192
    73
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    74
         cast_to_rep (Atom (16, 0))
blanchet@33192
    75
             (cast_to_rep (Vect (2, Atom (4, 0)))
blanchet@33192
    76
                  (cast_to_rep (Vect (2, Struct [Atom (2, 0), Atom (2, 0)]))
blanchet@33192
    77
                               atom16_v1)),
blanchet@33192
    78
         atom16_v1)),
blanchet@33192
    79
   ("rep_conversion_vect_vect_2",
blanchet@33192
    80
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    81
         cast_to_rep (Atom (16, 0))
blanchet@33192
    82
             (cast_to_rep (Vect (2, Struct [Atom (2, 0), Atom (2, 0)]))
blanchet@33192
    83
                  (cast_to_rep (Vect (2, Atom (4, 0))) atom16_v1)),
blanchet@33192
    84
         atom16_v1)),
blanchet@33192
    85
   ("rep_conversion_vect_vect_3",
blanchet@33192
    86
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    87
         cast_to_rep (Atom (16, 0))
blanchet@33192
    88
             (cast_to_rep (Vect (2, Atom (4, 0)))
blanchet@33192
    89
                  (cast_to_rep (Vect (2, Vect (2, Atom (2, 0)))) atom16_v1)),
blanchet@33192
    90
         atom16_v1)),
blanchet@33192
    91
   ("rep_conversion_vect_vect_4",
blanchet@33192
    92
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    93
         cast_to_rep (Atom (16, 0))
blanchet@33192
    94
             (cast_to_rep (Vect (2, Vect (2, Atom (2, 0))))
blanchet@33192
    95
                  (cast_to_rep (Vect (2, Atom (4, 0))) atom16_v1)),
blanchet@33192
    96
         atom16_v1)),
blanchet@33192
    97
   ("rep_conversion_func_func_1",
blanchet@33192
    98
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
    99
         cast_to_rep (Atom (36, 0))
blanchet@33192
   100
             (cast_to_rep (Func (Atom (2, 0),
blanchet@33192
   101
                                 Struct [Atom (2, 0), Atom (3, 0)]))
blanchet@33192
   102
                  (cast_to_rep (Func (Atom (2, 0), Atom (6, 0))) atom36_v1)),
blanchet@33192
   103
         atom36_v1)),
blanchet@33192
   104
   ("rep_conversion_func_func_2",
blanchet@33192
   105
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   106
         cast_to_rep (Atom (36, 0))
blanchet@33192
   107
             (cast_to_rep (Func (Atom (2, 0), Atom (6, 0)))
blanchet@33192
   108
                  (cast_to_rep (Func (Atom (2, 0),
blanchet@33192
   109
                                Struct [Atom (2, 0), Atom (3, 0)]))
blanchet@33192
   110
                       atom36_v1)),
blanchet@33192
   111
         atom36_v1)),
blanchet@33192
   112
   ("rep_conversion_atom_formula_atom",
blanchet@33192
   113
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   114
         cast_to_rep (Atom (2, 0)) (cast_to_rep (Formula Neut) atom2_v1),
blanchet@33192
   115
         atom2_v1)),
blanchet@33192
   116
   ("rep_conversion_atom_struct_atom1",
blanchet@33192
   117
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   118
         cast_to_rep (Atom (6, 0))
blanchet@33192
   119
                     (cast_to_rep (Struct [Atom (3, 0), Atom (2, 0)]) atom6_v1),
blanchet@33192
   120
         atom6_v1)),
blanchet@33192
   121
   ("rep_conversion_atom_struct_atom_2",
blanchet@33192
   122
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   123
         cast_to_rep (Atom (24, 0))
blanchet@33192
   124
             (cast_to_rep (Struct [Struct [Atom (3, 0), Atom (4, 0)],
blanchet@33192
   125
                                   Atom (2, 0)]) atom24_v1),
blanchet@33192
   126
         atom24_v1)),
blanchet@33192
   127
   ("rep_conversion_atom_vect_func_atom_1",
blanchet@33192
   128
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   129
         cast_to_rep (Atom (16, 0))
blanchet@33192
   130
             (cast_to_rep (Vect (4, Atom (2, 0)))
blanchet@33192
   131
                  (cast_to_rep (Func (Atom (4, 0), Atom (2, 0))) atom16_v1)),
blanchet@33192
   132
         atom16_v1)),
blanchet@33192
   133
   ("rep_conversion_atom_vect_func_atom_2",
blanchet@33192
   134
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   135
         cast_to_rep (Atom (16, 0))
blanchet@33192
   136
             (cast_to_rep (Vect (4, Atom (2, 0)))
blanchet@33192
   137
                  (cast_to_rep (Func (Atom (4, 0), Atom (2, 0))) atom16_v1)),
blanchet@33192
   138
         atom16_v1)),
blanchet@33192
   139
   ("rep_conversion_atom_vect_func_atom_3",
blanchet@33192
   140
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   141
         cast_to_rep (Atom (16, 0))
blanchet@33192
   142
             (cast_to_rep (Vect (4, Atom (2, 0)))
blanchet@33192
   143
                  (cast_to_rep (Func (Atom (4, 0), Formula Neut)) atom16_v1)),
blanchet@33192
   144
         atom16_v1)),
blanchet@33192
   145
   ("rep_conversion_atom_func_vect_atom_1",
blanchet@33192
   146
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   147
         cast_to_rep (Atom (16, 0))
blanchet@33192
   148
             (cast_to_rep (Func (Atom (4, 0), Atom (2, 0)))
blanchet@33192
   149
                  (cast_to_rep (Vect (4, Atom (2, 0))) atom16_v1)),
blanchet@33192
   150
         atom16_v1)),
blanchet@33192
   151
   ("rep_conversion_atom_func_vect_atom_2",
blanchet@33192
   152
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   153
         cast_to_rep (Atom (16, 0))
blanchet@33192
   154
             (cast_to_rep (Func (Atom (4, 0), Atom (2, 0)))
blanchet@33192
   155
                  (cast_to_rep (Vect (4, Atom (2, 0))) atom16_v1)),
blanchet@33192
   156
         atom16_v1)),
blanchet@33192
   157
   ("rep_conversion_atom_func_vect_atom_3",
blanchet@33192
   158
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   159
         cast_to_rep (Atom (16, 0))
blanchet@33192
   160
             (cast_to_rep (Func (Atom (4, 0), Formula Neut))
blanchet@33192
   161
                  (cast_to_rep (Vect (4, Atom (2, 0))) atom16_v1)),
blanchet@33192
   162
         atom16_v1)),
blanchet@33192
   163
   ("rep_conversion_atom_func_vect_atom_5",
blanchet@33192
   164
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   165
         cast_to_rep (Atom (16, 0))
blanchet@33192
   166
             (cast_to_rep (Func (Atom (1, 0), Atom (16, 0)))
blanchet@33192
   167
                  (cast_to_rep (Vect (1, Atom (16, 0))) atom16_v1)),
blanchet@33192
   168
         atom16_v1)),
blanchet@33192
   169
   ("rep_conversion_atom_vect_atom",
blanchet@33192
   170
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   171
         cast_to_rep (Atom (36, 0))
blanchet@33192
   172
             (cast_to_rep (Vect (2, Struct [Atom (2, 0), Atom (3, 0)]))
blanchet@33192
   173
                          atom36_v1),
blanchet@33192
   174
         atom36_v1)),
blanchet@33192
   175
   ("rep_conversion_atom_func_atom",
blanchet@33192
   176
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   177
         cast_to_rep (Atom (36, 0))
blanchet@33192
   178
             (cast_to_rep (Func (Atom (2, 0),
blanchet@33192
   179
                           Struct [Atom (2, 0), Atom (3, 0)])) atom36_v1),
blanchet@33192
   180
         atom36_v1)),
blanchet@33192
   181
   ("rep_conversion_struct_atom1_1",
blanchet@33192
   182
    Op2 (Eq, bool_T, Formula Neut,
blanchet@33192
   183
         cast_to_rep (Struct [Atom (1, 0), Atom (1, 0)]) atom1_v1,
blanchet@38190
   184
                      struct_atom1_atom1_v1))]
blanchet@33192
   185
blanchet@35284
   186
fun problem_for_nut ctxt (name, u) =
blanchet@33192
   187
  let
blanchet@33192
   188
    val debug = false
blanchet@33192
   189
    val peephole_optim = true
blanchet@33192
   190
    val nat_card = 4
blanchet@33192
   191
    val int_card = 9
blanchet@33192
   192
    val j0 = 0
blanchet@33192
   193
    val constrs = kodkod_constrs peephole_optim nat_card int_card j0
blanchet@33192
   194
    val (free_rels, pool, table) =
blanchet@33192
   195
      rename_free_vars (fst (add_free_and_const_names u ([], []))) initial_pool
blanchet@33192
   196
                       NameTable.empty
blanchet@33192
   197
    val u = Op1 (Not, type_of u, rep_of u, u)
blanchet@33192
   198
            |> rename_vars_in_nut pool table
blanchet@35280
   199
    val formula = kodkod_formula_from_nut Typtab.empty constrs u
blanchet@33192
   200
    val bounds = map (bound_for_plain_rel ctxt debug) free_rels
blanchet@33192
   201
    val univ_card = univ_card nat_card int_card j0 bounds formula
blanchet@33192
   202
    val declarative_axioms = map (declarative_axiom_for_plain_rel constrs)
blanchet@33192
   203
                                 free_rels
blanchet@33192
   204
    val formula = fold_rev s_and declarative_axioms formula
blanchet@33192
   205
  in
blanchet@33192
   206
    {comment = name, settings = settings, univ_card = univ_card,
blanchet@33192
   207
     tuple_assigns = [], bounds = bounds, int_bounds = [], expr_assigns = [],
blanchet@33192
   208
     formula = formula}
blanchet@33192
   209
  end
blanchet@33192
   210
blanchet@35284
   211
fun run_all_tests () =
blanchet@38186
   212
  let
blanchet@55199
   213
    val {debug, overlord, timeout, ...} = Nitpick_Commands.default_params @{theory} []
blanchet@38186
   214
    val max_threads = 1
blanchet@38186
   215
    val max_solutions = 1
blanchet@38186
   216
  in
blanchet@54816
   217
    case Kodkod.solve_any_problem debug overlord timeout max_threads max_solutions
blanchet@38186
   218
                                  (map (problem_for_nut @{context}) tests) of
blanchet@38190
   219
      Kodkod.Normal ([], _, _) => ()
blanchet@38190
   220
    | _ => error "Tests failed."
blanchet@38190
   221
  end
blanchet@33192
   222
blanchet@33192
   223
end;