1.1 --- a/src/HOL/TPTP/ATP_Problem_Import.thy	Wed Apr 18 21:28:49 2012 +0200
     1.2 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Wed Apr 18 22:16:05 2012 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* ATP Problem Importer *}
     1.5  
     1.6  theory ATP_Problem_Import
     1.7 -imports Complex_Main
     1.8 +imports Complex_Main TPTP_Interpret
     1.9  uses ("atp_problem_import.ML")
    1.10  begin
    1.11  

     2.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Wed Apr 18 21:28:49 2012 +0200
     2.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Wed Apr 18 22:16:05 2012 +0200
     2.3 @@ -22,9 +22,10 @@
     2.4  open ATP_Proof
     2.5  
     2.6  
     2.7 -(** General TPTP parsing **)
     2.8 +(** Crude TPTP CNF and FOF parsing **)
     2.9  
    2.10  exception SYNTAX of string
    2.11 +exception THF of unit
    2.12  
    2.13  val tptp_explode = raw_explode o strip_spaces_except_between_idents
    2.14  
    2.15 @@ -53,7 +54,8 @@
    2.16     || Scan.this_string "hypothesis" || Scan.this_string "conjecture"
    2.17     || Scan.this_string "negated_conjecture") --| $$ "," -- parse_formula
    2.18        --| $$ ")" --| $$ "."
    2.19 -  >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
    2.20 +    >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
    2.21 +  || Scan.this_string "thf" >> (fn _ => raise THF ())
    2.22  
    2.23  val parse_problem =
    2.24    Scan.repeat parse_include
    2.25 @@ -104,11 +106,22 @@
    2.26  
    2.27  fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t
    2.28  
    2.29 -fun read_tptp_file file_name =
    2.30 -  case parse_tptp_problem (File.read (Path.explode file_name)) of
    2.31 -    (_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
    2.32 -  | (phis, []) =>
    2.33 -    map (HOLogic.mk_Trueprop o close_hol_prop o hol_prop_from_formula) phis
    2.34 +fun mk_meta_not P = Logic.mk_implies (P, @{prop False})
    2.35 +
    2.36 +fun get_tptp_formula (_, role, _, P, _) =
    2.37 +  P |> role = TPTP_Syntax.Role_Conjecture ? mk_meta_not
    2.38 +
    2.39 +fun read_tptp_file thy file_name =
    2.40 +  let val path = Path.explode file_name in
    2.41 +    (case parse_tptp_problem (File.read path) of
    2.42 +       (_, s :: ss) =>
    2.43 +       raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
    2.44 +     | (phis, []) =>
    2.45 +       map (HOLogic.mk_Trueprop o close_hol_prop o hol_prop_from_formula) phis)
    2.46 +    handle THF () =>
    2.47 +    TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy
    2.48 +    |> fst |> #3 |> map get_tptp_formula
    2.49 +  end
    2.50  
    2.51  fun print_szs_from_outcome s =
    2.52    "% SZS status " ^
    2.53 @@ -127,11 +140,10 @@
    2.54  
    2.55  fun nitpick_tptp_file file_name =
    2.56    let
    2.57 -    val ts = read_tptp_file file_name
    2.58 +    val ts = read_tptp_file @{theory} file_name
    2.59      val state = Proof.init @{context}
    2.60      val params =
    2.61 -      [("card iota", "1\<emdash>100"),
    2.62 -       ("card", "1\<emdash>8"),
    2.63 +      [("card", "1\<emdash>100"),
    2.64         ("box", "false"),
    2.65         ("sat_solver", "smart"),
    2.66         ("max_threads", "1"),
    2.67 @@ -160,7 +172,7 @@
    2.68  
    2.69  fun refute_tptp_file file_name =
    2.70    let
    2.71 -    val ts = read_tptp_file file_name
    2.72 +    val ts = read_tptp_file @{theory} file_name
    2.73      val params =
    2.74        [("maxtime", "10000"),
    2.75         ("assms", "true"),