src/HOL/TPTP/atp_problem_import.ML
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 64561 a7664ca9ffc5
child 69597 ff784d5a5bfb
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
blanchet@55208
     1
(*  Title:      HOL/TPTP/atp_problem_import.ML
blanchet@46324
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@46324
     3
    Copyright   2012
blanchet@46324
     4
blanchet@46324
     5
Import TPTP problems as Isabelle terms or goals.
blanchet@46324
     6
*)
blanchet@46324
     7
blanchet@46324
     8
signature ATP_PROBLEM_IMPORT =
blanchet@46324
     9
sig
blanchet@54434
    10
  val read_tptp_file : theory -> (string * term -> 'a) -> string ->
blanchet@54434
    11
    'a list * ('a list * 'a list) * Proof.context
blanchet@47794
    12
  val nitpick_tptp_file : theory -> int -> string -> unit
blanchet@47794
    13
  val refute_tptp_file : theory -> int -> string -> unit
blanchet@64561
    14
  val can_tac : Proof.context -> (Proof.context -> tactic) -> term -> bool
blanchet@47845
    15
  val SOLVE_TIMEOUT :  int -> string -> tactic -> tactic
blanchet@57812
    16
  val atp_tac : Proof.context -> int -> (string * string) list -> int -> term list -> string ->
blanchet@57812
    17
    int -> tactic
blanchet@47845
    18
  val smt_solver_tac : string -> Proof.context -> int -> tactic
blanchet@47845
    19
  val freeze_problem_consts : theory -> term -> term
blanchet@47845
    20
  val make_conj : term list * term list -> term list -> term
blanchet@47794
    21
  val sledgehammer_tptp_file : theory -> int -> string -> unit
blanchet@48083
    22
  val isabelle_tptp_file : theory -> int -> string -> unit
blanchet@48083
    23
  val isabelle_hot_tptp_file : theory -> int -> string -> unit
blanchet@54472
    24
  val translate_tptp_file : theory -> string -> string -> unit
blanchet@46324
    25
end;
blanchet@46324
    26
blanchet@46324
    27
structure ATP_Problem_Import : ATP_PROBLEM_IMPORT =
blanchet@46324
    28
struct
blanchet@46324
    29
blanchet@47643
    30
open ATP_Util
blanchet@47643
    31
open ATP_Problem
blanchet@47643
    32
open ATP_Proof
blanchet@54434
    33
open ATP_Problem_Generate
blanchet@54434
    34
open ATP_Systems
blanchet@47643
    35
blanchet@47776
    36
val debug = false
blanchet@47776
    37
val overlord = false
blanchet@47776
    38
blanchet@47643
    39
blanchet@47771
    40
(** TPTP parsing **)
blanchet@47643
    41
blanchet@54434
    42
fun exploded_absolute_path file_name =
blanchet@54434
    43
  Path.explode file_name
blanchet@54434
    44
  |> (fn path => path |> not (Path.is_absolute path) ? Path.append (Path.explode "$PWD"))
blanchet@54434
    45
blanchet@47785
    46
fun read_tptp_file thy postproc file_name =
blanchet@47644
    47
  let
blanchet@47718
    48
    fun has_role role (_, role', _, _) = (role' = role)
blanchet@57809
    49
    fun get_prop f (name, _, P, _) = P |> f |> close_form |> pair name |> postproc
blanchet@57809
    50
blanchet@54434
    51
    val path = exploded_absolute_path file_name
blanchet@47714
    52
    val ((_, _, problem), thy) =
blanchet@57809
    53
      TPTP_Interpret.interpret_file true [Path.dir path, Path.explode "$TPTP"] path [] [] thy
blanchet@57809
    54
    val (conjs, defs_and_nondefs) = problem
blanchet@57809
    55
      |> List.partition (has_role TPTP_Syntax.Role_Conjecture)
blanchet@57809
    56
      ||> List.partition (has_role TPTP_Syntax.Role_Definition)
blanchet@47644
    57
  in
blanchet@57809
    58
    (map (get_prop I) conjs,
wenzelm@59058
    59
     apply2 (map (get_prop Logic.varify_global)) defs_and_nondefs,
blanchet@57812
    60
     Named_Target.theory_init thy)
blanchet@47557
    61
  end
blanchet@46325
    62
blanchet@47771
    63
blanchet@57547
    64
(** Nitpick **)
blanchet@46324
    65
blanchet@47718
    66
fun aptrueprop f ((t0 as @{const Trueprop}) $ t1) = t0 $ f t1
blanchet@47718
    67
  | aptrueprop f t = f t
blanchet@47718
    68
blanchet@57547
    69
fun is_legitimate_tptp_def (@{const Trueprop} $ t) = is_legitimate_tptp_def t
blanchet@57547
    70
  | is_legitimate_tptp_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
blanchet@57547
    71
    (is_Const t orelse is_Free t) andalso not (exists_subterm (curry (op =) t) u)
blanchet@57547
    72
  | is_legitimate_tptp_def _ = false
blanchet@57547
    73
blanchet@47794
    74
fun nitpick_tptp_file thy timeout file_name =
blanchet@46325
    75
  let
blanchet@54434
    76
    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
blanchet@47771
    77
    val thy = Proof_Context.theory_of ctxt
blanchet@57809
    78
    val (defs, pseudo_defs) = defs
blanchet@57809
    79
      |> map (ATP_Util.abs_extensionalize_term ctxt #> aptrueprop (hol_open_form I))
blanchet@57809
    80
      |> List.partition (is_legitimate_tptp_def o perhaps (try HOLogic.dest_Trueprop)
blanchet@57809
    81
        o ATP_Util.unextensionalize_def)
blanchet@47991
    82
    val nondefs = pseudo_defs @ nondefs
blanchet@47714
    83
    val state = Proof.init ctxt
blanchet@46325
    84
    val params =
blanchet@61569
    85
      [("card", "1-100"),
blanchet@46325
    86
       ("box", "false"),
blanchet@46325
    87
       ("max_threads", "1"),
blanchet@47791
    88
       ("batch_size", "5"),
blanchet@47718
    89
       ("falsify", if null conjs then "false" else "true"),
blanchet@46325
    90
       ("verbose", "true"),
blanchet@47776
    91
       ("debug", if debug then "true" else "false"),
blanchet@47776
    92
       ("overlord", if overlord then "true" else "false"),
blanchet@46325
    93
       ("show_consts", "true"),
blanchet@47755
    94
       ("format", "1"),
blanchet@46325
    95
       ("max_potential", "0"),
blanchet@47718
    96
       ("timeout", string_of_int timeout),
blanchet@47718
    97
       ("tac_timeout", string_of_int ((timeout + 49) div 50))]
blanchet@55199
    98
      |> Nitpick_Commands.default_params thy
blanchet@46325
    99
    val i = 1
blanchet@46325
   100
    val n = 1
blanchet@46325
   101
    val step = 0
blanchet@46325
   102
    val subst = []
blanchet@46325
   103
  in
blanchet@57809
   104
    Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst defs nondefs
blanchet@57809
   105
      (case conjs of conj :: _ => conj | [] => @{prop True});
blanchet@47718
   106
    ()
blanchet@46325
   107
  end
blanchet@46324
   108
blanchet@46324
   109
blanchet@46324
   110
(** Refute **)
blanchet@46324
   111
blanchet@47794
   112
fun refute_tptp_file thy timeout file_name =
blanchet@46325
   113
  let
blanchet@52031
   114
    fun print_szs_of_outcome falsify s =
blanchet@47766
   115
      "% SZS status " ^
blanchet@47766
   116
      (if s = "genuine" then
blanchet@47766
   117
         if falsify then "CounterSatisfiable" else "Satisfiable"
blanchet@47766
   118
       else
blanchet@61310
   119
         "GaveUp")
wenzelm@58843
   120
      |> writeln
blanchet@54434
   121
    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
blanchet@46325
   122
    val params =
blanchet@47714
   123
      [("maxtime", string_of_int timeout),
blanchet@47714
   124
       ("maxvars", "100000")]
blanchet@46325
   125
  in
blanchet@47718
   126
    Refute.refute_term ctxt params (defs @ nondefs)
blanchet@57809
   127
      (case conjs of conj :: _ => conj | [] => @{prop True})
blanchet@52031
   128
    |> print_szs_of_outcome (not (null conjs))
blanchet@46325
   129
  end
blanchet@46324
   130
blanchet@46324
   131
blanchet@47766
   132
(** Sledgehammer and Isabelle (combination of provers) **)
blanchet@47766
   133
blanchet@64561
   134
fun can_tac ctxt tactic conj =
blanchet@64561
   135
  can (Goal.prove_internal ctxt [] (Thm.cterm_of ctxt conj)) (fn [] => tactic ctxt)
blanchet@47771
   136
blanchet@47766
   137
fun SOLVE_TIMEOUT seconds name tac st =
blanchet@47766
   138
  let
wenzelm@58843
   139
    val _ = writeln ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
blanchet@47766
   140
    val result =
wenzelm@62519
   141
      Timeout.apply (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
blanchet@64561
   142
      handle Timeout.TIMEOUT _ => NONE | ERROR _ => NONE
blanchet@47766
   143
  in
blanchet@57809
   144
    (case result of
wenzelm@58843
   145
      NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
wenzelm@58843
   146
    | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
blanchet@47766
   147
  end
blanchet@46324
   148
blanchet@47812
   149
fun nitpick_finite_oracle_tac ctxt timeout i th =
blanchet@47812
   150
  let
blanchet@47812
   151
    fun is_safe (Type (@{type_name fun}, Ts)) = forall is_safe Ts
blanchet@47812
   152
      | is_safe @{typ prop} = true
blanchet@47812
   153
      | is_safe @{typ bool} = true
blanchet@47812
   154
      | is_safe _ = false
blanchet@57809
   155
blanchet@47812
   156
    val conj = Thm.term_of (Thm.cprem_of th i)
blanchet@47812
   157
  in
blanchet@47812
   158
    if exists_type (not o is_safe) conj then
blanchet@47812
   159
      Seq.empty
blanchet@47812
   160
    else
blanchet@47812
   161
      let
blanchet@47812
   162
        val thy = Proof_Context.theory_of ctxt
blanchet@47812
   163
        val state = Proof.init ctxt
blanchet@47812
   164
        val params =
blanchet@47812
   165
          [("box", "false"),
blanchet@47812
   166
           ("max_threads", "1"),
blanchet@47812
   167
           ("verbose", "true"),
blanchet@47812
   168
           ("debug", if debug then "true" else "false"),
blanchet@47812
   169
           ("overlord", if overlord then "true" else "false"),
blanchet@47812
   170
           ("max_potential", "0"),
blanchet@47812
   171
           ("timeout", string_of_int timeout)]
blanchet@55199
   172
          |> Nitpick_Commands.default_params thy
blanchet@47812
   173
        val i = 1
blanchet@47812
   174
        val n = 1
blanchet@47812
   175
        val step = 0
blanchet@47812
   176
        val subst = []
blanchet@47812
   177
        val (outcome, _) =
blanchet@57809
   178
          Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst [] [] conj
blanchet@57809
   179
      in
wenzelm@59498
   180
        if outcome = "none" then ALLGOALS (Skip_Proof.cheat_tac ctxt) th else Seq.empty
blanchet@57809
   181
      end
blanchet@47812
   182
  end
blanchet@47812
   183
blanchet@57812
   184
fun atp_tac ctxt completeness override_params timeout assms prover =
blanchet@47946
   185
  let
blanchet@57812
   186
    val thy = Proof_Context.theory_of ctxt
blanchet@57812
   187
    val assm_ths0 = map (Skip_Proof.make_thm thy) assms
blanchet@57812
   188
    val ((assm_name, _), ctxt) = ctxt
blanchet@64445
   189
      |> Config.put Sledgehammer_Prover_ATP.atp_completish (if completeness > 0 then 3 else 0)
blanchet@57812
   190
      |> Local_Theory.note ((@{binding thms}, []), assm_ths0)
blanchet@57812
   191
blanchet@52071
   192
    fun ref_of th = (Facts.named (Thm.derivation_name th), [])
blanchet@57812
   193
    val ref_of_assms = (Facts.named assm_name, [])
blanchet@47946
   194
  in
blanchet@47946
   195
    Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
blanchet@57809
   196
      ([("debug", if debug then "true" else "false"),
blanchet@57809
   197
        ("overlord", if overlord then "true" else "false"),
blanchet@57809
   198
        ("provers", prover),
blanchet@57809
   199
        ("timeout", string_of_int timeout)] @
blanchet@57809
   200
       (if completeness > 0 then
blanchet@57809
   201
          [("type_enc", if completeness = 1 then "mono_native" else "poly_tags")]
blanchet@57809
   202
        else
blanchet@57809
   203
          []) @
blanchet@57809
   204
       override_params)
blanchet@57812
   205
      {add = ref_of_assms :: map ref_of [ext, @{thm someI}], del = [], only = true} []
blanchet@47946
   206
  end
blanchet@47765
   207
blanchet@57812
   208
fun sledgehammer_tac demo ctxt timeout assms i =
blanchet@47766
   209
  let
blanchet@47946
   210
    val frac = if demo then 16 else 12
blanchet@48143
   211
    fun slice mult completeness prover =
blanchet@47946
   212
      SOLVE_TIMEOUT (mult * timeout div frac)
blanchet@57809
   213
        (prover ^ (if completeness > 0 then "(" ^ string_of_int completeness ^ ")" else ""))
blanchet@57812
   214
        (atp_tac ctxt completeness [] (mult * timeout div frac) assms prover i)
blanchet@47766
   215
  in
fleury@57154
   216
    slice 2 0 ATP_Proof.spassN
fleury@57154
   217
    ORELSE slice 2 0 ATP_Proof.vampireN
fleury@57154
   218
    ORELSE slice 2 0 ATP_Proof.eN
fleury@57154
   219
    ORELSE slice 2 0 ATP_Proof.z3_tptpN
fleury@57154
   220
    ORELSE slice 1 1 ATP_Proof.spassN
fleury@57154
   221
    ORELSE slice 1 2 ATP_Proof.eN
fleury@57154
   222
    ORELSE slice 1 1 ATP_Proof.vampireN
fleury@57154
   223
    ORELSE slice 1 2 ATP_Proof.vampireN
blanchet@47946
   224
    ORELSE
blanchet@47946
   225
      (if demo then
fleury@57154
   226
         slice 2 0 ATP_Proof.satallaxN
fleury@57154
   227
         ORELSE slice 2 0 ATP_Proof.leo2N
blanchet@47946
   228
       else
blanchet@47946
   229
         no_tac)
blanchet@47766
   230
  end
blanchet@47766
   231
blanchet@47832
   232
fun smt_solver_tac solver ctxt =
blanchet@47832
   233
  let
blanchet@47832
   234
    val ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver solver)
blanchet@47832
   235
  in SMT_Solver.smt_tac ctxt [] end
blanchet@47832
   236
blanchet@57812
   237
fun auto_etc_tac ctxt timeout assms i =
blanchet@57809
   238
  SOLVE_TIMEOUT (timeout div 20) "nitpick" (nitpick_finite_oracle_tac ctxt (timeout div 20) i)
blanchet@57809
   239
  ORELSE SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac ctxt i)
blanchet@47788
   240
  ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
blanchet@47794
   241
  ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
blanchet@57812
   242
    (auto_tac ctxt THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) assms ATP_Proof.spassN))
