# HG changeset patch # User blanchet # Date 1266405248 -3600 # Node ID 9b8f351cced6dcc2eab5e458124f8b8c0d6be0bf # Parent a219865c02c95d8840e3122ab855984c17ec5d74 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested diff -r a219865c02c9 -r 9b8f351cced6 doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Wed Feb 17 11:20:09 2010 +0100 +++ b/doc-src/Nitpick/nitpick.tex Wed Feb 17 12:14:08 2010 +0100 @@ -472,7 +472,9 @@ \prew \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\ \textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount] -\slshape Nitpick found a potential counterexample: \\[2\smallskipamount] +\slshape Warning: The conjecture either trivially holds or (more likely) lies outside Nitpick's supported +fragment. Only potential counterexamples may be found. \\[2\smallskipamount] +Nitpick found a potential counterexample: \\[2\smallskipamount] \hbox{}\qquad Free variable: \nopagebreak \\ \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount] Confirmation by ``\textit{auto}'': The above counterexample is genuine. diff -r a219865c02c9 -r 9b8f351cced6 src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Feb 17 11:20:09 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Feb 17 12:14:08 2010 +0100 @@ -266,7 +266,7 @@ next case (Branch t u) thus ?case nitpick - nitpick [non_std "'a bin_tree", show_consts] + nitpick [non_std, show_all] oops lemma "labels (swap t a b) = diff -r a219865c02c9 -r 9b8f351cced6 src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Wed Feb 17 11:20:09 2010 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Wed Feb 17 12:14:08 2010 +0100 @@ -167,6 +167,7 @@ val max_arity : int -> int val arity_of_rel_expr : rel_expr -> int + val is_problem_trivially_false : problem -> bool val problems_equivalent : problem -> problem -> bool val solve_any_problem : bool -> Time.time option -> int -> int -> problem list -> outcome @@ -491,6 +492,10 @@ | arity_of_decl (DeclSome ((n, _), _)) = n | arity_of_decl (DeclSet ((n, _), _)) = n +(* problem -> bool *) +fun is_problem_trivially_false ({formula = False, ...} : problem) = true + | is_problem_trivially_false _ = false + (* string -> bool *) val is_relevant_setting = not o member (op =) ["solver", "delay"] @@ -1014,7 +1019,7 @@ val indexed_problems = if j >= 0 then [(j, nth problems j)] else - filter (not_equal False o #formula o snd) + filter (is_problem_trivially_false o snd) (0 upto length problems - 1 ~~ problems) val triv_js = filter_out (AList.defined (op =) indexed_problems) (0 upto length problems - 1) diff -r a219865c02c9 -r 9b8f351cced6 src/HOL/Tools/Nitpick/minipick.ML --- a/src/HOL/Tools/Nitpick/minipick.ML Wed Feb 17 11:20:09 2010 +0100 +++ b/src/HOL/Tools/Nitpick/minipick.ML Wed Feb 17 12:14:08 2010 +0100 @@ -84,7 +84,7 @@ fun atom_from_formula f = RelIf (f, true_atom, false_atom) (* Proof.context -> (typ -> int) -> styp list -> term -> formula *) -fun kodkod_formula_for_term ctxt card frees = +fun kodkod_formula_from_term ctxt card frees = let (* typ -> rel_expr -> rel_expr *) fun R_rep_from_S_rep (T as Type ("fun", [T1, @{typ bool}])) r = @@ -145,7 +145,7 @@ | Term.Var _ => raise SAME () | Bound _ => raise SAME () | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s) - | _ => raise TERM ("Minipick.kodkod_formula_for_term.to_F", [t])) + | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t])) handle SAME () => formula_from_atom (to_R_rep Ts t) (* typ list -> term -> rel_expr *) and to_S_rep Ts t = @@ -306,7 +306,7 @@ val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees val declarative_axioms = map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees - val formula = kodkod_formula_for_term ctxt card frees neg_t + val formula = kodkod_formula_from_term ctxt card frees neg_t |> fold_rev (curry And) declarative_axioms val univ_card = univ_card 0 0 0 bounds formula val problem = diff -r a219865c02c9 -r 9b8f351cced6 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Feb 17 11:20:09 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Feb 17 12:14:08 2010 +0100 @@ -130,7 +130,7 @@ sel_names: nut list, nonsel_names: nut list, rel_table: nut NameTable.table, - liberal: bool, + unsound: bool, scope: scope, core: KK.formula, defs: KK.formula list} @@ -157,15 +157,15 @@ (Path.variable "ISABELLE_HOME_USER" :: map Path.basic ["etc", "components"]))) ^ "\"." -val max_liberal_delay_ms = 200 -val max_liberal_delay_percent = 2 +val max_unsound_delay_ms = 200 +val max_unsound_delay_percent = 2 (* Time.time option -> int *) -fun liberal_delay_for_timeout NONE = max_liberal_delay_ms - | liberal_delay_for_timeout (SOME timeout) = - Int.max (0, Int.min (max_liberal_delay_ms, +fun unsound_delay_for_timeout NONE = max_unsound_delay_ms + | unsound_delay_for_timeout (SOME timeout) = + Int.max (0, Int.min (max_unsound_delay_ms, Time.toMilliseconds timeout - * max_liberal_delay_percent div 100)) + * max_unsound_delay_percent div 100)) (* Time.time option -> bool *) fun passed_deadline NONE = false @@ -434,7 +434,7 @@ val too_big_scopes = Unsynchronized.ref [] (* bool -> scope -> rich_problem option *) - fun problem_for_scope liberal + fun problem_for_scope unsound (scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) = let val _ = not (exists (fn other => scope_less_eq other scope) @@ -469,10 +469,10 @@ (univ_card nat_card int_card main_j0 [] KK.True) val _ = check_arity min_univ_card min_highest_arity - val core_u = choose_reps_in_nut scope liberal rep_table false core_u - val def_us = map (choose_reps_in_nut scope liberal rep_table true) + val core_u = choose_reps_in_nut scope unsound rep_table false core_u + val def_us = map (choose_reps_in_nut scope unsound rep_table true) def_us - val nondef_us = map (choose_reps_in_nut scope liberal rep_table false) + val nondef_us = map (choose_reps_in_nut scope unsound rep_table false) nondef_us (* val _ = List.app (priority o string_for_nut ctxt) @@ -488,21 +488,19 @@ val core_u = rename_vars_in_nut pool rel_table core_u val def_us = map (rename_vars_in_nut pool rel_table) def_us val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us - (* nut -> KK.formula *) - val to_f = kodkod_formula_from_nut bits ofs liberal kk - val core_f = to_f core_u - val def_fs = map to_f def_us - val nondef_fs = map to_f nondef_us + val core_f = kodkod_formula_from_nut bits ofs kk core_u + val def_fs = map (kodkod_formula_from_nut bits ofs kk) def_us + val nondef_fs = map (kodkod_formula_from_nut bits ofs kk) nondef_us val formula = fold (fold s_and) [def_fs, nondef_fs] core_f - val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^ + val comment = (if unsound then "unsound" else "sound") ^ "\n" ^ PrintMode.setmp [] multiline_string_for_scope scope val kodkod_sat_solver = Kodkod_SAT.sat_solver_spec effective_sat_solver |> snd val bit_width = if bits = 0 then 16 else bits + 1 - val delay = if liberal then + val delay = if unsound then Option.map (fn time => Time.- (time, Time.now ())) deadline - |> liberal_delay_for_timeout + |> unsound_delay_for_timeout else 0 val settings = [("solver", commas (map quote kodkod_sat_solver)), @@ -540,13 +538,13 @@ expr_assigns = [], formula = formula}, {free_names = free_names, sel_names = sel_names, nonsel_names = nonsel_names, rel_table = rel_table, - liberal = liberal, scope = scope, core = core_f, + unsound = unsound, scope = scope, core = core_f, defs = nondef_fs @ def_fs @ declarative_axioms}) end handle TOO_LARGE (loc, msg) => if loc = "Nitpick_Kodkod.check_arity" andalso not (Typtab.is_empty ofs) then - problem_for_scope liberal + problem_for_scope unsound {hol_ctxt = hol_ctxt, card_assigns = card_assigns, bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = Typtab.empty} @@ -556,13 +554,13 @@ else (Unsynchronized.change too_big_scopes (cons scope); print_v (fn () => ("Limit reached: " ^ msg ^ - ". Skipping " ^ (if liberal then "potential" + ". Skipping " ^ (if unsound then "potential" else "genuine") ^ " component of scope.")); NONE) | TOO_SMALL (loc, msg) => (print_v (fn () => ("Limit reached: " ^ msg ^ - ". Skipping " ^ (if liberal then "potential" + ". Skipping " ^ (if unsound then "potential" else "genuine") ^ " component of scope.")); NONE) @@ -577,7 +575,7 @@ val scopes = Unsynchronized.ref [] val generated_scopes = Unsynchronized.ref [] - val generated_problems = Unsynchronized.ref [] + val generated_problems = Unsynchronized.ref ([] : rich_problem list) val checked_problems = Unsynchronized.ref (SOME []) val met_potential = Unsynchronized.ref 0 @@ -711,7 +709,7 @@ | KK.Normal (sat_ps, unsat_js) => let val (lib_ps, con_ps) = - List.partition (#liberal o snd o nth problems o fst) sat_ps + List.partition (#unsound o snd o nth problems o fst) sat_ps in update_checked_problems problems (unsat_js @ map fst lib_ps); if null con_ps then @@ -728,9 +726,9 @@ (0, 0, donno) else let - (* "co_js" is the list of conservative problems whose - liberal pendants couldn't be satisfied and hence that - most probably can't be satisfied themselves. *) + (* "co_js" is the list of sound problems whose unsound + pendants couldn't be satisfied and hence that most + probably can't be satisfied themselves. *) val co_js = map (fn j => j - 1) unsat_js |> filter (fn j => @@ -743,7 +741,7 @@ val problems = problems |> filter_out_indices bye_js |> max_potential <= 0 - ? filter_out (#liberal o snd) + ? filter_out (#unsound o snd) in solve_any_problem max_potential max_genuine donno false problems @@ -763,7 +761,7 @@ (map fst sat_ps @ unsat_js) val problems = problems |> filter_out_indices bye_js - |> filter_out (#liberal o snd) + |> filter_out (#unsound o snd) in solve_any_problem 0 max_genuine donno false problems end end end @@ -807,10 +805,10 @@ () (* scope * bool -> rich_problem list * bool -> rich_problem list * bool *) - fun add_problem_for_scope (scope as {datatypes, ...}, liberal) + fun add_problem_for_scope (scope as {datatypes, ...}, unsound) (problems, donno) = (check_deadline (); - case problem_for_scope liberal scope of + case problem_for_scope unsound scope of SOME problem => (problems |> (null problems orelse @@ -826,6 +824,28 @@ ([], donno) val _ = Unsynchronized.change generated_problems (append problems) val _ = Unsynchronized.change generated_scopes (append scopes) + val _ = + if j + 1 = n then + let + val (unsound_problems, sound_problems) = + List.partition (#unsound o snd) (!generated_problems) + in + if not (null sound_problems) andalso + forall (KK.is_problem_trivially_false o fst) + sound_problems then + print_m (fn () => + "Warning: The conjecture either trivially holds or (more \ + \likely) lies outside Nitpick's supported fragment." ^ + (if exists (not o KK.is_problem_trivially_false o fst) + unsound_problems then + " Only potential counterexamples may be found." + else + "")) + else + () + end + else + () in solve_any_problem max_potential max_genuine donno true (rev problems) end @@ -838,7 +858,7 @@ let (* rich_problem list -> rich_problem list *) val do_filter = - if !met_potential = max_potential then filter_out (#liberal o snd) + if !met_potential = max_potential then filter_out (#unsound o snd) else I val total = length (!scopes) val unsat = diff -r a219865c02c9 -r 9b8f351cced6 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Feb 17 11:20:09 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Feb 17 12:14:08 2010 +0100 @@ -36,7 +36,7 @@ hol_context -> int -> int Typtab.table -> kodkod_constrs -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list val kodkod_formula_from_nut : - int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula + int -> int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula end; structure Nitpick_Kodkod : NITPICK_KODKOD = @@ -954,8 +954,8 @@ acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes @ maps (other_axioms_for_datatype hol_ctxt bits ofs kk rel_table) dtypes -(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *) -fun kodkod_formula_from_nut bits ofs liberal +(* int -> int Typtab.table -> kodkod_constrs -> nut -> KK.formula *) +fun kodkod_formula_from_nut bits ofs (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not, kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no, kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union, diff -r a219865c02c9 -r 9b8f351cced6 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Feb 17 11:20:09 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Feb 17 12:14:08 2010 +0100 @@ -892,7 +892,7 @@ (* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *) fun choose_reps_in_nut (scope as {hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}) - liberal table def = + unsound table def = let val bool_atom_R = Atom (2, offset_of_type ofs bool_T) (* polarity -> bool -> rep *) @@ -1036,7 +1036,7 @@ if is_constructive u then s_op2 Eq T (Formula Neut) u1' u2' else opt_opt_case () in - if liberal orelse polar = Neg orelse + if unsound orelse polar = Neg orelse is_concrete_type datatypes (type_of u1) then case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of (true, true) => opt_opt_case () @@ -1138,7 +1138,7 @@ else let val quant_u = s_op2 oper T (Formula polar) u1' u2' in if def orelse - (liberal andalso (polar = Pos) = (oper = All)) orelse + (unsound andalso (polar = Pos) = (oper = All)) orelse is_complete_type datatypes (type_of u1) then quant_u else diff -r a219865c02c9 -r 9b8f351cced6 src/HOL/Tools/Nitpick/nitpick_tests.ML --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Wed Feb 17 11:20:09 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Wed Feb 17 12:14:08 2010 +0100 @@ -308,7 +308,7 @@ NameTable.empty val u = Op1 (Not, type_of u, rep_of u, u) |> rename_vars_in_nut pool table - val formula = kodkod_formula_from_nut bits Typtab.empty false constrs u + val formula = kodkod_formula_from_nut bits Typtab.empty constrs u val bounds = map (bound_for_plain_rel ctxt debug) free_rels val univ_card = univ_card nat_card int_card j0 bounds formula val declarative_axioms = map (declarative_axiom_for_plain_rel constrs)