--- 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;
--- 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;"