blanchet@47946
   243
  ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i)
blanchet@47946
   244
  ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" ctxt i)
blanchet@60543
   245
  ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc4" (smt_solver_tac "cvc4" ctxt i)
blanchet@47812
   246
  ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i)
blanchet@47794
   247
  ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
blanchet@47832
   248
  ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac ctxt [] i)
blanchet@47812
   249
  ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac ctxt i)
blanchet@47771
   250
blanchet@47794
   251
fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator
blanchet@47785
   252
blanchet@47785
   253
(* Isabelle's standard automatic tactics ("auto", etc.) are more eager to
blanchet@47785
   254
   unfold "definitions" of free variables than of constants (cf. PUZ107^5). *)
blanchet@47794
   255
fun freeze_problem_consts thy =
blanchet@47794
   256
  let val is_problem_const = String.isPrefix (problem_const_prefix thy) in
blanchet@57809
   257
    map_aterms
blanchet@57809
   258
      (fn t as Const (s, T) => if is_problem_const s then Free (Long_Name.base_name s, T) else t
blanchet@57809
   259
        | t => t)
blanchet@47794
   260
  end
blanchet@47785
   261
blanchet@47776
   262
fun make_conj (defs, nondefs) conjs =
blanchet@57809
   263
  Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => @{prop False})
blanchet@47771
   264
