48 end; |
48 end; |
49 |
49 |
50 (* a special version of repeat_RS *) |
50 (* a special version of repeat_RS *) |
51 fun repeat_someI_ex th = repeat_RS th someI_ex; |
51 fun repeat_someI_ex th = repeat_RS th someI_ex; |
52 |
52 |
|
53 fun writeln_strs _ [] = () |
|
54 | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss); |
53 |
55 |
54 (* write out a subgoal as tptp clauses to the file "xxxx_N"*) |
56 (* write out a subgoal as tptp clauses to the file "xxxx_N"*) |
55 fun tptp_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) = |
57 fun tptp_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) = |
56 let |
58 let |
57 val clss = map (ResClause.make_conjecture_clause_thm) thms |
59 val clss = map (ResClause.make_conjecture_clause_thm) thms |
59 val tfree_clss = map ResClause.tfree_clause (ResLib.flat_noDup tfree_litss) |
61 val tfree_clss = map ResClause.tfree_clause (ResLib.flat_noDup tfree_litss) |
60 val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses |
62 val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses |
61 val arity_cls = map ResClause.tptp_arity_clause arity_clauses |
63 val arity_cls = map ResClause.tptp_arity_clause arity_clauses |
62 val out = TextIO.openOut(pf n) |
64 val out = TextIO.openOut(pf n) |
63 in |
65 in |
64 ResLib.writeln_strs out (List.concat (map ResClause.tptp_clause axclauses)); |
66 writeln_strs out (List.concat (map ResClause.tptp_clause axclauses)); |
65 ResLib.writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls); |
67 writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls); |
66 TextIO.closeOut out |
68 TextIO.closeOut out |
67 end; |
69 end; |
68 |
70 |
69 (* write out a subgoal in DFG format to the file "xxxx_N"*) |
71 (* write out a subgoal in DFG format to the file "xxxx_N"*) |
70 fun dfg_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) = |
72 fun dfg_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) = |
72 (*FIXME: classrel_clauses and arity_clauses*) |
74 (*FIXME: classrel_clauses and arity_clauses*) |
73 val probN = ResClause.clauses2dfg clss (!problem_name ^ "_" ^ Int.toString n) |
75 val probN = ResClause.clauses2dfg clss (!problem_name ^ "_" ^ Int.toString n) |
74 axclauses [] [] [] |
76 axclauses [] [] [] |
75 val out = TextIO.openOut(pf n) |
77 val out = TextIO.openOut(pf n) |
76 in |
78 in |
77 ResLib.writeln_strs out [probN]; TextIO.closeOut out |
79 writeln_strs out [probN]; TextIO.closeOut out |
78 end; |
80 end; |
79 |
81 |
80 |
82 |
81 (*********************************************************************) |
83 (*********************************************************************) |
82 (* call prover with settings and problem file for the current subgoal *) |
84 (* call prover with settings and problem file for the current subgoal *) |
83 (*********************************************************************) |
85 (*********************************************************************) |
84 (* now passing in list of skolemized thms and list of sgterms to go with them *) |
86 (* now passing in list of skolemized thms and list of sgterms to go with them *) |
85 fun watcher_call_provers sign sg_terms (childin, childout,pid) = |
87 fun watcher_call_provers sign sg_terms (childin, childout, pid) = |
86 let |
88 let |
87 fun make_atp_list [] n = [] |
89 fun make_atp_list [] n = [] |
88 | make_atp_list (sg_term::xs) n = |
90 | make_atp_list (sg_term::xs) n = |
89 let |
91 let |
90 val goalstring = Sign.string_of_term sign sg_term |
92 val goalstring = Sign.string_of_term sign sg_term |
91 val _ = debug ("goalstring in make_atp_lists is " ^ goalstring) |
|
92 val probfile = prob_pathname n |
93 val probfile = prob_pathname n |
93 val time = Int.toString (!time_limit) |
94 val time = Int.toString (!time_limit) |
94 val _ = debug ("problem file in watcher_call_provers is " ^ probfile) |
|
95 in |
95 in |
|
96 debug ("goalstring in make_atp_lists is\n" ^ goalstring); |
|
97 debug ("problem file in watcher_call_provers is " ^ probfile); |
96 (*Avoid command arguments containing spaces: Poly/ML and SML/NJ |
98 (*Avoid command arguments containing spaces: Poly/ML and SML/NJ |
97 versions of Unix.execute treat them differently!*) |
99 versions of Unix.execute treat them differently!*) |
|
100 (*options are separated by Watcher.setting_sep, currently #"%"*) |
98 if !prover = "spass" |
101 if !prover = "spass" |
99 then |
102 then |
100 let val optionline = |
103 let val optionline = |
101 if !AtpCommunication.reconstruct |
104 if !AtpCommunication.reconstruct |
102 (*Proof reconstruction works for only a limited set of |
105 (*Proof reconstruction works for only a limited set of |
163 writenext (n-1); |
166 writenext (n-1); |
164 all_tac))]) n th; |
167 all_tac))]) n th; |
165 ()) |
168 ()) |
166 in writenext (length prems); clause_arr end; |
169 in writenext (length prems); clause_arr end; |
167 |
170 |
168 val last_watcher_pid = ref (NONE : Posix.Process.pid option); |
171 val last_watcher_pid = |
|
172 ref (NONE : (TextIO.instream * TextIO.outstream * Posix.Process.pid) option); |
169 |
173 |
170 |
174 |
171 (*writes out the current clasimpset to a tptp file; |
175 (*writes out the current clasimpset to a tptp file; |
172 turns off xsymbol at start of function, restoring it at end *) |
176 turns off xsymbol at start of function, restoring it at end *) |
173 val isar_atp = setmp print_mode [] |
177 val isar_atp = setmp print_mode [] |
174 (fn (ctxt, th) => |
178 (fn (ctxt, th) => |
175 if Thm.no_prems th then () |
179 if Thm.no_prems th then () |
176 else |
180 else |
177 let |
181 let |
|
182 val _ = (*Set up signal handler to tidy away dead processes*) |
|
183 IsaSignal.signal (IsaSignal.chld, |
|
184 IsaSignal.SIG_HANDLE (fn _ => |
|
185 (Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []); |
|
186 debug "Child signal received\n"))); |
178 val _ = (case !last_watcher_pid of NONE => () |
187 val _ = (case !last_watcher_pid of NONE => () |
179 | SOME pid => (*FIXME: should kill ATP processes too; at least they time out*) |
188 | SOME (_, childout, pid) => |
180 (debug ("Killing old watcher, pid = " ^ |
189 (debug ("Killing old watcher, pid = " ^ |
181 Int.toString (ResLib.intOfPid pid)); |
190 Int.toString (ResLib.intOfPid pid)); |
182 Watcher.killWatcher pid)) |
191 Watcher.killWatcher pid)) |
183 handle OS.SysErr _ => debug "Attempt to kill watcher failed"; |
192 handle OS.SysErr _ => debug "Attempt to kill watcher failed"; |
184 val clause_arr = write_problem_files prob_pathname (ctxt,th) |
193 val clause_arr = write_problem_files prob_pathname (ctxt,th) |
185 val (childin, childout, pid) = Watcher.createWatcher (th, clause_arr) |
194 val (childin, childout, pid) = Watcher.createWatcher (th, clause_arr) |
186 in |
195 in |
187 last_watcher_pid := SOME pid; |
196 last_watcher_pid := SOME (childin, childout, pid); |
188 debug ("proof state: " ^ string_of_thm th); |
197 debug ("proof state: " ^ string_of_thm th); |
189 debug ("pid: " ^ Int.toString (ResLib.intOfPid pid)); |
198 debug ("pid: " ^ Int.toString (ResLib.intOfPid pid)); |
190 watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid) |
199 watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid) |
191 end); |
200 end); |
192 |
201 |
206 val proof = Toplevel.proof_of state |
215 val proof = Toplevel.proof_of state |
207 val (ctxt, (_, goal)) = Proof.get_goal proof |
216 val (ctxt, (_, goal)) = Proof.get_goal proof |
208 handle Proof.STATE _ => error "No goal present"; |
217 handle Proof.STATE _ => error "No goal present"; |
209 val thy = ProofContext.theory_of ctxt; |
218 val thy = ProofContext.theory_of ctxt; |
210 in |
219 in |
211 debug ("initial thm in isar_atp: " ^ |
220 debug ("initial thm in isar_atp:\n" ^ |
212 Pretty.string_of (ProofContext.pretty_thm ctxt goal)); |
221 Pretty.string_of (ProofContext.pretty_thm ctxt goal)); |
213 debug ("subgoals in isar_atp: " ^ |
222 debug ("subgoals in isar_atp:\n" ^ |
214 Pretty.string_of (ProofContext.pretty_term ctxt |
223 Pretty.string_of (ProofContext.pretty_term ctxt |
215 (Logic.mk_conjunction_list (Thm.prems_of goal)))); |
224 (Logic.mk_conjunction_list (Thm.prems_of goal)))); |
216 debug ("number of subgoals in isar_atp: " ^ Int.toString (Thm.nprems_of goal)); |
225 debug ("number of subgoals in isar_atp: " ^ Int.toString (Thm.nprems_of goal)); |
217 debug ("current theory: " ^ Context.theory_name thy); |
226 debug ("current theory: " ^ Context.theory_name thy); |
218 hook_count := !hook_count +1; |
227 hook_count := !hook_count +1; |