author | blanchet |
Fri, 27 Apr 2012 22:36:27 +0200 | |
changeset 47812 | bb477988edb4 |
parent 47811 | 1e8eb643540d |
child 47832 | 7df66b448c4a |
permissions | -rw-r--r-- |
46324 | 1 |
(* Title: HOL/TPTP/atp_problem_import.ML |
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 |
|
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
10 |
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
|
11 |
val refute_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
|
12 |
val sledgehammer_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 isabelle_tptp_file : theory -> int -> string -> unit |
46325 | 14 |
val translate_tptp_file : string -> string -> string -> unit |
46324 | 15 |
end; |
16 |
||
17 |
structure ATP_Problem_Import : ATP_PROBLEM_IMPORT = |
|
18 |
struct |
|
19 |
||
47643
e33c2be488fe
reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents:
47565
diff
changeset
|
20 |
open ATP_Util |
e33c2be488fe
reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents:
47565
diff
changeset
|
21 |
open ATP_Problem |
e33c2be488fe
reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents:
47565
diff
changeset
|
22 |
open ATP_Proof |
e33c2be488fe
reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents:
47565
diff
changeset
|
23 |
|
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
|
24 |
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
|
25 |
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
|
26 |
|
47643
e33c2be488fe
reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents:
47565
diff
changeset
|
27 |
|
47771 | 28 |
(** TPTP parsing **) |
47643
e33c2be488fe
reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents:
47565
diff
changeset
|
29 |
|
47565
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
30 |
(* cf. "close_form" in "refute.ML" *) |
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
31 |
fun close_form t = |
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
32 |
fold (fn ((s, i), T) => fn t' => |
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
33 |
Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t'))) |
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
34 |
(Term.add_vars t []) t |
46324 | 35 |
|
47785 | 36 |
fun read_tptp_file thy postproc file_name = |
47644 | 37 |
let |
47718
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
38 |
fun has_role role (_, role', _, _) = (role' = role) |
47785 | 39 |
fun get_prop (_, _, P, _) = |
40 |
P |> Logic.varify_global |> close_form |> postproc |
|
47644 | 41 |
val path = |
42 |
Path.explode file_name |
|
43 |
|> (fn path => |
|
44 |
path |> not (Path.is_absolute path) |
|
45 |
? Path.append (Path.explode "$PWD")) |
|
47714 | 46 |
val ((_, _, problem), thy) = |
47 |
TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy |
|
47718
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
48 |
val (conjs, defs_and_nondefs) = |
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
49 |
problem |> List.partition (has_role TPTP_Syntax.Role_Conjecture) |
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
50 |
||> List.partition (has_role TPTP_Syntax.Role_Definition) |
47644 | 51 |
in |
47718
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
52 |
(map get_prop conjs, pairself (map get_prop) defs_and_nondefs, |
47771 | 53 |
thy |> Theory.checkpoint |> Proof_Context.init_global) |
47557
32f35b3d9e42
started integrating Nik's parser into TPTP command-line tools
blanchet
parents:
46325
diff
changeset
|
54 |
end |
46325 | 55 |
|
47771 | 56 |
|
46324 | 57 |
(** Nitpick (alias Nitrox) **) |
58 |
||
47718
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
59 |
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
|
60 |
| aptrueprop f t = f t |
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
61 |
|
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
62 |
fun nitpick_tptp_file thy timeout file_name = |
46325 | 63 |
let |
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
64 |
val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name |
47771 | 65 |
val thy = Proof_Context.theory_of ctxt |
47718
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
66 |
val defs = defs |> map (ATP_Util.extensionalize_term ctxt |
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
67 |
#> aptrueprop (open_form I)) |
47714 | 68 |
val state = Proof.init ctxt |
46325 | 69 |
val params = |
47557
32f35b3d9e42
started integrating Nik's parser into TPTP command-line tools
blanchet
parents:
46325
diff
changeset
|
70 |
[("card", "1\<emdash>100"), |
46325 | 71 |
("box", "false"), |
72 |
("max_threads", "1"), |
|
47791 | 73 |
("batch_size", "5"), |
47718
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
74 |
("falsify", if null conjs then "false" else "true"), |
46325 | 75 |
("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
|
76 |
("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
|
77 |
("overlord", if overlord then "true" else "false"), |
46325 | 78 |
("show_consts", "true"), |
47755 | 79 |
("format", "1"), |
46325 | 80 |
("max_potential", "0"), |
47718
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
81 |
("timeout", string_of_int timeout), |
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
82 |
("tac_timeout", string_of_int ((timeout + 49) div 50))] |
47714 | 83 |
|> Nitpick_Isar.default_params thy |
46325 | 84 |
val i = 1 |
85 |
val n = 1 |
|
86 |
val step = 0 |
|
87 |
val subst = [] |
|
88 |
in |
|
47715
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47714
diff
changeset
|
89 |
Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst |
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
90 |
defs nondefs (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
|
91 |
() |
46325 | 92 |
end |
46324 | 93 |
|
94 |
||
95 |
(** Refute **) |
|
96 |
||
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
97 |
fun refute_tptp_file thy timeout file_name = |
46325 | 98 |
let |
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
99 |
fun print_szs_from_outcome falsify s = |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
100 |
"% SZS status " ^ |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
101 |
(if s = "genuine" then |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
102 |
if falsify then "CounterSatisfiable" else "Satisfiable" |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
103 |
else |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
104 |
"Unknown") |
47788 | 105 |
|> Output.urgent_message |
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
106 |
val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name |
46325 | 107 |
val params = |
47714 | 108 |
[("maxtime", string_of_int timeout), |
109 |
("maxvars", "100000")] |
|
46325 | 110 |
in |
47718
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
111 |
Refute.refute_term ctxt params (defs @ nondefs) |
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
112 |
(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
|
113 |
|> print_szs_from_outcome (not (null conjs)) |
46325 | 114 |
end |
46324 | 115 |
|
116 |
||
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
117 |
(** Sledgehammer and Isabelle (combination of provers) **) |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
118 |
|
47785 | 119 |
fun can_tac ctxt tactic conj = can (Goal.prove ctxt [] [] conj) (K tactic) |
47771 | 120 |
|
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
121 |
fun SOLVE_TIMEOUT seconds name tac st = |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
122 |
let |
47788 | 123 |
val _ = Output.urgent_message ("running " ^ name ^ " for " ^ |
124 |
string_of_int seconds ^ " s") |
|
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
125 |
val result = |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
126 |
TimeLimit.timeLimit (Time.fromSeconds seconds) |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
127 |
(fn () => SINGLE (SOLVE tac) st) () |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
128 |
handle TimeLimit.TimeOut => NONE |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
129 |
| ERROR _ => NONE |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
130 |
in |
47785 | 131 |
case result of |
47788 | 132 |
NONE => (Output.urgent_message ("FAILURE: " ^ name); Seq.empty) |
133 |
| 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
|
134 |
end |
46324 | 135 |
|
47812 | 136 |
fun nitpick_finite_oracle_tac ctxt timeout i th = |
137 |
let |
|
138 |
fun is_safe (Type (@{type_name fun}, Ts)) = forall is_safe Ts |
|
139 |
| is_safe @{typ prop} = true |
|
140 |
| is_safe @{typ bool} = true |
|
141 |
| is_safe _ = false |
|
142 |
val conj = Thm.term_of (Thm.cprem_of th i) |
|
143 |
in |
|
144 |
if exists_type (not o is_safe) conj then |
|
145 |
Seq.empty |
|
146 |
else |
|
147 |
let |
|
148 |
val thy = Proof_Context.theory_of ctxt |
|
149 |
val state = Proof.init ctxt |
|
150 |
val params = |
|
151 |
[("box", "false"), |
|
152 |
("max_threads", "1"), |
|
153 |
("verbose", "true"), |
|
154 |
("debug", if debug then "true" else "false"), |
|
155 |
("overlord", if overlord then "true" else "false"), |
|
156 |
("max_potential", "0"), |
|
157 |
("timeout", string_of_int timeout)] |
|
158 |
|> Nitpick_Isar.default_params thy |
|
159 |
val i = 1 |
|
160 |
val n = 1 |
|
161 |
val step = 0 |
|
162 |
val subst = [] |
|
163 |
val (outcome, _) = |
|
164 |
Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst |
|
165 |
[] [] conj |
|
166 |
in if outcome = "none" then Skip_Proof.cheat_tac thy th else Seq.empty end |
|
167 |
end |
|
168 |
||
47788 | 169 |
fun atp_tac ctxt override_params timeout prover = |
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
170 |
Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt |
47788 | 171 |
([("debug", if debug then "true" else "false"), |
172 |
("overlord", if overlord then "true" else "false"), |
|
173 |
("provers", prover), |
|
174 |
("timeout", string_of_int timeout)] @ override_params) |
|
47811 | 175 |
{add = [(Facts.named (Thm.derivation_name ext), [])], |
176 |
del = [], only = true} |
|
47765 | 177 |
|
47785 | 178 |
fun sledgehammer_tac ctxt timeout i = |
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
179 |
let |
47788 | 180 |
fun slice overload_params fraq prover = |
181 |
SOLVE_TIMEOUT (timeout div fraq) prover |
|
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
182 |
(atp_tac ctxt overload_params (timeout div fraq) prover i) |
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
183 |
in |
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
184 |
slice [] 5 ATP_Systems.satallaxN |
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
185 |
ORELSE slice [] 5 ATP_Systems.leo2N |
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
186 |
ORELSE slice [] 5 ATP_Systems.spassN |
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
187 |
ORELSE slice [] 5 ATP_Systems.vampireN |
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
188 |
ORELSE slice [] 5 ATP_Systems.eN |
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
189 |
end |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
190 |
|
47785 | 191 |
fun auto_etc_tac ctxt timeout i = |
47812 | 192 |
SOLVE_TIMEOUT (timeout div 20) "nitpick" |
193 |
(nitpick_finite_oracle_tac ctxt (timeout div 20) i) |
|
194 |
ORELSE SOLVE_TIMEOUT (timeout div 10) "simp" |
|
195 |
(asm_full_simp_tac (simpset_of ctxt) i) |
|
47788 | 196 |
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
|
197 |
ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass" |
47785 | 198 |
(auto_tac ctxt |
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
199 |
THEN ALLGOALS (atp_tac ctxt [] (timeout div 5) ATP_Systems.spassN)) |
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
200 |
ORELSE SOLVE_TIMEOUT (timeout div 5) "smt" (SMT_Solver.smt_tac ctxt [] i) |
47812 | 201 |
ORELSE SOLVE_TIMEOUT (timeout div 20) "fast" (fast_tac ctxt i) |
202 |
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
|
203 |
ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i) |
47812 | 204 |
ORELSE SOLVE_TIMEOUT (timeout div 20) "arith" (Arith_Data.arith_tac ctxt i) |
205 |
ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac ctxt i) |
|
47771 | 206 |
|
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
207 |
fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator |
47785 | 208 |
|
209 |
(* Isabelle's standard automatic tactics ("auto", etc.) are more eager to |
|
210 |
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
|
211 |
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
|
212 |
let val is_problem_const = String.isPrefix (problem_const_prefix thy) in |
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
213 |
map_aterms (fn t as Const (s, T) => |
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
214 |
if is_problem_const s then Free (Long_Name.base_name s, T) |
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
215 |
else t |
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
216 |
| t => t) |
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
217 |
end |
47785 | 218 |
|
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
|
219 |
fun make_conj (defs, nondefs) conjs = |
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
|
220 |
Logic.list_implies (rev defs @ rev nondefs, |
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
|
221 |
case conjs of conj :: _ => conj | [] => @{prop False}) |
47771 | 222 |
|
223 |
fun print_szs_from_success conjs success = |
|
47788 | 224 |
Output.urgent_message ("% SZS status " ^ |
225 |
(if success then |
|
226 |
if null conjs then "Unsatisfiable" else "Theorem" |
|
227 |
else |
|
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
228 |
"Unknown")) |
47765 | 229 |
|
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
230 |
fun sledgehammer_tptp_file thy timeout file_name = |
47771 | 231 |
let |
47785 | 232 |
val (conjs, assms, ctxt) = |
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
233 |
read_tptp_file thy (freeze_problem_consts thy) file_name |
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
|
234 |
val conj = make_conj assms conjs |
47771 | 235 |
in |
47785 | 236 |
can_tac ctxt (sledgehammer_tac ctxt timeout 1) conj |
47771 | 237 |
|> print_szs_from_success conjs |
238 |
end |
|
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47765
diff
changeset
|
239 |
|
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
240 |
fun isabelle_tptp_file thy timeout file_name = |
47771 | 241 |
let |
47785 | 242 |
val (conjs, assms, ctxt) = |
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47793
diff
changeset
|
243 |
read_tptp_file thy (freeze_problem_consts thy) file_name |
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
|
244 |
val conj = make_conj assms conjs |
47771 | 245 |
in |
47811 | 246 |
(can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse |
247 |
can_tac ctxt (sledgehammer_tac ctxt (timeout div 2) 1) conj orelse |
|
47788 | 248 |
can_tac ctxt (atp_tac ctxt [] timeout ATP_Systems.satallaxN 1) conj) |
47771 | 249 |
|> print_szs_from_success conjs |
250 |
end |
|
46324 | 251 |
|
252 |
(** Translator between TPTP(-like) file formats **) |
|
253 |
||
46325 | 254 |
fun translate_tptp_file format in_file_name out_file_name = () |
46324 | 255 |
|
256 |
end; |