22 open ATP_Proof |
22 open ATP_Proof |
23 |
23 |
24 |
24 |
25 (** TPTP parsing based on ML-Yacc-generated "TPTP_Parser" **) |
25 (** TPTP parsing based on ML-Yacc-generated "TPTP_Parser" **) |
26 |
26 |
27 fun mk_meta_not P = Logic.mk_implies (P, @{prop False}) |
|
28 |
|
29 (* cf. "close_form" in "refute.ML" *) |
27 (* cf. "close_form" in "refute.ML" *) |
30 fun close_form t = |
28 fun close_form t = |
31 fold (fn ((s, i), T) => fn t' => |
29 fold (fn ((s, i), T) => fn t' => |
32 Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t'))) |
30 Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t'))) |
33 (Term.add_vars t []) t |
31 (Term.add_vars t []) t |
34 |
32 |
35 fun get_tptp_formula (_, role, P, _) = |
|
36 P |> Logic.varify_global |> close_form |
|
37 |> role = TPTP_Syntax.Role_Conjecture ? mk_meta_not |
|
38 |
|
39 fun read_tptp_file thy file_name = |
33 fun read_tptp_file thy file_name = |
40 let |
34 let |
|
35 fun has_role role (_, role', _, _) = (role' = role) |
|
36 fun get_prop (_, _, P, _) = P |> Logic.varify_global |> close_form |
41 val path = |
37 val path = |
42 Path.explode file_name |
38 Path.explode file_name |
43 |> (fn path => |
39 |> (fn path => |
44 path |> not (Path.is_absolute path) |
40 path |> not (Path.is_absolute path) |
45 ? Path.append (Path.explode "$PWD")) |
41 ? Path.append (Path.explode "$PWD")) |
46 val ((_, _, problem), thy) = |
42 val ((_, _, problem), thy) = |
47 TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy |
43 TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy |
48 val partitioned_problem = |
44 val (conjs, defs_and_nondefs) = |
49 List.partition (fn (_, role, _, _) => role = TPTP_Syntax.Role_Definition) |
45 problem |> List.partition (has_role TPTP_Syntax.Role_Conjecture) |
50 problem |
46 ||> List.partition (has_role TPTP_Syntax.Role_Definition) |
51 in |
47 in |
52 (exists (fn (_, role, _, _) => role = TPTP_Syntax.Role_Conjecture) problem, |
48 (map get_prop conjs, pairself (map get_prop) defs_and_nondefs, |
53 pairself (map get_tptp_formula) partitioned_problem, Theory.checkpoint thy) |
49 Theory.checkpoint thy) |
54 end |
50 end |
55 |
51 |
56 (** Isabelle (combination of provers) **) |
52 (** Isabelle (combination of provers) **) |
57 |
53 |
58 fun isabelle_tptp_file timeout file_name = () |
54 fun isabelle_tptp_file timeout file_name = () |
59 |
55 |
60 |
56 |
61 (** Nitpick (alias Nitrox) **) |
57 (** Nitpick (alias Nitrox) **) |
62 |
58 |
|
59 fun aptrueprop f ((t0 as @{const Trueprop}) $ t1) = t0 $ f t1 |
|
60 | aptrueprop f t = f t |
|
61 |
63 fun nitpick_tptp_file timeout file_name = |
62 fun nitpick_tptp_file timeout file_name = |
64 let |
63 let |
65 val (falsify, (defs, nondefs), thy) = read_tptp_file @{theory} file_name |
64 val (conjs, (defs, nondefs), thy) = read_tptp_file @{theory} file_name |
66 val ctxt = Proof_Context.init_global thy |
65 val ctxt = Proof_Context.init_global thy |
67 val defs = defs |> map (ATP_Util.extensionalize_term ctxt) |
66 val defs = defs |> map (ATP_Util.extensionalize_term ctxt |
|
67 #> aptrueprop (open_form I)) |
68 val state = Proof.init ctxt |
68 val state = Proof.init ctxt |
69 val params = |
69 val params = |
70 [("card", "1\<emdash>100"), |
70 [("card", "1\<emdash>100"), |
71 ("box", "false"), |
71 ("box", "false"), |
72 ("sat_solver", "smart"), |
72 ("sat_solver", "smart"), |
73 ("max_threads", "1"), |
73 ("max_threads", "1"), |
74 ("batch_size", "10"), |
74 ("batch_size", "10"), |
75 ("falsify", if falsify then "true" else "false"), |
75 ("falsify", if null conjs then "false" else "true"), |
76 (* ("debug", "true"), *) |
76 (* ("debug", "true"), *) |
77 ("verbose", "true"), |
77 ("verbose", "true"), |
78 (* ("overlord", "true"), *) |
78 (* ("overlord", "true"), *) |
79 ("show_consts", "true"), |
79 ("show_consts", "true"), |
80 ("format", "1000"), |
80 ("format", "1000"), |
81 ("max_potential", "0"), |
81 ("max_potential", "0"), |
82 ("timeout", string_of_int timeout)] |
82 ("timeout", string_of_int timeout), |
|
83 ("tac_timeout", string_of_int ((timeout + 49) div 50))] |
83 |> Nitpick_Isar.default_params thy |
84 |> Nitpick_Isar.default_params thy |
84 val i = 1 |
85 val i = 1 |
85 val n = 1 |
86 val n = 1 |
86 val step = 0 |
87 val step = 0 |
87 val subst = [] |
88 val subst = [] |
88 in |
89 in |
89 Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst |
90 Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst |
90 defs nondefs (if falsify then @{prop False} else @{prop True}); () |
91 defs nondefs (case conjs of conj :: _ => conj | _ => @{prop True}); |
|
92 () |
91 end |
93 end |
92 |
94 |
93 |
95 |
94 (** Refute **) |
96 (** Refute **) |
95 |
97 |