author | blanchet |
Wed, 18 Apr 2012 23:13:11 +0200 | |
changeset 47565 | 762eb0dacaa6 |
parent 47562 | a72239723ae8 |
child 47643 | e33c2be488fe |
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 |
|
10 |
val isabelle_tptp_file : string -> unit |
|
11 |
val nitpick_tptp_file : string -> unit |
|
12 |
val refute_tptp_file : string -> unit |
|
13 |
val sledgehammer_tptp_file : 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 |
||
47565
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
20 |
(** TPTP parsing **) |
46324 | 21 |
|
47565
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
22 |
(* cf. "close_form" in "refute.ML" *) |
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
23 |
fun close_form t = |
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
24 |
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
|
25 |
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
|
26 |
(Term.add_vars t []) t |
46324 | 27 |
|
47557
32f35b3d9e42
started integrating Nik's parser into TPTP command-line tools
blanchet
parents:
46325
diff
changeset
|
28 |
fun mk_meta_not P = Logic.mk_implies (P, @{prop False}) |
32f35b3d9e42
started integrating Nik's parser into TPTP command-line tools
blanchet
parents:
46325
diff
changeset
|
29 |
|
47562 | 30 |
fun get_tptp_formula (_, role, P, _) = |
47565
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
31 |
P |> Logic.varify_global |> close_form |
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
32 |
|> role = TPTP_Syntax.Role_Conjecture ? mk_meta_not |
47557
32f35b3d9e42
started integrating Nik's parser into TPTP command-line tools
blanchet
parents:
46325
diff
changeset
|
33 |
|
32f35b3d9e42
started integrating Nik's parser into TPTP command-line tools
blanchet
parents:
46325
diff
changeset
|
34 |
fun read_tptp_file thy file_name = |
47565
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
35 |
let |
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
36 |
val path = Path.explode file_name |
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
37 |
val problem = |
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
38 |
TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy |
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
39 |
|> fst |> #3 |
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
40 |
in |
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
41 |
(exists (fn (_, role, _, _) => role = TPTP_Syntax.Role_Conjecture) problem, |
762eb0dacaa6
remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents:
47562
diff
changeset
|
42 |
map get_tptp_formula problem) |
47557
32f35b3d9e42
started integrating Nik's parser into TPTP command-line tools
blanchet
parents:
46325
diff
changeset
|
43 |
end |
46325 | 44 |
|
46324 | 45 |
(** Isabelle (combination of provers) **) |
46 |
||
47 |
fun isabelle_tptp_file file_name = () |
|
48 |
||
49 |
||
50 |
(** Nitpick (alias Nitrox) **) |
|
51 |
||
52 |
fun nitpick_tptp_file file_name = |
|
46325 | 53 |
let |
47562 | 54 |
val (falsify, ts) = read_tptp_file @{theory} file_name |
46325 | 55 |
val state = Proof.init @{context} |
56 |
val params = |
|
47557
32f35b3d9e42
started integrating Nik's parser into TPTP command-line tools
blanchet
parents:
46325
diff
changeset
|
57 |
[("card", "1\<emdash>100"), |
46325 | 58 |
("box", "false"), |
59 |
("sat_solver", "smart"), |
|
60 |
("max_threads", "1"), |
|
61 |
("batch_size", "10"), |
|
47562 | 62 |
("falsify", if falsify then "true" else "false"), |
46325 | 63 |
(* ("debug", "true"), *) |
64 |
("verbose", "true"), |
|
65 |
(* ("overlord", "true"), *) |
|
66 |
("show_consts", "true"), |
|
67 |
("format", "1000"), |
|
68 |
("max_potential", "0"), |
|
69 |
("timeout", "none"), |
|
70 |
("expect", Nitpick.genuineN)] |
|
71 |
|> Nitpick_Isar.default_params @{theory} |
|
72 |
val i = 1 |
|
73 |
val n = 1 |
|
74 |
val step = 0 |
|
75 |
val subst = [] |
|
76 |
in |
|
47562 | 77 |
Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst ts |
78 |
(if falsify then @{prop False} else @{prop True}); () |
|
46325 | 79 |
end |
46324 | 80 |
|
81 |
||
82 |
(** Refute **) |
|
83 |
||
47562 | 84 |
fun print_szs_from_outcome falsify s = |
85 |
"% SZS status " ^ |
|
86 |
(if s = "genuine" then |
|
87 |
if falsify then "CounterSatisfiable" else "Satisfiable" |
|
88 |
else |
|
89 |
"Unknown") |
|
90 |
|> writeln |
|
91 |
||
46325 | 92 |
fun refute_tptp_file file_name = |
93 |
let |
|
47562 | 94 |
val (falsify, ts) = read_tptp_file @{theory} file_name |
46325 | 95 |
val params = |
96 |
[("maxtime", "10000"), |
|
97 |
("assms", "true"), |
|
98 |
("expect", Nitpick.genuineN)] |
|
99 |
in |
|
100 |
Refute.refute_term @{context} params ts @{prop False} |
|
47562 | 101 |
|> print_szs_from_outcome falsify |
46325 | 102 |
end |
46324 | 103 |
|
104 |
||
105 |
(** Sledgehammer **) |
|
106 |
||
107 |
fun sledgehammer_tptp_file file_name = () |
|
108 |
||
109 |
||
110 |
(** Translator between TPTP(-like) file formats **) |
|
111 |
||
46325 | 112 |
fun translate_tptp_file format in_file_name out_file_name = () |
46324 | 113 |
|
114 |
end; |