blanchet@52031
   265
fun print_szs_of_success conjs success =
wenzelm@58843
   266
  writeln ("% SZS status " ^
blanchet@57809
   267
    (if success then
blanchet@57809
   268
       if null conjs then "Unsatisfiable" else "Theorem"
blanchet@57809
   269
     else
blanchet@61310
   270
       "GaveUp"))
blanchet@47765
   271
blanchet@47794
   272
fun sledgehammer_tptp_file thy timeout file_name =
blanchet@47771
   273
  let
blanchet@57809
   274
    val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name
blanchet@57812
   275
    val conj = make_conj ([], []) conjs
blanchet@57812
   276
    val assms = op @ assms
blanchet@47771
   277
  in
blanchet@64561
   278
    can_tac ctxt (fn ctxt => sledgehammer_tac true ctxt timeout assms 1) conj
blanchet@52031
   279
    |> print_szs_of_success conjs
blanchet@47771
   280
  end
blanchet@47766
   281
blanchet@48083
   282
fun generic_isabelle_tptp_file demo thy timeout file_name =
blanchet@47771
   283
  let
blanchet@57809
   284
    val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name
blanchet@57812
   285
    val conj = make_conj ([], []) conjs
blanchet@57812
   286
    val full_conj = make_conj assms conjs
