1(*  Title:      HOL/TPTP/atp_problem_import.ML
2    Author:     Jasmin Blanchette, TU Muenchen
3    Copyright   2012
4
5Import TPTP problems as Isabelle terms or goals.
6*)
7
8signature ATP_PROBLEM_IMPORT =
9sig
10  val read_tptp_file : theory -> (string * term -> 'a) -> string ->
11    'a list * ('a list * 'a list) * Proof.context
12  val nitpick_tptp_file : theory -> int -> string -> unit
13  val refute_tptp_file : theory -> int -> string -> unit
14  val can_tac : Proof.context -> (Proof.context -> tactic) -> term -> bool
15  val SOLVE_TIMEOUT :  int -> string -> tactic -> tactic
16  val atp_tac : Proof.context -> int -> (string * string) list -> int -> term list -> string ->
17    int -> tactic
18  val smt_solver_tac : string -> Proof.context -> int -> tactic
19  val freeze_problem_consts : theory -> term -> term
20  val make_conj : term list * term list -> term list -> term
21  val sledgehammer_tptp_file : theory -> int -> string -> unit
22  val isabelle_tptp_file : theory -> int -> string -> unit
23  val isabelle_hot_tptp_file : theory -> int -> string -> unit
24  val translate_tptp_file : theory -> string -> string -> unit
25end;
26
27structure ATP_Problem_Import : ATP_PROBLEM_IMPORT =
28struct
29
30open ATP_Util
31open ATP_Problem
32open ATP_Proof
33open ATP_Problem_Generate
34open ATP_Systems
35
36val debug = false
37val overlord = false
38
39
40(** TPTP parsing **)
41
42fun exploded_absolute_path file_name =
43  Path.explode file_name
44  |> (fn path => path |> not (Path.is_absolute path) ? Path.append (Path.explode "$PWD"))
45
46fun read_tptp_file thy postproc file_name =
47  let
48    fun has_role role (_, role', _, _) = (role' = role)
49    fun get_prop f (name, _, P, _) = P |> f |> close_form |> pair name |> postproc
50
51    val path = exploded_absolute_path file_name
52    val ((_, _, problem), thy) =
53      TPTP_Interpret.interpret_file true [Path.dir path, Path.explode "$TPTP"] path [] [] thy
54    val (conjs, defs_and_nondefs) = problem
55      |> List.partition (has_role TPTP_Syntax.Role_Conjecture)
56      ||> List.partition (has_role TPTP_Syntax.Role_Definition)
57  in
58    (map (get_prop I) conjs,
59     apply2 (map (get_prop Logic.varify_global)) defs_and_nondefs,
60     Named_Target.theory_init thy)
61  end
62
63
64(** Nitpick **)
65
66fun aptrueprop f ((t0 as @{const Trueprop}) $ t1) = t0 $ f t1
67  | aptrueprop f t = f t
68
69fun is_legitimate_tptp_def (@{const Trueprop} $ t) = is_legitimate_tptp_def t
70  | is_legitimate_tptp_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
71    (is_Const t orelse is_Free t) andalso not (exists_subterm (curry (op =) t) u)
72  | is_legitimate_tptp_def _ = false
73
74fun nitpick_tptp_file thy timeout file_name =
75  let
76    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
77    val thy = Proof_Context.theory_of ctxt
78    val (defs, pseudo_defs) = defs
79      |> map (ATP_Util.abs_extensionalize_term ctxt #> aptrueprop (hol_open_form I))
80      |> List.partition (is_legitimate_tptp_def o perhaps (try HOLogic.dest_Trueprop)
81        o ATP_Util.unextensionalize_def)
82    val nondefs = pseudo_defs @ nondefs
83    val state = Proof.init ctxt
84    val params =
85      [("card", "1-100"),
86       ("box", "false"),
87       ("max_threads", "1"),
88       ("batch_size", "5"),
89       ("falsify", if null conjs then "false" else "true"),
90       ("verbose", "true"),
91       ("debug", if debug then "true" else "false"),
92       ("overlord", if overlord then "true" else "false"),
93       ("show_consts", "true"),
94       ("format", "1"),
95       ("max_potential", "0"),
96       ("timeout", string_of_int timeout),
97       ("tac_timeout", string_of_int ((timeout + 49) div 50))]
98      |> Nitpick_Commands.default_params thy
99    val i = 1
100    val n = 1
101    val step = 0
102    val subst = []
103  in
104    Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst defs nondefs
105      (case conjs of conj :: _ => conj | [] => @{prop True});
106    ()
107  end
108
109
110(** Refute **)
111
112fun refute_tptp_file thy timeout file_name =
113  let
114    fun print_szs_of_outcome falsify s =
115      "% SZS status " ^
116      (if s = "genuine" then
117         if falsify then "CounterSatisfiable" else "Satisfiable"
118       else
119         "GaveUp")
120      |> writeln
121    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
122    val params =
123      [("maxtime", string_of_int timeout),
124       ("maxvars", "100000")]
125  in
126    Refute.refute_term ctxt params (defs @ nondefs)
127      (case conjs of conj :: _ => conj | [] => @{prop True})
128    |> print_szs_of_outcome (not (null conjs))
129  end
130
131
132(** Sledgehammer and Isabelle (combination of provers) **)
133
134fun can_tac ctxt tactic conj =
135  can (Goal.prove_internal ctxt [] (Thm.cterm_of ctxt conj)) (fn [] => tactic ctxt)
136
137fun SOLVE_TIMEOUT seconds name tac st =
138  let
139    val _ = writeln ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
140    val result =
141      Timeout.apply (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
142      handle Timeout.TIMEOUT _ => NONE | ERROR _ => NONE
143  in
144    (case result of
145      NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
146    | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
147  end
148
149fun nitpick_finite_oracle_tac ctxt timeout i th =
150  let
151    fun is_safe (Type (@{type_name fun}, Ts)) = forall is_safe Ts
152      | is_safe @{typ prop} = true
153      | is_safe @{typ bool} = true
154      | is_safe _ = false
155
156    val conj = Thm.term_of (Thm.cprem_of th i)
157  in
158    if exists_type (not o is_safe) conj then
159      Seq.empty
160    else
161      let
162        val thy = Proof_Context.theory_of ctxt
163        val state = Proof.init ctxt
164        val params =
165          [("box", "false"),
166           ("max_threads", "1"),
167           ("verbose", "true"),
168           ("debug", if debug then "true" else "false"),
169           ("overlord", if overlord then "true" else "false"),
170           ("max_potential", "0"),
171           ("timeout", string_of_int timeout)]
172          |> Nitpick_Commands.default_params thy
173        val i = 1
174        val n = 1
175        val step = 0
176        val subst = []
177        val (outcome, _) =
178          Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst [] [] conj
179      in
180        if outcome = "none" then ALLGOALS (Skip_Proof.cheat_tac ctxt) th else Seq.empty
181      end
182  end
183
184fun atp_tac ctxt completeness override_params timeout assms prover =
185  let
186    val thy = Proof_Context.theory_of ctxt
187    val assm_ths0 = map (Skip_Proof.make_thm thy) assms
188    val ((assm_name, _), ctxt) = ctxt
189      |> Config.put Sledgehammer_Prover_ATP.atp_completish (if completeness > 0 then 3 else 0)
190      |> Local_Theory.note ((@{binding thms}, []), assm_ths0)
191
192    fun ref_of th = (Facts.named (Thm.derivation_name th), [])
193    val ref_of_assms = (Facts.named assm_name, [])
194  in
195    Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
196      ([("debug", if debug then "true" else "false"),
197        ("overlord", if overlord then "true" else "false"),
198        ("provers", prover),
199        ("timeout", string_of_int timeout)] @
200       (if completeness > 0 then
201          [("type_enc", if completeness = 1 then "mono_native" else "poly_tags")]
202        else
203          []) @
204       override_params)
205      {add = ref_of_assms :: map ref_of [ext, @{thm someI}], del = [], only = true} []
206  end
207
208fun sledgehammer_tac demo ctxt timeout assms i =
209  let
210    val frac = if demo then 16 else 12
211    fun slice mult completeness prover =
212      SOLVE_TIMEOUT (mult * timeout div frac)
213        (prover ^ (if completeness > 0 then "(" ^ string_of_int completeness ^ ")" else ""))
214        (atp_tac ctxt completeness [] (mult * timeout div frac) assms prover i)
215  in
216    slice 2 0 ATP_Proof.spassN
217    ORELSE slice 2 0 ATP_Proof.vampireN
218    ORELSE slice 2 0 ATP_Proof.eN
219    ORELSE slice 2 0 ATP_Proof.z3_tptpN
220    ORELSE slice 1 1 ATP_Proof.spassN
221    ORELSE slice 1 2 ATP_Proof.eN
222    ORELSE slice 1 1 ATP_Proof.vampireN
223    ORELSE slice 1 2 ATP_Proof.vampireN
224    ORELSE
225      (if demo then
226         slice 2 0 ATP_Proof.satallaxN
227         ORELSE slice 2 0 ATP_Proof.leo2N
228       else
229         no_tac)
230  end
231
232fun smt_solver_tac solver ctxt =
233  let
234    val ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver solver)
235  in SMT_Solver.smt_tac ctxt [] end
236
237fun auto_etc_tac ctxt timeout assms i =
238  SOLVE_TIMEOUT (timeout div 20) "nitpick" (nitpick_finite_oracle_tac ctxt (timeout div 20) i)
239  ORELSE SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac ctxt i)
240  ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
241  ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
242    (auto_tac ctxt THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) assms ATP_Proof.spassN))
243  ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i)
244  ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" ctxt i)
245  ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc4" (smt_solver_tac "cvc4" ctxt i)
246  ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i)
247  ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
248  ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac ctxt [] i)
249  ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac ctxt i)
250
251fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator
252
253(* Isabelle's standard automatic tactics ("auto", etc.) are more eager to
254   unfold "definitions" of free variables than of constants (cf. PUZ107^5). *)
255fun freeze_problem_consts thy =
256  let val is_problem_const = String.isPrefix (problem_const_prefix thy) in
257    map_aterms
258      (fn t as Const (s, T) => if is_problem_const s then Free (Long_Name.base_name s, T) else t
259        | t => t)
260  end
261
262fun make_conj (defs, nondefs) conjs =
263  Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => @{prop False})
264
265fun print_szs_of_success conjs success =
266  writeln ("% SZS status " ^
267    (if success then
268       if null conjs then "Unsatisfiable" else "Theorem"
269     else
270       "GaveUp"))
271
272fun sledgehammer_tptp_file thy timeout file_name =
273  let
274    val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name
275    val conj = make_conj ([], []) conjs
276    val assms = op @ assms
277  in
278    can_tac ctxt (fn ctxt => sledgehammer_tac true ctxt timeout assms 1) conj
279    |> print_szs_of_success conjs
280  end
281
282fun generic_isabelle_tptp_file demo thy timeout file_name =
283  let
284    val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name
285    val conj = make_conj ([], []) conjs
286    val full_conj = make_conj assms conjs
287    val assms = op @ assms
288    val (last_hope_atp, last_hope_completeness) =
289      if demo then (ATP_Proof.satallaxN, 0) else (ATP_Proof.vampireN, 2)
290  in
291    (can_tac ctxt (fn ctxt => auto_etc_tac ctxt (timeout div 2) assms 1) full_conj orelse
292     can_tac ctxt (fn ctxt => sledgehammer_tac demo ctxt (timeout div 2) assms 1) conj orelse
293     can_tac ctxt (fn ctxt => SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
294       (atp_tac ctxt last_hope_completeness [] timeout assms last_hope_atp 1)) full_conj)
295    |> print_szs_of_success conjs
296  end
297
298val isabelle_tptp_file = generic_isabelle_tptp_file false
299val isabelle_hot_tptp_file = generic_isabelle_tptp_file true
300
301
302(** Translator between TPTP(-like) file formats **)
303
304fun translate_tptp_file thy format_str file_name =
305  let
306    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name
307    val conj = make_conj ([], []) (map snd conjs)
308
309    val (format, type_enc, lam_trans) =
310      (case format_str of
311        "FOF" => (FOF, "mono_guards??", liftingN)
312      | "TF0" => (TFF Monomorphic, "mono_native", liftingN)
313      | "TH0" => (THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN)
314      | "DFG" => (DFG Monomorphic, "mono_native", liftingN)
315      | _ => error ("Unknown format " ^ quote format_str ^
316        " (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")"))
317    val generate_info = false
318    val uncurried_aliases = false
319    val readable_names = true
320    val presimp = true
321    val facts =
322      map (apfst (rpair (Global, Non_Rec_Def))) defs @
323      map (apfst (rpair (Global, General))) nondefs
324    val (atp_problem, _, _, _) =
325      generate_atp_problem ctxt generate_info format Hypothesis (type_enc_of_string Strict type_enc)
326        Translator
327        lam_trans uncurried_aliases readable_names presimp [] conj facts
328
329    val ord = effective_term_order ctxt spassN
330    val ord_info = K []
331    val lines = lines_of_atp_problem format ord ord_info atp_problem
332  in
333    List.app Output.physical_stdout lines
334  end
335
336end;
337