142 (*********************************************************************) |
142 (*********************************************************************) |
143 (* call SPASS with settings and problem file for the current subgoal *) |
143 (* call SPASS with settings and problem file for the current subgoal *) |
144 (* should be modified to allow other provers to be called *) |
144 (* should be modified to allow other provers to be called *) |
145 (*********************************************************************) |
145 (*********************************************************************) |
146 |
146 |
147 fun call_resolve_tac sign thms sg_term (childin, childout,pid) n = let |
147 fun call_resolve_tac sign thms sg_term (childin, childout,pid) n = |
148 val thmstring = Meson.concat_with_and (map string_of_thm thms) |
148 let val thmstring = Meson.concat_with_and (map string_of_thm thms) |
149 val thm_no = length thms |
149 val thm_no = length thms |
150 val _ = warning ("number of thms is : "^(string_of_int thm_no)) |
150 val _ = warning ("number of thms is : "^(string_of_int thm_no)) |
151 val _ = warning ("thmstring in call_res is: "^thmstring) |
151 val _ = warning ("thmstring in call_res is: "^thmstring) |
152 |
152 |
153 val goalstr = Sign.string_of_term sign sg_term |
153 val goalstr = Sign.string_of_term sign sg_term |
154 val goalproofstring = proofstring goalstr |
154 val goalproofstring = proofstring goalstr |
155 val no_returns =List.filter not_newline ( goalproofstring) |
155 val no_returns =List.filter not_newline ( goalproofstring) |
156 val goalstring = implode no_returns |
156 val goalstring = implode no_returns |
157 val _ = warning ("goalstring in call_res is: "^goalstring) |
157 val _ = warning ("goalstring in call_res is: "^goalstring) |
158 |
158 |
159 (*val prob_file =File.tmp_path (Path.basic newprobfile); *) |
159 (*val prob_file =File.tmp_path (Path.basic newprobfile); *) |
160 (*val _ =( warning ("calling make_clauses ")) |
160 (*val _ =( warning ("calling make_clauses ")) |
161 val clauses = make_clauses thms |
161 val clauses = make_clauses thms |
162 val _ =( warning ("called make_clauses "))*) |
162 val _ =( warning ("called make_clauses "))*) |
163 (*val _ = tptp_inputs clauses prob_file*) |
163 (*val _ = tptp_inputs clauses prob_file*) |
164 val thmstring = Meson.concat_with_and (map string_of_thm thms) |
164 val thmstring = Meson.concat_with_and (map string_of_thm thms) |
165 |
165 |
166 val goalstr = Sign.string_of_term sign sg_term |
166 val goalstr = Sign.string_of_term sign sg_term |
167 val goalproofstring = proofstring goalstr |
167 val goalproofstring = proofstring goalstr |
168 val no_returns =List.filter not_newline ( goalproofstring) |
168 val no_returns =List.filter not_newline ( goalproofstring) |
169 val goalstring = implode no_returns |
169 val goalstring = implode no_returns |
170 |
170 |
171 val thmproofstring = proofstring ( thmstring) |
171 val thmproofstring = proofstring ( thmstring) |
172 val no_returns =List.filter not_newline ( thmproofstring) |
172 val no_returns =List.filter not_newline ( thmproofstring) |
173 val thmstr = implode no_returns |
173 val thmstr = implode no_returns |
174 |
174 |
175 val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n) |
175 val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n) |
176 val axfile = (File.sysify_path axiom_file) |
176 val axfile = (File.sysify_path axiom_file) |
177 val hypsfile = (File.sysify_path hyps_file) |
177 val hypsfile = (File.sysify_path hyps_file) |
178 val clasimpfile = (File.sysify_path clasimp_file) |
178 val clasimpfile = (File.sysify_path clasimp_file) |
179 val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "hellofile"))) |
179 val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "hellofile"))) |
180 val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring); |
180 val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring); |
181 val _ = TextIO.flushOut outfile; |
181 val _ = TextIO.flushOut outfile; |
182 val _ = TextIO.closeOut outfile |
182 val _ = TextIO.closeOut outfile |
183 val spass_home = getenv "SPASS_HOME" |
183 in |
184 in |
184 (* without paramodulation *) |
185 (* without paramodulation *) |
185 (warning ("goalstring in call_res_tac is: "^goalstring)); |
186 (warning ("goalstring in call_res_tac is: "^goalstring)); |
186 (warning ("prob file in cal_res_tac is: "^probfile)); |
187 (warning ("prob file in cal_res_tac is: "^probfile)); |
187 (* Watcher.callResProvers(childout, |
188 (* Watcher.callResProvers(childout, |
188 [("spass",thmstr,goalstring,*spass_home*, |
189 [("spass",thmstr,goalstring,(*spass_home*), |
189 "-DocProof", |
190 "-DocProof", |
190 clasimpfile, axfile, hypsfile, probfile)]);*) |
191 clasimpfile, axfile, hypsfile, probfile)]);*) |
191 Watcher.callResProvers(childout, |
192 |
192 [("spass", thmstr, goalstring (*,spass_home*), |
193 Watcher.callResProvers(childout, |
193 getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell", |
194 [("spass",thmstr,goalstring(*,spass_home*),"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/spassshell", |
194 "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", |
195 "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", |
195 clasimpfile, axfile, hypsfile, probfile)]); |
196 clasimpfile, axfile, hypsfile, probfile)]); |
196 |
197 |
197 (* with paramodulation *) |
198 (* with paramodulation *) |
198 (*Watcher.callResProvers(childout, |
199 (*Watcher.callResProvers(childout, |
199 [("spass",thmstr,goalstring,spass_home, |
200 [("spass",thmstr,goalstring,spass_home, |
200 "-FullRed=0%-ISPm=1%-Split=0%-PObv=0%-DocProof", |
201 "-FullRed=0%-ISPm=1%-Split=0%-PObv=0%-DocProof", |
201 prob_path)]); *) |
202 prob_path)]); *) |
202 (* Watcher.callResProvers(childout, |
203 (* Watcher.callResProvers(childout, |
203 [("spass",thmstr,goalstring,spass_home, |
204 [("spass",thmstr,goalstring,spass_home, |
204 "-DocProof", prob_path)]);*) |
205 "-DocProof", prob_path)]);*) |
205 dummy_tac |
206 dummy_tac |
206 end |
207 end |
|
208 |
207 |
209 (**********************************************************) |
208 (**********************************************************) |
210 (* write out the current subgoal as a tptp file, probN, *) |
209 (* write out the current subgoal as a tptp file, probN, *) |
211 (* then call dummy_tac - should be call_res_tac *) |
210 (* then call dummy_tac - should be call_res_tac *) |
212 (**********************************************************) |
211 (**********************************************************) |