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