blanchet@57812
   287
    val assms = op @ assms
blanchet@48143
   288
    val (last_hope_atp, last_hope_completeness) =
fleury@57154
   289
      if demo then (ATP_Proof.satallaxN, 0) else (ATP_Proof.vampireN, 2)
blanchet@47771
   290
  in
blanchet@64561
   291
    (can_tac ctxt (fn ctxt => auto_etc_tac ctxt (timeout div 2) assms 1) full_conj orelse
blanchet@64561
   292
     can_tac ctxt (fn ctxt => sledgehammer_tac demo ctxt (timeout div 2) assms 1) conj orelse
blanchet@64561
   293
     can_tac ctxt (fn ctxt => SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
blanchet@57812
   294
       (atp_tac ctxt last_hope_completeness [] timeout assms last_hope_atp 1)) full_conj)
blanchet@52031
   295
    |> print_szs_of_success conjs
blanchet@47771
   296
  end
blanchet@46324
   297
blanchet@48083
   298
val isabelle_tptp_file = generic_isabelle_tptp_file false
blanchet@48083
   299
val isabelle_hot_tptp_file = generic_isabelle_tptp_file true
blanchet@47832
   300
blanchet@47832
   301
blanchet@46324
   302
(** Translator between TPTP(-like) file formats **)
blanchet@46324
   303
