tidying; ATP options including CASC mode for Vampire
authorpaulson
Wed Apr 19 10:41:37 2006 +0200 (2006-04-19 ago)
changeset 19445da75577642a9
parent 19444 085568445283
child 19446 30e1178d7a3b
tidying; ATP options including CASC mode for Vampire
src/HOL/Tools/res_atp.ML
     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)))