src/HOL/TPTP/atp_problem_import.ML
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 62718 27333dc58e28
child 64445 233a11ed2dfb
permissions -rw-r--r--
tuned proofs;
     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 -> 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 = can (Goal.prove ctxt [] [] conj) (K tactic)
   135 
   136 fun SOLVE_TIMEOUT seconds name tac st =
   137   let
   138     val _ = writeln ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
   139     val result =
   140       Timeout.apply (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
   141         handle Timeout.TIMEOUT _ => NONE | ERROR _ => NONE
   142   in
   143     (case result of
   144       NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
   145     | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
   146   end
   147 
   148 fun nitpick_finite_oracle_tac ctxt timeout i th =
   149   let
   150     fun is_safe (Type (@{type_name fun}, Ts)) = forall is_safe Ts
   151       | is_safe @{typ prop} = true
   152       | is_safe @{typ bool} = true
   153       | is_safe _ = false
   154 
   155     val conj = Thm.term_of (Thm.cprem_of th i)
   156   in
   157     if exists_type (not o is_safe) conj then
   158       Seq.empty
   159     else
   160       let
   161         val thy = Proof_Context.theory_of ctxt
   162         val state = Proof.init ctxt
   163         val params =
   164           [("box", "false"),
   165            ("max_threads", "1"),
   166            ("verbose", "true"),
   167            ("debug", if debug then "true" else "false"),
   168            ("overlord", if overlord then "true" else "false"),
   169            ("max_potential", "0"),
   170            ("timeout", string_of_int timeout)]
   171           |> Nitpick_Commands.default_params thy
   172         val i = 1
   173         val n = 1
   174         val step = 0
   175         val subst = []
   176         val (outcome, _) =
   177           Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst [] [] conj
   178       in
   179         if outcome = "none" then ALLGOALS (Skip_Proof.cheat_tac ctxt) th else Seq.empty
   180       end
   181   end
   182 
   183 fun atp_tac ctxt completeness override_params timeout assms prover =
   184   let
   185     val thy = Proof_Context.theory_of ctxt
   186     val assm_ths0 = map (Skip_Proof.make_thm thy) assms
   187     val ((assm_name, _), ctxt) = ctxt
   188       |> Config.put Sledgehammer_Prover_ATP.atp_completish (if completeness > 0 then 2 else 0)
   189       |> Local_Theory.note ((@{binding thms}, []), assm_ths0)
   190 
   191     fun ref_of th = (Facts.named (Thm.derivation_name th), [])
   192     val ref_of_assms = (Facts.named assm_name, [])
   193   in
   194     Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
   195       ([("debug", if debug then "true" else "false"),
   196         ("overlord", if overlord then "true" else "false"),
   197         ("provers", prover),
   198         ("timeout", string_of_int timeout)] @
   199        (if completeness > 0 then
   200           [("type_enc", if completeness = 1 then "mono_native" else "poly_tags")]
   201         else
   202           []) @
   203        override_params)
   204       {add = ref_of_assms :: map ref_of [ext, @{thm someI}], del = [], only = true} []
   205   end
   206 
   207 fun sledgehammer_tac demo ctxt timeout assms i =
   208   let
   209     val frac = if demo then 16 else 12
   210     fun slice mult completeness prover =
   211       SOLVE_TIMEOUT (mult * timeout div frac)
   212         (prover ^ (if completeness > 0 then "(" ^ string_of_int completeness ^ ")" else ""))
   213         (atp_tac ctxt completeness [] (mult * timeout div frac) assms prover i)
   214   in
   215     slice 2 0 ATP_Proof.spassN
   216     ORELSE slice 2 0 ATP_Proof.vampireN
   217     ORELSE slice 2 0 ATP_Proof.eN
   218     ORELSE slice 2 0 ATP_Proof.z3_tptpN
   219     ORELSE slice 1 1 ATP_Proof.spassN
   220     ORELSE slice 1 2 ATP_Proof.eN
   221     ORELSE slice 1 1 ATP_Proof.vampireN
   222     ORELSE slice 1 2 ATP_Proof.vampireN
   223     ORELSE
   224       (if demo then
   225          slice 2 0 ATP_Proof.satallaxN
   226          ORELSE slice 2 0 ATP_Proof.leo2N
   227        else
   228          no_tac)
   229   end
   230 
   231 fun smt_solver_tac solver ctxt =
   232   let
   233     val ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver solver)
   234   in SMT_Solver.smt_tac ctxt [] end
   235 
   236 fun auto_etc_tac ctxt timeout assms i =
   237   SOLVE_TIMEOUT (timeout div 20) "nitpick" (nitpick_finite_oracle_tac ctxt (timeout div 20) i)
   238   ORELSE SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac ctxt i)
   239   ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
   240   ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
   241     (auto_tac ctxt THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) assms ATP_Proof.spassN))
   242   ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i)
   243   ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" ctxt i)
   244   ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc4" (smt_solver_tac "cvc4" ctxt i)
   245   ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i)
   246   ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
   247   ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac ctxt [] i)
   248   ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac ctxt i)
   249 
   250 fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator
   251 
   252 (* Isabelle's standard automatic tactics ("auto", etc.) are more eager to
   253    unfold "definitions" of free variables than of constants (cf. PUZ107^5). *)
   254 fun freeze_problem_consts thy =
   255   let val is_problem_const = String.isPrefix (problem_const_prefix thy) in
   256     map_aterms
   257       (fn t as Const (s, T) => if is_problem_const s then Free (Long_Name.base_name s, T) else t
   258         | t => t)
   259   end
   260 
   261 fun make_conj (defs, nondefs) conjs =
   262   Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => @{prop False})
   263 
   264 fun print_szs_of_success conjs success =
   265   writeln ("% SZS status " ^
   266     (if success then
   267        if null conjs then "Unsatisfiable" else "Theorem"
   268      else
   269        "GaveUp"))
   270 
   271 fun sledgehammer_tptp_file thy timeout file_name =
   272   let
   273     val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name
   274     val conj = make_conj ([], []) conjs
   275     val assms = op @ assms
   276   in
   277     can_tac ctxt (sledgehammer_tac true ctxt timeout assms 1) conj
   278     |> print_szs_of_success conjs
   279   end
   280 
   281 fun generic_isabelle_tptp_file demo thy timeout file_name =
   282   let
   283     val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name
   284     val conj = make_conj ([], []) conjs
   285     val full_conj = make_conj assms conjs
   286     val assms = op @ assms
   287     val (last_hope_atp, last_hope_completeness) =
   288       if demo then (ATP_Proof.satallaxN, 0) else (ATP_Proof.vampireN, 2)
   289   in
   290     (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) assms 1) full_conj orelse
   291      can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) assms 1) conj orelse
   292      can_tac ctxt (SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
   293        (atp_tac ctxt last_hope_completeness [] timeout assms last_hope_atp 1)) full_conj)
   294     |> print_szs_of_success conjs
   295   end
   296 
   297 val isabelle_tptp_file = generic_isabelle_tptp_file false
   298 val isabelle_hot_tptp_file = generic_isabelle_tptp_file true
   299 
   300 
   301 (** Translator between TPTP(-like) file formats **)
   302 
   303 fun translate_tptp_file thy format_str file_name =
   304   let
   305     val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name
   306     val conj = make_conj ([], []) (map snd conjs)
   307 
   308     val (format, type_enc, lam_trans) =
   309       (case format_str of
   310         "FOF" => (FOF, "mono_guards??", liftingN)
   311       | "TF0" => (TFF Monomorphic, "mono_native", liftingN)
   312       | "TH0" => (THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN)
   313       | "DFG" => (DFG Monomorphic, "mono_native", liftingN)
   314       | _ => error ("Unknown format " ^ quote format_str ^
   315         " (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")"))
   316     val generate_info = false
   317     val uncurried_aliases = false
   318     val readable_names = true
   319     val presimp = true
   320     val facts =
   321       map (apfst (rpair (Global, Non_Rec_Def))) defs @
   322       map (apfst (rpair (Global, General))) nondefs
   323     val (atp_problem, _, _, _) =
   324       generate_atp_problem ctxt generate_info format Hypothesis (type_enc_of_string Strict type_enc)
   325         Translator
   326         lam_trans uncurried_aliases readable_names presimp [] conj facts
   327 
   328     val ord = effective_term_order ctxt spassN
   329     val ord_info = K []
   330     val lines = lines_of_atp_problem format ord ord_info atp_problem
   331   in
   332     List.app Output.physical_stdout lines
   333   end
   334 
   335 end;