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