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