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