--- a/src/HOL/Tools/ATP/atp_problem.ML Sun Aug 22 08:30:19 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Sun Aug 22 09:43:10 2010 +0200
@@ -22,7 +22,7 @@
val timestamp : unit -> string
val is_tptp_variable : string -> bool
val strings_for_tptp_problem :
- (string * string problem_line list) list -> string list
+ bool -> (string * string problem_line list) list -> string list
val nice_tptp_problem :
bool -> ('a * (string * string) problem_line list) list
-> ('a * string problem_line list) list
@@ -48,6 +48,10 @@
val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
+fun string_for_kind Axiom = "axiom"
+ | string_for_kind Hypothesis = "hypothesis"
+ | string_for_kind Conjecture = "conjecture"
+
fun string_for_term (ATerm (s, [])) = s
| string_for_term (ATerm ("equal", ts)) =
space_implode " = " (map string_for_term ts)
@@ -74,20 +78,26 @@
(map string_for_formula phis) ^ ")"
| string_for_formula (AAtom tm) = string_for_term tm
-fun string_for_problem_line (Fof (ident, kind, phi)) =
- "fof(" ^ ident ^ ", " ^
- (case kind of
- Axiom => "axiom"
- | Hypothesis => "hypothesis"
- | Conjecture => "conjecture") ^
- ",\n (" ^ string_for_formula phi ^ ")).\n"
-fun strings_for_tptp_problem problem =
+fun string_for_problem_line use_conjecture_for_hypotheses
+ (Fof (ident, kind, phi)) =
+ let
+ val (kind, phi) =
+ if kind = Hypothesis andalso use_conjecture_for_hypotheses then
+ (Conjecture, AConn (ANot, [phi]))
+ else
+ (kind, phi)
+ in
+ "fof(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^
+ string_for_formula phi ^ ")).\n"
+ end
+fun strings_for_tptp_problem use_conjecture_for_hypotheses problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
\% " ^ timestamp () ^ "\n" ::
maps (fn (_, []) => []
| (heading, lines) =>
"\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" ::
- map string_for_problem_line lines) problem
+ map (string_for_problem_line use_conjecture_for_hypotheses) lines)
+ problem
fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))