4 Minimalization of theorem list for metis by using an external automated theorem prover |
4 Minimalization of theorem list for metis by using an external automated theorem prover |
5 *) |
5 *) |
6 |
6 |
7 signature ATP_MINIMAL = |
7 signature ATP_MINIMAL = |
8 sig |
8 sig |
9 val minimalize: AtpManager.prover -> string -> int -> Proof.state -> |
9 val minimalize: AtpWrapper.prover -> string -> int -> Proof.state -> |
10 (string * thm list) list -> ((string * thm list) list * int) option * string |
10 (string * thm list) list -> ((string * thm list) list * int) option * string |
11 end |
11 end |
12 |
12 |
13 structure AtpMinimal: ATP_MINIMAL = |
13 structure AtpMinimal: ATP_MINIMAL = |
14 struct |
14 struct |
95 ("Timeout", Timeout), |
95 ("Timeout", Timeout), |
96 ("time limit exceeded", Timeout), |
96 ("time limit exceeded", Timeout), |
97 ("# Cannot determine problem status within resource limit", Timeout), |
97 ("# Cannot determine problem status within resource limit", Timeout), |
98 ("Error", Error)] |
98 ("Error", Error)] |
99 |
99 |
100 fun produce_answer (success, message, _, result_string, thm_name_vec, filtered) = |
100 fun produce_answer result = |
|
101 let |
|
102 val AtpWrapper.Prover_Result {success, message, proof=result_string, |
|
103 internal_thm_names=thm_name_vec, filtered_clauses=filtered, ...} = result |
|
104 in |
101 if success then |
105 if success then |
102 (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string) |
106 (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string) |
103 else |
107 else |
104 let |
108 let |
105 val failure = failure_strings |> get_first (fn (s, t) => |
109 val failure = failure_strings |> get_first (fn (s, t) => |
108 if is_some failure then |
112 if is_some failure then |
109 the failure |
113 the failure |
110 else |
114 else |
111 (Failure, result_string) |
115 (Failure, result_string) |
112 end |
116 end |
113 |
117 end |
114 |
118 |
115 (* wrapper for calling external prover *) |
119 (* wrapper for calling external prover *) |
116 |
120 |
117 fun sh_test_thms prover prover_name time_limit subgoalno state filtered name_thms_pairs = |
121 fun sh_test_thms prover time_limit subgoalno state filtered name_thms_pairs = |
118 let |
122 let |
119 val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ") |
123 val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ") |
120 val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs |
124 val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs |
121 val _ = debug_fn (fn () => print_names name_thm_pairs) |
125 val _ = debug_fn (fn () => print_names name_thm_pairs) |
122 val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs |
126 val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs |
123 val (result, proof) = |
127 val problem = AtpWrapper.ATP_Problem { |
124 produce_answer |
128 with_full_types = AtpManager.get_full_types (), |
125 (prover time_limit (SOME axclauses) filtered prover_name subgoalno (Proof.get_goal state)) |
129 subgoal = subgoalno, |
|
130 goal = Proof.get_goal state, |
|
131 axiom_clauses = SOME axclauses, |
|
132 filtered_clauses = filtered } |
|
133 val (result, proof) = produce_answer (prover problem time_limit) |
126 val _ = println (string_of_result result) |
134 val _ = println (string_of_result result) |
127 val _ = debug proof |
135 val _ = debug proof |
128 in |
136 in |
129 (result, proof) |
137 (result, proof) |
130 end |
138 end |
138 println ("Minimize called with " ^ length_string name_thms_pairs ^ " theorems, prover: " |
146 println ("Minimize called with " ^ length_string name_thms_pairs ^ " theorems, prover: " |
139 ^ prover_name ^ ", time limit: " ^ Int.toString time_limit ^ " seconds") |
147 ^ prover_name ^ ", time limit: " ^ Int.toString time_limit ^ " seconds") |
140 val _ = debug_fn (fn () => app (fn (n, tl) => |
148 val _ = debug_fn (fn () => app (fn (n, tl) => |
141 (debug n; app (fn t => |
149 (debug n; app (fn t => |
142 debug (" " ^ Display.string_of_thm (Proof.context_of state) t)) tl)) name_thms_pairs) |
150 debug (" " ^ Display.string_of_thm (Proof.context_of state) t)) tl)) name_thms_pairs) |
143 val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state |
151 val test_thms_fun = sh_test_thms prover time_limit 1 state |
144 fun test_thms filtered thms = |
152 fun test_thms filtered thms = |
145 case test_thms_fun filtered thms of (Success _, _) => true | _ => false |
153 case test_thms_fun filtered thms of (Success _, _) => true | _ => false |
146 val answer' = pair and answer'' = pair NONE |
154 val answer' = pair and answer'' = pair NONE |
147 in |
155 in |
148 (* try prove first to check result and get used theorems *) |
156 (* try prove first to check result and get used theorems *) |