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