(*  Title:      HOL/TPTP/atp_problem_import.ML

     Author:     Jasmin Blanchette, TU Muenchen

     Copyright   2012

 Import TPTP problems as Isabelle terms or goals.

 *)

 signature ATP_PROBLEM_IMPORT =

 sig

   val isabelle_tptp_file : string -> unit

   val nitpick_tptp_file : string -> unit

   val refute_tptp_file : string -> unit

   val sledgehammer_tptp_file : string -> unit

   val translate_tptp_file : string -> string -> string -> unit

 end;

 structure ATP_Problem_Import : ATP_PROBLEM_IMPORT =

 struct

 (** TPTP parsing **)

 (* cf. "close_form" in "refute.ML" *)

 fun close_form t =

   fold (fn ((s, i), T) => fn t' =>

            Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t')))

        (Term.add_vars t []) t

 fun mk_meta_not P = Logic.mk_implies (P, @{prop False})

 fun get_tptp_formula (_, role, P, _) =

   P |> Logic.varify_global |> close_form

     |> role = TPTP_Syntax.Role_Conjecture ? mk_meta_not

 fun read_tptp_file thy file_name =

   let

     val path = Path.explode file_name

     val problem =

       TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy

       |> fst |> #3

   in

     (exists (fn (_, role, _, _) => role = TPTP_Syntax.Role_Conjecture) problem,

      map get_tptp_formula problem)

   end

 (** Isabelle (combination of provers) **)

 fun isabelle_tptp_file file_name = ()

 (** Nitpick (alias Nitrox) **)

 fun nitpick_tptp_file file_name =

   let

     val (falsify, ts) = read_tptp_file @{theory} file_name

     val state = Proof.init @{context}

     val params =

       [("card", "1\<emdash>100"),

        ("box", "false"),

        ("sat_solver", "smart"),

        ("max_threads", "1"),

        ("batch_size", "10"),

        ("falsify", if falsify then "true" else "false"),

        (* ("debug", "true"), *)

        ("verbose", "true"),

        (* ("overlord", "true"), *)

        ("show_consts", "true"),

        ("format", "1000"),

        ("max_potential", "0"),

        ("timeout", "none"),

        ("expect", Nitpick.genuineN)]

       |> Nitpick_Isar.default_params @{theory}

     val i = 1

     val n = 1

     val step = 0

     val subst = []

   in

     Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst ts

         (if falsify then @{prop False} else @{prop True}); ()

   end

 (** Refute **)

 fun print_szs_from_outcome falsify s =

   "% SZS status " ^

   (if s = "genuine" then

      if falsify then "CounterSatisfiable" else "Satisfiable"

    else

      "Unknown")

   |> writeln

 fun refute_tptp_file file_name =

   let

     val (falsify, ts) = read_tptp_file @{theory} file_name

     val params =

       [("maxtime", "10000"),

        ("assms", "true"),

        ("expect", Nitpick.genuineN)]

   in

     Refute.refute_term @{context} params ts @{prop False}

     |> print_szs_from_outcome falsify

   end

 (** Sledgehammer **)

 fun sledgehammer_tptp_file file_name = ()

 (** Translator between TPTP(-like) file formats **)

 fun translate_tptp_file format in_file_name out_file_name = ()

 end;