equal
deleted
inserted
replaced
5 Minimization of fact list for Metis using external provers. |
5 Minimization of fact list for Metis using external provers. |
6 *) |
6 *) |
7 |
7 |
8 signature SLEDGEHAMMER_MINIMIZE = |
8 signature SLEDGEHAMMER_MINIMIZE = |
9 sig |
9 sig |
10 type locality = ATP_Translate.locality |
10 type locality = ATP_Problem_Generate.locality |
11 type play = ATP_Reconstruct.play |
11 type play = ATP_Proof_Reconstruct.play |
12 type params = Sledgehammer_Provers.params |
12 type params = Sledgehammer_Provers.params |
13 |
13 |
14 val binary_min_facts : int Config.T |
14 val binary_min_facts : int Config.T |
15 val minimize_facts : |
15 val minimize_facts : |
16 string -> params -> bool -> int -> int -> Proof.state |
16 string -> params -> bool -> int -> int -> Proof.state |
24 structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE = |
24 structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE = |
25 struct |
25 struct |
26 |
26 |
27 open ATP_Util |
27 open ATP_Util |
28 open ATP_Proof |
28 open ATP_Proof |
29 open ATP_Translate |
29 open ATP_Problem_Generate |
30 open ATP_Reconstruct |
30 open ATP_Proof_Reconstruct |
31 open Sledgehammer_Util |
31 open Sledgehammer_Util |
32 open Sledgehammer_Filter |
32 open Sledgehammer_Filter |
33 open Sledgehammer_Provers |
33 open Sledgehammer_Provers |
34 |
34 |
35 (* wrapper for calling external prover *) |
35 (* wrapper for calling external prover *) |