# HG changeset patch
# User blanchet
# Date 1327336832 -3600
# Node ID b170ab46513a0f2a4414529e19a1edb5eeb77b4d
# Parent  e4bccf5ec61eb9efe5ce8b4a40b545b5f55d1c6b
implemented "tptp_refute" tool

diff -r e4bccf5ec61e -r b170ab46513a src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Mon Jan 23 17:40:32 2012 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Mon Jan 23 17:40:32 2012 +0100
@@ -11,7 +11,7 @@
   val nitpick_tptp_file : string -> unit
   val refute_tptp_file : string -> unit
   val sledgehammer_tptp_file : string -> unit
-  val translate_tptp_file : string -> unit
+  val translate_tptp_file : string -> string -> string -> unit
 end;
 
 structure ATP_Problem_Import : ATP_PROBLEM_IMPORT =
@@ -20,9 +20,6 @@
 open ATP_Util
 open ATP_Problem
 open ATP_Proof
-open Nitpick_Util
-open Nitpick
-open Nitpick_Isar
 
 
 (** General TPTP parsing **)
@@ -69,7 +66,7 @@
   o tptp_explode
 
 val iota_T = @{typ iota}
-val quant_T = (iota_T --> bool_T) --> bool_T
+val quant_T = @{typ "(iota => bool) => bool"}
 
 fun is_variable s = Char.isUpper (String.sub (s, 0))
 
@@ -101,12 +98,25 @@
         | AIff => HOLogic.mk_eq
         | ANot => raise Fail "binary \"ANot\"")
   | AConn _ => raise Fail "malformed AConn"
-  | AAtom u => hol_term_from_fo_term bool_T u
+  | AAtom u => hol_term_from_fo_term @{typ bool} u
 
 fun mk_all x t = Const (@{const_name All}, quant_T) $ lambda x t
 
 fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t
 
+fun read_tptp_file file_name =
+  case parse_tptp_problem (File.read (Path.explode file_name)) of
+    (_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
+  | (phis, []) =>
+    map (HOLogic.mk_Trueprop o close_hol_prop o hol_prop_from_formula) phis
+
+fun print_szs_from_outcome s =
+  "% SZS status " ^
+  (if s = Nitpick.genuineN then
+     "CounterSatisfiable"
+   else
+     "Unknown")
+  |> writeln
 
 (** Isabelle (combination of provers) **)
 
@@ -116,46 +126,49 @@
 (** Nitpick (alias Nitrox) **)
 
 fun nitpick_tptp_file file_name =
-  case parse_tptp_problem (File.read (Path.explode file_name)) of
-    (_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
-  | (phis, []) =>
-    let
-      val ts = map (HOLogic.mk_Trueprop o close_hol_prop
-                    o hol_prop_from_formula) phis
-(*
-      val _ = warning (PolyML.makestring phis)
-      val _ = app (warning o Syntax.string_of_term @{context}) ts
-*)
-      val state = Proof.init @{context}
-      val params =
-        [("card iota", "1\<emdash>100"),
-         ("card", "1\<emdash>8"),
-         ("box", "false"),
-         ("sat_solver", "smart"),
-         ("max_threads", "1"),
-         ("batch_size", "10"),
-         (* ("debug", "true"), *)
-         ("verbose", "true"),
-         (* ("overlord", "true"), *)
-         ("show_consts", "true"),
-         ("format", "1000"),
-         ("max_potential", "0"),
-         ("timeout", "none"),
-         ("expect", genuineN)]
-        |> default_params @{theory}
-      val i = 1
-      val n = 1
-      val step = 0
-      val subst = []
-    in
-      pick_nits_in_term state params Normal i n step subst ts @{prop False};
-      ()
-    end
+  let
+    val ts = read_tptp_file file_name
+    val state = Proof.init @{context}
+    val params =
+      [("card iota", "1\<emdash>100"),
+       ("card", "1\<emdash>8"),
+       ("box", "false"),
+       ("sat_solver", "smart"),
+       ("max_threads", "1"),
+       ("batch_size", "10"),
+       (* ("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.Normal i n step subst ts
+        @{prop False}
+    |> fst |> print_szs_from_outcome
+  end
 
 
 (** Refute **)
 
-fun refute_tptp_file file_name = ()
+fun refute_tptp_file file_name =
+  let
+    val ts = read_tptp_file file_name
+    val params =
+      [("maxtime", "10000"),
+       ("assms", "true"),
+       ("expect", Nitpick.genuineN)]
+  in
+    Refute.refute_term @{context} params ts @{prop False}
+    |> print_szs_from_outcome
+  end
 
 
 (** Sledgehammer **)
@@ -165,6 +178,6 @@
 
 (** Translator between TPTP(-like) file formats **)
 
-fun translate_tptp_file file_name = ()
+fun translate_tptp_file format in_file_name out_file_name = ()
 
 end;
diff -r e4bccf5ec61e -r b170ab46513a src/HOL/TPTP/lib/Tools/tptp_translate
--- a/src/HOL/TPTP/lib/Tools/tptp_translate	Mon Jan 23 17:40:32 2012 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_translate	Mon Jan 23 17:40:32 2012 +0100
@@ -9,21 +9,20 @@
 
 function usage() {
   echo
-  echo "Usage: isabelle $PRG FORMAT FILE"
+  echo "Usage: isabelle $PRG FORMAT IN_FILE OUT_FILE"
   echo
-  echo "  Translates TPTP file to specified TPTP format (\"CNF\", \"FOF\", \"TFF0\", \"TFF1\", or \"THF0\")."
+  echo "  Translates TPTP input file to specified TPTP format (\"CNF\", \"FOF\", \"TFF0\", \"TFF1\", or \"THF0\")."
   echo
   exit 1
 }
 
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
+[ "$#" -ne 3 -o "$1" = "-?" ] && usage
 
 SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
 
-for FILE in "$@"
-do
-  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.translate_tptp_file \"$FILE\" *} end;" \
-    > /tmp/$SCRATCH.thy
-  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
-done
+args=("$@")
+
+echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
+ML {* ATP_Problem_Import.translate_tptp_file \"${args[0]}\" \"${args[1]}\" \"${args[2]}\" *} end;" \
+  > /tmp/$SCRATCH.thy
+"$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"