1.1 --- a/src/HOL/Tools/res_atp.ML Tue Apr 18 05:38:18 2006 +0200
1.2 +++ b/src/HOL/Tools/res_atp.ML Wed Apr 19 10:41:37 2006 +0200
1.3 @@ -342,9 +342,17 @@
1.4 val linkup_logic_mode = ref Fol;
1.5
1.6 fun tptp_writer logic goals filename (axioms,classrels,arities) =
1.7 - if is_fol_logic logic then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
1.8 - else
1.9 - ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) (get_all_helpers());
1.10 + if is_fol_logic logic
1.11 + then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
1.12 + else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities)
1.13 + (get_all_helpers());
1.14 +
1.15 +(*2006-04-07: not working: goals has type thm list (not term list as above) and
1.16 + axioms has type ResClause.clause list (not (thm * (string * int)) list as above)*)
1.17 +fun dfg_writer logic goals filename (axioms,classrels,arities) =
1.18 + if is_fol_logic logic
1.19 + then ResClause.dfg_write_file goals filename (axioms, classrels, arities)
1.20 + else error "DFG output for higher-order translations is not implemented"
1.21
1.22
1.23 fun write_subgoal_file mode ctxt conjectures user_thms n =
1.24 @@ -360,7 +368,7 @@
1.25 val keep_types = if is_fol_logic prob_logic then !fol_keep_types else is_typed_hol ()
1.26 val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
1.27 val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
1.28 - val writer = tptp_writer
1.29 + val writer = (*if !prover = "spass" then dfg_writer else*) tptp_writer
1.30 val file = atp_input_file()
1.31 in
1.32 (writer prob_logic goal_cls file (axclauses_as_thms,classrel_clauses,arity_clauses);
1.33 @@ -405,37 +413,30 @@
1.34 val time = Int.toString (!time_limit)
1.35 in
1.36 Output.debug ("problem file in watcher_call_provers is " ^ probfile);
1.37 - (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
1.38 - versions of Unix.execute treat them differently!*)
1.39 (*options are separated by Watcher.setting_sep, currently #"%"*)
1.40 if !prover = "spass"
1.41 then
1.42 - let val baseopts = "%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
1.43 - val infopts =
1.44 - if !AtpCommunication.reconstruct
1.45 - (*Proof reconstruction needs a limited set of inf rules*)
1.46 - then space_implode "%" (!custom_spass)
1.47 - else "-Auto%-SOS=1"
1.48 - val spass = helper_path "SPASS_HOME" "SPASS"
1.49 - in
1.50 - ([("spass", spass, infopts ^ baseopts, probfile)] @
1.51 - make_atp_list xs (n+1))
1.52 + let val spass = helper_path "SPASS_HOME" "SPASS"
1.53 + val sopts =
1.54 + "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
1.55 + in
1.56 + ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1)
1.57 end
1.58 else if !prover = "vampire"
1.59 then
1.60 let val vampire = helper_path "VAMPIRE_HOME" "vampire"
1.61 + val casc = if !time_limit > 70 then "--mode casc%" else ""
1.62 + val vopts = casc ^ "-m 100000%-t " ^ time
1.63 in
1.64 - ([("vampire", vampire, "-m 100000%-t " ^ time, probfile)] @
1.65 - make_atp_list xs (n+1)) (*BEWARE! spaces in options!*)
1.66 + ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
1.67 end
1.68 else if !prover = "E"
1.69 then
1.70 let val Eprover = helper_path "E_HOME" "eproof"
1.71 in
1.72 - ([("E", Eprover,
1.73 - "--tptp-in%-l5%-xAuto%-tAuto%--cpu-limit=" ^ time,
1.74 - probfile)] @
1.75 - make_atp_list xs (n+1))
1.76 + ("E", Eprover,
1.77 + "--tptp-in%-l5%-xAuto%-tAuto%--cpu-limit=" ^ time, probfile) ::
1.78 + make_atp_list xs (n+1)
1.79 end
1.80 else error ("Invalid prover name: " ^ !prover)
1.81 end
1.82 @@ -476,7 +477,7 @@
1.83 val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
1.84 val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
1.85 val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
1.86 - val writer = (*if !prover ~= "spass" then *)tptp_writer
1.87 + val writer = (*if !prover = "spass" then dfg_writer else*) tptp_writer
1.88 fun write_all [] _ = []
1.89 | write_all (subgoal::subgoals) k =
1.90 (writer goals_logic subgoal (pf k) (axclauses,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1))
1.91 @@ -490,7 +491,7 @@
1.92 fun kill_last_watcher () =
1.93 (case !last_watcher_pid of
1.94 NONE => ()
1.95 - | SOME (_, childout, pid, files) =>
1.96 + | SOME (_, _, pid, files) =>
1.97 (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid);
1.98 Watcher.killWatcher pid;
1.99 ignore (map (try OS.FileSys.remove) files)))