blanchet@54472
   304
fun translate_tptp_file thy format_str file_name =
blanchet@54434
   305
  let
blanchet@54472
   306
    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name
blanchet@54434
   307
    val conj = make_conj ([], []) (map snd conjs)
blanchet@54434
   308
blanchet@54434
   309
    val (format, type_enc, lam_trans) =
blanchet@54434
   310
      (case format_str of
blanchet@54434
   311
        "FOF" => (FOF, "mono_guards??", liftingN)
blanchet@54547
   312
      | "TF0" => (TFF Monomorphic, "mono_native", liftingN)
blanchet@54547
   313
      | "TH0" => (THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN)
blanchet@54434
   314
      | "DFG" => (DFG Monomorphic, "mono_native", liftingN)
blanchet@54434
   315
      | _ => error ("Unknown format " ^ quote format_str ^
blanchet@54547
   316
        " (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")"))
blanchet@61860
   317
    val generate_info = false
blanchet@54434
   318
    val uncurried_aliases = false
blanchet@54434
   319
    val readable_names = true
blanchet@54434
   320
    val presimp = true
blanchet@57809
   321
    val facts =
blanchet@57809
   322
      map (apfst (rpair (Global, Non_Rec_Def))) defs @
blanchet@54434
   323
      map (apfst (rpair (Global, General))) nondefs
blanchet@57268
   324
    val (atp_problem, _, _, _) =
blanchet@61860
   325
      generate_atp_problem ctxt generate_info format Hypothesis (type_enc_of_string Strict type_enc)
blanchet@61860
   326
        Translator
blanchet@54434
   327
        lam_trans uncurried_aliases readable_names presimp [] conj facts
blanchet@54434
   328
blanchet@54434
   329
    val ord = effective_term_order ctxt spassN
blanchet@54434
   330
    val ord_info = K []
blanchet@54434
   331
    val lines = lines_of_atp_problem format ord ord_info atp_problem
blanchet@54434
   332
  in
blanchet@54472
   333
    List.app Output.physical_stdout lines
blanchet@54434
   334
  end
blanchet@46324
   335
blanchet@46324
   336
end;