author | wenzelm |
Sun, 05 Oct 2014 22:18:40 +0200 | |
changeset 58550 | f65911a725ba |
parent 57812 | 8dc9dc241973 |
child 58843 | 521cea5fa777 |
permissions | -rw-r--r-- |
55208 | 1 |
(* Title: HOL/TPTP/atp_problem_import.ML |
46324 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
Copyright 2012 |
|
4 |
||
5 |
Import TPTP problems as Isabelle terms or goals. |
|
6 |
*) |
|
7 |
||
8 |
signature ATP_PROBLEM_IMPORT = |
|
9 |
sig |
|
54434 | 10 |
val read_tptp_file : theory -> (string * term -> 'a) -> string -> |
11 |
'a list * ('a list * 'a list) * Proof.context |
|
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
12 |
val nitpick_tptp_file : theory -> int -> string -> unit |
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
13 |
val refute_tptp_file : theory -> int -> string -> unit |
47845 | 14 |
val can_tac : Proof.context -> tactic -> term -> bool |
15 |
val SOLVE_TIMEOUT : int -> string -> tactic -> tactic |
|
57812
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
16 |
val atp_tac : Proof.context -> int -> (string * string) list -> int -> term list -> string -> |
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
17 |
int -> tactic |
47845 | 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 |
|
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
21 |
val sledgehammer_tptp_file : theory -> int -> string -> unit |
48083
a4148c95134d
renamed TPTP commands to agree with Sutcliffe's terminology
blanchet
parents:
48082
diff
changeset
|
22 |
val isabelle_tptp_file : theory -> int -> string -> unit |
a4148c95134d
renamed TPTP commands to agree with Sutcliffe's terminology
blanchet
parents:
48082
diff
changeset
|
23 |
val isabelle_hot_tptp_file : theory -> int -> string -> unit |
54472
073f041d83ae
send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life
blanchet
parents:
54434
diff
changeset
|
24 |
val translate_tptp_file : theory -> string -> string -> unit |
46324 | 25 |
end; |
26 |
||
27 |
structure ATP_Problem_Import : ATP_PROBLEM_IMPORT = |
|
28 |
struct |
|
29 |
||
47643
e33c2be488fe
reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents:
47565
diff
changeset
|
30 |
open ATP_Util |
e33c2be488fe
reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents:
47565
diff
changeset
|
31 |
open ATP_Problem |
e33c2be488fe
reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents:
47565
diff
changeset
|
32 |
open ATP_Proof |
54434 | 33 |
open ATP_Problem_Generate |
34 |
open ATP_Systems |
|
47643
e33c2be488fe
reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents:
47565
diff
changeset
|
35 |
|
47776
024cf0f7fb6d
further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
blanchet
parents:
47771
diff
changeset
|
36 |
val debug = false |
024cf0f7fb6d
further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
blanchet
parents:
47771
diff
changeset
|
37 |
val overlord = false |
024cf0f7fb6d
further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
blanchet
parents:
47771
diff
changeset
|
38 |
|
47643
e33c2be488fe
reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents:
47565
diff
changeset
|
39 |
|
47771 | 40 |
(** TPTP parsing **) |
47643
e33c2be488fe
reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents:
47565
diff
changeset
|
41 |
|
54434 | 42 |
fun 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 |
||
47785 | 46 |
fun read_tptp_file thy postproc file_name = |
47644 | 47 |
let |
47718
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
48 |
fun has_role role (_, role', _, _) = (role' = role) |
57809 | 49 |
fun get_prop f (name, _, P, _) = P |> f |> close_form |> pair name |> postproc |
50 |
||
54434 | 51 |
val path = exploded_absolute_path file_name |
47714 | 52 |
val ((_, _, problem), thy) = |
57809 | 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) |
|
47644 | 57 |
in |
57809 | 58 |
(map (get_prop I) conjs, |
59 |
pairself (map (get_prop Logic.varify_global)) defs_and_nondefs, |
|
57812
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
60 |
Named_Target.theory_init thy) |
47557
32f35b3d9e42
started integrating Nik's parser into TPTP command-line tools
blanchet
parents:
46325
diff
changeset
|
61 |
end |
46325 | 62 |
|
47771 | 63 |
|
57547
677b07d777c3
don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
blanchet
parents:
57268
diff
changeset
|
64 |
(** Nitpick **) |
46324 | 65 |
|
47718
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
66 |
fun aptrueprop f ((t0 as @{const Trueprop}) $ t1) = t0 $ f t1 |
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
67 |
| aptrueprop f t = f t |
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
68 |
|
57547
677b07d777c3
don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
blanchet
parents:
57268
diff
changeset
|
69 |
fun is_legitimate_tptp_def (@{const Trueprop} $ t) = is_legitimate_tptp_def t |
677b07d777c3
don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
blanchet
parents:
57268
diff
changeset
|
70 |
| is_legitimate_tptp_def (Const (@{const_name HOL.eq}, _) $ t $ u) = |
677b07d777c3
don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
blanchet
parents:
57268
diff
changeset
|
71 |
(is_Const t orelse is_Free t) andalso not (exists_subterm (curry (op =) t) u) |
677b07d777c3
don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
blanchet
parents:
57268
diff
changeset
|
72 |
| is_legitimate_tptp_def _ = false |
677b07d777c3
don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
blanchet
parents:
57268
diff
changeset
|
73 |
|
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
74 |
fun nitpick_tptp_file thy timeout file_name = |
46325 | 75 |
let |
54434 | 76 |
val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name |
47771 | 77 |
val thy = Proof_Context.theory_of ctxt |
57809 | 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) |
|
47991
3eb598b044ad
make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
blanchet
parents:
47957
diff
changeset
|
82 |
val nondefs = pseudo_defs @ nondefs |
47714 | 83 |
val state = Proof.init ctxt |
46325 | 84 |
val params = |
47557
32f35b3d9e42
started integrating Nik's parser into TPTP command-line tools
blanchet
parents:
46325
diff
changeset
|
85 |
[("card", "1\<emdash>100"), |
46325 | 86 |
("box", "false"), |
87 |
("max_threads", "1"), |
|
47791 | 88 |
("batch_size", "5"), |
47718
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
89 |
("falsify", if null conjs then "false" else "true"), |
46325 | 90 |
("verbose", "true"), |
47776
024cf0f7fb6d
further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
blanchet
parents:
47771
diff
changeset
|
91 |
("debug", if debug then "true" else "false"), |
024cf0f7fb6d
further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
blanchet
parents:
47771
diff
changeset
|
92 |
("overlord", if overlord then "true" else "false"), |
46325 | 93 |
("show_consts", "true"), |
47755 | 94 |
("format", "1"), |
46325 | 95 |
("max_potential", "0"), |
47718
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
96 |
("timeout", string_of_int timeout), |
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
97 |
("tac_timeout", string_of_int ((timeout + 49) div 50))] |
55199 | 98 |
|> Nitpick_Commands.default_params thy |
46325 | 99 |
val i = 1 |
100 |
val n = 1 |
|
101 |
val step = 0 |
|
102 |
val subst = [] |
|
103 |
in |
|
57809 | 104 |
Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst defs nondefs |
105 |
(case conjs of conj :: _ => conj | [] => @{prop True}); |
|
47718
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
106 |
() |
46325 | 107 |
end |
46324 | 108 |
|
109 |
||
110 |
(** Refute **) |
|
111 |
||
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
112 |
fun refute_tptp_file thy timeout file_name = |
46325 | 113 |
let |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51717
diff
changeset
|
114 |
fun print_szs_of_outcome falsify s = |
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
115 |
"% SZS status " ^ |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
116 |
(if s = "genuine" then |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
117 |
if falsify then "CounterSatisfiable" else "Satisfiable" |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
118 |
else |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
119 |
"Unknown") |
47788 | 120 |
|> Output.urgent_message |
54434 | 121 |
val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name |
46325 | 122 |
val params = |
47714 | 123 |
[("maxtime", string_of_int timeout), |
124 |
("maxvars", "100000")] |
|
46325 | 125 |
in |
47718
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
126 |
Refute.refute_term ctxt params (defs @ nondefs) |
57809 | 127 |
(case conjs of conj :: _ => conj | [] => @{prop True}) |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51717
diff
changeset
|
128 |
|> print_szs_of_outcome (not (null conjs)) |
46325 | 129 |
end |
46324 | 130 |
|
131 |
||
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
132 |
(** Sledgehammer and Isabelle (combination of provers) **) |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
133 |
|
47785 | 134 |
fun can_tac ctxt tactic conj = can (Goal.prove ctxt [] [] conj) (K tactic) |
47771 | 135 |
|
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
136 |
fun SOLVE_TIMEOUT seconds name tac st = |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
137 |
let |
57809 | 138 |
val _ = Output.urgent_message ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s") |
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
139 |
val result = |
57809 | 140 |
TimeLimit.timeLimit (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) () |
141 |
handle |
|
142 |
TimeLimit.TimeOut => NONE |
|
143 |
| ERROR _ => NONE |
|
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
144 |
in |
57809 | 145 |
(case result of |
47788 | 146 |
NONE => (Output.urgent_message ("FAILURE: " ^ name); Seq.empty) |
57809 | 147 |
| SOME st' => (Output.urgent_message ("SUCCESS: " ^ name); Seq.single st')) |
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
148 |
end |
46324 | 149 |
|
47812 | 150 |
fun nitpick_finite_oracle_tac ctxt timeout i th = |
151 |
let |
|
152 |
fun is_safe (Type (@{type_name fun}, Ts)) = forall is_safe Ts |
|
153 |
| is_safe @{typ prop} = true |
|
154 |
| is_safe @{typ bool} = true |
|
155 |
| is_safe _ = false |
|
57809 | 156 |
|
47812 | 157 |
val conj = Thm.term_of (Thm.cprem_of th i) |
158 |
in |
|
159 |
if exists_type (not o is_safe) conj then |
|
160 |
Seq.empty |
|
161 |
else |
|
162 |
let |
|
163 |
val thy = Proof_Context.theory_of ctxt |
|
164 |
val state = Proof.init ctxt |
|
165 |
val params = |
|
166 |
[("box", "false"), |
|
167 |
("max_threads", "1"), |
|
168 |
("verbose", "true"), |
|
169 |
("debug", if debug then "true" else "false"), |
|
170 |
("overlord", if overlord then "true" else "false"), |
|
171 |
("max_potential", "0"), |
|
172 |
("timeout", string_of_int timeout)] |
|
55199 | 173 |
|> Nitpick_Commands.default_params thy |
47812 | 174 |
val i = 1 |
175 |
val n = 1 |
|
176 |
val step = 0 |
|
177 |
val subst = [] |
|
178 |
val (outcome, _) = |
|
57809 | 179 |
Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst [] [] conj |
180 |
in |
|
181 |
if outcome = "none" then ALLGOALS Skip_Proof.cheat_tac th else Seq.empty |
|
182 |
end |
|
47812 | 183 |
end |
184 |
||
57812
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
185 |
fun atp_tac ctxt completeness override_params timeout assms prover = |
47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
47845
diff
changeset
|
186 |
let |
57812
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
187 |
val thy = Proof_Context.theory_of ctxt |
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
188 |
val assm_ths0 = map (Skip_Proof.make_thm thy) assms |
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
189 |
val ((assm_name, _), ctxt) = ctxt |
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
190 |
|> Config.put Sledgehammer_Prover_ATP.atp_completish (completeness > 0) |
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
191 |
|> Local_Theory.note ((@{binding thms}, []), assm_ths0) |
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
192 |
|
52071 | 193 |
fun ref_of th = (Facts.named (Thm.derivation_name th), []) |
57812
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
194 |
val ref_of_assms = (Facts.named assm_name, []) |
47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
47845
diff
changeset
|
195 |
in |
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
47845
diff
changeset
|
196 |
Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt |
57809 | 197 |
([("debug", if debug then "true" else "false"), |
198 |
("overlord", if overlord then "true" else "false"), |
|
199 |
("provers", prover), |
|
200 |
("timeout", string_of_int timeout)] @ |
|
201 |
(if completeness > 0 then |
|
202 |
[("type_enc", if completeness = 1 then "mono_native" else "poly_tags")] |
|
203 |
else |
|
204 |
[]) @ |
|
205 |
override_params) |
|
57812
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
206 |
{add = ref_of_assms :: map ref_of [ext, @{thm someI}], del = [], only = true} [] |
47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
47845
diff
changeset
|
207 |
end |
47765 | 208 |
|
57812
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
209 |
fun sledgehammer_tac demo ctxt timeout assms i = |
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
210 |
let |
47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
47845
diff
changeset
|
211 |
val frac = if demo then 16 else 12 |
48143 | 212 |
fun slice mult completeness prover = |
47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
47845
diff
changeset
|
213 |
SOLVE_TIMEOUT (mult * timeout div frac) |
57809 | 214 |
(prover ^ (if completeness > 0 then "(" ^ string_of_int completeness ^ ")" else "")) |
57812
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
215 |
(atp_tac ctxt completeness [] (mult * timeout div frac) assms prover i) |
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
216 |
in |
57154 | 217 |
slice 2 0 ATP_Proof.spassN |
218 |
ORELSE slice 2 0 ATP_Proof.vampireN |
|
219 |
ORELSE slice 2 0 ATP_Proof.eN |
|
220 |
ORELSE slice 2 0 ATP_Proof.z3_tptpN |
|
221 |
ORELSE slice 1 1 ATP_Proof.spassN |
|
222 |
ORELSE slice 1 2 ATP_Proof.eN |
|
223 |
ORELSE slice 1 1 ATP_Proof.vampireN |
|
224 |
ORELSE slice 1 2 ATP_Proof.vampireN |
|
47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
47845
diff
changeset
|
225 |
ORELSE |
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
47845
diff
changeset
|
226 |
(if demo then |
57154 | 227 |
slice 2 0 ATP_Proof.satallaxN |
228 |
ORELSE slice 2 0 ATP_Proof.leo2N |
|
47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
47845
diff
changeset
|
229 |
else |
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
47845
diff
changeset
|
230 |
no_tac) |
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
231 |
end |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
232 |
|
47832 | 233 |
fun smt_solver_tac solver ctxt = |
234 |
let |
|
235 |
val ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver solver) |
|
236 |
in SMT_Solver.smt_tac ctxt [] end |
|
237 |
||
57812
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
238 |
fun auto_etc_tac ctxt timeout assms i = |
57809 | 239 |
SOLVE_TIMEOUT (timeout div 20) "nitpick" (nitpick_finite_oracle_tac ctxt (timeout div 20) i) |
240 |
ORELSE SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac ctxt i) |
|
47788 | 241 |
ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i) |
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
242 |
ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass" |
57812
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
243 |
(auto_tac ctxt THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) assms ATP_Proof.spassN)) |
47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
47845
diff
changeset
|
244 |
ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i) |
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
47845
diff
changeset
|
245 |
ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" ctxt i) |
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
47845
diff
changeset
|
246 |
ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc3" (smt_solver_tac "cvc3" ctxt i) |
47812 | 247 |
ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i) |
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
248 |
ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i) |
47832 | 249 |
ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac ctxt [] i) |
47812 | 250 |
ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac ctxt i) |
47771 | 251 |
|
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
252 |
fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator |
47785 | 253 |
|
254 |
(* Isabelle's standard automatic tactics ("auto", etc.) are more eager to |
|
255 |
unfold "definitions" of free variables than of constants (cf. PUZ107^5). *) |
|
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
256 |
fun freeze_problem_consts thy = |
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
257 |
let val is_problem_const = String.isPrefix (problem_const_prefix thy) in |
57809 | 258 |
map_aterms |
259 |
(fn t as Const (s, T) => if is_problem_const s then Free (Long_Name.base_name s, T) else t |
|
260 |
| t => t) |
|
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
261 |
end |
47785 | 262 |
|
47776
024cf0f7fb6d
further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
blanchet
parents:
47771
diff
changeset
|
263 |
fun make_conj (defs, nondefs) conjs = |
57809 | 264 |
Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => @{prop False}) |
47771 | 265 |
|
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51717
diff
changeset
|
266 |
fun print_szs_of_success conjs success = |
47788 | 267 |
Output.urgent_message ("% SZS status " ^ |
57809 | 268 |
(if success then |
269 |
if null conjs then "Unsatisfiable" else "Theorem" |
|
270 |
else |
|
271 |
"Unknown")) |
|
47765 | 272 |
|
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
273 |
fun sledgehammer_tptp_file thy timeout file_name = |
47771 | 274 |
let |
57809 | 275 |
val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name |
57812
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
276 |
val conj = make_conj ([], []) conjs |
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
277 |
val assms = op @ assms |
47771 | 278 |
in |
57812
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
279 |
can_tac ctxt (sledgehammer_tac true ctxt timeout assms 1) conj |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51717
diff
changeset
|
280 |
|> print_szs_of_success conjs |
47771 | 281 |
end |
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
282 |
|
48083
a4148c95134d
renamed TPTP commands to agree with Sutcliffe's terminology
blanchet
parents:
48082
diff
changeset
|
283 |
fun generic_isabelle_tptp_file demo thy timeout file_name = |
47771 | 284 |
let |
57809 | 285 |
val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name |
57812
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
286 |
val conj = make_conj ([], []) conjs |
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
287 |
val full_conj = make_conj assms conjs |
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
288 |
val assms = op @ assms |
48143 | 289 |
val (last_hope_atp, last_hope_completeness) = |
57154 | 290 |
if demo then (ATP_Proof.satallaxN, 0) else (ATP_Proof.vampireN, 2) |
47771 | 291 |
in |
57812
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
292 |
(can_tac ctxt (auto_etc_tac ctxt (timeout div 2) assms 1) full_conj orelse |
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
293 |
can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) assms 1) conj orelse |
48082 | 294 |
can_tac ctxt (SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)") |
57812
8dc9dc241973
make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents:
57809
diff
changeset
|
295 |
(atp_tac ctxt last_hope_completeness [] timeout assms last_hope_atp 1)) full_conj) |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51717
diff
changeset
|
296 |
|> print_szs_of_success conjs |
47771 | 297 |
end |
46324 | 298 |
|
48083
a4148c95134d
renamed TPTP commands to agree with Sutcliffe's terminology
blanchet
parents:
48082
diff
changeset
|
299 |
val isabelle_tptp_file = generic_isabelle_tptp_file false |
a4148c95134d
renamed TPTP commands to agree with Sutcliffe's terminology
blanchet
parents:
48082
diff
changeset
|
300 |
val isabelle_hot_tptp_file = generic_isabelle_tptp_file true |
47832 | 301 |
|
302 |
||
46324 | 303 |
(** Translator between TPTP(-like) file formats **) |
304 |
||
54472
073f041d83ae
send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life
blanchet
parents:
54434
diff
changeset
|
305 |
fun translate_tptp_file thy format_str file_name = |
54434 | 306 |
let |
54472
073f041d83ae
send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life
blanchet
parents:
54434
diff
changeset
|
307 |
val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name |
54434 | 308 |
val conj = make_conj ([], []) (map snd conjs) |
309 |
||
310 |
val (format, type_enc, lam_trans) = |
|
311 |
(case format_str of |
|
312 |
"FOF" => (FOF, "mono_guards??", liftingN) |
|
54547
c999e2533487
renamed TFF0/THF0 to three-letter acronyms, in keeping with new TPTP policy
blanchet
parents:
54472
diff
changeset
|
313 |
| "TF0" => (TFF Monomorphic, "mono_native", liftingN) |
c999e2533487
renamed TFF0/THF0 to three-letter acronyms, in keeping with new TPTP policy
blanchet
parents:
54472
diff
changeset
|
314 |
| "TH0" => (THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN) |
54434 | 315 |
| "DFG" => (DFG Monomorphic, "mono_native", liftingN) |
316 |
| _ => error ("Unknown format " ^ quote format_str ^ |
|
54547
c999e2533487
renamed TFF0/THF0 to three-letter acronyms, in keeping with new TPTP policy
blanchet
parents:
54472
diff
changeset
|
317 |
" (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")")) |
54434 | 318 |
val uncurried_aliases = false |
319 |
val readable_names = true |
|
320 |
val presimp = true |
|
57809 | 321 |
val facts = |
322 |
map (apfst (rpair (Global, Non_Rec_Def))) defs @ |
|
54434 | 323 |
map (apfst (rpair (Global, General))) nondefs |
57268 | 324 |
val (atp_problem, _, _, _) = |
325 |
generate_atp_problem ctxt format Hypothesis (type_enc_of_string Strict type_enc) Translator |
|
54434 | 326 |
lam_trans uncurried_aliases readable_names presimp [] conj facts |
327 |
||
328 |
val ord = effective_term_order ctxt spassN |
|
329 |
val ord_info = K [] |
|
330 |
val lines = lines_of_atp_problem format ord ord_info atp_problem |
|
331 |
in |
|
54472
073f041d83ae
send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life
blanchet
parents:
54434
diff
changeset
|
332 |
List.app Output.physical_stdout lines |
54434 | 333 |
end |
46324 | 334 |
|
335 |
end; |