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