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 |
|
|
20 |
open ATP_Util
|
|
21 |
open ATP_Problem
|
|
22 |
open ATP_Proof
|
|
23 |
|
|
24 |
|
|
25 |
(** General TPTP parsing **)
|
|
26 |
|
|
27 |
exception SYNTAX of string
|
|
28 |
|
|
29 |
val tptp_explode = raw_explode o strip_spaces_except_between_idents
|
|
30 |
|
|
31 |
fun parse_file_path (c :: ss) =
|
|
32 |
if c = "'" orelse c = "\"" then
|
|
33 |
ss |> chop_while (curry (op <>) c) |>> implode ||> tl
|
|
34 |
else
|
|
35 |
raise SYNTAX "invalid file path"
|
|
36 |
| parse_file_path [] = raise SYNTAX "invalid file path"
|
|
37 |
|
|
38 |
fun parse_include x =
|
|
39 |
let
|
|
40 |
val (file_name, rest) =
|
|
41 |
(Scan.this_string "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
|
|
42 |
--| $$ ".") x
|
|
43 |
val path = file_name |> Path.explode
|
|
44 |
val path =
|
|
45 |
path |> not (Path.is_absolute path) ? Path.append (Path.explode "$TPTP")
|
|
46 |
in ((), (path |> File.read |> tptp_explode) @ rest) end
|
|
47 |
|
|
48 |
val parse_cnf_or_fof =
|
|
49 |
(Scan.this_string "cnf" || Scan.this_string "fof") |-- $$ "(" |--
|
|
50 |
Scan.many (not_equal ",") |-- $$ "," |--
|
|
51 |
(Scan.this_string "axiom" || Scan.this_string "definition"
|
|
52 |
|| Scan.this_string "theorem" || Scan.this_string "lemma"
|
|
53 |
|| Scan.this_string "hypothesis" || Scan.this_string "conjecture"
|
|
54 |
|| Scan.this_string "negated_conjecture") --| $$ "," -- parse_formula
|
|
55 |
--| $$ ")" --| $$ "."
|
|
56 |
>> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
|
|
57 |
|
|
58 |
val parse_problem =
|
|
59 |
Scan.repeat parse_include
|
|
60 |
|-- Scan.repeat (parse_cnf_or_fof --| Scan.repeat parse_include)
|
|
61 |
|
|
62 |
val parse_tptp_problem =
|
|
63 |
Scan.finite Symbol.stopper
|
|
64 |
(Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")
|
|
65 |
parse_problem))
|
|
66 |
o tptp_explode
|
|
67 |
|
|
68 |
val iota_T = @{typ iota}
|
46325
|
69 |
val quant_T = @{typ "(iota => bool) => bool"}
|
46324
|
70 |
|
|
71 |
fun is_variable s = Char.isUpper (String.sub (s, 0))
|
|
72 |
|
|
73 |
fun hol_term_from_fo_term res_T (ATerm (x, us)) =
|
|
74 |
let val ts = map (hol_term_from_fo_term iota_T) us in
|
|
75 |
list_comb ((case x of
|
|
76 |
"$true" => @{const_name True}
|
|
77 |
| "$false" => @{const_name False}
|
|
78 |
| "=" => @{const_name HOL.eq}
|
|
79 |
| "equal" => @{const_name HOL.eq}
|
|
80 |
| _ => x, map fastype_of ts ---> res_T)
|
|
81 |
|> (if is_variable x then Free else Const), ts)
|
|
82 |
end
|
|
83 |
|
|
84 |
fun hol_prop_from_formula phi =
|
|
85 |
case phi of
|
|
86 |
AQuant (_, [], phi') => hol_prop_from_formula phi'
|
|
87 |
| AQuant (q, (x, _) :: xs, phi') =>
|
|
88 |
Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex},
|
|
89 |
quant_T)
|
|
90 |
$ lambda (Free (x, iota_T)) (hol_prop_from_formula (AQuant (q, xs, phi')))
|
|
91 |
| AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u')
|
|
92 |
| AConn (c, [u1, u2]) =>
|
|
93 |
pairself hol_prop_from_formula (u1, u2)
|
|
94 |
|> (case c of
|
|
95 |
AAnd => HOLogic.mk_conj
|
|
96 |
| AOr => HOLogic.mk_disj
|
|
97 |
| AImplies => HOLogic.mk_imp
|
|
98 |
| AIff => HOLogic.mk_eq
|
|
99 |
| ANot => raise Fail "binary \"ANot\"")
|
|
100 |
| AConn _ => raise Fail "malformed AConn"
|
46325
|
101 |
| AAtom u => hol_term_from_fo_term @{typ bool} u
|
46324
|
102 |
|
|
103 |
fun mk_all x t = Const (@{const_name All}, quant_T) $ lambda x t
|
|
104 |
|
|
105 |
fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t
|
|
106 |
|
46325
|
107 |
fun read_tptp_file file_name =
|
|
108 |
case parse_tptp_problem (File.read (Path.explode file_name)) of
|
|
109 |
(_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
|
|
110 |
| (phis, []) =>
|
|
111 |
map (HOLogic.mk_Trueprop o close_hol_prop o hol_prop_from_formula) phis
|
|
112 |
|
|
113 |
fun print_szs_from_outcome s =
|
|
114 |
"% SZS status " ^
|
|
115 |
(if s = Nitpick.genuineN then
|
|
116 |
"CounterSatisfiable"
|
|
117 |
else
|
|
118 |
"Unknown")
|
|
119 |
|> writeln
|
46324
|
120 |
|
|
121 |
(** Isabelle (combination of provers) **)
|
|
122 |
|
|
123 |
fun isabelle_tptp_file file_name = ()
|
|
124 |
|
|
125 |
|
|
126 |
(** Nitpick (alias Nitrox) **)
|
|
127 |
|
|
128 |
fun nitpick_tptp_file file_name =
|
46325
|
129 |
let
|
|
130 |
val ts = read_tptp_file file_name
|
|
131 |
val state = Proof.init @{context}
|
|
132 |
val params =
|
|
133 |
[("card iota", "1\<emdash>100"),
|
|
134 |
("card", "1\<emdash>8"),
|
|
135 |
("box", "false"),
|
|
136 |
("sat_solver", "smart"),
|
|
137 |
("max_threads", "1"),
|
|
138 |
("batch_size", "10"),
|
|
139 |
(* ("debug", "true"), *)
|
|
140 |
("verbose", "true"),
|
|
141 |
(* ("overlord", "true"), *)
|
|
142 |
("show_consts", "true"),
|
|
143 |
("format", "1000"),
|
|
144 |
("max_potential", "0"),
|
|
145 |
("timeout", "none"),
|
|
146 |
("expect", Nitpick.genuineN)]
|
|
147 |
|> Nitpick_Isar.default_params @{theory}
|
|
148 |
val i = 1
|
|
149 |
val n = 1
|
|
150 |
val step = 0
|
|
151 |
val subst = []
|
|
152 |
in
|
|
153 |
Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst ts
|
|
154 |
@{prop False}
|
|
155 |
|> fst |> print_szs_from_outcome
|
|
156 |
end
|
46324
|
157 |
|
|
158 |
|
|
159 |
(** Refute **)
|
|
160 |
|
46325
|
161 |
fun refute_tptp_file file_name =
|
|
162 |
let
|
|
163 |
val ts = read_tptp_file file_name
|
|
164 |
val params =
|
|
165 |
[("maxtime", "10000"),
|
|
166 |
("assms", "true"),
|
|
167 |
("expect", Nitpick.genuineN)]
|
|
168 |
in
|
|
169 |
Refute.refute_term @{context} params ts @{prop False}
|
|
170 |
|> print_szs_from_outcome
|
|
171 |
end
|
46324
|
172 |
|
|
173 |
|
|
174 |
(** Sledgehammer **)
|
|
175 |
|
|
176 |
fun sledgehammer_tptp_file file_name = ()
|
|
177 |
|
|
178 |
|
|
179 |
(** Translator between TPTP(-like) file formats **)
|
|
180 |
|
46325
|
181 |
fun translate_tptp_file format in_file_name out_file_name = ()
|
46324
|
182 |
|
|
183 |
end;
|