src/HOL/Tools/Nitpick/nitpick.ML
author blanchet
Tue Oct 27 14:40:24 2009 +0100 (2009-10-27 ago)
changeset 33232 f93390060bbe
parent 33192 08a39a957ed7
child 33233 f9ff11344ec4
permissions -rw-r--r--
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
renamed Nitpick's ML structures from NitpickXxx to Nitpick_Xxx and added KODKODI_JAVA_LIBRARY_PATH to LD_LIBRARY_PATH before invoking Kodkodi
     1 (*  Title:      HOL/Nitpick/Tools/nitpick.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2008, 2009
     4 
     5 Finite model generation for HOL formulas using Kodkod.
     6 *)
     7 
     8 signature NITPICK =
     9 sig
    10   type params = {
    11     cards_assigns: (typ option * int list) list,
    12     maxes_assigns: (styp option * int list) list,
    13     iters_assigns: (styp option * int list) list,
    14     bisim_depths: int list,
    15     boxes: (typ option * bool option) list,
    16     monos: (typ option * bool option) list,
    17     wfs: (styp option * bool option) list,
    18     sat_solver: string,
    19     blocking: bool,
    20     falsify: bool,
    21     debug: bool,
    22     verbose: bool,
    23     overlord: bool,
    24     user_axioms: bool option,
    25     assms: bool,
    26     coalesce_type_vars: bool,
    27     destroy_constrs: bool,
    28     specialize: bool,
    29     skolemize: bool,
    30     star_linear_preds: bool,
    31     uncurry: bool,
    32     fast_descrs: bool,
    33     peephole_optim: bool,
    34     timeout: Time.time option,
    35     tac_timeout: Time.time option,
    36     sym_break: int,
    37     sharing_depth: int,
    38     flatten_props: bool,
    39     max_threads: int,
    40     show_skolems: bool,
    41     show_datatypes: bool,
    42     show_consts: bool,
    43     evals: term list,
    44     formats: (term option * int list) list,
    45     max_potential: int,
    46     max_genuine: int,
    47     check_potential: bool,
    48     check_genuine: bool,
    49     batch_size: int,
    50     expect: string}
    51 
    52   val register_frac_type : string -> (string * string) list -> theory -> theory
    53   val unregister_frac_type : string -> theory -> theory
    54   val register_codatatype : typ -> string -> styp list -> theory -> theory
    55   val unregister_codatatype : typ -> theory -> theory
    56   val pick_nits_in_term :
    57     Proof.state -> params -> bool -> term list -> term -> string * Proof.state
    58   val pick_nits_in_subgoal :
    59     Proof.state -> params -> bool -> int -> string * Proof.state
    60 end;
    61 
    62 structure Nitpick : NITPICK =
    63 struct
    64 
    65 open Nitpick_Util
    66 open Nitpick_HOL
    67 open Nitpick_Mono
    68 open Nitpick_Scope
    69 open Nitpick_Peephole
    70 open Nitpick_Rep
    71 open Nitpick_Nut
    72 open Nitpick_Kodkod
    73 open Nitpick_Model
    74 
    75 type params = {
    76   cards_assigns: (typ option * int list) list,
    77   maxes_assigns: (styp option * int list) list,
    78   iters_assigns: (styp option * int list) list,
    79   bisim_depths: int list,
    80   boxes: (typ option * bool option) list,
    81   monos: (typ option * bool option) list,
    82   wfs: (styp option * bool option) list,
    83   sat_solver: string,
    84   blocking: bool,
    85   falsify: bool,
    86   debug: bool,
    87   verbose: bool,
    88   overlord: bool,
    89   user_axioms: bool option,
    90   assms: bool,
    91   coalesce_type_vars: bool,
    92   destroy_constrs: bool,
    93   specialize: bool,
    94   skolemize: bool,
    95   star_linear_preds: bool,
    96   uncurry: bool,
    97   fast_descrs: bool,
    98   peephole_optim: bool,
    99   timeout: Time.time option,
   100   tac_timeout: Time.time option,
   101   sym_break: int,
   102   sharing_depth: int,
   103   flatten_props: bool,
   104   max_threads: int,
   105   show_skolems: bool,
   106   show_datatypes: bool,
   107   show_consts: bool,
   108   evals: term list,
   109   formats: (term option * int list) list,
   110   max_potential: int,
   111   max_genuine: int,
   112   check_potential: bool,
   113   check_genuine: bool,
   114   batch_size: int,
   115   expect: string}
   116 
   117 type problem_extension = {
   118   free_names: nut list,
   119   sel_names: nut list,
   120   nonsel_names: nut list,
   121   rel_table: nut NameTable.table,
   122   liberal: bool,
   123   scope: scope,
   124   core: Kodkod.formula,
   125   defs: Kodkod.formula list}
   126 
   127 type rich_problem = Kodkod.problem * problem_extension
   128 
   129 (* Proof.context -> string -> term list -> Pretty.T list *)
   130 fun pretties_for_formulas _ _ [] = []
   131   | pretties_for_formulas ctxt s ts =
   132     [Pretty.str (s ^ plural_s_for_list ts ^ ":"),
   133      Pretty.indent indent_size (Pretty.chunks
   134          (map2 (fn j => fn t =>
   135                    Pretty.block [t |> shorten_const_names_in_term
   136                                    |> Syntax.pretty_term ctxt,
   137                                  Pretty.str (if j = 1 then "." else ";")])
   138                (length ts downto 1) ts))]
   139 
   140 val max_liberal_delay_ms = 200
   141 val max_liberal_delay_percent = 2
   142 
   143 (* Time.time option -> int *)
   144 fun liberal_delay_for_timeout NONE = max_liberal_delay_ms
   145   | liberal_delay_for_timeout (SOME timeout) =
   146     Int.max (0, Int.min (max_liberal_delay_ms,
   147                          Time.toMilliseconds timeout
   148                          * max_liberal_delay_percent div 100))
   149 
   150 (* Time.time option -> bool *)
   151 fun passed_deadline NONE = false
   152   | passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS
   153 
   154 (* ('a * bool option) list -> bool *)
   155 fun none_true asgns = forall (not_equal (SOME true) o snd) asgns
   156 
   157 val weaselly_sorts =
   158   [@{sort default}, @{sort zero}, @{sort one}, @{sort plus}, @{sort minus},
   159    @{sort uminus}, @{sort times}, @{sort inverse}, @{sort abs}, @{sort sgn},
   160    @{sort ord}, @{sort eq}, @{sort number}]
   161 (* theory -> typ -> bool *)
   162 fun is_tfree_with_weaselly_sort thy (TFree (_, S)) =
   163     exists (curry (Sign.subsort thy) S) weaselly_sorts
   164   | is_tfree_with_weaselly_sort _ _ = false
   165 (* theory term -> bool *)
   166 val has_weaselly_sorts =
   167   exists_type o exists_subtype o is_tfree_with_weaselly_sort
   168 
   169 (* Time.time -> Proof.state -> params -> bool -> term -> string * Proof.state *)
   170 fun pick_them_nits_in_term deadline state (params : params) auto orig_assm_ts
   171                            orig_t =
   172   let
   173     val timer = Timer.startRealTimer ()
   174     val thy = Proof.theory_of state
   175     val ctxt = Proof.context_of state
   176     val {cards_assigns, maxes_assigns, iters_assigns, bisim_depths, boxes,
   177          monos, wfs, sat_solver, blocking, falsify, debug, verbose, overlord,
   178          user_axioms, assms, coalesce_type_vars, destroy_constrs, specialize,
   179          skolemize, star_linear_preds, uncurry, fast_descrs, peephole_optim,
   180          tac_timeout, sym_break, sharing_depth, flatten_props, max_threads,
   181          show_skolems, show_datatypes, show_consts, evals, formats,
   182          max_potential, max_genuine, check_potential, check_genuine, batch_size,
   183          ...} =
   184       params
   185     val state_ref = Unsynchronized.ref state
   186     (* Pretty.T -> unit *)
   187     val pprint =
   188       if auto then
   189         Unsynchronized.change state_ref o Proof.goal_message o K
   190         o curry Pretty.blk 0 o cons (Pretty.str "") o single
   191         o Pretty.mark Markup.hilite
   192       else
   193         priority o Pretty.string_of
   194     (* (unit -> Pretty.T) -> unit *)
   195     fun pprint_m f = () |> not auto ? pprint o f
   196     fun pprint_v f = () |> verbose ? pprint o f
   197     fun pprint_d f = () |> debug ? pprint o f
   198     (* string -> unit *)
   199     val print = pprint o curry Pretty.blk 0 o pstrs
   200     (* (unit -> string) -> unit *)
   201     fun print_m f = pprint_m (curry Pretty.blk 0 o pstrs o f)
   202     fun print_v f = pprint_v (curry Pretty.blk 0 o pstrs o f)
   203     fun print_d f = pprint_d (curry Pretty.blk 0 o pstrs o f)
   204 
   205     (* unit -> unit *)
   206     fun check_deadline () =
   207       if debug andalso passed_deadline deadline then raise TimeLimit.TimeOut
   208       else ()
   209     (* unit -> 'a *)
   210     fun do_interrupted () =
   211       if passed_deadline deadline then raise TimeLimit.TimeOut
   212       else raise Interrupt
   213 
   214     val _ = print_m (K "Nitpicking...")
   215     val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
   216                 else orig_t
   217     val assms_t = if assms orelse auto then
   218                     Logic.mk_conjunction_list (neg_t :: orig_assm_ts)
   219                   else
   220                     neg_t
   221     val (assms_t, evals) =
   222       assms_t :: evals
   223       |> coalesce_type_vars ? coalesce_type_vars_in_terms
   224       |> hd pairf tl
   225     val original_max_potential = max_potential
   226     val original_max_genuine = max_genuine
   227 (*
   228     val _ = priority ("*** " ^ Syntax.string_of_term ctxt orig_t)
   229     val _ = List.app (fn t => priority ("*** " ^ Syntax.string_of_term ctxt t))
   230                      orig_assm_ts
   231 *)
   232     val max_bisim_depth = fold Integer.max bisim_depths ~1
   233     val case_names = case_const_names thy
   234     val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy
   235     val def_table = const_def_table ctxt defs
   236     val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
   237     val simp_table = Unsynchronized.ref (const_simp_table ctxt)
   238     val psimp_table = const_psimp_table ctxt
   239     val intro_table = inductive_intro_table ctxt def_table
   240     val ground_thm_table = ground_theorem_table thy
   241     val ersatz_table = ersatz_table thy
   242     val (ext_ctxt as {skolems, special_funs, wf_cache, ...}) =
   243       {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
   244        user_axioms = user_axioms, debug = debug, wfs = wfs,
   245        destroy_constrs = destroy_constrs, specialize = specialize,
   246        skolemize = skolemize, star_linear_preds = star_linear_preds,
   247        uncurry = uncurry, fast_descrs = fast_descrs, tac_timeout = tac_timeout,
   248        evals = evals, case_names = case_names, def_table = def_table,
   249        nondef_table = nondef_table, user_nondefs = user_nondefs,
   250        simp_table = simp_table, psimp_table = psimp_table,
   251        intro_table = intro_table, ground_thm_table = ground_thm_table,
   252        ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
   253        special_funs = Unsynchronized.ref [],
   254        unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref []}
   255     val frees = Term.add_frees assms_t []
   256     val _ = null (Term.add_tvars assms_t [])
   257             orelse raise NOT_SUPPORTED "schematic type variables"
   258     val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
   259          core_t) = preprocess_term ext_ctxt assms_t
   260     val got_all_user_axioms =
   261       got_all_mono_user_axioms andalso no_poly_user_axioms
   262 
   263     (* styp * (bool * bool) -> unit *)
   264     fun print_wf (x, (gfp, wf)) =
   265       pprint (Pretty.blk (0,
   266           pstrs ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"")
   267           @ Syntax.pretty_term ctxt (Const x) ::
   268           pstrs (if wf then
   269                    "\" was proved well-founded. Nitpick can compute it \
   270                    \efficiently."
   271                  else
   272                    "\" could not be proved well-founded. Nitpick might need to \
   273                    \unroll it.")))
   274     val _ = if verbose then List.app print_wf (!wf_cache) else ()
   275     val _ =
   276       pprint_d (fn () =>
   277           Pretty.chunks
   278               (pretties_for_formulas ctxt "Preprocessed formula" [core_t] @
   279                pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @
   280                pretties_for_formulas ctxt "Relevant nondefinitional axiom"
   281                                      nondef_ts))
   282     val _ = List.app (ignore o Term.type_of) (core_t :: def_ts @ nondef_ts)
   283             handle TYPE (_, Ts, ts) =>
   284                    raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
   285 
   286     val unique_scope = forall (equal 1 o length o snd) cards_assigns
   287     (* typ -> bool *)
   288     fun is_free_type_monotonic T =
   289       unique_scope orelse
   290       case triple_lookup (type_match thy) monos T of
   291         SOME (SOME b) => b
   292       | _ => formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
   293     fun is_datatype_monotonic T =
   294       unique_scope orelse
   295       case triple_lookup (type_match thy) monos T of
   296         SOME (SOME b) => b
   297       | _ =>
   298         not (is_pure_typedef thy T) orelse is_univ_typedef thy T
   299         orelse is_number_type thy T
   300         orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
   301     val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
   302              |> sort TermOrd.typ_ord
   303     val (all_dataTs, all_free_Ts) =
   304       List.partition (is_integer_type orf is_datatype thy) Ts
   305     val (mono_dataTs, nonmono_dataTs) =
   306       List.partition is_datatype_monotonic all_dataTs
   307     val (mono_free_Ts, nonmono_free_Ts) =
   308       List.partition is_free_type_monotonic all_free_Ts
   309 
   310     val _ =
   311       if not unique_scope andalso not (null mono_free_Ts) then
   312         print_v (fn () =>
   313                     let
   314                       val ss = map (quote o string_for_type ctxt) mono_free_Ts
   315                     in
   316                       "The type" ^ plural_s_for_list ss ^ " " ^
   317                       space_implode " " (serial_commas "and" ss) ^ " " ^
   318                       (if none_true monos then
   319                          "passed the monotonicity test"
   320                        else
   321                          (if length ss = 1 then "is" else "are") ^
   322                          " considered monotonic") ^
   323                       ". Nitpick might be able to skip some scopes."
   324                     end)
   325       else
   326         ()
   327     val mono_Ts = mono_dataTs @ mono_free_Ts
   328     val nonmono_Ts = nonmono_dataTs @ nonmono_free_Ts
   329 
   330 (*
   331     val _ = priority "Monotonic datatypes:"
   332     val _ = List.app (priority o string_for_type ctxt) mono_dataTs
   333     val _ = priority "Nonmonotonic datatypes:"
   334     val _ = List.app (priority o string_for_type ctxt) nonmono_dataTs
   335     val _ = priority "Monotonic free types:"
   336     val _ = List.app (priority o string_for_type ctxt) mono_free_Ts
   337     val _ = priority "Nonmonotonic free types:"
   338     val _ = List.app (priority o string_for_type ctxt) nonmono_free_Ts
   339 *)
   340 
   341     val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t
   342     val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq)
   343                      def_ts
   344     val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq)
   345                         nondef_ts
   346     val (free_names, const_names) =
   347       fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
   348     val nonsel_names = filter_out (is_sel o nickname_of) const_names
   349     val would_be_genuine = got_all_user_axioms andalso none_true wfs
   350 (*
   351     val _ = List.app (priority o string_for_nut ctxt)
   352                      (core_u :: def_us @ nondef_us)
   353 *)
   354     val need_incremental = Int.max (max_potential, max_genuine) >= 2
   355     val effective_sat_solver =
   356       if sat_solver <> "smart" then
   357         if need_incremental andalso
   358            not (sat_solver mem Kodkod_SAT.configured_sat_solvers true) then
   359           (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \
   360                        \be used instead of " ^ quote sat_solver ^ "."));
   361            "SAT4J")
   362         else
   363           sat_solver
   364       else
   365         Kodkod_SAT.smart_sat_solver_name need_incremental
   366     val _ =
   367       if sat_solver = "smart" then
   368         print_v (fn () => "Using SAT solver " ^ quote effective_sat_solver ^
   369                           ". The following" ^
   370                           (if need_incremental then " incremental " else " ") ^
   371                           "solvers are configured: " ^
   372                           commas (map quote (Kodkod_SAT.configured_sat_solvers
   373                                                        need_incremental)) ^ ".")
   374       else
   375         ()
   376 
   377     val too_big_scopes = Unsynchronized.ref []
   378 
   379     (* bool -> scope -> rich_problem option *)
   380     fun problem_for_scope liberal
   381             (scope as {card_assigns, bisim_depth, datatypes, ofs, ...}) =
   382       let
   383         val _ = not (exists (fn other => scope_less_eq other scope)
   384                             (!too_big_scopes))
   385                 orelse raise LIMIT ("Nitpick.pick_them_nits_in_term.\
   386                                     \problem_for_scope", "too big scope")
   387 (*
   388         val _ = priority "Offsets:"
   389         val _ = List.app (fn (T, j0) =>
   390                              priority (string_for_type ctxt T ^ " = " ^
   391                                        string_of_int j0))
   392                          (Typtab.dest ofs)
   393 *)
   394         val all_precise = forall (is_precise_type datatypes) Ts
   395         (* nut list -> rep NameTable.table -> nut list * rep NameTable.table *)
   396         val repify_consts = choose_reps_for_consts scope all_precise
   397         val main_j0 = offset_of_type ofs bool_T
   398         val (nat_card, nat_j0) = spec_of_type scope nat_T
   399         val (int_card, int_j0) = spec_of_type scope int_T
   400         val _ = forall (equal main_j0) [nat_j0, int_j0]
   401                 orelse raise BAD ("Nitpick.pick_them_nits_in_term.\
   402                                   \problem_for_scope", "bad offsets")
   403         val kk = kodkod_constrs peephole_optim nat_card int_card main_j0
   404         val (free_names, rep_table) =
   405           choose_reps_for_free_vars scope free_names NameTable.empty
   406         val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table
   407         val (nonsel_names, rep_table) = repify_consts nonsel_names rep_table
   408         val min_highest_arity =
   409           NameTable.fold (curry Int.max o arity_of_rep o snd) rep_table 1
   410         val min_univ_card =
   411           NameTable.fold (curry Int.max o min_univ_card_of_rep o snd) rep_table
   412                          (univ_card nat_card int_card main_j0 [] Kodkod.True)
   413         val _ = check_arity min_univ_card min_highest_arity
   414 
   415         val core_u = choose_reps_in_nut scope liberal rep_table false core_u
   416         val def_us = map (choose_reps_in_nut scope liberal rep_table true)
   417                          def_us
   418         val nondef_us = map (choose_reps_in_nut scope liberal rep_table false)
   419                             nondef_us
   420 (*
   421         val _ = List.app (priority o string_for_nut ctxt)
   422                          (free_names @ sel_names @ nonsel_names @
   423                           core_u :: def_us @ nondef_us)
   424 *)
   425         val (free_rels, pool, rel_table) =
   426           rename_free_vars free_names initial_pool NameTable.empty
   427         val (sel_rels, pool, rel_table) =
   428           rename_free_vars sel_names pool rel_table
   429         val (other_rels, pool, rel_table) =
   430           rename_free_vars nonsel_names pool rel_table
   431         val core_u = rename_vars_in_nut pool rel_table core_u
   432         val def_us = map (rename_vars_in_nut pool rel_table) def_us
   433         val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
   434         (* nut -> Kodkod.formula *)
   435         val to_f = kodkod_formula_from_nut ofs liberal kk
   436         val core_f = to_f core_u
   437         val def_fs = map to_f def_us
   438         val nondef_fs = map to_f nondef_us
   439         val formula = fold (fold s_and) [def_fs, nondef_fs] core_f
   440         val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^
   441                       PrintMode.setmp [] multiline_string_for_scope scope
   442         val kodkod_sat_solver = Kodkod_SAT.sat_solver_spec effective_sat_solver
   443                                 |> snd
   444         val delay = if liberal then
   445                       Option.map (fn time => Time.- (time, Time.now ()))
   446                                  deadline
   447                       |> liberal_delay_for_timeout
   448                     else
   449                       0
   450         val settings = [("solver", commas (map quote kodkod_sat_solver)),
   451                         ("skolem_depth", "-1"),
   452                         ("bit_width", "16"),
   453                         ("symmetry_breaking", signed_string_of_int sym_break),
   454                         ("sharing", signed_string_of_int sharing_depth),
   455                         ("flatten", Bool.toString flatten_props),
   456                         ("delay", signed_string_of_int delay)]
   457         val plain_rels = free_rels @ other_rels
   458         val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels
   459         val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
   460         val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
   461         val dtype_axioms = declarative_axioms_for_datatypes ext_ctxt ofs kk
   462                                                             rel_table datatypes
   463         val declarative_axioms = plain_axioms @ dtype_axioms
   464         val univ_card = univ_card nat_card int_card main_j0
   465                                   (plain_bounds @ sel_bounds) formula
   466         val built_in_bounds = bounds_for_built_in_rels_in_formula debug
   467                                   univ_card nat_card int_card main_j0 formula
   468         val bounds = built_in_bounds @ plain_bounds @ sel_bounds
   469                      |> not debug ? merge_bounds
   470         val highest_arity =
   471           fold Integer.max (map (fst o fst) (maps fst bounds)) 0
   472         val formula = fold_rev s_and declarative_axioms formula
   473         val _ = if formula = Kodkod.False then ()
   474                 else check_arity univ_card highest_arity
   475       in
   476         SOME ({comment = comment, settings = settings, univ_card = univ_card,
   477                tuple_assigns = [], bounds = bounds,
   478                int_bounds = sequential_int_bounds univ_card,
   479                expr_assigns = [], formula = formula},
   480               {free_names = free_names, sel_names = sel_names,
   481                nonsel_names = nonsel_names, rel_table = rel_table,
   482                liberal = liberal, scope = scope, core = core_f,
   483                defs = nondef_fs @ def_fs @ declarative_axioms})
   484       end
   485       handle LIMIT (loc, msg) =>
   486              if loc = "Nitpick_Kodkod.check_arity"
   487                 andalso not (Typtab.is_empty ofs) then
   488                problem_for_scope liberal
   489                    {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
   490                     bisim_depth = bisim_depth, datatypes = datatypes,
   491                     ofs = Typtab.empty}
   492              else if loc = "Nitpick.pick_them_nits_in_term.\
   493                            \problem_for_scope" then
   494                NONE
   495              else
   496                (Unsynchronized.change too_big_scopes (cons scope);
   497                 print_v (fn () => ("Limit reached: " ^ msg ^
   498                                    ". Dropping " ^ (if liberal then "potential"
   499                                                     else "genuine") ^
   500                                    " component of scope."));
   501                 NONE)
   502 
   503     (* int -> (''a * int list list) list -> ''a -> Kodkod.tuple_set *)
   504     fun tuple_set_for_rel univ_card =
   505       Kodkod.TupleSet o map (kk_tuple debug univ_card) o the
   506       oo AList.lookup (op =)
   507 
   508     val word_model = if falsify then "counterexample" else "model"
   509 
   510     val scopes = Unsynchronized.ref []
   511     val generated_scopes = Unsynchronized.ref []
   512     val generated_problems = Unsynchronized.ref []
   513     val checked_problems = Unsynchronized.ref (SOME [])
   514     val met_potential = Unsynchronized.ref 0
   515 
   516     (* rich_problem list -> int list -> unit *)
   517     fun update_checked_problems problems =
   518       List.app (Unsynchronized.change checked_problems o Option.map o cons
   519                 o nth problems)
   520 
   521     (* bool -> Kodkod.raw_bound list -> problem_extension -> bool option *)
   522     fun print_and_check_model genuine bounds
   523             ({free_names, sel_names, nonsel_names, rel_table, scope, ...}
   524              : problem_extension) =
   525       let
   526         val (reconstructed_model, codatatypes_ok) =
   527           reconstruct_hol_model {show_skolems = show_skolems,
   528                                  show_datatypes = show_datatypes,
   529                                  show_consts = show_consts}
   530               scope formats frees free_names sel_names nonsel_names rel_table
   531               bounds
   532         val would_be_genuine = would_be_genuine andalso codatatypes_ok
   533       in
   534         pprint (Pretty.chunks
   535             [Pretty.blk (0,
   536                  (pstrs ("Nitpick found a" ^
   537                          (if not genuine then " potential "
   538                           else if would_be_genuine then " "
   539                           else " likely genuine ") ^ word_model) @
   540                   (case pretties_for_scope scope verbose of
   541                      [] => []
   542                    | pretties => pstrs " for " @ pretties) @
   543                   [Pretty.str ":\n"])),
   544              Pretty.indent indent_size reconstructed_model]);
   545         if genuine then
   546           (if check_genuine then
   547              (case prove_hol_model scope tac_timeout free_names sel_names
   548                                    rel_table bounds assms_t of
   549                 SOME true => print ("Confirmation by \"auto\": The above " ^
   550                                     word_model ^ " is really genuine.")
   551               | SOME false =>
   552                 if would_be_genuine then
   553                   error ("A supposedly genuine " ^ word_model ^ " was shown to\
   554                          \be spurious by \"auto\".\nThis should never happen.\n\
   555                          \Please send a bug report to blanchet\
   556                          \te@in.tum.de.")
   557                 else
   558                   print ("Refutation by \"auto\": The above " ^ word_model ^
   559                          " is spurious.")
   560               | NONE => print "No confirmation by \"auto\".")
   561            else
   562              ();
   563            if has_weaselly_sorts thy orig_t then
   564              print "Hint: Maybe you forgot a type constraint?"
   565            else
   566              ();
   567            if not would_be_genuine then
   568              if no_poly_user_axioms then
   569                let
   570                  val options =
   571                    [] |> not got_all_mono_user_axioms
   572                          ? cons ("user_axioms", "\"true\"")
   573                       |> not (none_true wfs)
   574                          ? cons ("wf", "\"smart\" or \"false\"")
   575                       |> not codatatypes_ok
   576                          ? cons ("bisim_depth", "a nonnegative value")
   577                  val ss =
   578                    map (fn (name, value) => quote name ^ " set to " ^ value)
   579                        options
   580                in
   581                  print ("Try again with " ^
   582                         space_implode " " (serial_commas "and" ss) ^
   583                         " to confirm that the " ^ word_model ^ " is genuine.")
   584                end
   585              else
   586                print ("Nitpick is unable to guarantee the authenticity of \
   587                       \the " ^ word_model ^ " in the presence of polymorphic \
   588                       \axioms.")
   589            else
   590              ();
   591            NONE)
   592         else
   593           if not genuine then
   594             (Unsynchronized.inc met_potential;
   595              if check_potential then
   596                let
   597                  val status = prove_hol_model scope tac_timeout free_names
   598                                               sel_names rel_table bounds assms_t
   599                in
   600                  (case status of
   601                     SOME true => print ("Confirmation by \"auto\": The above " ^
   602                                         word_model ^ " is genuine.")
   603                   | SOME false => print ("Refutation by \"auto\": The above " ^
   604                                          word_model ^ " is spurious.")
   605                   | NONE => print "No confirmation by \"auto\".");
   606                  status
   607                end
   608              else
   609                NONE)
   610           else
   611             NONE
   612       end
   613     (* int -> int -> int -> bool -> rich_problem list -> int * int * int *)
   614     fun solve_any_problem max_potential max_genuine donno first_time problems =
   615       let
   616         val max_potential = Int.max (0, max_potential)
   617         val max_genuine = Int.max (0, max_genuine)
   618         (* bool -> int * Kodkod.raw_bound list -> bool option *)
   619         fun print_and_check genuine (j, bounds) =
   620           print_and_check_model genuine bounds (snd (nth problems j))
   621         val max_solutions = max_potential + max_genuine
   622                             |> not need_incremental ? curry Int.min 1
   623       in
   624         if max_solutions <= 0 then
   625           (0, 0, donno)
   626         else
   627           case Kodkod.solve_any_problem overlord deadline max_threads
   628                                         max_solutions (map fst problems) of
   629             Kodkod.Normal ([], unsat_js) =>
   630             (update_checked_problems problems unsat_js;
   631              (max_potential, max_genuine, donno))
   632           | Kodkod.Normal (sat_ps, unsat_js) =>
   633             let
   634               val (lib_ps, con_ps) =
   635                 List.partition (#liberal o snd o nth problems o fst) sat_ps
   636             in
   637               update_checked_problems problems (unsat_js @ map fst lib_ps);
   638               if null con_ps then
   639                 let
   640                   val num_genuine = Library.take (max_potential, lib_ps)
   641                                     |> map (print_and_check false)
   642                                     |> filter (equal (SOME true)) |> length
   643                   val max_genuine = max_genuine - num_genuine
   644                   val max_potential = max_potential
   645                                       - (length lib_ps - num_genuine)
   646                 in
   647                   if max_genuine <= 0 then
   648                     (0, 0, donno)
   649                   else
   650                     let
   651                       (* "co_js" is the list of conservative problems whose
   652                          liberal pendants couldn't be satisfied and hence that
   653                          most probably can't be satisfied themselves. *)
   654                       val co_js =
   655                         map (fn j => j - 1) unsat_js
   656                         |> filter (fn j =>
   657                                       j >= 0 andalso
   658                                       scopes_equivalent
   659                                           (#scope (snd (nth problems j)))
   660                                           (#scope (snd (nth problems (j + 1)))))
   661                       val bye_js = sort_distinct int_ord (map fst sat_ps @
   662                                                           unsat_js @ co_js)
   663                       val problems =
   664                         problems |> filter_out_indices bye_js
   665                                  |> max_potential <= 0
   666                                     ? filter_out (#liberal o snd)
   667                     in
   668                       solve_any_problem max_potential max_genuine donno false
   669                                         problems
   670                     end
   671                 end
   672               else
   673                 let
   674                   val _ = Library.take (max_genuine, con_ps)
   675                           |> List.app (ignore o print_and_check true)
   676                   val max_genuine = max_genuine - length con_ps
   677                 in
   678                   if max_genuine <= 0 orelse not first_time then
   679                     (0, max_genuine, donno)
   680                   else
   681                     let
   682                       val bye_js = sort_distinct int_ord
   683                                                  (map fst sat_ps @ unsat_js)
   684                       val problems =
   685                         problems |> filter_out_indices bye_js
   686                                  |> filter_out (#liberal o snd)
   687                     in solve_any_problem 0 max_genuine donno false problems end
   688                 end
   689             end
   690           | Kodkod.TimedOut unsat_js =>
   691             (update_checked_problems problems unsat_js; raise TimeLimit.TimeOut)
   692           | Kodkod.Interrupted NONE =>
   693             (checked_problems := NONE; do_interrupted ())
   694           | Kodkod.Interrupted (SOME unsat_js) =>
   695             (update_checked_problems problems unsat_js; do_interrupted ())
   696           | Kodkod.Error (s, unsat_js) =>
   697             (update_checked_problems problems unsat_js;
   698              print_v (K ("Kodkod error: " ^ s ^ "."));
   699              (max_potential, max_genuine, donno + 1))
   700       end
   701 
   702     (* int -> int -> scope list -> int * int * int -> int * int * int *)
   703     fun run_batch j n scopes (max_potential, max_genuine, donno) =
   704       let
   705         val _ =
   706           if null scopes then
   707             print_m (K "The scope specification is inconsistent.")
   708           else if verbose then
   709             pprint (Pretty.chunks
   710                 [Pretty.blk (0,
   711                      pstrs ((if n > 1 then
   712                                "Batch " ^ string_of_int (j + 1) ^ " of " ^
   713                                signed_string_of_int n ^ ": "
   714                              else
   715                                "") ^
   716                             "Trying " ^ string_of_int (length scopes) ^
   717                             " scope" ^ plural_s_for_list scopes ^ ":")),
   718                  Pretty.indent indent_size
   719                      (Pretty.chunks (map2
   720                           (fn j => fn scope =>
   721                               Pretty.block (
   722                                   (case pretties_for_scope scope true of
   723                                      [] => [Pretty.str "Empty"]
   724                                    | pretties => pretties) @
   725                                   [Pretty.str (if j = 1 then "." else ";")]))
   726                           (length scopes downto 1) scopes))])
   727           else
   728             ()
   729         (* scope * bool -> rich_problem list * bool
   730            -> rich_problem list * bool *)
   731         fun add_problem_for_scope (scope as {datatypes, ...}, liberal)
   732                                   (problems, donno) =
   733           (check_deadline ();
   734            case problem_for_scope liberal scope of
   735              SOME problem =>
   736              (problems
   737               |> (null problems orelse
   738                   not (Kodkod.problems_equivalent (fst problem)
   739                                                   (fst (hd problems))))
   740                   ? cons problem, donno)
   741            | NONE => (problems, donno + 1))
   742         val (problems, donno) =
   743           fold add_problem_for_scope
   744                (map_product pair scopes
   745                     ((if max_genuine > 0 then [false] else []) @
   746                      (if max_potential > 0 then [true] else [])))
   747                ([], donno)
   748         val _ = Unsynchronized.change generated_problems (append problems)
   749         val _ = Unsynchronized.change generated_scopes (append scopes)
   750       in
   751         solve_any_problem max_potential max_genuine donno true (rev problems)
   752       end
   753 
   754     (* rich_problem list -> scope -> int *)
   755     fun scope_count (problems : rich_problem list) scope =
   756       length (filter (scopes_equivalent scope o #scope o snd) problems)
   757     (* string -> string *)
   758     fun excipit did_so_and_so =
   759       let
   760         (* rich_problem list -> rich_problem list *)
   761         val do_filter =
   762           if !met_potential = max_potential then filter_out (#liberal o snd)
   763           else I
   764         val total = length (!scopes)
   765         val unsat =
   766           fold (fn scope =>
   767                    case scope_count (do_filter (!generated_problems)) scope of
   768                      0 => I
   769                    | n =>
   770                      if scope_count (do_filter (these (!checked_problems)))
   771                                     scope = n then
   772                        Integer.add 1
   773                      else
   774                        I) (!generated_scopes) 0
   775       in
   776         "Nitpick " ^ did_so_and_so ^
   777         (if is_some (!checked_problems) andalso total > 0 then
   778            " after checking " ^
   779            string_of_int (Int.min (total - 1, unsat)) ^ " of " ^
   780            string_of_int total ^ " scope" ^ plural_s total
   781          else
   782            "") ^ "."
   783       end
   784 
   785     (* int -> int -> scope list -> int * int * int -> Kodkod.outcome *)
   786     fun run_batches _ _ [] (max_potential, max_genuine, donno) =
   787         if donno > 0 andalso max_genuine > 0 then
   788           (print_m (fn () => excipit "ran out of resources"); "unknown")
   789         else if max_genuine = original_max_genuine then
   790           if max_potential = original_max_potential then
   791             (print_m (K ("Nitpick found no " ^ word_model ^ ".")); "none")
   792           else
   793             (print_m (K ("Nitpick could not find " ^
   794                          (if max_genuine = 1 then "a better " ^ word_model ^ "."
   795                           else "any better " ^ word_model ^ "s.")));
   796              "potential")
   797         else
   798           if would_be_genuine then "genuine" else "likely_genuine"
   799       | run_batches j n (batch :: batches) z =
   800         let val (z as (_, max_genuine, _)) = run_batch j n batch z in
   801           run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
   802         end
   803 
   804     val _ = scopes := all_scopes ext_ctxt sym_break cards_assigns maxes_assigns
   805                                  iters_assigns bisim_depths mono_Ts nonmono_Ts
   806     val batches = batch_list batch_size (!scopes)
   807     val outcome_code =
   808       (run_batches 0 (length batches) batches (max_potential, max_genuine, 0)
   809        handle Exn.Interrupt => do_interrupted ())
   810       handle TimeLimit.TimeOut =>
   811              (print_m (fn () => excipit "ran out of time");
   812               if !met_potential > 0 then "potential" else "unknown")
   813            | Exn.Interrupt => if auto orelse debug then raise Interrupt
   814                               else error (excipit "was interrupted")
   815     val _ = print_v (fn () => "Total time: " ^
   816                               signed_string_of_int (Time.toMilliseconds
   817                                     (Timer.checkRealTimer timer)) ^ " ms.")
   818   in (outcome_code, !state_ref) end
   819   handle Exn.Interrupt =>
   820          if auto orelse #debug params then
   821            raise Interrupt
   822          else
   823            if passed_deadline deadline then
   824              (priority "Nitpick ran out of time."; ("unknown", state))
   825            else
   826              error "Nitpick was interrupted."
   827 
   828 (* Proof.state -> params -> bool -> term -> string * Proof.state *)
   829 fun pick_nits_in_term state (params as {debug, timeout, expect, ...})
   830                       auto orig_assm_ts orig_t =
   831   let
   832     val deadline = Option.map (curry Time.+ (Time.now ())) timeout
   833     val outcome as (outcome_code, _) =
   834       time_limit (if debug then NONE else timeout)
   835           (pick_them_nits_in_term deadline state params auto orig_assm_ts)
   836           orig_t
   837   in
   838     if expect = "" orelse outcome_code = expect then outcome
   839     else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
   840   end
   841 
   842 (* Proof.state -> params -> thm -> int -> string * Proof.state *)
   843 fun pick_nits_in_subgoal state params auto subgoal =
   844   let
   845     val ctxt = Proof.context_of state
   846     val t = state |> Proof.get_goal |> snd |> snd |> prop_of
   847   in
   848     if Logic.count_prems t = 0 then
   849       (priority "No subgoal!"; ("none", state))
   850     else
   851       let
   852         val assms = map term_of (Assumption.all_assms_of ctxt)
   853         val (t, frees) = Logic.goal_params t subgoal
   854       in pick_nits_in_term state params auto assms (subst_bounds (frees, t)) end
   855   end
   856 
   857 end;